From f780c92154d3b7511681aeb473dc0b3ccb25b764 Mon Sep 17 00:00:00 2001 From: Tomas Skrivan Date: Tue, 12 May 2026 00:33:49 +0200 Subject: [PATCH 1/8] allow fun_prop to call discharger on ModelWithCorners --- Mathlib/Tactic/FunProp/Core.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Tactic/FunProp/Core.lean b/Mathlib/Tactic/FunProp/Core.lean index d49e135fa7e438..85b9b7573c8670 100644 --- a/Mathlib/Tactic/FunProp/Core.lean +++ b/Mathlib/Tactic/FunProp/Core.lean @@ -71,7 +71,7 @@ def synthesizeArgs (thmId : Origin) (xs : Array Expr) else -- try user provided discharger let ctx : Context ← read - if (← isProp type) then + if ((← isProp type) || type.isAppOfArity' `ModelWithCorners 7) then if let some proof ← ctx.disch type then if (← isDefEq x proof) then continue From 70571963bda481995acb1f88829d8b6de43a02a2 Mon Sep 17 00:00:00 2001 From: Tomas Skrivan Date: Tue, 12 May 2026 00:56:50 +0200 Subject: [PATCH 2/8] add comment explaining the check --- Mathlib/Tactic/FunProp/Core.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Tactic/FunProp/Core.lean b/Mathlib/Tactic/FunProp/Core.lean index 85b9b7573c8670..dfda941e951795 100644 --- a/Mathlib/Tactic/FunProp/Core.lean +++ b/Mathlib/Tactic/FunProp/Core.lean @@ -71,6 +71,10 @@ def synthesizeArgs (thmId : Origin) (xs : Array Expr) else -- try user provided discharger let ctx : Context ← read + -- to use fun_prop for MDifferentiable we need provide specialize discharger for + -- ModelWithCorners. For now it is hardcoded here as this is the only case we can think of + -- when to use discharger on non-Prop hypothesis. In future, we might want to generalize + -- this with an attribute or something similar. if ((← isProp type) || type.isAppOfArity' `ModelWithCorners 7) then if let some proof ← ctx.disch type then if (← isDefEq x proof) then From 1edf6f4a3fd2ed032e7acf61df9b5b90a1bb2f5e Mon Sep 17 00:00:00 2001 From: Tomas Skrivan Date: Tue, 12 May 2026 01:02:30 +0200 Subject: [PATCH 3/8] add test that does not depend on mathlib --- MathlibTest/fun_prop_dev.lean | 77 +++++++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) diff --git a/MathlibTest/fun_prop_dev.lean b/MathlibTest/fun_prop_dev.lean index a2c6252f06388c..dc9f64dab5957d 100644 --- a/MathlibTest/fun_prop_dev.lean +++ b/MathlibTest/fun_prop_dev.lean @@ -732,3 +732,80 @@ example {f : α → FooHom α} (hf : Con f) : Con fun x ↦ f x (f x x x) x := b fun_prop end BundledMorphismWithFunctionValues + +section MDifferentiableMock + +variable {α β γ δ : Type*} {ι : Type*} {E : ι → Type*} + +class Dummy (A : Type*) +instance : Dummy A := ⟨⟩ + +/-- Mock model-with-corners data. +The `Dummy` nonsense it to just match arity of the real ModelWithCorners -/ +structure ModelWithCorners (M : Type*) [Dummy M] [Dummy M] [Dummy M] [Dummy M] [Dummy M] [Dummy M] where + name : Unit := () + +def ModelWithCorners.prod (I : ModelWithCorners α) (J : ModelWithCorners β) : + ModelWithCorners (α × β) := {name:=()} + +/-- Mock manifold differentiability. The source and target model data are explicit arguments, +as for real `MDifferentiable I I' f`. -/ +@[fun_prop] +opaque MDifferentiable {M M' : Type*} (I : ModelWithCorners M) (I' : ModelWithCorners M') (f : M → M') : Prop + +namespace MDifferentiable + +variable {I : ModelWithCorners α} {I' : ModelWithCorners β} {I'' : ModelWithCorners γ} {I''' : ModelWithCorners δ} + +@[fun_prop] +theorem id (I : ModelWithCorners α) : MDifferentiable I I (id : α → α) := silentSorry + +@[fun_prop] +theorem const (I : ModelWithCorners α) (I' : ModelWithCorners β) (y : β) : + MDifferentiable I I' (fun _ : α => y) := silentSorry + +@[fun_prop] +theorem comp (g : β → γ) (f : α → β) + (hg : MDifferentiable I' I'' g) (hf : MDifferentiable I I' f) : + MDifferentiable I I'' (fun x => g (f x)) := silentSorry + +@[fun_prop] +theorem apply (i : ι) (I : ModelWithCorners ((x : ι) → E x)) (I' : ModelWithCorners (E i)) : + MDifferentiable I I' (fun f : (x : ι) → E x => f i) := silentSorry + +@[fun_prop] +theorem pi (f : α → (i : ι) → E i) + (Iα : ModelWithCorners α) (IE : (i : ι) → ModelWithCorners (E i)) + (IPi : ModelWithCorners ((i : ι) → E i)) + (hf : ∀ i, MDifferentiable Iα (IE i) (fun x => f x i)) : + MDifferentiable Iα IPi (fun x i => f x i) := silentSorry + +@[fun_prop] +theorem prod_mk (f : α → β) (g : α → γ) + (Iβγ : ModelWithCorners (β × γ)) + (hf : MDifferentiable I I' f) (hg : MDifferentiable I I'' g) : + MDifferentiable I Iβγ (fun x => (f x, g x)) := silentSorry + +@[fun_prop] +theorem fst (Iαβ : ModelWithCorners (α × β)) : + MDifferentiable Iαβ I (fun x : α × β => x.1) := silentSorry + +@[fun_prop] +theorem snd (Iαβ : ModelWithCorners (α × β)) : + MDifferentiable Iαβ I' (fun x : α × β => x.2) := silentSorry + +end MDifferentiable + +variable {Iα : ModelWithCorners α} + +@[fun_prop] +theorem mdiff_add [Add α] : MDifferentiable (Iα.prod Iα) Iα (fun xy : α×α => xy.1 + xy.2) := silentSorry +@[fun_prop] +theorem mdiff_mul [Mul α] : MDifferentiable (Iα.prod Iα) Iα (fun xy : α×α => xy.1 * xy.2) := silentSorry + +example [Add α] [Mul α] : + MDifferentiable Iα Iα (fun x => x * x + x) := by + fail_if_success fun_prop + fun_prop (disch:=assumption) + +end MDifferentiableMock From 3d3312c736d3864c23b521af8c519a4cab432013 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 12 May 2026 03:48:08 +0200 Subject: [PATCH 4/8] Fix review nits --- MathlibTest/fun_prop_dev.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/MathlibTest/fun_prop_dev.lean b/MathlibTest/fun_prop_dev.lean index dc9f64dab5957d..bd5cea940d48a0 100644 --- a/MathlibTest/fun_prop_dev.lean +++ b/MathlibTest/fun_prop_dev.lean @@ -733,15 +733,16 @@ example {f : α → FooHom α} (hf : Con f) : Con fun x ↦ f x (f x x x) x := b end BundledMorphismWithFunctionValues +/-! Test imitating the discharging of `ModelWithCorners` metavariables -/ section MDifferentiableMock -variable {α β γ δ : Type*} {ι : Type*} {E : ι → Type*} +variable {α β γ δ ι : Type*} {E : ι → Type*} class Dummy (A : Type*) instance : Dummy A := ⟨⟩ /-- Mock model-with-corners data. -The `Dummy` nonsense it to just match arity of the real ModelWithCorners -/ +The `Dummy` parameters are necessary (only) to match the arity of the real `ModelWithCorners` -/ structure ModelWithCorners (M : Type*) [Dummy M] [Dummy M] [Dummy M] [Dummy M] [Dummy M] [Dummy M] where name : Unit := () @@ -799,13 +800,12 @@ end MDifferentiable variable {Iα : ModelWithCorners α} @[fun_prop] -theorem mdiff_add [Add α] : MDifferentiable (Iα.prod Iα) Iα (fun xy : α×α => xy.1 + xy.2) := silentSorry +theorem mdiff_add [Add α] : MDifferentiable (Iα.prod Iα) Iα (fun x ↦ x.1 + x.2) := silentSorry @[fun_prop] -theorem mdiff_mul [Mul α] : MDifferentiable (Iα.prod Iα) Iα (fun xy : α×α => xy.1 * xy.2) := silentSorry +theorem mdiff_mul [Mul α] : MDifferentiable (Iα.prod Iα) Iα (fun x ↦ x.1 * x.2) := silentSorry -example [Add α] [Mul α] : - MDifferentiable Iα Iα (fun x => x * x + x) := by +example [Add α] [Mul α] : MDifferentiable Iα Iα (fun x ↦ x * x + x) := by fail_if_success fun_prop - fun_prop (disch:=assumption) + fun_prop (disch := assumption) end MDifferentiableMock From 4a3c27805e0881813e2db7ce6057afbb7b1b6066 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 12 May 2026 00:56:02 +0200 Subject: [PATCH 5/8] cherry-pick: previous prototype for the find_model tactic --- Mathlib/Geometry/Manifold/Notation.lean | 125 ++++++++++++++++++++++++ 1 file changed, 125 insertions(+) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index 38236c1bc87c81..228a7db05355e8 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -805,6 +805,125 @@ def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do return (srcI, tgtI) | _ => throwError "Expected{indentD e}\nof type{indentD etype}\nto be a function" +/-- Try to find a `ModelWithCorners` for a given base field, model normed space and model +topological space, using information from the local context and a few hard-coded rules. -/ +-- FIXME: do we need to handle baseInfo again? perhaps not, let's try without! +def findModelForFunpropInner (field model top : Expr) : + TermElabM <| Option (Expr × NormedSpaceInfo) := do + trace[Elab.DiffGeo.FunPropM] "Trying to solve a goal `ModelWithCorners {field} {model} {top}`" + if let some m ← tryStrategy m!"Assumption" fromAssumption then + return some (m, none) + if let some m ← tryStrategy m!"Normed space" fromNormedSpace then + return some (m, none) + -- TODO: implement the remaining strategies, and then the inner to outer part! + return none +where + -- TODO: go over this entire logic and make it somewhat sound and complete! + /-- Try to find a model with corners with given base field, model space and topological space + within the local hypotheses: throw an error if this is not successful. -/ + fromAssumption : TermElabM Expr := do + let some m ← findSomeLocalHyp? fun fvar type ↦ do + match_expr type with + | ModelWithCorners k _ E _ _ H _ => do + if (← withReducible (pureIsDefEq k field)) && (← withReducible (pureIsDefEq E model)) && + (← withReducible (pureIsDefEq H top)) then + return some fvar + else return none + | _ => return none + | throwError "Couldn't find a `ModelWithCorners {field} {model} {top}` in the local context." + return m + -- TODO: replace this with `fromSelf` above! + fromNormedSpace : TermElabM Expr := do + if !(← withReducible (pureIsDefEq model top)) then + throwError "`{model}` is a normed space, but `{top}` is not defeq to it" + -- Check for a space of continuous linear maps. We omit a check if E is a normed space over 𝕜: + -- for `E →L[𝕜] F` to type-check in the first place, both `E` and `F` must have been normed + -- spaces over `𝕜`. + if (← isCLMReduciblyDefeqCoefficients model).isSome then + trace[Elab.DiffGeo.FunProp] "`{model}` is a space of continuous linear maps" + -- XXX: check K and the model are defeq? + let eK : Term ← Term.exprToSyntax field + let eT : Term ← Term.exprToSyntax model + Term.elabTerm (← ``(𝓘($eK, $eT))) none + else + -- Check for a normed space in the assumptions. + + if let some (K, inst) ← fromNormedSpace.fromAssumption field model then + mkAppOptM ``modelWithCornersSelf #[K, none, model, none, inst] -- omit (K, model)) for now + else + throwError "Couldn't find a `NormedSpace` structure on `{model}` among local instances." + fromNormedSpace.fromAssumption (field space : Expr) : TermElabM <| Option (Expr × Expr) := do + let some (K, inst) ← findSomeLocalInstanceOf? ``NormedSpace fun inst type ↦ do + match_expr type with + | NormedSpace K E _ _ => + if (← withReducible (pureIsDefEq K field)) && (← withReducible (pureIsDefEq E space)) then + return some (K, inst) + else return none + | _ => return none + | throwError "Couldn't find a `NormedSpace` structure on `{model}` among local instances." + trace[Elab.DiffGeo.FunPropM] "`{model}` is a normed space over the field `{K}`" + return some (K, inst) + +/-- The workhorse method for the `find_model` tactic: try to find a `ModelWithCorners` with given +base field `field`, model normed space `model` and topological space `top`, using local hypotheses +and a few hard-coded rules. No typeclass search is performed. -/ +def findModelForFunprop (field model top : Expr) : TermElabM <| Option Expr := do + trace[Elab.DiffGeo.FunPropM] "Searching for some `ModelWithCorners {field} {model} {top}`" + match ← go field model top with + | some (u, _) => return u + | _ => + trace[Elab.DiffGeo.FunPropM] "Could not find a `ModelWithCorners {field} {model} {top}`" + return none +where + /-- Workhorse method for `findModelForFunprop`: also return whether we synthesised a model + with corners on a product of normed spaces. -/ + go (field model top : Expr) : TermElabM <| Option (Expr × NormedSpaceInfo) := do + -- At first, try finding a model on the space itself. + if let some (m, r) ← findModelForFunpropInner field model top then return some (m, r) + throwError "" + +/-- The main entry point of the `find_model` tactic: connects the workhose definition +`findModelForFunProp` with the tactic world. -/ +def findModelForFunprop' (g : MVarId) : TermElabM Unit := do + match_expr (← withReducible g.getType') with + | ModelWithCorners k _ E _ _ H _ => + match ← findModelForFunprop k E H with + -- TODO: is this the way? how to do this correctly? + | some e => g.assign e + | none => throwError "Could not find a `ModelWithCorners {k} {E} {H}`" + | _ => throwError "Goal is not of the form `ModelWithCorners 𝕜 E H`" + +/-- The `find_model` tactic solves goals of the form `ModelWithCorners k E H`: +models with corners are constructed using the local context and a few built-in rules. +No typeclass search is performed for this tactic. + +This tactic is used within `fun_prop` to work with differentiability goals on manifolds. +-/ +elab (name := findModelTac) "find_model" : tactic => withMainContext do + -- We manually inline `liftMetaFinishingTactic` to allow `findModelForFunprop'` to use + -- the `TermElabM` monad (and `tryStrategy`), as this is more ergonomic. + findModelForFunprop' (← getMainGoal) + replaceMainGoal [] + +open Command in +/-- Tries to find a model with corners of a given type: if `e` is a term of type +`ModelWithCorners 𝕜 E H`, construct a model with corners using the local hypotheses and a few +built-in rules. This is the core routine for the `#find_model` command. -/ +def findModelCmd (goal : TSyntax `term) : CommandElabM Unit := do + withoutModifyingEnv <| do + runTermElabM <| fun _vars => do + -- TODO: does this do what I want it to? + let eE ← Term.elabTerm goal none + let m ← mkFreshExprMVar eE + -- TODO: how to surface error messages from the inner loop here? + findModelForFunprop' m.mvarId! + + +/-- `#find_model t` tries to construct a `ModelWithCorners` of a given type: assumes `t` is a term +of type `ModelWithCorners k E H`. This can be used to test the `find_model` tactic. +This uses local hypotheses and a few built-in rules, but does not perform typeclass search. -/ +elab (name := findModelCommand) "#find_model " goal:term : command => do findModelCmd goal + end Elab open Elab @@ -971,6 +1090,12 @@ Trace class for the `MDiff` elaborator and friends, which infer a model with cor -/ initialize registerTraceClass `Elab.DiffGeo.MDiff (inherited := true) +/-- +Trace class for the use `fun_prop` on manifolds, for trying to solve goals of the form +`ModelWithCorners 𝕜 E H` using local hypotheses and a few hard-coded rules. +-/ +initialize registerTraceClass `Elab.DiffGeo.FunPropM (inherited := true) + end trace section delaborators From f645cecffec2a443b455f09d9224afdd843e13cb Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 12 May 2026 00:56:44 +0200 Subject: [PATCH 6/8] wip. add test for this tactic; does it work already? --- .../DifferentialGeometry/FunPropM.lean | 101 ++++++++++++++++++ 1 file changed, 101 insertions(+) create mode 100644 MathlibTest/DifferentialGeometry/FunPropM.lean diff --git a/MathlibTest/DifferentialGeometry/FunPropM.lean b/MathlibTest/DifferentialGeometry/FunPropM.lean new file mode 100644 index 00000000000000..9840b2e2ebe461 --- /dev/null +++ b/MathlibTest/DifferentialGeometry/FunPropM.lean @@ -0,0 +1,101 @@ + +import Mathlib.Geometry.Manifold.Notation +import Mathlib.Geometry.Manifold.Instances.Sphere + +/-- error: Goal is not of the form `ModelWithCorners 𝕜 E H` -/ +#guard_msgs in +#find_model true + +/-- error: Goal is not of the form `ModelWithCorners 𝕜 E H` -/ +#guard_msgs in +#find_model (2 + 2 = true) + +variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type*} [NormedAddCommGroup E] + [NormedSpace 𝕜 E] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type*} + [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type*} [TopologicalSpace H'] + {I' : ModelWithCorners 𝕜 E' H'} {M : Type*} [TopologicalSpace M] [ChartedSpace H M] + {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] + {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] + +-- TODO: add #find_model as an exception to the hash_command linter, +-- or make #find_model print the model it found! +set_option linter.hashCommand false + +/-- error: Goal is not of the form `ModelWithCorners 𝕜 E H` -/ +#guard_msgs in +#find_model M + +/-- error: Goal is not of the form `ModelWithCorners 𝕜 E H` -/ +#guard_msgs in +#find_model (ModelWithCorners 𝕜) + +-- Local hypotheses (no matter if these are standard or make sense). +set_option trace.Elab.DiffGeo true in +/-- +trace: [Elab.DiffGeo.FunPropM] Searching for some `ModelWithCorners 𝕜 E H` +[Elab.DiffGeo.FunPropM] Trying to solve a goal `ModelWithCorners 𝕜 E H` +[Elab.DiffGeo.MDiff] ✅️ Assumption + [Elab.DiffGeo.MDiff] Found model: `I` +-/ +#guard_msgs in +#find_model ModelWithCorners 𝕜 E H + +#guard_msgs in +variable (I : ModelWithCorners 𝕜 (E × E) (H × E)) in +#find_model ModelWithCorners 𝕜 (E × E) (H × E) + +#guard_msgs in +variable (I := I.prod I) in +#find_model ModelWithCorners 𝕜 (E × E) (ModelProd H H) + +set_option trace.Elab.DiffGeo true in +/-- +error: ⏎ +--- +trace: [Elab.DiffGeo.FunPropM] Searching for some `ModelWithCorners 𝕜 E →L[𝕜] E E →L[𝕜] E` +[Elab.DiffGeo.FunPropM] Trying to solve a goal `ModelWithCorners 𝕜 E →L[𝕜] E E →L[𝕜] E` +[Elab.DiffGeo.MDiff] ❌️ Assumption + [Elab.DiffGeo.MDiff] Failed with error: + Couldn't find a `ModelWithCorners 𝕜 E →L[𝕜] E E →L[𝕜] E` in the local context. +[Elab.DiffGeo.MDiff] ❌️ Normed space + [Elab.DiffGeo.MDiff] Failed with error: + elaboration function for `Manifold.«term𝓘(_,_)»` has not been implemented + 𝓘(?m✝, ?m✝¹) +-/ +#guard_msgs in +#find_model ModelWithCorners 𝕜 (E →L[𝕜] E) (E →L[𝕜] E) + +-- TODO: why are the error messages being swallowed? + +set_option trace.Elab.DiffGeo true in +/-- +error: ⏎ +--- +trace: [Elab.DiffGeo.FunPropM] Searching for some `ModelWithCorners 𝕜 E H'` +[Elab.DiffGeo.FunPropM] Trying to solve a goal `ModelWithCorners 𝕜 E H'` +[Elab.DiffGeo.MDiff] ❌️ Assumption + [Elab.DiffGeo.MDiff] Failed with error: + Couldn't find a `ModelWithCorners 𝕜 E H'` in the local context. +[Elab.DiffGeo.MDiff] ❌️ Normed space + [Elab.DiffGeo.MDiff] Failed with error: + `E` is a normed space, but `H'` is not defeq to it +-/ +#guard_msgs in +#find_model ModelWithCorners 𝕜 E H' + +-- Normed fields: TODO implement this! +/-- error: -/ +#guard_msgs in +#find_model ModelWithCorners 𝕜 𝕜 𝕜 + +/-- error: -/ +#guard_msgs in +#find_model ModelWithCorners ℝ ℝ ℝ + +/-- error: -/ +#guard_msgs in +#find_model ModelWithCorners ℂ ℂ ℂ + +-- Euclidean space. (check the hypotheses) + +-- what about products? disjoint unions? open subsets? From 2ffd0dfad391d768e99dc5dddba70767b5d13180 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 12 May 2026 04:49:15 +0200 Subject: [PATCH 7/8] Fix the build; untested --- Mathlib/Geometry/Manifold/Notation.lean | 30 ++++++++++++------------- 1 file changed, 14 insertions(+), 16 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index 228a7db05355e8..373dc07215e5db 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -809,12 +809,10 @@ def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do topological space, using information from the local context and a few hard-coded rules. -/ -- FIXME: do we need to handle baseInfo again? perhaps not, let's try without! def findModelForFunpropInner (field model top : Expr) : - TermElabM <| Option (Expr × NormedSpaceInfo) := do + TermElabM <| Option FindModelResult := do trace[Elab.DiffGeo.FunPropM] "Trying to solve a goal `ModelWithCorners {field} {model} {top}`" - if let some m ← tryStrategy m!"Assumption" fromAssumption then - return some (m, none) - if let some m ← tryStrategy m!"Normed space" fromNormedSpace then - return some (m, none) + if let some m ← tryStrategy m!"Assumption" fromAssumption then return some m + if let some m ← tryStrategy m!"Normed space" fromNormedSpace then return some m -- TODO: implement the remaining strategies, and then the inner to outer part! return none where @@ -839,19 +837,19 @@ where -- Check for a space of continuous linear maps. We omit a check if E is a normed space over 𝕜: -- for `E →L[𝕜] F` to type-check in the first place, both `E` and `F` must have been normed -- spaces over `𝕜`. - if (← isCLMReduciblyDefeqCoefficients model).isSome then + try + let (_k, _V, _W) ← isCLMReduciblyDefeqCoefficients model trace[Elab.DiffGeo.FunProp] "`{model}` is a space of continuous linear maps" -- XXX: check K and the model are defeq? let eK : Term ← Term.exprToSyntax field let eT : Term ← Term.exprToSyntax model Term.elabTerm (← ``(𝓘($eK, $eT))) none - else - -- Check for a normed space in the assumptions. - - if let some (K, inst) ← fromNormedSpace.fromAssumption field model then - mkAppOptM ``modelWithCornersSelf #[K, none, model, none, inst] -- omit (K, model)) for now - else - throwError "Couldn't find a `NormedSpace` structure on `{model}` among local instances." + catch _ => + -- Check for a normed space in the assumptions. + if let some (K, inst) ← fromNormedSpace.fromAssumption field model then + mkAppOptM ``modelWithCornersSelf #[K, none, model, none, inst] -- omit (K, model)) for now + else + throwError "Couldn't find a `NormedSpace` structure on `{model}` among local instances." fromNormedSpace.fromAssumption (field space : Expr) : TermElabM <| Option (Expr × Expr) := do let some (K, inst) ← findSomeLocalInstanceOf? ``NormedSpace fun inst type ↦ do match_expr type with @@ -870,16 +868,16 @@ and a few hard-coded rules. No typeclass search is performed. -/ def findModelForFunprop (field model top : Expr) : TermElabM <| Option Expr := do trace[Elab.DiffGeo.FunPropM] "Searching for some `ModelWithCorners {field} {model} {top}`" match ← go field model top with - | some (u, _) => return u + | some { model := u } => return u | _ => trace[Elab.DiffGeo.FunPropM] "Could not find a `ModelWithCorners {field} {model} {top}`" return none where /-- Workhorse method for `findModelForFunprop`: also return whether we synthesised a model with corners on a product of normed spaces. -/ - go (field model top : Expr) : TermElabM <| Option (Expr × NormedSpaceInfo) := do + go (field model top : Expr) : TermElabM <| Option FindModelResult := do -- At first, try finding a model on the space itself. - if let some (m, r) ← findModelForFunpropInner field model top then return some (m, r) + if let some m ← findModelForFunpropInner field model top then return some m throwError "" /-- The main entry point of the `find_model` tactic: connects the workhose definition From 93bab93fa39f69b853e2390b34cb8840b507c82a Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 12 May 2026 04:54:16 +0200 Subject: [PATCH 8/8] tracing output update --- MathlibTest/DifferentialGeometry/FunPropM.lean | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/MathlibTest/DifferentialGeometry/FunPropM.lean b/MathlibTest/DifferentialGeometry/FunPropM.lean index 9840b2e2ebe461..c8eeff1be6fcfd 100644 --- a/MathlibTest/DifferentialGeometry/FunPropM.lean +++ b/MathlibTest/DifferentialGeometry/FunPropM.lean @@ -1,4 +1,3 @@ - import Mathlib.Geometry.Manifold.Notation import Mathlib.Geometry.Manifold.Instances.Sphere @@ -54,13 +53,13 @@ error: ⏎ --- trace: [Elab.DiffGeo.FunPropM] Searching for some `ModelWithCorners 𝕜 E →L[𝕜] E E →L[𝕜] E` [Elab.DiffGeo.FunPropM] Trying to solve a goal `ModelWithCorners 𝕜 E →L[𝕜] E E →L[𝕜] E` -[Elab.DiffGeo.MDiff] ❌️ Assumption +[Elab.DiffGeo.MDiff] 💥️ Assumption [Elab.DiffGeo.MDiff] Failed with error: Couldn't find a `ModelWithCorners 𝕜 E →L[𝕜] E E →L[𝕜] E` in the local context. -[Elab.DiffGeo.MDiff] ❌️ Normed space +[Elab.DiffGeo.MDiff] 💥️ Normed space + [Elab.DiffGeo.MDiff] `E →L[𝕜] E` is a space of continuous (semi-)linear maps [Elab.DiffGeo.MDiff] Failed with error: - elaboration function for `Manifold.«term𝓘(_,_)»` has not been implemented - 𝓘(?m✝, ?m✝¹) + Couldn't find a `NormedSpace` structure on `E →L[𝕜] E` among local instances. -/ #guard_msgs in #find_model ModelWithCorners 𝕜 (E →L[𝕜] E) (E →L[𝕜] E) @@ -73,10 +72,10 @@ error: ⏎ --- trace: [Elab.DiffGeo.FunPropM] Searching for some `ModelWithCorners 𝕜 E H'` [Elab.DiffGeo.FunPropM] Trying to solve a goal `ModelWithCorners 𝕜 E H'` -[Elab.DiffGeo.MDiff] ❌️ Assumption +[Elab.DiffGeo.MDiff] 💥️ Assumption [Elab.DiffGeo.MDiff] Failed with error: Couldn't find a `ModelWithCorners 𝕜 E H'` in the local context. -[Elab.DiffGeo.MDiff] ❌️ Normed space +[Elab.DiffGeo.MDiff] 💥️ Normed space [Elab.DiffGeo.MDiff] Failed with error: `E` is a normed space, but `H'` is not defeq to it -/