dev: towards fun_prop on manifolds

Mathlib/Geometry/Manifold/Notation.lean

@@ -805,6 +805,123 @@ 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 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
+  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
+  -- 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 `𝕜`.
+    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
+    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
+        | 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 { 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 FindModelResult := do
+    -- At first, try finding a model on the space itself.
+    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
+`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 +1088,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

Mathlib/Tactic/FunProp/Core.lean

@@ -71,7 +71,11 @@ def synthesizeArgs (thmId : Origin) (xs : Array Expr)
       else
         -- try user provided discharger
         let ctx : Context ← read
-        if (← isProp type) then
+        -- 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
               continue

MathlibTest/DifferentialGeometry/FunPropM.lean

@@ -0,0 +1,100 @@
+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] `E →L[𝕜] E` is a space of continuous (semi-)linear maps
+  [Elab.DiffGeo.MDiff] Failed with error:
+      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)
+
+-- 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?

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
+
+/-! Test imitating the discharging of `ModelWithCorners` metavariables -/
+section MDifferentiableMock
+
+variable {α β γ δ ι : Type*} {E : ι → Type*}
+
+class Dummy (A : Type*)
+instance : Dummy A := ⟨⟩
+
+/-- Mock model-with-corners data.
+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 := ()
+
+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 x ↦ x.1 + x.2) := silentSorry
+@[fun_prop]
+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
+  fail_if_success fun_prop
+  fun_prop (disch := assumption)
+
+end MDifferentiableMock