Differential geometry elaborators experiment

Stream: mathlib4

[Patrick Massot]

Differential geometry is known to be very heavy to manipulate in Mathlib. The first part is the type class proliferation. “Let M be a manifold over a non-discrete normed field 𝕜” is spelled

open Bundle

open scoped Bundle Manifold ContDiff

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]

variable (n : WithTop ℕ∞) {E : Type*} [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I n M]

and “let V be a vector bundle over M” is spelled

variable
  (F : Type*) [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  (V : M → Type*) [TopologicalSpace (TotalSpace F V)]
  [∀ x, AddCommGroup (V x)] [∀ x, Module 𝕜 (V x)] [∀ x : M, TopologicalSpace (V x)]
  [FiberBundle F V] [VectorBundle 𝕜 F V] [ContMDiffVectorBundle n F V I]

This has been discussed many times and one day Kyle will save us from this.

[Patrick Massot]

What I want to discuss today is the next step. Saying “let σ be a section of V” is very easy, this is what dependent type is all about: (σ : Π x : M, V x). But then if we want to say σ is differentiable at m : M it becomes awful:

MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (σ x)) m

There are two issues here. First we need to turn σ into a function into the total space of V, and this total space need to be assigned a manifold structure. This is the job of fun x ↦ TotalSpace.mk' F x (σ x) where F is needed to specify that the target is meant to be TotalSpace F V. It looks crazy because TotalSpace F Vdoes not use F at all, but type class synthesis needs this dependence to endow TotalSpace F V with extra structure (I guess, I don’t know the details).

Sometimes this TotalSpace.mk' also requires type annotations. For instance if E and E' are normed spaces we can form the trivial bundle E × E' and turn s : E → E' into a function to the total space by

fun a ↦ (TotalSpace.mk' E' a (s a) : TotalSpace E' (Trivial E E'))

before being able to say that s is differentiable in the manifold sense.

Returning to

MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (σ x)) m

the second issue is the specification of the ModelWithCorners, I on the source and and I.prod 𝓘(𝕜, F) on the target. Those are obviously what we mean here, but there is no way unification or instance synthesis can infer them from the type M → TotalSpace F V of (fun x ↦ TotalSpace.mk' F x (σ x)) (and m has type M).

[Patrick Massot]

Again, there is no way our general elaboration mechanisms (unification and instance synthesis) can invent those parameters. But this is Lean 4, so if general elaboration is not enough, we can roll our own. The goal of this thread is to discuss experiments in this direction. Those experiments can be improved in many ways, but I find them encouraging. They allow to write

/-- info: MDifferentiableAt I (I.prod 𝓘(𝕜, F)) fun x ↦ TotalSpace.mk' F x (σ x) : M → Prop -/
#guard_msgs in
#check MDifferentiableAt% (T% σ)

/-- info: MDifferentiableAt I (I.prod 𝓘(𝕜, E)) (fun m ↦ TotalSpace.mk' E m (X m)) m : Prop -/
#guard_msgs in
#check MDifferentiableAt% (T% X) m

/-- info: MDifferentiableAt I I' f m : Prop -/
#guard_msgs in
#check MDifferentiableAt% f m

variable (g : E → E')

/-- info: MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') g : E → Prop -/
#guard_msgs in
#check MDifferentiableAt% g

[Patrick Massot]

The T% elaborator does the TotalSpace.mk' job, inferring F and implicit arguments without annotations.

[Patrick Massot]

The MDifferentiableAt% elaborator figures out the ModelWithCorners arguments.

[Patrick Massot]

The effect on a random file from the covariant derivative wip can be seen at https://github.com/grunweg/mathlib4/commit/52a89f0da0f087d1b0f96927c11af8da23924fd8

[Patrick Massot]

The elaborators and more tests can be seen at https://github.com/grunweg/mathlib4/commit/4ec3b0f6048e877f88b821439d10d8c8da6ef72a

[Patrick Massot]

The core function is find_model (e : Expr) (baseInfo : Option (Expr × Expr) := none) : TermElabM Expr which tries to find a ModelWithCorners for some given type e. The algorithm (which could easily be made extensible) is currently

• if e matches TotalSpace F V for some F and V
  * if Vmatches TangentSpace I xfor some I and X then return I.prod I.tangent
  * otherwise do something I skip for simplicity
• start looping over the local context
  * if we ChartedSpace H e then remember who is H (and stop the loop)
  * if we see NormedSpace K e then remember who is K (and stop the loop)
• if we found some K then return 𝓘(K, e)
• if we found some Hstart a new loop on the local context to find some ModelWithCorners _ e H and return it
• if everything else failed, try synthesizing a normed field instance for e and return the corresponding model over itself.

[Patrick Massot]

Note how almost all those checks are purely syntactical. Only the last thing tried is using instance synthesis. So hopefully this is fast enough. And in the worst case scenario those elaborators could trigger a code action to replace them with explicit terms.

[Patrick Massot]

Last remarks:

• the % in the notation is only a convention for elaborator, any syntax can do
• those elaborators do not prevent anyone from writing direct calls to MDifferentiableAt and friends.

[Patrick Massot]

Now the question to @Sébastien Gouëzel, @Heather Macbeth, @Floris van Doorn, @Yury G. Kudryashov, @Oliver Nash and everybody interested in differential geometry in Mathlib is: do we want to push in this direction?

[Floris van Doorn]

Patrick Massot said:

What I want to discuss today is the next step. Saying “let σ be a section of V” is very easy, this is what dependent type is all about: (σ : Π x : M, V x). But then if we want to say σ is differentiable at m : M it becomes awful:

FYI: there is docs#ContMDiffSection.

[Patrick Massot]

This is only for globally smooth sections.

[Floris van Doorn]

fair

[Floris van Doorn]

It's an interesting direction to use such elaborators. It definitely looks a lot nicer!

For the problem of specifying the ModelWithCorners, I'm wondering if there is some approach using classes (+ outParams?) to maybe not specify the model with corners every time, since usually the model with corners is unique. But term elaborators are probably more flexible, since it does allow you to specify the model with corners if you want.

I think your current approach is a reasonable to pursue.

[Yury G. Kudryashov]

AFAIR, the main reason we can't rely on typeclasses to find the model with corners is that E \x F has two candidates: 𝓘(𝕜, _) and (𝓘(𝕜, E)).prod (𝓘(𝕜, F). It would be nice to have some "do the right thing in most cases, allow overriding as needed" way to deal with it.

[Sébastien Gouëzel]

I agree that the elaborators look great, and that they're definitely worth pursuing.

I had some tried ago another idea: make I an outparam. For that, one should solve the product issue by forgetful inheritance, i.e., embed in every topological space a charted space structure over itself. I consider this as a failed argument, but you can have a look at the branch at #26776. This is not obvious to implement because a charted space structure involves partial homeos, which are already defined using a topology. So I used an auxiliary class TopologicalSpaceWithoutAtlas, built just enough topology with it to be able to define an atlas, and then defined TopologicalSpace on top of it.

Most things work (painfully) once this is done, but I encountered an issue with fiber bundles. Our current definition for a fiber bundle E -> B is that it should have a charted space structure over B x F, where F is a model for the fiber. And once B has a charted space structure over some H, then this is automatically transported to a charted space structure over H x F (well, more precisely ModelProd H F in the current implementation). With the new framework, as B has a charted space structure over itself, then the fiber bundle charted space structure over B x F is automatically transported (among others) to a new charted space structure over B x F which is not defeq to the previous one, and boom, diamond. I solved it in the PR by requiring in the definition of a fiber bundle E -> B that it should have a charted space structure over ModelProd B F, which is then automatically transported (among others) to a charted space structure over B x F, solving the diamond.

This works, but I'm not sure how much of a gain this is compared to the current situation: we can make I an outparam, but the definition of topological spaces is more complicated (which is a pain in many places) and we still need ModelProd anyway. So I don't think it's worth pursuing, but I thought I should mention it as a failed experiment.

[Sébastien Gouëzel]

Do I understand correctly that we could use your elaborator as a notation? I feel that MDifferentiableAt% looks a little bit weird, but if instead we use a notation like MDiffAt f x (scoped in Manifold) this would feel completely standard. And we could add all the variants MDiff f, MDiff[s] f (for MDifferentiableOn I J f s), MDiffAt f x, MDiffAt[s] f x, and also CMDiff n f, CMDiff[s] n f, CMDiffAt n f x, CMDiffAt[s] n f x for coherence and completeness. (If you have better notation ideas, it's even better)

[Patrick Massot]

Yes, as I wrote earlier, the % sign seems to be a tradition for elaborators, but it has no technical necessity. We can switch to your notation very easily.

[Patrick Massot]

Do you have a suggestion for the T% elaborator?

[Sébastien Gouëzel]

No good idea for T% on my side. total would work, but it's not really self-explanatory, and it's longer than T%.

[Michael Rothgang]

Small detail: the new delaborators don't pretty-print as they should, so the commandStart linter complains about them. Is probably not hard to fix.

[Damiano Testa]

Can you point me to a commit which oleans, so that I can take a look?

[Damiano Testa]

If the doc-string of the notation also contains how you would like it to print, that makes it easier to figure out what should happen!

[Michael Rothgang]

I made a PR with these elaborators at #27021: as this blocks most of the remaining work in #26221, I'm arguing it's useful to land this now, with a clear label "experimental" and a promise to clean this up in the future.

[Michael Rothgang]

@Floris van Doorn @Kyle Miller Would one of you like to take a look?

[Michael Rothgang]

Damiano Testa said:

Can you point me to a commit which oleans, so that I can take a look?

Thanks! #26221 builds (CI fails because there are sorries). The doc-strings should contain the expected formatting now. One example of a linter error is in VectorBundle/GramSchmidtOrtho.lean.

[Michael Rothgang]

One question that came up: how can one scope these elaborators to the Manifold namespace? I tried the obvious things elab[Manifold]:max and elab:max[Manifold, but neither worked.

[Yaël Dillies]

scoped[Manifold] elab ... is the christened syntax, but if it doesn't work then namespace Manifold elab ... end Manifold should definitely work

[Michael Rothgang]

Thanks for the extremely quick answer :heart: scoped[Manifold] elab didn't work, but putting it inside namespace Manifold did.

[Yaël Dillies]

It would be great to get scoped[Manifold] elab fixed. I don't remember the full story, but I believe @Kyle Miller does

[Michael Rothgang]

See also #mathlib4 > scoped[NS] doesn't work with syntax

[Michael Rothgang]

I just added a new pair of very similar elaborators: mfderiv% f expands to mfderiv I J f, and mfderiv[s] f expands to mfderivWithin I J f s. Better naming suggestions, particularly for the first one, are very welcome!

[Dominic Steinitz]

Probably because I am newish to Lean but I found it picking instances (in differential geometry) that I didn't want it to. Eventually I gave up with having to write e.g.

 @IsManifold ℝ _ _ _ _ _ _ (𝓡 1) ⊤ S1 _ S1.chartedSpace

and defined a new data type wrapping the entity in which I was interested:

def MobiusBase := Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1

structure S1 where
  point : MobiusBase

and now I am in full control.

I have no idea whether this the right approach but it seems to be working in that I have no unpleasant surprises.

I can't help feeling that although this initiative makes things simpler in some ways, a new user such as myself might not realise what was happening under the covers.

[Patrick Massot]

I’m afraid we don’t have enough context to help you here. Could you write a #mwe?

[Dominic Steinitz]

Patrick Massot said:

I’m afraid we don’t have enough context to help you here. Could you write a #mwe?

Yes I am working on one which will be a blog post but don't hold your breath.

[Michael Rothgang]

At @Sébastien Gouëzel 's request, let me bring #27021 on the agenda again: in the past weeks, that PR has seen some amount of polish, including extended documentation and tests and improvements to robustness and error messages.

Is there anything blocking the landing of this PR, to start experimentation? (This does block much of the Levi-Civita connection work, for example --- as un-doing the use of the elaborators to re-do them later would be a massive waste of time.)

[Michael Rothgang]

@Floris van Doorn has been reviewing much of the meta code (in person). Which of these changes we discussed do you insist on happening before a first merge? (The code has clear warnings about being not polished yet.)

[Sébastien Gouëzel]

I've written on the PR that I will merge it in one week if nobody with meta expertise shows up in between, because I consider the extensive test coverage a proof that it's working well.

[Thomas Murrills]

I can give this (another) review, if it's desired. :) (Am I interpreting correctly that you would like someone to show up within one week? :grinning_face_with_smiling_eyes:)

My understanding is that the intended design is finalized and agreed-upon, and a review ought to be targeted at the meta code and implementation. Is that right? (Or, what specifically would be helpful for a meta-focused review to consider?)

[Sébastien Gouëzel]

Yes, that's perfectly right.

[Michael Rothgang]

I can confirm: the general design works well --- if you see a completely new way to do this, I'm very happy to hear about it after merging a first version.

[Michael Rothgang]

Also: thanks a lot for volunteering to review this PR! The diff is huge, but that's because most of it are tests.

[Thomas Murrills]

I'm checking the implementation of the algorithm, and I'd like to clarify something about this part of it:

Patrick Massot said:

• if we found some Hstart a new loop on the local context to find some ModelWithCorners _ e H and return it
• if everything else failed, try synthesizing a normed field instance for e and return the corresponding model over itself.

If we find an H, but then fail to find a ModelWithCorners, should we still try to synthesize a normed field instance, or just fail? (Currently, we just fail; I suspect we might want to try synthesizing a normed field instance instead!)

[Thomas Murrills]

By the way, just as a progress update here:

My suggested changes for this PR will be mostly straightforward—refactoring for readability/maintainability of meta code, fixing metaprogramming gotchas/implementation details, and fixing typos/style.

However, there are a decent number of such changes, and many of the straightforward changes span many lines (e.g. because they change some approach in a uniform way, such as changing PrettyPrinter.delab to Term.exprToSyntax).

There were also a small number of significant fixes/refactors necessary: for example, care needs to be taken with TermElabM in findModel when attempting multiple successive elaborations, and the for loops ought to be replaced with a different (simpler) approach for finding instances and local declarations. (I take the opportunity to improve tracing slightly when refactoring findModel, but otherwise do not add any features.)

It is a bit unconventional for a review, but given that the GitHub review interface is a bit awkward for making large suggestions, I think the most convenient thing to do here is for me to:

1. open a PR to your branch, where each commit is a single suggested change
2. add review comments explaining each suggested change and linking to the corresponding commit in that PR which performs it.

I'll submit the comments all at once when I'm finished. :) (I may open the PR to your branch as a draft before that, but please feel free to ignore it until I've completed the actual review.)

I'm planning to look over documentation and stress-test the test coverage tomorrow; with the code itself mostly fully reviewed now, I'm hoping to finish the review tomorrow or this weekend. The test file looks great, though, so I don't expect to find any issues! :)

[Thomas Murrills]

Also, to get into something specific: the reason the MDiffAt2 elaborator fails is because we run findModel on the fvar src : M introduced by forallBoundedTelescope, when we should be running it on the type of src!

However, MDiffAt2 actually appears a bit less robust to me: it seems to allow the fvar introduced by forallBoundedTelescope to be picked up by findModel (potentially, though this would be unusual), and we do not check that it is absent from the result (or abstract it). Is there an example where the (rest of the) approach of MDiffAt2 would be expected to succeed but MDiffAt wouldn't?

[Michael Rothgang]

Thomas Murrills said:

By the way, just as a progress update here:

My suggested changes for this PR will be mostly straightforward—refactoring for readability/maintainability of meta code, fixing metaprogramming gotchas/implementation details, and fixing typos/style.

However, there are a decent number of such changes, and many of the straightforward changes span many lines (e.g. because they change some approach in a uniform way, such as changing PrettyPrinter.delab to Term.exprToSyntax).

There were also a small number of significant fixes/refactors necessary: for example, care needs to be taken with TermElabM in findModel when attempting multiple successive elaborations, and the for loops ought to be replaced with a different (simpler) approach for finding instances and local declarations. (I take the opportunity to improve tracing slightly when refactoring findModel, but otherwise do not add any features.)

It is a bit unconventional for a review, but given that the GitHub review interface is a bit awkward for making large suggestions, I think the most convenient thing to do here is for me to:

1. open a PR to your branch, where each commit is a single suggested change
2. add review comments explaining each suggested change and linking to the corresponding commit in that PR which performs it.

I'll submit the comments all at once when I'm finished. :) (I may open the PR to your branch as a draft before that, but please feel free to ignore it until I've completed the actual review.)

I'm planning to look over documentation and stress-test the test coverage tomorrow; with the code itself mostly fully reviewed now, I'm hoping to finish the review tomorrow or this weekend. The test file looks great, though, so I don't expect to find any issues! :)

Thanks a lot, that sounds very promising. A PR into the PR branch works very well!

[Michael Rothgang]

Thomas Murrills said:

Also, to get into something specific: the reason the MDiffAt2 elaborator fails is because we run findModel on the fvar src : M introduced by forallBoundedTelescope, when we should be running it on the type of src!

However, MDiffAt2 actually appears a bit less robust to me: it seems to allow the fvar introduced by forallBoundedTelescope to be picked up by findModel (potentially, though this would be unusual), and we do not check that it is absent from the result (or abstract it). Is there an example where the (rest of the) approach of MDiffAt2 would be expected to succeed but MDiffAt wouldn't?

Good question. I learned that using forallBoundedTelescope is apparently better, but cannot yet detail why - so let me pass this question on:
@Floris van Doorn You strongly felt that MDiffAt was not a robust approach. Can you elaborate and perhaps answer this question? Thanks!

[Michael Rothgang]

Thomas Murrills said:

I'm checking the implementation of the algorithm, and I'd like to clarify something about this part of it:

Patrick Massot said:

• if we found some Hstart a new loop on the local context to find some ModelWithCorners _ e H and return it
• if everything else failed, try synthesizing a normed field instance for e and return the corresponding model over itself.

If we find an H, but then fail to find a ModelWithCorners, should we still try to synthesize a normed field instance, or just fail? (Currently, we just fail; I suspect we might want to try synthesizing a normed field instance instead!)

Good question! Indeed, the current code is not maximally robust, in several aspects:

• if there are several ChartedSpace instances on M, involving different types H, we currently just pick the first one. (There may be situations where we want the second one. Say, about a complex manifold also being regarded as a real manifold, or so. I can construct a test if needed, though that'll be a bit onerous.)
• if there is a ChartedSpace instance on H, but no matching model in sight... I'd need to think if/when this can happen (we should have a test, though perhaps this could be added after the initial version). I can imagine looking for a normed field instance being helpful.

[Thomas Murrills]

Just to check, is T% intended to be scoped to the Manifold namespace? (I'm checking the module docstring, and it seems to only say the differentiability elaborators are scoped.)

[Michael Rothgang]

Yes, it is. (That module doc-string should be fixed, and the T% elaborator scoped if it isn't already.)

[Thomas Murrills]

Sounds good, I'll fold that into my suggestions. :)

[Michael Rothgang]

Thanks a lot for your thorough review! I just have two small questions. Otherwise, I merged your PR (and will deal with the last two requests tonight).

[Michael Rothgang]

Let me start a bikeshed about the first one already: are there strong opinions where the elaborators should live? (The current proposal is Mathlib.Geometry.Manifold.Elaborators, but this would be the first module in mathlib called Elaborators.)

[Edward van de Meent]

some other options: Notation or Elab

[Edward van de Meent]

we already have Mathlib.Order.Notation which does some delaborating and adds some macros

[Edward van de Meent]

and looking further, there's a bunch more Notation files. I don't think that the difference between notation created implemented as a macro and notation implemented by an elaborator are too different.

[Edward van de Meent]

all to say, I'd be in favor of just naming it Notation

[Thomas Murrills]

Notation sounds good to me too, especially since delaborators are intended via TODO. :) Thanks for finding the precedent!

[Michael Rothgang]

All review comments are now addressed; there is one last issue (which is a question of differential geometry, not metaprogramming).

Given a function on the total space of a tangent bundle, what's the correct way to talk about its smoothness? (More specifically, if M is a manifold over I and h: Bundle.TotalSpace F (TangentSpace I : M → Type _) → F; right now MDiff h does not type-check, and indeed probably shouldn't. But what's the correct way to say "a function from the tangent bundle to another manifold is smooth"?

[Michael Rothgang]

And there is a follow-up question by Thomas:

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

[Michael Rothgang]

@Sébastien Gouëzel @Floris van Doorn This is touching parts of mathlib's differential geometry that you probably know better than me, so your opinion would be most welcome!

[Sébastien Gouëzel]

Michael Rothgang said:

But what's the correct way to say "a function from the tangent bundle to another manifold is smooth"?

The tangent bundle is just a manifold in the usual sense, with the model with corners I.tangent (which is just an abbrev for I.prod 𝓘(𝕜, E)). So, to say that a function f from the tangent bundle is differentiable, you would just say MDifferentiable I.tangent J f, as usual.

[Michael Rothgang]

Thanks, that was reassuring.

[Michael Rothgang]

From my side, the PR is now ready for review (and probably, merging).

[Michael Rothgang]

@Thomas Murrills If you like a puzzle, you can join me in #30307, debugging why the extension I made to the elaborator does not fire. (There's a coercion PartialEquiv to functions. My very vague guess: that is not applied because the custom elaborator forgot to do this?)

[Michael Rothgang]

@Sébastien Gouëzel Ping: all review comments are fully addressed; I consider the PR ready for merging.

[Michael Rothgang]

#30307 is now ready for review: it allows the elaborators to apply to anything which coerces to functions (including partial homeomorphisms (e.g., charts), partial equivalences (e.g., extended charts) and bundled smooth sections).

[Michael Rothgang]

#28032 builds on top of that one and adds support for inferring the model with corners on a TangentBundle, as well as a few more tests.

[Thomas Murrills]

Great! :D I’ll review these today. :)

[Michael Rothgang]

#30307 has been approved by Thomas . Would a maintainer like to take a look? @Floris van Doorn @Sébastien Gouëzel It's a small, well-tested and uncontroversial addition to the linters. (For another data point, I have tested this on almost all of mathlib in #30357 and not found any issues.)

[Michael Rothgang]

Current status update: the past week has seen some significant activity on the elaborators. There are now in-flight PRs which add new elaborators (e.g. HasMFDeriv(Within)At), support coercions, and adds support for inferring the model with corners in more cases. ##30357 shows that this can be used to golf mathlib's differential geometry library significantly.

[Michael Rothgang]

#30503 tracks the overall progress and missing features

[Michael Rothgang]

@Thomas Murrills has been reviewing these PRs, but cannot merge them. A maintainer's look is appreciated. Right now, these PRs are a linear sequence (also to avoid conflicts).

[Michael Rothgang]

The first PR is #30307, supporting coercions: I consider this ready to go.

[Michael Rothgang]

The next PR in the sequence is #28032, adding support for inferring the model with corners in a few more cases, and making a few clean-ups to style, tracing messages and tests. +200/-84 lines; Thomas already approved this.

[Michael Rothgang]

Here's a design question for this thread: an in-progress PR of mine also infers the model with corners on a product. Given a product of normed spaces, there are two possible models to infer, either 𝓘(𝕜, E × F) on E × F, or 𝓘(𝕜, E).prod 𝓘(𝕜, F) on ModelProd E F (which is defined to be E × F`). What should the elaborators do in this case?

[Michael Rothgang]

(a) try to respect this decision, and infer the right model depending on whether it's a ModelProd or a product? (Might be tricky, given the elaborator otherwise checks for equivalence of types up to defeq.)

[Michael Rothgang]

(b) in such cases, do not infer a model for now and print a message stating this (This is the most conservative option)

[Michael Rothgang]

(c) Always infer the former model --- and change mathlib to never use statements about the latter. (Indeed, there is only one lemma in mathlib involving the latter, and that lemma is only used 12 times. So this might be feasible.) Put differently, writing the elaborators this way would enforce that most lemmas only use the former model (and single out any other examples as different).

[Michael Rothgang]

(d) Something else, such as having an option to control which model is inferred.

[Michael Rothgang]

What do you think? @Floris van Doorn @Sebastian Ullrich @Patrick Massot @Heather Macbeth @Yury G. Kudryashov?

[Yury G. Kudryashov]

You get the latter model, e.g., if you specialize a lemma about ModelProd to normed spaces. We can't totally get rid of it. As a minimum, we need Iff/Eq/Diffeomorphism lemmas/defs saying that the two models are equivalent.

[Michael Rothgang]

Sure! We do have one lemma like this.

[Michael Rothgang]

My question about option (c) is: do we want any lemmas in mathlib to be stated in terms of the latter model, or should we have a rule "lemmas are always stated about the former, and if you option the latter (e.g. by specialisation), you must rewrite into the former immediately"?

[Yury G. Kudryashov]

I think that we shouldn't use the latter model except for lemmas/defs saying that it's equivalent to the former model.

[Sebastian Ullrich]

@Michael Rothgang I'm not sure you summoned the right Sebasti[ae]n here!

[Sébastien Gouëzel]

I don't think you can really do (a), because the model space can typically not be inferred from the context. I wouldn't do (c), because it doesn't seem to me that one model is really more natural than the other -- even more, I'd say that "(c'): inferring 𝓘(𝕜, E).prod 𝓘(𝕜, F)" is maybe more natural, because this is what should be inferred for all product manifolds, and special casing vector spaces is bound to create a mess. So I'd go either for (c') or for (b).

[Michael Rothgang]

Indeed, that was an auto-complete failure. I meant Sébastien.

[Michael Rothgang]

Thanks for all the comments so far. Let me summarize the options:
(b) conservative (and easy to implement); not the best long-term solution
Do not infer a model on a product of normed spaces and print a message stating this. This is annoying, but it could (presumably) be made to print the possible options, so users could still write the elaborator first and then get the right suggestion.
(c') Always infer 𝓘(𝕜, E).prod 𝓘(𝕜, F), because this is what you get when specialising a theorem for product manifolds.

---

Not good options
(a) try to guess which product is wanted (e.g., depending on whether it's a ModelProd or a product). Seems not possible in practice.
(c) Always infer 𝓘(𝕜, E × F)` and require all mathlib lemmas to be stated this way
Con: there's no clear reason one model is more natural --- one might even argue the other one is better.

[Yury G. Kudryashov]

I trust @Sébastien Gouëzel 's judgement more than mine here, so please disregard my comment above.

[Michael Rothgang]

Barring further comments, I suggest to do first (b) and (c'): implementation-wise, it's good to iron out all the kinks and unexpected bugs around products before attempting this case where failures could truly be informational. Once that part works well, I'll try (c') and see how it goes.

[Michael Rothgang]

#30412 is the next PR in the sequence: its diff is somewhat large (+-350-400 lines), but very simple: it just splits the test file in two.

[Michael Rothgang]

#30577 is now ready for review: it adds a test for something that should clearly work (and already works)

[Michael Rothgang]

#30413 is a more substantial change: it adds elaborators for HasMFDeriv{Within}At, and supports finding a model with corners in a few more cases. Adds about 50 lines of meta code, and 280 lines of tests.