[Merged by Bors] - feat: support coercions in the differential geometry elaborators by grunweg · Pull Request #30307 · leanprover-community/mathlib4

grunweg · 2025-10-07T18:47:35Z

Generalise the CMDiff, MDiff and mfderiv elaborators (and its friends) to apply to any object which coerces to a function. We can such speak about the smoothness of a PartialEquiv, OpenPartialHomeomorph (or the future ClosedPartialHomeomorph and PartialHomeomorph), smooth section or bundled smooth map without the need for a coercion.

As a by-product, add new functions Lean.Meta.ensure{HasType,IsFunction,IsSort} which apply the respective coercion if necessary.

While at it, add more sections (and section headers) to the test file for the elaborators.

I have forward-ported this PR to #26221 and not noticed any issues yet.

depends on: [Merged by Bors] - feat: custom elaborators for differential geometry #27021

github-actions · 2025-10-07T18:48:37Z

PR summary c7bb7934b2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Lean.Meta.ensureHasType
+ Lean.Meta.ensureIsFunction
+ Lean.Meta.ensureIsSort

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

thorimur · 2025-10-08T01:37:59Z

I think you're right about coercions being the issue. Perhaps we should just try to coerce everything which isn't a function before findModels (instead of matching OpenPartialHomeoMorph and PartialEquiv at all)?

coerceToFunction? is the relevant declaration here! (Note that it attempts to coerce expressions to functions even if they're already functions, thus returning none in that case.)

We could do this in findModels, but this then means we either need to

return the coerced e for use in our expressions
pass a continuation to findModels (i.e. such that we'd write something like withFindModels ef es fun ef es => mkAppM ``MDifferentiableWithinAt #[srcI, tgtI, ef, es]). But notice that we need to pass es as an argument to the continuation with this approach. To avoid weird unnecessary case splits on es? : Option Expr, we would want to split this into two declarations, withFindModels and withFindModelsUsingSet (up to naming).

But the easiest and clearest approach is probably just to define something like

/-- 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"

for convenience (probably in the namespace Lean.Meta, in Mathlib.Lean.Meta.Basic? I do think this would be a relatively uncontroversial addition to the meta API) and then write

scoped elab:max "MDiffAt[" s:term "]" ppSpace f:term:arg : term => do
  let es ← Term.elabTerm s none
  let ef ← ensureIsFun <|← Term.elabTerm f none
  let (srcI, tgtI) ← findModels ef es
  mkAppM ``MDifferentiableWithinAt #[srcI, tgtI, ef, es]

(and likewise elsewhere!) :)

thorimur · 2025-10-08T01:47:02Z

Note: we could also use ensureHasType (or ensureHasTypeWithErrorMsgs for better errors, if we can figure out what the arguments actually mean!) to coerce es to a Set in findModels. 👀 This PR could then be about adding coercions more generally.

grunweg · 2025-10-08T04:22:14Z

Thanks for your detective help! I tried your second approach, and generally it works really well 🎉

~~I just noticed, however, that a different error message regresses~~
Found the issue and fixed this; one should check the type of n before checking if f is a function.

mathlib4-dependent-issues-bot · 2025-10-08T14:48:41Z

This PR/issue depends on:

~~[Merged by Bors] - feat: custom elaborators for differential geometry #27021~~
By Dependent Issues (🤖). Happy coding!

Tests still fial, but one is a clear bug in my code

And probably, want to insert a coercion...

grunweg · 2025-10-08T18:28:50Z

I just rebased on top of master, added a last few tests and moved the new meta function to Lean.Meta.Basic.
(Probably, this should go into Lean.Meta.Coe instead of Basic; so pedantically, this might be suitable for a new file...)

Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

thorimur

LGTM after addressing these comments! :)

MathlibTest/DifferentialGeometry/Notation.lean

thorimur · 2025-10-09T16:11:57Z

Mathlib/Geometry/Manifold/Notation.lean

  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.


I like this change! But it should read as follows, right? (If we wanted to support leaving off n, we could change the parser to parse optional arguments in a subsequent PR!)

Suggested change

-- in case e.g. just `n` was forgotten.

-- in case e.g. `n` and `f` were accidentally swapped.

Actually, I mean it as I wrote it: there are some tests for error messages if just n is missing (not swapped). Before this PR, they complain that the first argument (i.e., f) has type E \to M and not WithTop N\infty.
When I checked for the type of f first, this part of the error got lost: see 27ede4a for the details.
I much prefer the error about n first.

Does this make sense?

(I don't think we want to support leaving out n: that information matters, and Lean cannot synthesize it out of thin air.)

there are some tests for error messages if just n is missing (not swapped).

Hmm, really? I'm surprised—isn't e.g. CMDiffAt f, where n is missing, a parse error?

(That's why I was suggesting the possibility of parsing optional arguments, by the way: not so we could synthesize the data, but so we could at least make it to elaboration, then throw a descriptive error saying that more arguments are needed! :) )

Re: approval for this PR, for any maintainer reading: the precise wording of this comment is all that's being discussed here, which in my opinion is probably not a crucial enough issue to hold up this PR (especially since many opportunities to reword are waiting in the wings). :)

Hmm, really? I'm surprised—isn't e.g. CMDiffAt f, where n is missing, a parse error?

Actually, you're right: there are commented tests for this, because this is a parse error (as you said).
Let me add parsing optional arguments as a TODO item to #30503.

Mathlib/Geometry/Manifold/Notation.lean

Mathlib/Lean/Meta/Basic.lean

Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

grunweg · 2025-10-10T00:18:57Z

We need a better approach to organizing both the Mathlib/Lean/ folder and additions to the meta API in Mathlib imo.

Strongly agree with both. Would you like to start a zulip discussion? (Medium-term, it would be nice to upstream these to Lean core... that's certainly a better place to put them!)

grunweg · 2025-10-10T00:19:23Z

Thanks for the close look again. I have addressed or responded to all comments.

Vierkantor

Nice work!

bors d+

Vierkantor · 2025-10-14T08:15:15Z

Mathlib/Geometry/Manifold/Notation.lean

 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


Suggested change

let ef ← ensureIsFunction <|← Term.elabTerm f none

let ef ← ensureIsFunction <| ← Term.elabTerm f none

(You use <|← consistently, so it seems to be a style choice. But don't we have as a style rule to put spaces around operators?)

I've added spaces now. It does look a little weird, but consistency seems good.

Sorry, this may have been my influence; I use <|← consistently. :) @Vierkantor you're right that the style rule is spaces; I'm not sure where I picked this up!

But, I can't tell if <|← is actually more readable (cuts down on tokens and whitespace), or if I've just grown used to it! I like it enough, though, that I at least wanted to discuss it on zulip. :)

Vierkantor · 2025-10-14T08:58:19Z

Mathlib/Lean/Meta/Basic.lean

+/-- 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 <|
+    throwError "Expected{indentD e}\nof type{indentD ty}\nto be a function, or to be coercible to \
+      a function"


I would have expected this to exist already! But searching through lean4/batteries/mathlib4 for usages of coerceToFunction?, there does not seem to be anything similar.

Do you know if we have something similar for coeSort and coe? If not, can you add them?

I don't think they exist either; I have just added them. While cargo-culting them was not too hard, a areful review is welcome!

Side note: would a PR adding these three declarations to core be welcome?

re upstreaming: No objections from me, but I would probably merge this first and then ask @kmill if core is interested in maintaining them.

Two weeks later, let me follow-up on this.
@kmill In this PR, I've added a few new functions to Mathlib/Lean/Meta/Basic.lean: Lean.Meta.ensureHasType, Lean.Meta.ensureIsFunction and Lean.Meta.ensureIsSort. Is Lean core interested in maintaining them?

mathlib-bors · 2025-10-14T08:59:04Z

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Mathlib/Lean/Meta/Basic.lean

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

grunweg · 2025-10-14T12:59:44Z

Thanks for the review! I'll wait for CI to finish, then hit the merge button.

grunweg · 2025-10-14T13:52:36Z

bors merge

) Generalise the `CMDiff`, `MDiff` and `mfderiv` elaborators (and its friends) to apply to any object which coerces to a function. We can such speak about the smoothness of a `PartialEquiv`, `OpenPartialHomeomorph` (or the future `ClosedPartialHomeomorph` and `PartialHomeomorph`), smooth section or bundled smooth map without the need for a coercion. As a by-product, add new functions `Lean.Meta.ensure{HasType,IsFunction,IsSort}` which apply the respective coercion if necessary. While at it, add more sections (and section headers) to the test file for the elaborators. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2025-10-14T14:50:13Z

Pull request successfully merged into master.

Build succeeded:

…nprover-community#30307) Generalise the `CMDiff`, `MDiff` and `mfderiv` elaborators (and its friends) to apply to any object which coerces to a function. We can such speak about the smoothness of a `PartialEquiv`, `OpenPartialHomeomorph` (or the future `ClosedPartialHomeomorph` and `PartialHomeomorph`), smooth section or bundled smooth map without the need for a coercion. As a by-product, add new functions `Lean.Meta.ensure{HasType,IsFunction,IsSort}` which apply the respective coercion if necessary. While at it, add more sections (and section headers) to the test file for the elaborators. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 7, 2025

grunweg force-pushed the diffgeo-custom-elaborators-charts-v2 branch 2 times, most recently from 1d8f1f1 to caae86f Compare October 8, 2025 04:17

grunweg added t-meta Tactics, attributes or user commands t-differential-geometry Manifolds etc labels Oct 8, 2025

grunweg force-pushed the diffgeo-custom-elaborators-charts-v2 branch from 9190b3b to 9b44efa Compare October 8, 2025 14:43

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 8, 2025

grunweg force-pushed the diffgeo-custom-elaborators-charts-v2 branch from 9b44efa to e1987c5 Compare October 8, 2025 15:17

grunweg added 9 commits October 8, 2025 08:18

wip: support partial homeos and partial equivs

1156f65

Tests still fial, but one is a clear bug in my code

Progress

b1423f0

wip: copied the missing code; need to dedup

ff45f43

And probably, want to insert a coercion...

Better approach; add tests for the remaining cases

7a4facf

Typo fix

d5aa960

Note a regressed error message

27ede4a

Restore

ad86d3e

One more test

72eb400

Update docs

8353626

grunweg force-pushed the diffgeo-custom-elaborators-charts-v2 branch from e1987c5 to 8353626 Compare October 8, 2025 15:18

grunweg mentioned this pull request Oct 8, 2025

Mr. Covariant Derivatives #26221

Draft

35 tasks

grunweg added 3 commits October 8, 2025 11:16

chore: slightly better headings for the tests file

c9d331e

chore: move tests about coercions

b71b4fa

Three more tests

a51a29c

grunweg changed the title ~~feat: custom elaborator support for OpenPartialHomeomorph, PartialEquiv~~ feat: support coercions in the differential geometry elaborators Oct 8, 2025

Move to Lean.Meta.Basic

461280d

Update Mathlib/Geometry/Manifold/Notation.lean

f82cd2c

Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

thorimur reviewed Oct 9, 2025

View reviewed changes

grunweg and others added 2 commits October 9, 2025 17:17

Apply suggestions from code review

339a7bd

Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

[pre-commit.ci lite] apply automatic fixes

732742b

grunweg mentioned this pull request Oct 13, 2025

Tracking issue for differential geometry elaborators #30503

Open

26 tasks

Comment

84ce24a

grunweg mentioned this pull request Oct 13, 2025

feat: add custom elaborators for immersions #30504

Open

3 tasks

Vierkantor approved these changes Oct 14, 2025

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 14, 2025

Vierkantor self-assigned this Oct 14, 2025

grunweg added 2 commits October 14, 2025 14:13

More spaces

e380f14

Add variant functions

0655fee

Vierkantor reviewed Oct 14, 2025

View reviewed changes

Mathlib/Lean/Meta/Basic.lean Outdated Show resolved Hide resolved

Vierkantor reviewed Oct 14, 2025

View reviewed changes

Mathlib/Lean/Meta/Basic.lean Outdated Show resolved Hide resolved

grunweg and others added 2 commits October 14, 2025 14:53

Update Mathlib/Lean/Meta/Basic.lean

70f2cc7

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Update Mathlib/Lean/Meta/Basic.lean

c18ec53

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Vierkantor approved these changes Oct 14, 2025

View reviewed changes

Fix

882d4bb

mathlib-bors bot changed the title ~~feat: support coercions in the differential geometry elaborators~~ [Merged by Bors] - feat: support coercions in the differential geometry elaborators Oct 14, 2025

mathlib-bors bot closed this Oct 14, 2025

grunweg deleted the diffgeo-custom-elaborators-charts-v2 branch October 14, 2025 21:01

	-- in case e.g. just `n` was forgotten.
	-- in case e.g. `n` and `f` were accidentally swapped.

	let ef ← ensureIsFunction <\|← Term.elabTerm f none
	let ef ← ensureIsFunction <\| ← Term.elabTerm f none

Conversation

grunweg commented Oct 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 7, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c7bb7934b2

Import changes for modified files

Declarations diff

Uh oh!

thorimur commented Oct 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

thorimur commented Oct 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg commented Oct 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Oct 8, 2025

Uh oh!

grunweg commented Oct 8, 2025

Uh oh!

thorimur left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thorimur Oct 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

grunweg Oct 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

grunweg commented Oct 10, 2025

Uh oh!

grunweg commented Oct 10, 2025

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Oct 14, 2025

Uh oh!

Uh oh!

Uh oh!

grunweg commented Oct 14, 2025

Uh oh!

grunweg commented Oct 14, 2025

Uh oh!

mathlib-bors bot commented Oct 14, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

grunweg commented Oct 7, 2025 •

edited

Loading

github-actions bot commented Oct 7, 2025 •

edited

Loading

thorimur commented Oct 8, 2025 •

edited

Loading

thorimur commented Oct 8, 2025 •

edited

Loading

grunweg commented Oct 8, 2025 •

edited

Loading

thorimur Oct 10, 2025 •

edited

Loading

grunweg Oct 13, 2025 •

edited

Loading