[Merged by Bors] - feat: custom elaborators for differential geometry by grunweg · Pull Request #27021 · leanprover-community/mathlib4

grunweg · 2025-07-12T08:25:18Z

Add two sets of custom elaborators for differential geometry, to

infer the model with corners in MDifferentiable{WithinAt,At,On} or ContMDiff{WithinAt,At,On} expressions from the local context, and provide shorter notation in that setting
do the same for mfderiv: mfderiv% f is shorthand for mfderiv I J f; mfderiv[s] f x is short for mfderivWithin I J f s
convert a fibre bundle section from a dependent section to a function into the total space, making working with differentiability of sections of fibre bundles less cumbersome

This was discussed on zulip, to overall broad consensus.

This code has substantial tests (which have caught bugs in the past). It has also been tested in the branch in #26221 (uncovering minor issues, but not substantial ones --- the worst of which have been fixed).
Many thanks go to fpvandoorn (for lots of in-person comments on improving the meta code), and to thorimur for rewriting the entire implementation from ground up to be much more robust and maintainable.

A number of tweaks and extensions can be made in future PRs: this set of elaborators is useful already.
Once it is deemed sufficiently robust, differential geometry files can be converted to use it.

From the path towards geodesics and the Levi-Civita connection.

Co-authored-by: Patrick Massot patrickmassot@free.fr

github-actions · 2025-07-12T08:26:25Z

PR summary b4264fbd75

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Geometry.Manifold.Notation` (new file)	2076

Declarations diff

+ findModel
+ findModels

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).

sgouezel · 2025-07-12T08:42:20Z

Thanks for this! I agree that this is extremely useful, and should be merged quickly if that's possible. However, I think that the scoping to the Manifold namespace is really important, and should be included in the current PR.

grunweg · 2025-07-12T08:44:17Z

Sure, I'm happy to do this - can you point me at how?

grunweg · 2025-07-12T08:45:05Z

Trying the obvious things elab[Manifold]:max "CMDiff" nt:term:arg t:term:arg : term => do ... and elab:max[Manifold] "CMDiff" nt:term:arg t:term:arg : term => do did not work.

(edit: But Yael suggested a fix on zulip, thanks!)

Mathlib/Geometry/Manifold/Elaborators.lean

Mathlib/Geometry/Manifold/Traces.lean

MathlibTest/DifferentialGeometry/Elaborators.lean

grunweg

Thanks for the comments; let me look into them now!

Mathlib/Geometry/Manifold/Elaborators.lean

This depends on the custom elaborators added in leanprover-community#27021; for some reason, using these fails. To be investigated!

Add two sets of custom elaborators for differential geometry, to - infer the model with corners in `MDifferentiable{WithinAt,At,On}` or `ContMDiff{WithinAt,At,On}` expressions from the local context, and provide shorter notation in that setting - convert a fibre bundle section from a dependent section to a function into the total space, making working with differentiability of sections of fibre bundles less cumbersome This was [discussed on zulip](...), to overall broad consensus. This code has substantial tests and has been tried in the branch in leanprover-community#26221 (uncovering minor issues, but not substantial ones). The implementation itself is of prototype quality and will be cleaned up in the future. Once it is more robust, more differential geometry files can be converted to use it. ----------- I agree that merging not fully polished code is not ideal, but propose doing so for two reasons: - the work in leanprover-community#26221 used these elaborators extensively (to test them). Reverting those changes, merging the code, only to re-apply them is not a good use of time. Merging this PR now enables merging the work in leanprover-community#26221 soon. - the feature is clearly useful and not going away: in the files that use it, it works well already. Holding off on further adopting, but merging it now seems like a good compromise.

grunweg · 2025-10-07T02:46:12Z

My current opinion is that

the current test should definitely stay, as a regression test (I've updated its comment to clarify this)
I don't expect the TopologicalSpace instance to be found;
there should be a test for the correct spelling of this.

I've asked on zulip about this last point.

grunweg · 2025-10-07T14:41:16Z

Added a regression test about the wrong arg precendence for parsing s.

grunweg · 2025-10-07T14:49:23Z

With a little reminder on zulip, I found the right spelling for smoothness and added a test covering it.

grunweg · 2025-10-07T14:54:11Z

Hmm, relatedly, I notice that TangentBundle is an abbrev for Bundle.TotalSpace _ (TangentSpace _). Should findModel see TangentBundle as a Bundle.TotalSpace, or handle it as a separate case (or not handle it)? If the former, then we should use match_expr ← whnfR e with in fromTotalSpace to unwrap TangentBundle. But if it has separate instances, it might make sense to handle it as a separate case if at all (presumably in a subsequent PR!).

This is a question of the algorithm's spec, so I'll defer to those with greater library knowledge in this area. :)

I think that

the elaborators should definitely support TangentBundle (either now, or in a follow-up)
TangentBundle has separate instances, but not about manifolds... so I wondered if just changing the match_expr suffices. Trying it out, the answer seems to be no. So, it might be best to add a new case to findModel, and perhaps do so in a follow-up.

grunweg · 2025-10-07T14:55:15Z

In other words: from my side, this PR is ready to get merged. There are a number of folliow-up changes I'd like to make, but these can be subsequent PRs.

Mathlib/Lean/Elab/Term.lean

thorimur · 2025-10-07T21:31:16Z

LGTM (after updating Mathlib.Lean.Elab.Term + noshake)! 🎉

Thanks so much for your work on this, and to the others who contributed—and especially for your responsiveness during the review process! I'm very excited to see these continue to be iterated on and—hopefully at some not-too-distant date!—start to be used in Mathlib. :)

grunweg · 2025-10-08T01:40:57Z

CI passes on this PR. I've gone over the diff again, and also resolved all stale review comments. I'll keep Thomas' more substantial meta comments open (for future me to re-read them); they are all addressed. All in all, this seems ready for merging (but I'm of course biased).

@thorimur Let me just repeat again that I'm really grateful for your extremely detailed review. I learned a lot (and will probably learn more as I return to your comments to re-process them). It was a pleasure, until next time/ one of the follow-up changes :-)
Would you like to add yourself to the authors of this file? I have no idea what mathlib's etiquette says, but you have certainly rewritten the meta code significantly.

thorimur · 2025-10-08T02:24:14Z

I'm so glad my comments were useful to you! :) I'm always happy to talk about metaprogramming, so if you return to these comments later, feel free to ask me further questions about them (e.g. on Zulip)! :)

Would you like to add yourself to the authors of this file? I have no idea what mathlib's etiquette says, but you have certainly rewritten the meta code significantly.

Hmm, I'm actually not sure if I should be on the author's list either!

I once heard someone say that the authors list is basically the answer to "who do I ping if I need to address something in this file", and from that perspective, I'd be happy to take on the responsibility of being among those pinged.

On the other hand, I'm not sure if it's a great idea to set a precedent of receiving authorship credit as a reviewer.

I'm perfectly okay with either outcome, but I'd rather defer to an opinion from a maintainer on what should happen here than ask to be there myself.

(If this turns out to be complicated, though, perhaps let's leave me off and not hold up the PR any further—I'd like to stay involved with these elaborators, so maybe I'll contribute to this file directly in the future and render the question moot. :) )

sgouezel · 2025-10-08T08:19:43Z

bors d+
I think it definitely makes sense to add you as a second author to the file (not the least because then you will feel responsible for it, and then we can ping you again :-)

mathlib-bors · 2025-10-08T08:19:46Z

✌️ 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/Geometry/Manifold/Notation.lean

grunweg · 2025-10-08T14:28:20Z

Thanks for the review! I've added Thomas as an author; let's merge this!
bors merge

Add two sets of custom elaborators for differential geometry, to - infer the model with corners in `MDifferentiable{WithinAt,At,On}` or `ContMDiff{WithinAt,At,On}` expressions from the local context, and provide shorter notation in that setting - do the same for mfderiv: `mfderiv% f` is shorthand for `mfderiv I J f`; `mfderiv[s] f x` is short for `mfderivWithin I J f s` - convert a fibre bundle section from a dependent section to a function into the total space, making working with differentiability of sections of fibre bundles less cumbersome This was [discussed on zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Differential.20geometry.20elaborators.20experiment/with/528035295), to overall broad consensus. This code has substantial tests (which have caught bugs in the past). It has also been tested in the branch in #26221 (uncovering minor issues, but not substantial ones Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com> Co-authored-by: thorimur <thomasmurrills@gmail.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2025-10-08T14:42:05Z

Pull request successfully merged into master.

Build succeeded:

This depends on the custom elaborators added in leanprover-community#27021; for some reason, using these fails. To be investigated!

…ity#27021) Add two sets of custom elaborators for differential geometry, to - infer the model with corners in `MDifferentiable{WithinAt,At,On}` or `ContMDiff{WithinAt,At,On}` expressions from the local context, and provide shorter notation in that setting - do the same for mfderiv: `mfderiv% f` is shorthand for `mfderiv I J f`; `mfderiv[s] f x` is short for `mfderivWithin I J f s` - convert a fibre bundle section from a dependent section to a function into the total space, making working with differentiability of sections of fibre bundles less cumbersome This was [discussed on zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Differential.20geometry.20elaborators.20experiment/with/528035295), to overall broad consensus. This code has substantial tests (which have caught bugs in the past). It has also been tested in the branch in leanprover-community#26221 (uncovering minor issues, but not substantial ones Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com> Co-authored-by: thorimur <thomasmurrills@gmail.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

github-actions bot added the t-differential-geometry Manifolds etc label Jul 12, 2025

grunweg added the t-meta Tactics, attributes or user commands label Jul 12, 2025

grunweg force-pushed the diffgeo-custom-elaborators branch from 6f64439 to 7c4c0b0 Compare July 12, 2025 08:28

grunweg force-pushed the diffgeo-custom-elaborators branch from 7d3d364 to 54aae78 Compare July 12, 2025 08:56

This was referenced Jul 12, 2025

feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections #27025

Open

Mr. Covariant Derivatives #26221

Draft

grunweg mentioned this pull request Jul 30, 2025

feat: Gram-Schmidt orthonormalisation preserves continuity of sections #27694

Open

2 tasks

leanprover-community-bot-assistant assigned robertylewis Aug 3, 2025

sgouezel reviewed Sep 29, 2025

View reviewed changes

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 29, 2025

grunweg commented Sep 30, 2025

View reviewed changes

Mathlib/Geometry/Manifold/Elaborators.lean Outdated Show resolved Hide resolved

grunweg force-pushed the diffgeo-custom-elaborators branch 2 times, most recently from 1ee60c5 to 2dc7a2c Compare September 30, 2025 09:40

grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 30, 2025

grunweg force-pushed the diffgeo-custom-elaborators branch from 2dc7a2c to 6a84a48 Compare September 30, 2025 09:46

grunweg added a commit to grunweg/mathlib4 that referenced this pull request Sep 30, 2025

feat: local frames

e7aadb3

This depends on the custom elaborators added in leanprover-community#27021; for some reason, using these fails. To be investigated!

grunweg mentioned this pull request Sep 30, 2025

[Merged by Bors] - feat: local frames in a vector bundle #30083

Closed

4 tasks

grunweg added 9 commits September 30, 2025 13:54

Remove unused deprecated elaborators; noshake

81c019b

Scope delaborators

6b09d20

More minimal imports

7be9e94

Use double backticks

aeacd20

Manual noshake

79c9622

chore(Elaborators): fix a few typos in doc-strings

0fa641c

feat: custom elaborator for mderiv(Within)

2e80df4

And add some tests, including some for (already fine) error messages

e77fbc4

grunweg added 2 commits October 6, 2025 19:46

chore: move test

6217313

chore: add regression test for precendence in the "on/within" set

41046cd

Clarify failing test, and document the right spelling with TangentBundle

faf1b24

grunweg force-pushed the diffgeo-custom-elaborators branch from 3b2f1f2 to faf1b24 Compare October 7, 2025 14:48

grunweg mentioned this pull request Oct 7, 2025

[Merged by Bors] - feat: support coercions in the differential geometry elaborators #30307

Closed

1 task

thorimur reviewed Oct 7, 2025

View reviewed changes

Mathlib/Lean/Elab/Term.lean Outdated Show resolved Hide resolved

Noshake; fix bad merge/import

8e5d337

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

grunweg commented Oct 8, 2025

View reviewed changes

Mathlib/Geometry/Manifold/Notation.lean Outdated Show resolved Hide resolved

Update Mathlib/Geometry/Manifold/Notation.lean

fb2e2b6

mathlib-bors bot changed the title ~~feat: custom elaborators for differential geometry~~ [Merged by Bors] - feat: custom elaborators for differential geometry Oct 8, 2025

mathlib-bors bot closed this Oct 8, 2025

grunweg deleted the diffgeo-custom-elaborators branch October 8, 2025 16:27

grunweg added a commit to grunweg/mathlib4 that referenced this pull request Oct 8, 2025

feat: local frames

f4ec99c

This depends on the custom elaborators added in leanprover-community#27021; for some reason, using these fails. To be investigated!

grunweg mentioned this pull request Oct 13, 2025

Tracking issue for differential geometry elaborators #30503

Open

26 tasks

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary b4264fbd75

Import changes for modified files

Declarations diff

Uh oh!

sgouezel commented Jul 12, 2025

Uh oh!

grunweg commented Jul 12, 2025

Uh oh!

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

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

grunweg commented Oct 7, 2025

Uh oh!

grunweg commented Oct 7, 2025

Uh oh!

grunweg commented Oct 7, 2025

Uh oh!

grunweg commented Oct 7, 2025

Uh oh!

grunweg commented Oct 7, 2025

Uh oh!

Uh oh!

thorimur commented Oct 7, 2025

Uh oh!

grunweg commented Oct 8, 2025

Uh oh!

thorimur commented Oct 8, 2025

Uh oh!

sgouezel commented Oct 8, 2025

Uh oh!

mathlib-bors bot commented Oct 8, 2025

Uh oh!

Uh oh!

grunweg commented Oct 8, 2025

Uh oh!

mathlib-bors bot commented Oct 8, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

grunweg commented Jul 12, 2025 •

edited

Loading

github-actions bot commented Jul 12, 2025 •

edited

Loading

grunweg commented Jul 12, 2025 •

edited

Loading