From 1156f65bb67faf671df5ba4e0e0cb8e2b5951d9b Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 7 Oct 2025 10:45:46 -0700 Subject: [PATCH 01/22] wip: support partial homeos and partial equivs Tests still fial, but one is a clear bug in my code --- Mathlib/Geometry/Manifold/Notation.lean | 6 +++++ .../DifferentialGeometry/Notation.lean | 27 +++++++++++++++++++ 2 files changed, 33 insertions(+) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index 52b60ff0e38028..32ed1844585823 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -337,6 +337,12 @@ def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do the set {es} : {estype}" let tgtI ← findModel tgt (src, srcI) return (srcI, tgtI) + | mkApp4 (.const ``OpenPartialHomeomorph [_uX, _uY]) X Y _ _ => + trace[Elab.DiffGeo.MDiff] m!"found a partial homeomorphism from {X} to {Y}" + return (X, Y) + | mkApp4 (.const ``PartialEquiv [_uX, _uY]) X Y _ _ => + trace[Elab.DiffGeo.MDiff] m!"found a partial equivalence from {X} to {Y}" + return (X, Y) | _ => throwError "Expected{indentD e}\nof type{indentD etype}\nto be a function" end Elab diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index 1620190e4fb9a9..8a69c180bed569 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -120,6 +120,33 @@ variable {f : M → M'} {s : Set M} {m : M} #guard_msgs in #check MDiff[s] f +-- A partial homeomorphism or partial equivalence. +variable {φ : OpenPartialHomeomorph M E} {ψ : PartialEquiv M E} + +#check MDifferentiableWithinAt I 𝓘(𝕜, E) ψ +#check MDifferentiableWithinAt I 𝓘(𝕜, E) ψ s +/-- +error: Application type mismatch: The argument + M +has type + Type u_4 +but is expected to have type + ModelWithCorners ?𝕜 ?E ?H +in the application + @MDifferentiableWithinAt ?𝕜 ?inst✝ ?E ?inst✝¹ ?inst✝² ?H ?inst✝³ M +-/ +#guard_msgs in +#check MDiffAt[s] φ +/-- +error: Expected + ψ +of type + PartialEquiv M E +to be a function +-/ +#guard_msgs in +#check MDiffAt[s] ψ + -- Testing an error message. section From b1423f0414e9305bd4b57205634770ac023cbaa4 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 7 Oct 2025 10:49:58 -0700 Subject: [PATCH 02/22] Progress --- Mathlib/Geometry/Manifold/Notation.lean | 16 +++++++++------- MathlibTest/DifferentialGeometry/Notation.lean | 13 ++++++++----- 2 files changed, 17 insertions(+), 12 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index 32ed1844585823..c8d89d69526475 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -337,13 +337,15 @@ def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do the set {es} : {estype}" let tgtI ← findModel tgt (src, srcI) return (srcI, tgtI) - | mkApp4 (.const ``OpenPartialHomeomorph [_uX, _uY]) X Y _ _ => - trace[Elab.DiffGeo.MDiff] m!"found a partial homeomorphism from {X} to {Y}" - return (X, Y) - | mkApp4 (.const ``PartialEquiv [_uX, _uY]) X Y _ _ => - trace[Elab.DiffGeo.MDiff] m!"found a partial equivalence from {X} to {Y}" - return (X, Y) - | _ => throwError "Expected{indentD e}\nof type{indentD etype}\nto be a function" + | _ => + match_expr etype with + | OpenPartialHomeomorph X Y _ _ => + trace[Elab.DiffGeo.MDiff] m!"found a partial homeomorphism from {X} to {Y}" + return (X, Y) + | PartialEquiv X Y => + trace[Elab.DiffGeo.MDiff] m!"found a partial equivalence from {X} to {Y}" + return (X, Y) + | _ => throwError "Expected{indentD e}\nof type{indentD etype}\nto be a function" end Elab diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index 8a69c180bed569..eea48096f883f8 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -138,11 +138,14 @@ in the application #guard_msgs in #check MDiffAt[s] φ /-- -error: Expected - ψ -of type - PartialEquiv M E -to be a function +error: Application type mismatch: The argument + M +has type + Type u_4 +but is expected to have type + ModelWithCorners ?𝕜 ?E ?H +in the application + @MDifferentiableWithinAt ?𝕜 ?inst✝ ?E ?inst✝¹ ?inst✝² ?H ?inst✝³ M -/ #guard_msgs in #check MDiffAt[s] ψ From ff45f43a08f36699913c80e102be9fb1942f721c Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 7 Oct 2025 10:56:47 -0700 Subject: [PATCH 03/22] wip: copied the missing code; need to dedup And probably, want to insert a coercion... --- Mathlib/Geometry/Manifold/Notation.lean | 40 ++++++++++++++++--- .../DifferentialGeometry/Notation.lean | 21 ++++++---- 2 files changed, 47 insertions(+), 14 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index c8d89d69526475..4bf94abd4569fb 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -339,12 +339,40 @@ def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do return (srcI, tgtI) | _ => match_expr etype with - | OpenPartialHomeomorph X Y _ _ => - trace[Elab.DiffGeo.MDiff] m!"found a partial homeomorphism from {X} to {Y}" - return (X, Y) - | PartialEquiv X Y => - trace[Elab.DiffGeo.MDiff] m!"found a partial equivalence from {X} to {Y}" - return (X, Y) + | OpenPartialHomeomorph src tgt _ _ => + trace[Elab.DiffGeo.MDiff] m!"found a partial homeomorphism from {src} to {tgt}" + if tgt.hasLooseBVars then + -- TODO: try `T%` here, and if it works, add an interactive suggestion to use it + throwError "Term {e} is a dependent function, of type {etype}\nHint: you can use the `T%` \ + elaborator to convert a dependent function to a non-dependent one" + let srcI ← findModel src + if let some es := es then + let estype ← inferType es + /- Note: we use `isDefEq` here since persistent metavariable assignments in `src` and + `estype` are acceptable. + TODO: consider attempting to coerce `es` to a `Set`. -/ + if !(← isDefEq estype <|← mkAppM ``Set #[src]) then + throwError "The domain {src} of {e} is not definitionally equal to the carrier type of \ + the set {es} : {estype}" + let tgtI ← findModel tgt (src, srcI) + return (srcI, tgtI) + | PartialEquiv src tgt => + trace[Elab.DiffGeo.MDiff] m!"found a partial equivalence from {src} to {tgt}" + if tgt.hasLooseBVars then + -- TODO: try `T%` here, and if it works, add an interactive suggestion to use it + throwError "Term {e} is a dependent function, of type {etype}\nHint: you can use the `T%` \ + elaborator to convert a dependent function to a non-dependent one" + let srcI ← findModel src + if let some es := es then + let estype ← inferType es + /- Note: we use `isDefEq` here since persistent metavariable assignments in `src` and + `estype` are acceptable. + TODO: consider attempting to coerce `es` to a `Set`. -/ + if !(← isDefEq estype <|← mkAppM ``Set #[src]) then + throwError "The domain {src} of {e} is not definitionally equal to the carrier type of \ + the set {es} : {estype}" + let tgtI ← findModel tgt (src, srcI) + return (srcI, tgtI) | _ => throwError "Expected{indentD e}\nof type{indentD etype}\nto be a function" end Elab diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index eea48096f883f8..edcbd12f1976e9 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -125,31 +125,36 @@ variable {φ : OpenPartialHomeomorph M E} {ψ : PartialEquiv M E} #check MDifferentiableWithinAt I 𝓘(𝕜, E) ψ #check MDifferentiableWithinAt I 𝓘(𝕜, E) ψ s + + /-- error: Application type mismatch: The argument - M + φ has type - Type u_4 + OpenPartialHomeomorph M E but is expected to have type - ModelWithCorners ?𝕜 ?E ?H + ?M → ?M' in the application - @MDifferentiableWithinAt ?𝕜 ?inst✝ ?E ?inst✝¹ ?inst✝² ?H ?inst✝³ M + MDifferentiableWithinAt I 𝓘(𝕜, E) φ -/ #guard_msgs in #check MDiffAt[s] φ + /-- error: Application type mismatch: The argument - M + ψ has type - Type u_4 + PartialEquiv M E but is expected to have type - ModelWithCorners ?𝕜 ?E ?H + ?M → ?M' in the application - @MDifferentiableWithinAt ?𝕜 ?inst✝ ?E ?inst✝¹ ?inst✝² ?H ?inst✝³ M + MDifferentiableWithinAt I 𝓘(𝕜, E) ψ -/ #guard_msgs in #check MDiffAt[s] ψ +#exit + -- Testing an error message. section From 7a4facf79e5efb32bebeba2fdd77639adc9368cc Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 7 Oct 2025 21:05:37 -0700 Subject: [PATCH 04/22] Better approach; add tests for the remaining cases --- Mathlib/Geometry/Manifold/Notation.lean | 65 +++++----------- .../DifferentialGeometry/Notation.lean | 75 +++++++++++++------ 2 files changed, 69 insertions(+), 71 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index 4bf94abd4569fb..f57d8cd7423d25 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -312,6 +312,13 @@ where let iTerm : Term ← ``(𝓘($eT, $eT)) Term.elabTerm iTerm none +/-- Ensures that `e` is a function. Attempts to coerce `e` to a function if necessary. -/ +def ensureIsFunction (e : Expr) : MetaM Expr := do + let ty ← whnf <|← instantiateMVars <|← inferType e + if ty.isForall then return e else (← coerceToFunction? e).getDM <| + throwError "Expected{indentD e}\nof type{indentD ty}\nto be a function, or to be coercible to \ + a function" + /-- If the type of `e` is a non-dependent function between spaces `src` and `tgt`, try to find a model with corners on both `src` and `tgt`. If successful, return both models. @@ -337,43 +344,7 @@ def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do the set {es} : {estype}" let tgtI ← findModel tgt (src, srcI) return (srcI, tgtI) - | _ => - match_expr etype with - | OpenPartialHomeomorph src tgt _ _ => - trace[Elab.DiffGeo.MDiff] m!"found a partial homeomorphism from {src} to {tgt}" - if tgt.hasLooseBVars then - -- TODO: try `T%` here, and if it works, add an interactive suggestion to use it - throwError "Term {e} is a dependent function, of type {etype}\nHint: you can use the `T%` \ - elaborator to convert a dependent function to a non-dependent one" - let srcI ← findModel src - if let some es := es then - let estype ← inferType es - /- Note: we use `isDefEq` here since persistent metavariable assignments in `src` and - `estype` are acceptable. - TODO: consider attempting to coerce `es` to a `Set`. -/ - if !(← isDefEq estype <|← mkAppM ``Set #[src]) then - throwError "The domain {src} of {e} is not definitionally equal to the carrier type of \ - the set {es} : {estype}" - let tgtI ← findModel tgt (src, srcI) - return (srcI, tgtI) - | PartialEquiv src tgt => - trace[Elab.DiffGeo.MDiff] m!"found a partial equivalence from {src} to {tgt}" - if tgt.hasLooseBVars then - -- TODO: try `T%` here, and if it works, add an interactive suggestion to use it - throwError "Term {e} is a dependent function, of type {etype}\nHint: you can use the `T%` \ - elaborator to convert a dependent function to a non-dependent one" - let srcI ← findModel src - if let some es := es then - let estype ← inferType es - /- Note: we use `isDefEq` here since persistent metavariable assignments in `src` and - `estype` are acceptable. - TODO: consider attempting to coerce `es` to a `Set`. -/ - if !(← isDefEq estype <|← mkAppM ``Set #[src]) then - throwError "The domain {src} of {e} is not definitionally equal to the carrier type of \ - the set {es} : {estype}" - let tgtI ← findModel tgt (src, srcI) - return (srcI, tgtI) - | _ => throwError "Expected{indentD e}\nof type{indentD etype}\nto be a function" + | _ => throwError "Expected{indentD e}\nof type{indentD etype}\nto be a function" end Elab @@ -384,7 +355,7 @@ trying to determine `I` and `J` from the local context. The argument `x` can be omitted. -/ scoped elab:max "MDiffAt[" s:term "]" ppSpace f:term:arg : term => do let es ← Term.elabTerm s none - let ef ← Term.elabTerm f none + let ef ← ensureIsFunction <|← Term.elabTerm f none let (srcI, tgtI) ← findModels ef es mkAppM ``MDifferentiableWithinAt #[srcI, tgtI, ef, es] @@ -392,7 +363,7 @@ scoped elab:max "MDiffAt[" s:term "]" ppSpace f:term:arg : term => do trying to determine `I` and `J` from the local context. The argument `x` can be omitted. -/ scoped elab:max "MDiffAt" ppSpace t:term:arg : term => do - let e ← Term.elabTerm t none + let e ← ensureIsFunction <|← Term.elabTerm t none let (srcI, tgtI) ← findModels e none mkAppM ``MDifferentiableAt #[srcI, tgtI, e] @@ -419,14 +390,14 @@ scoped elab:max "MDiffAt" ppSpace t:term:arg : term => do trying to determine `I` and `J` from the local context. -/ scoped elab:max "MDiff[" s:term "]" ppSpace t:term:arg : term => do let es ← Term.elabTerm s none - let et ← Term.elabTerm t none + let et ← ensureIsFunction <|← Term.elabTerm t none let (srcI, tgtI) ← findModels et es mkAppM ``MDifferentiableOn #[srcI, tgtI, et, es] /-- `MDiff f` elaborates to `MDifferentiable I J f`, trying to determine `I` and `J` from the local context. -/ scoped elab:max "MDiff" ppSpace t:term:arg : term => do - let e ← Term.elabTerm t none + let e ← ensureIsFunction <|← Term.elabTerm t none let (srcI, tgtI) ← findModels e none mkAppM ``MDifferentiable #[srcI, tgtI, e] @@ -436,7 +407,7 @@ trying to determine `I` and `J` from the local context. The argument `x` can be omitted. -/ scoped elab:max "CMDiffAt[" s:term "]" ppSpace nt:term:arg ppSpace f:term:arg : term => do let es ← Term.elabTerm s none - let ef ← Term.elabTerm f none + let ef ← ensureIsFunction <|← Term.elabTerm f none let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞) let (srcI, tgtI) ← findModels ef es mkAppM ``ContMDiffWithinAt #[srcI, tgtI, ne, ef, es] @@ -446,7 +417,7 @@ trying to determine `I` and `J` from the local context. `n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported). The argument `x` can be omitted. -/ scoped elab:max "CMDiffAt" ppSpace nt:term:arg ppSpace t:term:arg : term => do - let e ← Term.elabTerm t none + let e ← ensureIsFunction <|← Term.elabTerm t none let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞) let (srcI, tgtI) ← findModels e none mkAppM ``ContMDiffAt #[srcI, tgtI, ne, e] @@ -456,7 +427,7 @@ trying to determine `I` and `J` from the local context. `n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported). -/ scoped elab:max "CMDiff[" s:term "]" ppSpace nt:term:arg ppSpace f:term:arg : term => do let es ← Term.elabTerm s none - let ef ← Term.elabTerm f none + let ef ← ensureIsFunction <|← Term.elabTerm f none let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞) let (srcI, tgtI) ← findModels ef es mkAppM ``ContMDiffOn #[srcI, tgtI, ne, ef, es] @@ -465,7 +436,7 @@ scoped elab:max "CMDiff[" s:term "]" ppSpace nt:term:arg ppSpace f:term:arg : te trying to determine `I` and `J` from the local context. `n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported). -/ scoped elab:max "CMDiff" ppSpace nt:term:arg ppSpace f:term:arg : term => do - let e ← Term.elabTerm f none + let e ← ensureIsFunction <|← Term.elabTerm f none let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞) let (srcI, tgtI) ← findModels e none mkAppM ``ContMDiff #[srcI, tgtI, ne, e] @@ -474,14 +445,14 @@ scoped elab:max "CMDiff" ppSpace nt:term:arg ppSpace f:term:arg : term => do trying to determine `I` and `J` from the local context. -/ scoped elab:max "mfderiv[" s:term "]" ppSpace t:term:arg : term => do let es ← Term.elabTerm s none - let e ← Term.elabTerm t none + let e ← ensureIsFunction <|← Term.elabTerm t none let (srcI, tgtI) ← findModels e es mkAppM ``mfderivWithin #[srcI, tgtI, e, es] /-- `mfderiv% f x` elaborates to `mfderiv I J f x`, trying to determine `I` and `J` from the local context. -/ scoped elab:max "mfderiv%" ppSpace t:term:arg : term => do - let e ← Term.elabTerm t none + let e ← ensureIsFunction <|← Term.elabTerm t none let (srcI, tgtI) ← findModels e none mkAppM ``mfderiv #[srcI, tgtI, e] diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index edcbd12f1976e9..137e6987691007 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -120,40 +120,67 @@ variable {f : M → M'} {s : Set M} {m : M} #guard_msgs in #check MDiff[s] f --- A partial homeomorphism or partial equivalence. +/-! A partial homeomorphism or partial equivalence. More generally, this works for any type +with a coercion to (possibly dependent) functions. -/ +section coercion + variable {φ : OpenPartialHomeomorph M E} {ψ : PartialEquiv M E} -#check MDifferentiableWithinAt I 𝓘(𝕜, E) ψ -#check MDifferentiableWithinAt I 𝓘(𝕜, E) ψ s +/-- info: MDifferentiableWithinAt I 𝓘(𝕜, E) (↑φ) s : M → Prop -/ +#guard_msgs in +#check MDiffAt[s] φ +/-- info: MDifferentiableWithinAt I 𝓘(𝕜, E) (↑ψ) s : M → Prop -/ +#guard_msgs in +#check MDiffAt[s] ψ -/-- -error: Application type mismatch: The argument - φ -has type - OpenPartialHomeomorph M E -but is expected to have type - ?M → ?M' -in the application - MDifferentiableWithinAt I 𝓘(𝕜, E) φ --/ +/-- info: MDifferentiableAt I 𝓘(𝕜, E) ↑φ : M → Prop -/ #guard_msgs in -#check MDiffAt[s] φ +#check MDiffAt φ + +/-- info: MDifferentiableAt I 𝓘(𝕜, E) ↑ψ : M → Prop -/ +#guard_msgs in +#check MDiffAt ψ + +/-- info: MDifferentiableOn I 𝓘(𝕜, E) (↑φ) s : Prop -/ +#guard_msgs in +#check MDiff[s] φ + +/-- info: MDifferentiableOn I 𝓘(𝕜, E) (↑ψ) s : Prop -/ +#guard_msgs in +#check MDiff[s] ψ + +/-- info: MDifferentiable I 𝓘(𝕜, E) ↑φ : Prop -/ +#guard_msgs in +#check MDiff φ + +/-- info: ContMDiffWithinAt I 𝓘(𝕜, E) 2 (↑ψ) s : M → Prop -/ +#guard_msgs in +#check CMDiffAt[s] 2 ψ + +/-- info: ContMDiffOn I 𝓘(𝕜, E) 2 (↑φ) s : Prop -/ +#guard_msgs in +#check CMDiff[s] 2 φ + +/-- info: ContMDiffAt I 𝓘(𝕜, E) 2 ↑φ : M → Prop -/ +#guard_msgs in +#check CMDiffAt 2 φ + +/-- info: ContMDiff I 𝓘(𝕜, E) 2 ↑ψ : Prop -/ +#guard_msgs in +#check CMDiff 2 ψ + +/-- info: mfderiv I 𝓘(𝕜, E) ↑φ : (x : M) → TangentSpace I x →L[𝕜] TangentSpace 𝓘(𝕜, E) (↑φ x) -/ +#guard_msgs in +#check mfderiv% φ /-- -error: Application type mismatch: The argument - ψ -has type - PartialEquiv M E -but is expected to have type - ?M → ?M' -in the application - MDifferentiableWithinAt I 𝓘(𝕜, E) ψ +info: mfderivWithin I 𝓘(𝕜, E) (↑ψ) s : (x : M) → TangentSpace I x →L[𝕜] TangentSpace 𝓘(𝕜, E) (↑ψ x) -/ #guard_msgs in -#check MDiffAt[s] ψ +#check mfderiv[s] ψ -#exit +end coercion -- Testing an error message. section From d5aa960d061686318fe72d9b395069a8e2fa040f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 7 Oct 2025 21:16:01 -0700 Subject: [PATCH 05/22] Typo fix --- MathlibTest/DifferentialGeometry/Notation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index 137e6987691007..e9dc98d499ab07 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -544,7 +544,7 @@ variable [IsManifold I 1 M] [IsManifold I' 1 M'] -- TODO: can there be better error messages when forgetting the smoothness exponent? section error --- yields a parse error, "unexpected toekn '/--'; expected term" +-- yields a parse error, "unexpected token '/--'; expected term" -- #check CMDiffAt[s] f /-- From 27ede4a6f7939e9707ae2cdccc7670068bfd9932 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 7 Oct 2025 21:19:41 -0700 Subject: [PATCH 06/22] Note a regressed error message --- .../DifferentialGeometry/Notation.lean | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index e9dc98d499ab07..f8b5fe317bd0f3 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -547,7 +547,8 @@ section error -- yields a parse error, "unexpected token '/--'; expected term" -- #check CMDiffAt[s] f -/-- +-- TODO: the old error message here was better; somehow restore it! +/- error: Type mismatch f has type @@ -555,30 +556,24 @@ has type of sort `Type (max u_10 u_4)` but is expected to have type WithTop ℕ∞ of sort `Type` ---- +-/ + +/-- error: Expected m of type M -to be a function +to be a function, or to be coercible to a function -/ #guard_msgs in #check CMDiffAt[s] f m /-- -error: Type mismatch - f -has type - M → M' -of sort `Type (max u_10 u_4)` but is expected to have type - WithTop ℕ∞ -of sort `Type` ---- error: Expected m of type M -to be a function +to be a function, or to be coercible to a function -/ #guard_msgs in #check CMDiffAt[s] f m From ad86d3e4eefcb30ef8ee9b8c3e0dc585942a169a Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 7 Oct 2025 21:23:47 -0700 Subject: [PATCH 07/22] Restore --- Mathlib/Geometry/Manifold/Notation.lean | 6 +++--- MathlibTest/DifferentialGeometry/Notation.lean | 17 +++++++++++------ 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index f57d8cd7423d25..70738e65b20a83 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -407,8 +407,8 @@ trying to determine `I` and `J` from the local context. The argument `x` can be omitted. -/ scoped elab:max "CMDiffAt[" s:term "]" ppSpace nt:term:arg ppSpace f:term:arg : term => do let es ← Term.elabTerm s none - let ef ← ensureIsFunction <|← Term.elabTerm f none let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞) + let ef ← ensureIsFunction <|← Term.elabTerm f none let (srcI, tgtI) ← findModels ef es mkAppM ``ContMDiffWithinAt #[srcI, tgtI, ne, ef, es] @@ -427,8 +427,8 @@ trying to determine `I` and `J` from the local context. `n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported). -/ scoped elab:max "CMDiff[" s:term "]" ppSpace nt:term:arg ppSpace f:term:arg : term => do let es ← Term.elabTerm s none - let ef ← ensureIsFunction <|← Term.elabTerm f none let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞) + let ef ← ensureIsFunction <|← Term.elabTerm f none let (srcI, tgtI) ← findModels ef es mkAppM ``ContMDiffOn #[srcI, tgtI, ne, ef, es] @@ -436,8 +436,8 @@ scoped elab:max "CMDiff[" s:term "]" ppSpace nt:term:arg ppSpace f:term:arg : te trying to determine `I` and `J` from the local context. `n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported). -/ scoped elab:max "CMDiff" ppSpace nt:term:arg ppSpace f:term:arg : term => do - let e ← ensureIsFunction <|← Term.elabTerm f none let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞) + let e ← ensureIsFunction <|← Term.elabTerm f none let (srcI, tgtI) ← findModels e none mkAppM ``ContMDiff #[srcI, tgtI, ne, e] diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index f8b5fe317bd0f3..571b20df1691ed 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -541,14 +541,13 @@ variable {f : M → M'} {s : Set M} {m : M} variable [IsManifold I 1 M] [IsManifold I' 1 M'] --- TODO: can there be better error messages when forgetting the smoothness exponent? +-- Testing error messages when forgetting the smoothness exponent or swapping arguments. section error -- yields a parse error, "unexpected token '/--'; expected term" -- #check CMDiffAt[s] f --- TODO: the old error message here was better; somehow restore it! -/- +/-- error: Type mismatch f has type @@ -556,9 +555,7 @@ has type of sort `Type (max u_10 u_4)` but is expected to have type WithTop ℕ∞ of sort `Type` --/ - -/-- +--- error: Expected m of type @@ -569,6 +566,14 @@ to be a function, or to be coercible to a function #check CMDiffAt[s] f m /-- +error: Type mismatch + f +has type + M → M' +of sort `Type (max u_10 u_4)` but is expected to have type + WithTop ℕ∞ +of sort `Type` +--- error: Expected m of type From 72eb400cb76e8c20e39ed59689fdaba5f5810819 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 7 Oct 2025 21:26:44 -0700 Subject: [PATCH 08/22] One more test --- Mathlib/Geometry/Manifold/Notation.lean | 3 +++ .../DifferentialGeometry/Notation.lean | 22 +++++++++++++++++-- 2 files changed, 23 insertions(+), 2 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index 70738e65b20a83..da3e2237e0c8a2 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -401,6 +401,9 @@ scoped elab:max "MDiff" ppSpace t:term:arg : term => do let (srcI, tgtI) ← findModels e none mkAppM ``MDifferentiable #[srcI, tgtI, e] +-- We ensure the type of `n` before checking `f` is a function to provide better error messages +-- in case e.g. just `n` was forgotten. + /-- `CMDiffAt[s] n f x` elaborates to `ContMDiffWithinAt I J n f s x`, trying to determine `I` and `J` from the local context. `n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported). diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index 571b20df1691ed..fa4a78341cc13b 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -581,11 +581,29 @@ of type to be a function, or to be coercible to a function -/ #guard_msgs in -#check CMDiffAt[s] f m +#check CMDiff[s] f m --- yields a parse error, "unexpected toekn '/--'; expected term" +-- yields a parse error, "unexpected token '/--'; expected term" -- #check CMDiffAt f +/-- +error: Type mismatch + f +has type + M → M' +of sort `Type (max u_10 u_4)` but is expected to have type + WithTop ℕ∞ +of sort `Type` +--- +error: Expected + n +of type + Option ℕ∞ +to be a function, or to be coercible to a function +-/ +#guard_msgs in +#check CMDiff f n + end error /-- info: ContMDiffWithinAt I I' 1 f s : M → Prop -/ From 835362615642d78b65f6705ac2fda26d1ae80f0b Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 7 Oct 2025 21:28:43 -0700 Subject: [PATCH 09/22] Update docs --- Mathlib/Geometry/Manifold/Notation.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index da3e2237e0c8a2..fb11e846759653 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -67,7 +67,7 @@ variable {s : E → E'} in These elaborators can be combined: `CMDiffAt[u] n (T% s) x` **Warning.** These elaborators are a proof of concept; the implementation should be considered a -prototype. Don't rewrite all of mathlib to use it just yet. Notable bugs and limitations include +prototype. Don't rewrite all of mathlib to use it just yet. Notable limitations include the following. ## TODO @@ -76,10 +76,8 @@ the following. is correct 90% of the time). For products of vector spaces `E × F`, this could print a warning about making a choice between the model in `E × F` and the product of the models on `E` and `F`. -- extend the elaborators to support `OpenPartialHomeomorph`s and `PartialEquiv`s -- better error messages (as needed) -- further testing and fixing of edge cases -- add tests for all of the above +- better error messages (as needed), with tests +- further testing and fixing of edge cases (with tests) - add delaborators for these elaborators -/ From c9d331eb42bdd4e8d0a6d1551ab79dcab0fc91b9 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 8 Oct 2025 11:16:08 -0700 Subject: [PATCH 10/22] chore: slightly better headings for the tests file --- MathlibTest/DifferentialGeometry/Notation.lean | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index fa4a78341cc13b..01c589b98e23e2 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -92,11 +92,13 @@ end TotalSpace /-! Tests for the elaborators for `MDifferentiable{WithinAt,At,On}`. -/ section differentiability --- Start with some basic tests: a simple function, both in applied and unapplied form. variable {EM' : Type*} [NormedAddCommGroup EM'] [NormedSpace 𝕜 EM'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 EM' H') {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] +/-! Some basic tests: a simple function, both in applied and unapplied form -/ +section basic + -- General case: a function between two manifolds. variable {f : M → M'} {s : Set M} {m : M} @@ -368,12 +370,16 @@ variable {f : 𝕜 → 𝕜} {u : Set 𝕜} {a : 𝕜} #guard_msgs in #check MDiff[u] f --- This elaborator can be combined with the total space elaborator. --- XXX: these tests might be incomplete; extend as needed! +end basic variable {σ : Π x : M, V x} {σ' : (x : E) → Trivial E E' x} {s : E → E'} variable (X : (m : M) → TangentSpace I m) [IsManifold I 1 M] +/-! These elaborators can be combined with the total space elaborator. -/ +section interaction + +-- XXX: these tests might be incomplete; extend as needed! + /-- info: MDifferentiableAt I (I.prod 𝓘(𝕜, E)) fun m ↦ TotalSpace.mk' E m (X m) : M → Prop -/ #guard_msgs in #check MDiffAt (T% X) @@ -388,6 +394,8 @@ info: MDifferentiableAt 𝓘(𝕜, E) (𝓘(𝕜, E).prod 𝓘(𝕜, E')) fun x #guard_msgs in #check MDiffAt (T% σ') +end interaction + section variable [IsManifold I 2 M] From b71b4fa1bb30f59fa0f71759215748edcc9d3419 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 8 Oct 2025 11:17:48 -0700 Subject: [PATCH 11/22] chore: move tests about coercions --- .../DifferentialGeometry/Notation.lean | 126 +++++++++--------- 1 file changed, 64 insertions(+), 62 deletions(-) diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index 01c589b98e23e2..86abc8d1d3bbe8 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -122,68 +122,6 @@ variable {f : M → M'} {s : Set M} {m : M} #guard_msgs in #check MDiff[s] f -/-! A partial homeomorphism or partial equivalence. More generally, this works for any type -with a coercion to (possibly dependent) functions. -/ -section coercion - -variable {φ : OpenPartialHomeomorph M E} {ψ : PartialEquiv M E} - -/-- info: MDifferentiableWithinAt I 𝓘(𝕜, E) (↑φ) s : M → Prop -/ -#guard_msgs in -#check MDiffAt[s] φ - -/-- info: MDifferentiableWithinAt I 𝓘(𝕜, E) (↑ψ) s : M → Prop -/ -#guard_msgs in -#check MDiffAt[s] ψ - -/-- info: MDifferentiableAt I 𝓘(𝕜, E) ↑φ : M → Prop -/ -#guard_msgs in -#check MDiffAt φ - -/-- info: MDifferentiableAt I 𝓘(𝕜, E) ↑ψ : M → Prop -/ -#guard_msgs in -#check MDiffAt ψ - -/-- info: MDifferentiableOn I 𝓘(𝕜, E) (↑φ) s : Prop -/ -#guard_msgs in -#check MDiff[s] φ - -/-- info: MDifferentiableOn I 𝓘(𝕜, E) (↑ψ) s : Prop -/ -#guard_msgs in -#check MDiff[s] ψ - -/-- info: MDifferentiable I 𝓘(𝕜, E) ↑φ : Prop -/ -#guard_msgs in -#check MDiff φ - -/-- info: ContMDiffWithinAt I 𝓘(𝕜, E) 2 (↑ψ) s : M → Prop -/ -#guard_msgs in -#check CMDiffAt[s] 2 ψ - -/-- info: ContMDiffOn I 𝓘(𝕜, E) 2 (↑φ) s : Prop -/ -#guard_msgs in -#check CMDiff[s] 2 φ - -/-- info: ContMDiffAt I 𝓘(𝕜, E) 2 ↑φ : M → Prop -/ -#guard_msgs in -#check CMDiffAt 2 φ - -/-- info: ContMDiff I 𝓘(𝕜, E) 2 ↑ψ : Prop -/ -#guard_msgs in -#check CMDiff 2 ψ - -/-- info: mfderiv I 𝓘(𝕜, E) ↑φ : (x : M) → TangentSpace I x →L[𝕜] TangentSpace 𝓘(𝕜, E) (↑φ x) -/ -#guard_msgs in -#check mfderiv% φ - -/-- -info: mfderivWithin I 𝓘(𝕜, E) (↑ψ) s : (x : M) → TangentSpace I x →L[𝕜] TangentSpace 𝓘(𝕜, E) (↑ψ x) --/ -#guard_msgs in -#check mfderiv[s] ψ - -end coercion - -- Testing an error message. section @@ -372,6 +310,70 @@ variable {f : 𝕜 → 𝕜} {u : Set 𝕜} {a : 𝕜} end basic +/-! A partial homeomorphism or partial equivalence. More generally, this works for any type +with a coercion to (possibly dependent) functions. -/ +section coercion + +variable {s : Set M} {m : M} + +variable {φ : OpenPartialHomeomorph M E} {ψ : PartialEquiv M E} + +/-- info: MDifferentiableWithinAt I 𝓘(𝕜, E) (↑φ) s : M → Prop -/ +#guard_msgs in +#check MDiffAt[s] φ + +/-- info: MDifferentiableWithinAt I 𝓘(𝕜, E) (↑ψ) s : M → Prop -/ +#guard_msgs in +#check MDiffAt[s] ψ + +/-- info: MDifferentiableAt I 𝓘(𝕜, E) ↑φ : M → Prop -/ +#guard_msgs in +#check MDiffAt φ + +/-- info: MDifferentiableAt I 𝓘(𝕜, E) ↑ψ : M → Prop -/ +#guard_msgs in +#check MDiffAt ψ + +/-- info: MDifferentiableOn I 𝓘(𝕜, E) (↑φ) s : Prop -/ +#guard_msgs in +#check MDiff[s] φ + +/-- info: MDifferentiableOn I 𝓘(𝕜, E) (↑ψ) s : Prop -/ +#guard_msgs in +#check MDiff[s] ψ + +/-- info: MDifferentiable I 𝓘(𝕜, E) ↑φ : Prop -/ +#guard_msgs in +#check MDiff φ + +/-- info: ContMDiffWithinAt I 𝓘(𝕜, E) 2 (↑ψ) s : M → Prop -/ +#guard_msgs in +#check CMDiffAt[s] 2 ψ + +/-- info: ContMDiffOn I 𝓘(𝕜, E) 2 (↑φ) s : Prop -/ +#guard_msgs in +#check CMDiff[s] 2 φ + +/-- info: ContMDiffAt I 𝓘(𝕜, E) 2 ↑φ : M → Prop -/ +#guard_msgs in +#check CMDiffAt 2 φ + +/-- info: ContMDiff I 𝓘(𝕜, E) 2 ↑ψ : Prop -/ +#guard_msgs in +#check CMDiff 2 ψ + +/-- info: mfderiv I 𝓘(𝕜, E) ↑φ : (x : M) → TangentSpace I x →L[𝕜] TangentSpace 𝓘(𝕜, E) (↑φ x) -/ +#guard_msgs in +#check mfderiv% φ + +/-- +info: mfderivWithin I 𝓘(𝕜, E) (↑ψ) s : (x : M) → TangentSpace I x →L[𝕜] TangentSpace 𝓘(𝕜, E) (↑ψ x) +-/ +#guard_msgs in +#check mfderiv[s] ψ + +end coercion + variable {σ : Π x : M, V x} {σ' : (x : E) → Trivial E E' x} {s : E → E'} variable (X : (m : M) → TangentSpace I m) [IsManifold I 1 M] From a51a29c5aea048736618f668cd6e27fac2ad1160 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 8 Oct 2025 11:21:24 -0700 Subject: [PATCH 12/22] Three more tests --- MathlibTest/DifferentialGeometry/Notation.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index 86abc8d1d3bbe8..03db1697dd981a 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -372,6 +372,24 @@ info: mfderivWithin I 𝓘(𝕜, E) (↑ψ) s : (x : M) → TangentSpace I x → #guard_msgs in #check mfderiv[s] ψ +/-- +info: mfderivWithin I 𝓘(𝕜, E) (↑ψ) s : (x : M) → TangentSpace I x →L[𝕜] TangentSpace 𝓘(𝕜, E) (↑ψ x) +-/ +#guard_msgs in +variable {f : ContMDiffSection I F n V} in +#check mfderiv[s] ψ + +/-- info: mfderiv I I' ⇑g : (x : M) → TangentSpace I x →L[𝕜] TangentSpace I' (g x) -/ +#guard_msgs in +variable {g : ContMDiffMap I I' M M' n} in +#check mfderiv% g + +-- An example of "any type" which coerces to functions. +/-- info: mfderiv I I' ⇑g : (x : M) → TangentSpace I x →L[𝕜] TangentSpace I' (g x) -/ +#guard_msgs in +variable {g : Equiv M M'} in +#check mfderiv% g + end coercion variable {σ : Π x : M, V x} {σ' : (x : E) → Trivial E E' x} {s : E → E'} From 461280d038edd28ff4cceb017b8f7d6167f6a53e Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 8 Oct 2025 11:27:58 -0700 Subject: [PATCH 13/22] Move to Lean.Meta.Basic --- Mathlib/Geometry/Manifold/Notation.lean | 9 +-------- Mathlib/Lean/Meta/Basic.lean | 7 +++++++ 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index fb11e846759653..8fcb2768eac0dd 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -310,13 +310,6 @@ where let iTerm : Term ← ``(𝓘($eT, $eT)) Term.elabTerm iTerm none -/-- Ensures that `e` is a function. Attempts to coerce `e` to a function if necessary. -/ -def ensureIsFunction (e : Expr) : MetaM Expr := do - let ty ← whnf <|← instantiateMVars <|← inferType e - if ty.isForall then return e else (← coerceToFunction? e).getDM <| - throwError "Expected{indentD e}\nof type{indentD ty}\nto be a function, or to be coercible to \ - a function" - /-- If the type of `e` is a non-dependent function between spaces `src` and `tgt`, try to find a model with corners on both `src` and `tgt`. If successful, return both models. @@ -346,7 +339,7 @@ def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do end Elab -open Elab +open Elab Lean.Meta /-- `MDiffAt[s] f x` elaborates to `MDifferentiableWithinAt I J f s x`, trying to determine `I` and `J` from the local context. diff --git a/Mathlib/Lean/Meta/Basic.lean b/Mathlib/Lean/Meta/Basic.lean index c8bbf5bdb7d714..1895dafff6aa9f 100644 --- a/Mathlib/Lean/Meta/Basic.lean +++ b/Mathlib/Lean/Meta/Basic.lean @@ -94,3 +94,10 @@ def Lean.Meta.withEnsuringLocalInstance {α : Type} (inst : MVarId) (k : MetaM ( let (e, v) ← k let e' := (← e.abstractM #[inst']).instantiate1 instE return (e', v) + +/-- Ensures that `e` is a function. Attempts to coerce `e` to a function if necessary. -/ +def Lean.Meta.ensureIsFunction (e : Expr) : MetaM Expr := do + let ty ← whnf <|← instantiateMVars <|← inferType e + if ty.isForall then return e else (← coerceToFunction? e).getDM <| + throwError "Expected{indentD e}\nof type{indentD ty}\nto be a function, or to be coercible to \ + a function" From f82cd2ceca5b5a70cb7e7b55808b406915dce225 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 9 Oct 2025 09:40:40 -0700 Subject: [PATCH 14/22] Update Mathlib/Geometry/Manifold/Notation.lean Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com> --- Mathlib/Geometry/Manifold/Notation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index 8fcb2768eac0dd..0ce8edb886c0f8 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -339,7 +339,7 @@ def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do end Elab -open Elab Lean.Meta +open Elab /-- `MDiffAt[s] f x` elaborates to `MDifferentiableWithinAt I J f s x`, trying to determine `I` and `J` from the local context. From 339a7bddb49d9184be6eb195390acab42e072537 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 9 Oct 2025 17:17:16 -0700 Subject: [PATCH 15/22] Apply suggestions from code review Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com> --- Mathlib/Lean/Meta/Basic.lean | 3 ++- MathlibTest/DifferentialGeometry/Notation.lean | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Lean/Meta/Basic.lean b/Mathlib/Lean/Meta/Basic.lean index 1895dafff6aa9f..c25e9f61ddaeb7 100644 --- a/Mathlib/Lean/Meta/Basic.lean +++ b/Mathlib/Lean/Meta/Basic.lean @@ -95,7 +95,8 @@ def Lean.Meta.withEnsuringLocalInstance {α : Type} (inst : MVarId) (k : MetaM ( let e' := (← e.abstractM #[inst']).instantiate1 instE return (e', v) -/-- Ensures that `e` is a function. Attempts to coerce `e` to a function if necessary. -/ +/-- Checks that `e` is a function (i.e. that its type is a `.forallE` after `instantiateMVars` and +`whnf`). If not, coerces `e` to a function or fails with a descriptive error. -/ def Lean.Meta.ensureIsFunction (e : Expr) : MetaM Expr := do let ty ← whnf <|← instantiateMVars <|← inferType e if ty.isForall then return e else (← coerceToFunction? e).getDM <| diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index 03db1697dd981a..489e94833b6b6f 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -398,7 +398,7 @@ variable (X : (m : M) → TangentSpace I m) [IsManifold I 1 M] /-! These elaborators can be combined with the total space elaborator. -/ section interaction --- XXX: these tests might be incomplete; extend as needed! +-- Note: these tests might be incomplete; extend as needed! /-- info: MDifferentiableAt I (I.prod 𝓘(𝕜, E)) fun m ↦ TotalSpace.mk' E m (X m) : M → Prop -/ #guard_msgs in From 732742b0dec6b0637da195adb161f784af043a79 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Fri, 10 Oct 2025 00:17:53 +0000 Subject: [PATCH 16/22] [pre-commit.ci lite] apply automatic fixes --- Mathlib/Lean/Meta/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Lean/Meta/Basic.lean b/Mathlib/Lean/Meta/Basic.lean index c25e9f61ddaeb7..c0238fd0a3e8f0 100644 --- a/Mathlib/Lean/Meta/Basic.lean +++ b/Mathlib/Lean/Meta/Basic.lean @@ -95,7 +95,7 @@ def Lean.Meta.withEnsuringLocalInstance {α : Type} (inst : MVarId) (k : MetaM ( let e' := (← e.abstractM #[inst']).instantiate1 instE return (e', v) -/-- Checks that `e` is a function (i.e. that its type is a `.forallE` after `instantiateMVars` and +/-- Checks that `e` is a function (i.e. that its type is a `.forallE` after `instantiateMVars` and `whnf`). If not, coerces `e` to a function or fails with a descriptive error. -/ def Lean.Meta.ensureIsFunction (e : Expr) : MetaM Expr := do let ty ← whnf <|← instantiateMVars <|← inferType e From 84ce24a2143236d4da893db40e0ee48e176a0778 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 13 Oct 2025 14:41:10 +0200 Subject: [PATCH 17/22] Comment --- Mathlib/Geometry/Manifold/Notation.lean | 4 +++- MathlibTest/DifferentialGeometry/Notation.lean | 1 + 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index 0ce8edb886c0f8..74aade609805ce 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -393,7 +393,9 @@ scoped elab:max "MDiff" ppSpace t:term:arg : term => do mkAppM ``MDifferentiable #[srcI, tgtI, e] -- We ensure the type of `n` before checking `f` is a function to provide better error messages --- in case e.g. just `n` was forgotten. +-- in case e.g. `f` and `n` are swapped. +-- TODO: provide better error messages if just `n` is forgotten (say, by making `n` optional in +-- the parser and erroring later in the elaborator); currently, this yields just a parser error. /-- `CMDiffAt[s] n f x` elaborates to `ContMDiffWithinAt I J n f s x`, trying to determine `I` and `J` from the local context. diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean index 489e94833b6b6f..4f936d172c94d1 100644 --- a/MathlibTest/DifferentialGeometry/Notation.lean +++ b/MathlibTest/DifferentialGeometry/Notation.lean @@ -573,6 +573,7 @@ variable [IsManifold I 1 M] [IsManifold I' 1 M'] section error -- yields a parse error, "unexpected token '/--'; expected term" +-- TODO: make this parse, but error in the elaborator -- #check CMDiffAt[s] f /-- From e380f147ddb09e74d03c59f98cbc48453669e9b2 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 14 Oct 2025 14:13:44 +0200 Subject: [PATCH 18/22] More spaces --- Mathlib/Geometry/Manifold/Notation.lean | 32 ++++++++++++------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean index 74aade609805ce..315e7330bcda40 100644 --- a/Mathlib/Geometry/Manifold/Notation.lean +++ b/Mathlib/Geometry/Manifold/Notation.lean @@ -100,7 +100,7 @@ private def findSomeLocalInstanceOf? (c : Name) {α} (p : Expr → Expr → Meta MetaM (Option α) := do (← getLocalInstances).findSomeM? fun inst ↦ do if inst.className == c then - let type ← whnfR <|← instantiateMVars <|← inferType inst.fvar + let type ← whnfR <| ← instantiateMVars <| ← inferType inst.fvar p inst.fvar type else return none @@ -110,7 +110,7 @@ to `p`. -/ private def findSomeLocalHyp? {α} (p : Expr → Expr → MetaM (Option α)) : MetaM (Option α) := do (← getLCtx).findDeclRevM? fun decl ↦ do if decl.isImplementationDetail then return none - let type ← whnfR <|← instantiateMVars decl.type + let type ← whnfR <| ← instantiateMVars decl.type p decl.toExpr type end Elab @@ -132,7 +132,7 @@ run. -- TODO: factor out `MetaM` component for reuse scoped elab:max "T% " t:term:arg : term => do let e ← Term.elabTerm t none - let etype ← whnf <|← instantiateMVars <|← inferType e + let etype ← whnf <| ← instantiateMVars <| ← inferType e match etype with | .forallE x base tgt _ => withLocalDeclD x base fun x ↦ do let tgtHasLooseBVars := tgt.hasLooseBVars @@ -317,7 +317,7 @@ We pass `e` instead of just its type for better diagnostics. If `es` is `some`, we verify that `src` and the type of `es` are definitionally equal. -/ def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do - let etype ← whnf <|← instantiateMVars <|← inferType e + let etype ← whnf <| ← instantiateMVars <| ← inferType e match etype with | .forallE _ src tgt _ => if tgt.hasLooseBVars then @@ -330,7 +330,7 @@ def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do /- Note: we use `isDefEq` here since persistent metavariable assignments in `src` and `estype` are acceptable. TODO: consider attempting to coerce `es` to a `Set`. -/ - if !(← isDefEq estype <|← mkAppM ``Set #[src]) then + if !(← isDefEq estype <| ← mkAppM ``Set #[src]) then throwError "The domain {src} of {e} is not definitionally equal to the carrier type of \ the set {es} : {estype}" let tgtI ← findModel tgt (src, srcI) @@ -346,7 +346,7 @@ trying to determine `I` and `J` from the local context. The argument `x` can be omitted. -/ scoped elab:max "MDiffAt[" s:term "]" ppSpace f:term:arg : term => do let es ← Term.elabTerm s none - let ef ← ensureIsFunction <|← Term.elabTerm f none + let ef ← ensureIsFunction <| ← Term.elabTerm f none let (srcI, tgtI) ← findModels ef es mkAppM ``MDifferentiableWithinAt #[srcI, tgtI, ef, es] @@ -354,7 +354,7 @@ scoped elab:max "MDiffAt[" s:term "]" ppSpace f:term:arg : term => do trying to determine `I` and `J` from the local context. The argument `x` can be omitted. -/ scoped elab:max "MDiffAt" ppSpace t:term:arg : term => do - let e ← ensureIsFunction <|← Term.elabTerm t none + let e ← ensureIsFunction <| ← Term.elabTerm t none let (srcI, tgtI) ← findModels e none mkAppM ``MDifferentiableAt #[srcI, tgtI, e] @@ -364,7 +364,7 @@ scoped elab:max "MDiffAt" ppSpace t:term:arg : term => do -- The argument `x` can be omitted. -/ -- scoped elab:max "MDiffAt2" ppSpace t:term:arg : term => do -- let e ← Term.elabTerm t none --- let etype ← whnfR <|← instantiateMVars <|← inferType e +-- let etype ← whnfR <| ← instantiateMVars <| ← inferType e -- forallBoundedTelescope etype (some 1) fun src tgt ↦ do -- if let some src := src[0]? then -- let srcI ← findModel (← inferType src) @@ -381,14 +381,14 @@ scoped elab:max "MDiffAt" ppSpace t:term:arg : term => do trying to determine `I` and `J` from the local context. -/ scoped elab:max "MDiff[" s:term "]" ppSpace t:term:arg : term => do let es ← Term.elabTerm s none - let et ← ensureIsFunction <|← Term.elabTerm t none + let et ← ensureIsFunction <| ← Term.elabTerm t none let (srcI, tgtI) ← findModels et es mkAppM ``MDifferentiableOn #[srcI, tgtI, et, es] /-- `MDiff f` elaborates to `MDifferentiable I J f`, trying to determine `I` and `J` from the local context. -/ scoped elab:max "MDiff" ppSpace t:term:arg : term => do - let e ← ensureIsFunction <|← Term.elabTerm t none + let e ← ensureIsFunction <| ← Term.elabTerm t none let (srcI, tgtI) ← findModels e none mkAppM ``MDifferentiable #[srcI, tgtI, e] @@ -404,7 +404,7 @@ The argument `x` can be omitted. -/ scoped elab:max "CMDiffAt[" s:term "]" ppSpace nt:term:arg ppSpace f:term:arg : term => do let es ← Term.elabTerm s none let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞) - let ef ← ensureIsFunction <|← Term.elabTerm f none + let ef ← ensureIsFunction <| ← Term.elabTerm f none let (srcI, tgtI) ← findModels ef es mkAppM ``ContMDiffWithinAt #[srcI, tgtI, ne, ef, es] @@ -413,7 +413,7 @@ trying to determine `I` and `J` from the local context. `n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported). The argument `x` can be omitted. -/ scoped elab:max "CMDiffAt" ppSpace nt:term:arg ppSpace t:term:arg : term => do - let e ← ensureIsFunction <|← Term.elabTerm t none + let e ← ensureIsFunction <| ← Term.elabTerm t none let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞) let (srcI, tgtI) ← findModels e none mkAppM ``ContMDiffAt #[srcI, tgtI, ne, e] @@ -424,7 +424,7 @@ trying to determine `I` and `J` from the local context. scoped elab:max "CMDiff[" s:term "]" ppSpace nt:term:arg ppSpace f:term:arg : term => do let es ← Term.elabTerm s none let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞) - let ef ← ensureIsFunction <|← Term.elabTerm f none + let ef ← ensureIsFunction <| ← Term.elabTerm f none let (srcI, tgtI) ← findModels ef es mkAppM ``ContMDiffOn #[srcI, tgtI, ne, ef, es] @@ -433,7 +433,7 @@ trying to determine `I` and `J` from the local context. `n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported). -/ scoped elab:max "CMDiff" ppSpace nt:term:arg ppSpace f:term:arg : term => do let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞) - let e ← ensureIsFunction <|← Term.elabTerm f none + let e ← ensureIsFunction <| ← Term.elabTerm f none let (srcI, tgtI) ← findModels e none mkAppM ``ContMDiff #[srcI, tgtI, ne, e] @@ -441,14 +441,14 @@ scoped elab:max "CMDiff" ppSpace nt:term:arg ppSpace f:term:arg : term => do trying to determine `I` and `J` from the local context. -/ scoped elab:max "mfderiv[" s:term "]" ppSpace t:term:arg : term => do let es ← Term.elabTerm s none - let e ← ensureIsFunction <|← Term.elabTerm t none + let e ← ensureIsFunction <| ← Term.elabTerm t none let (srcI, tgtI) ← findModels e es mkAppM ``mfderivWithin #[srcI, tgtI, e, es] /-- `mfderiv% f x` elaborates to `mfderiv I J f x`, trying to determine `I` and `J` from the local context. -/ scoped elab:max "mfderiv%" ppSpace t:term:arg : term => do - let e ← ensureIsFunction <|← Term.elabTerm t none + let e ← ensureIsFunction <| ← Term.elabTerm t none let (srcI, tgtI) ← findModels e none mkAppM ``mfderiv #[srcI, tgtI, e] From 0655fee4d4c896054ce202fdbdc36c9a9c755d78 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 14 Oct 2025 14:25:20 +0200 Subject: [PATCH 19/22] Add variant functions --- Mathlib/Lean/Meta/Basic.lean | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/Mathlib/Lean/Meta/Basic.lean b/Mathlib/Lean/Meta/Basic.lean index c0238fd0a3e8f0..768fef3de11acd 100644 --- a/Mathlib/Lean/Meta/Basic.lean +++ b/Mathlib/Lean/Meta/Basic.lean @@ -95,10 +95,28 @@ def Lean.Meta.withEnsuringLocalInstance {α : Type} (inst : MVarId) (k : MetaM ( let e' := (← e.abstractM #[inst']).instantiate1 instE return (e', v) +/-- Checks that `e` has type `expectedType` (i.e. that its type is `expectedType` after +`instantiateMVars` and `whnf`). If not, coerces `e` to this type +or fails with a descriptive error. -/ +def Lean.Meta.ensureHasType (e expectedType : Expr) : MetaM Expr := do + let ty ← whnf <| ← instantiateMVars <| ← inferType e + let some name := expectedType.constName? + | throwError "expected type {expectedType} is not a constant" + if ty.isConstOf name then return e else (← coerceSimple? e expectedType).toOption.getDM <| + throwError "Expected{indentD e}\nto have type{indentD ty}\n or to be coercible to it" + /-- Checks that `e` is a function (i.e. that its type is a `.forallE` after `instantiateMVars` and `whnf`). If not, coerces `e` to a function or fails with a descriptive error. -/ def Lean.Meta.ensureIsFunction (e : Expr) : MetaM Expr := do - let ty ← whnf <|← instantiateMVars <|← inferType e + let ty ← whnf <| ← instantiateMVars <| ← inferType e if ty.isForall then return e else (← coerceToFunction? e).getDM <| throwError "Expected{indentD e}\nof type{indentD ty}\nto be a function, or to be coercible to \ a function" + +/-- Checks that `e` is a type (i.e. that its type is a `Sort` after `instantiateMVars` and +`whnf`). If not, coerces `e` to a Sort or fails with a descriptive error. -/ +def Lean.Meta.ensureIsSort (e : Expr) : MetaM Expr := do + let ty ← whnf <| ← instantiateMVars <| ← inferType e + if ty.isSort then return e else (← coerceToSort? e).getDM <| + throwError "Expected{indentD e}\nof type{indentD ty}\nto be a Sort, or to be coercible to \ + a Sort" From 70f2cc7b698ec653dcc0e0cc2ab81636430920ee Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 14 Oct 2025 14:53:40 +0200 Subject: [PATCH 20/22] Update Mathlib/Lean/Meta/Basic.lean Co-authored-by: Anne Baanen --- Mathlib/Lean/Meta/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Lean/Meta/Basic.lean b/Mathlib/Lean/Meta/Basic.lean index 768fef3de11acd..ff715a219f3ecc 100644 --- a/Mathlib/Lean/Meta/Basic.lean +++ b/Mathlib/Lean/Meta/Basic.lean @@ -100,10 +100,10 @@ def Lean.Meta.withEnsuringLocalInstance {α : Type} (inst : MVarId) (k : MetaM ( or fails with a descriptive error. -/ def Lean.Meta.ensureHasType (e expectedType : Expr) : MetaM Expr := do let ty ← whnf <| ← instantiateMVars <| ← inferType e - let some name := expectedType.constName? - | throwError "expected type {expectedType} is not a constant" - if ty.isConstOf name then return e else (← coerceSimple? e expectedType).toOption.getDM <| - throwError "Expected{indentD e}\nto have type{indentD ty}\n or to be coercible to it" + let ty ← inferType e + if ← withNewMCtxDepth (isDefEq ty expectedType) then return e else + (← coerceSimple? e expectedType).toOption.getDM <| + throwError "Expected{indentD e}\nto have type{indentD ty}\n or to be coercible to it" /-- Checks that `e` is a function (i.e. that its type is a `.forallE` after `instantiateMVars` and `whnf`). If not, coerces `e` to a function or fails with a descriptive error. -/ From c18ec5347c7b0cd2caac3eff4b1fefc2b1d72454 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 14 Oct 2025 14:53:57 +0200 Subject: [PATCH 21/22] Update Mathlib/Lean/Meta/Basic.lean Co-authored-by: Anne Baanen --- Mathlib/Lean/Meta/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Lean/Meta/Basic.lean b/Mathlib/Lean/Meta/Basic.lean index ff715a219f3ecc..609f14530da32e 100644 --- a/Mathlib/Lean/Meta/Basic.lean +++ b/Mathlib/Lean/Meta/Basic.lean @@ -95,8 +95,8 @@ def Lean.Meta.withEnsuringLocalInstance {α : Type} (inst : MVarId) (k : MetaM ( let e' := (← e.abstractM #[inst']).instantiate1 instE return (e', v) -/-- Checks that `e` has type `expectedType` (i.e. that its type is `expectedType` after -`instantiateMVars` and `whnf`). If not, coerces `e` to this type +/-- Checks that `e` has type `expectedType` (i.e. that its type is defeq to `expectedType` +at the current transparency). If not, coerces `e` to this type or fails with a descriptive error. -/ def Lean.Meta.ensureHasType (e expectedType : Expr) : MetaM Expr := do let ty ← whnf <| ← instantiateMVars <| ← inferType e From 882d4bb79c0444b75c2d184bb98277654cfc678a Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 14 Oct 2025 15:52:19 +0200 Subject: [PATCH 22/22] Fix --- Mathlib/Lean/Meta/Basic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Lean/Meta/Basic.lean b/Mathlib/Lean/Meta/Basic.lean index 609f14530da32e..9835a8ca50ace1 100644 --- a/Mathlib/Lean/Meta/Basic.lean +++ b/Mathlib/Lean/Meta/Basic.lean @@ -99,7 +99,6 @@ def Lean.Meta.withEnsuringLocalInstance {α : Type} (inst : MVarId) (k : MetaM ( at the current transparency). If not, coerces `e` to this type or fails with a descriptive error. -/ def Lean.Meta.ensureHasType (e expectedType : Expr) : MetaM Expr := do - let ty ← whnf <| ← instantiateMVars <| ← inferType e let ty ← inferType e if ← withNewMCtxDepth (isDefEq ty expectedType) then return e else (← coerceSimple? e expectedType).toOption.getDM <|