Normed modules

Stream: mathlib4

[David Loeffler]

Is there a typeclass in mathlib for normed modules over a normed ring satisfying ∀ a x, ‖a • x‖ = ‖a‖ * ‖x‖ (rather than just the inequality ∀ a x, ‖a • x‖ ≤ ‖a‖ * ‖x‖ which is what you get with BoundedSMul)? The two assumptions are equivalent if the ring is a normed division ring, but I'd like to use this for ℤ_[p]-modules.

[Kevin Buzzard]

(FWIW I think a BoundedSMul example where this stronger axiom fails would be the module $\Z/p\Z$ with the trivial norm $|v|=1$ for $v\not=0$)

[David Loeffler]

Sure; it wasn't my intention to suggest that every module (or every interesting module) satisfying BoundedSMul has this stronger property – a possibly more natural example is to take any Banach algebra that's not an integral domain, and consider it as a module over itself.

However, I do feel that modules satisfying this stronger property are useful enough that it would be nice to have a way of spelling the condition in mathlib.

[Eric Wieser]

I think we're also missing the analogous typeclass for norm_mul over rings like Int

[David Loeffler]

Eric Wieser said:

I think we're also missing the analogous typeclass for norm_mul over rings like Int

I agree. I think there are quite a few theorems being stated for NormedDivisionRing where the division isn't actually relevant, just in order to have norm_mul or norm_smul holding.

[David Loeffler]

I wonder what a good name for this would be? Maybe a ring with a strictly multiplicative norm can be a StrictNormedRing, and analogously StrictNormedModule?

[Kevin Buzzard]

I like Strict but right now this word is used in the naming convention in order theory to mean things like "preserves <". I guess you can argue that strict just means "stronger than <=" in both cases :-) I do feel like it's a good word mathematically for this concept.

[David Loeffler]

I had a look into defining StrictNormedRing but got sidetracked because the existing library file Analysis/Normed/Field/Basic is overdue a refactor anyway (it lives in a subdirectory Field but it contains the definition of a normed ring...) . I will make a pure refactor PR moving things to more sensible places, and then have a go at defining StrictNormedRing on top of that.

[David Loeffler]

It looks like we do have a name for the "unbundled" version of this (MulRingNorm for the strictly multiplicative version vs RingNorm for the sub-multiplicative one); just not for the version where it is bundled as "the" norm.

[Eric Wieser]

Another option here is a mixin typeclass that says the norm bound for SMul is tight, rather than inserting something into the typeclass hierarchy

[Eric Wieser]

(since if we do that we have to add all the Comm / Nonunital / Seminormed(?) versions too)

[David Loeffler]

Eric Wieser said:

Another option here is a mixin typeclass that says the norm bound for SMul is tight, rather than inserting something into the typeclass hierarchy

That's a really good idea actually, it will make it much less painful.

[Eric Wieser]

So StrictBoundedSMul, which would provide a toBoundedSMul instance

[Kevin Buzzard]

Or IsStrictBoundedSMul? Is it supposed to be a Prop?

[Eric Wieser]

If we want to go down that path I think we should rename BoundedSMul first

[Eric Wieser]

@loogle BoundedSMul

[loogle]

:search: BoundedSMul, NNReal.boundedSMul, and 209 more

[Eric Wieser]

That's quite a lot of renames, but hopefully very few deprecations

[Kevin Buzzard]

I would be happy not to open that can of worms, to be honest. The community still seems to be to be pretty divided on when we do and do not use Is. There is now some kind of official policy but I am not at all convinced that it is adhered to in practice.

[David Loeffler]

I would rather this rename be delayed at least until I have finished refactoring Analysis/Normed/* in order to disentangle normed rings and normed fields.

[Ruben Van de Velde]

I think there's a rough consensus that Is is good, but a lot of legacy code from before this was established

[David Loeffler]

David Loeffler said:

I would rather this rename be delayed at least until I have finished refactoring Analysis/Normed/* in order to disentangle normed rings and normed fields.

PR up at #22744.

[Yakov Pechersky]

Given that we have docs#NormOneClass as a mixin, would it make sense to have docs#NormMulClass? And then for normed modules use NormedSpace?

[David Loeffler]

Yakov Pechersky said:

Given that we have docs#NormOneClass as a mixin, would it make sense to have docs#NormMulClass? And then for normed modules use NormedSpace?

Even if the ring satisfies NormMulClass, it doesn't imply that all normed modules over that ring satisfy the stronger condition (think F_p as a module over Z_p). So we need an extra mixin typeclass for the modules too, NormedSpace isn't enough.

[David Loeffler]

I guess the names could be NormMulClass and NormSMulClass.

[Yakov Pechersky]

I think it's even worse because if I understood correctly, in your norm_M (r smul x) example, you'd want that to be equal to norm_M r * norm_M x, or abs_R r * norm_M x? If the former, wouldn't you get that from NormMulClass via docs#Algebra.algebraMap_eq_smul_one : edited, probably not...? And if the latter, wouldn't work with, for example, Q_p over Q, unless we include the "WithAbs" twist somehow.

[Eric Wieser]

Do we want this for metric spaces too like docs#BoundedSMul ? If so I think we should not use Norm in the name

[Yakov Pechersky]

Okay, how about saying that smul is IsUniformInducing?

[Kevin Buzzard]

My guess is that that "combinatorial" or "topological" assumption is weaker than being norm-preserving.

[Yakov Pechersky]

Or something that's the right way of saying that smul scales the uniformity in the expected manner. Which would work for metric spaces etc, iiuc

[Eric Wieser]

Tangentially; what's the deal with the generality of BoundedSMul? What's an example of a metric space that has a canonical zero but no norm?

[Yakov Pechersky]

https://math.stackexchange.com/a/170307

[Yakov Pechersky]

But that's a NormedSpace argument, sorry.

[Yakov Pechersky]

Maybe this? https://math.stackexchange.com/a/3519913

[David Loeffler]

I suspect the generality of BoundedSMul is determined by applications to NNReal, which explains why it assumes a zero but not an add group structure.

[Yakov Pechersky]

I've recorded the counterexample in #22810.

[David Loeffler]

David Loeffler said:

David Loeffler said:

I would rather this rename be delayed at least until I have finished refactoring Analysis/Normed/* in order to disentangle normed rings and normed fields.

PR up at #22744.

Now that #22744 is merged, I have made a PR that renames the Prop-valued typeclasses BoundedSMul and IsometricSMul / VAdd to IsXXX. See #22797. It touches a lot of files so I would be grateful for a quick review.

[David Loeffler]

See #22842 for a PR introducing a "NormMulClass" mixin typeclass for rings with a strictly multiplicative norm.

[Eric Wieser]

#23787 has the NormSMulClass mixin, but is not ideal performance-wise. I think we still want it, but it would be nice to track down if any of the performance loss is easily recoverable.

[David Loeffler]

I wonder if the performance problems we are having are related to the slightly indirect way that NormedSpace (over normed fields) is defined: that the definition of the class requires ∀ a x, ‖a • x‖ ≤ ‖a‖ * ‖x‖, but then we immediately show that this actually implies the a priori stronger condition ∀ a x, ‖a • x‖ = ‖a‖ * ‖x‖. This makes it difficult to integrate NormedSpace into a typeclass hierarchy which provides typeclasses describing both of these conditions for more general normed rings (where they are definitely not equivalent): situations like this, "A trivially implies B, but B in fact implies A under some auxiliary hypothesis C", seem to cause performance pain for typeclass resolution.

If we changed the definition of NormedSpace so exact multiplicativity ∀ a x, ‖a • x‖ = ‖a‖ * ‖x‖ was baked into the definition, and provided a lemma – not an instance – allowing one to construct NormedSpace instances given sub-multiplicativity, would that perhaps solve some of the problems? Then all the instances would "go downhill" so to speak; the "uphill" step, proving that the a-priori weaker condition actually implies the stronger one, wouldn't be part of the typeclass system.

Of course, there's a trade-off in that it means one needs to prove more when defining NormedSpace instances on concrete types. But I'm not sure it actually comes up that often: how frequent is it that one has a normed vector space for which it is really genuinely harder to prove ‖a • x‖ = ‖a‖ * ‖x‖ than ‖a • x‖ ≤ ‖a‖ * ‖x‖?

[Eric Wieser]

I don't think changing the field inside NormedSpace will have any effect on performance, or on what instance paths we can pick. Notions of downhill and uphill should be about the typeclass itself, not its implementation details

[Eric Wieser]

David Loeffler said:

But I'm not sure it actually comes up that often: how frequent is it that one has a normed vector space for which it is really genuinely harder to prove ‖a • x‖ = ‖a‖ * ‖x‖ than ‖a • x‖ ≤ ‖a‖ * ‖x‖?

I would say pretty much all the time. If you've set your type up in full generality, it's likely that you first provided a very general IsBoundedSMul instance. If you've done that anyway, the le proof is "free", while the new one requires some work. Of course, if you've also instantiated the NormMulClass in full generality, then by the time you get to NormedSpace both are free anyway.

[David Loeffler]

David Loeffler said:

how frequent is it that one has a normed vector space for which it is really genuinely harder to prove ‖a • x‖ = ‖a‖ * ‖x‖ than ‖a • x‖ ≤ ‖a‖ * ‖x‖?

Eric Wieser said:

I would say pretty much all the time.

Eric's response surprised me, so I decided to check in the library. So far, with only one single exception (operator norms on linear maps), the proofs of the norm_smul_le field of NormedSpace consist of proving equality and then using le_rfl or le_of_eq. So I think the evidence does not support Eric's assertion.

[Eric Wieser]

I was thinking of the ~10 cases where we prove the NormedSpace instance with norm_smul_le := norm_smul_le

[Eric Wieser]

David Loeffler said:

If we changed the definition of NormedSpace so exact multiplicativity ∀ a x, ‖a • x‖ = ‖a‖ * ‖x‖ was baked into the definition

In case it's relevant, this ends up reverting !3#2693.

[David Loeffler]

Eric Wieser said:

I was thinking of the ~10 cases where we prove the NormedSpace instance with norm_smul_le := norm_smul_le

A lot of those just become norm_smul := norm_smul (or disappear entirely).

[David Loeffler]

See the current version of #23787 for an attempt at changing NormedSpace to require norm_smul rather than norm_smul_le. Benchmarking now.

[David Loeffler]

What's the best way forward here? It seems that my proposal of adjusting the definition of NormedSpace doesn't worsen the slow-down caused by introducing NormSMulClass, but it doesn't solve it either (consistently with Eric's remark that the speed of instance search is independent of how the individual typeclasses are implemented). So we are at a standstill.

It's very frustrating to be blocked from adding new capabilities to mathlib because of the apparent impossibility of doing so without slowing down the existing functionality. Can we live with the slowdown? (~15% for the worst-affected files, but those are quite short; 0.3% overall slowdown across the whole of mathlib.) I'm afraid that I do not have the expertise to work out why the slowdown is occurring, or whether anything can be done to avoid it.

[Kevin Buzzard]

Here's my workflow for diagnosing slowdowns. Start with the github output of bench which is here. Next fire up two mathlibs, and check out the two commits mentioned at the top of that message (lake exe cache get works fine). Note that I am doing this on a machine with two monitors and 32 gigs of ram! Then go to a file which has suffered a lot (e.g. Mathlib.Analysis.Analytic.Basic in this case) and just do some completely dumb things (e.g. press a key in the module docstring in each file to get both versions of the file to recompile) and stare and hope you see something fishy. This part is very much hit-and-miss.

So let's try hitting and missing. I thought I saw HasFPowerSeriesWithinOnBall.tendsto_partialSum_prod taking a long time so let's look at that. On line 873 I add #count_heartbeats in in both files and we see that it's 4708 on master and 5607 on the branch, which is about a 20% speedup. But this is quite a big proof. Let's try something smaller -- radius is on line 117 and it's 3966 heartbeats on master and 4865 on the branch, and it's only one line long so this looks like much easier to take apart. But it's a def. The first theorem about it, le_radius_of_bound is 2729 on the branch and 2279 (note: not the same number) on master so that's also a 20% speedup and it's a one-line proof so this is definitely somewhere where we could start.

So delete #count_heartbeats in on line 120 and replace it with

set_option trace.profiler.useHeartbeats true in
set_option trace.profiler.threshold 10000 in
set_option trace.profiler true in

in both files. The set_option profiler.threshold 10000 in option might not do anything, you could not use heartbeats and instead use times in seconds but heartbeats are in my experience a more robust measurement (even though they will change from run to run, you can only trust them to a couple of sig figs for some reason). Clicking on the blue underline on the docstring gives

[Elab.command] [4127190.000000] /-- If `‖pₙ‖ rⁿ` is bounded in `n`, then the radius of `p` is at least `r`. -/
    theorem le_radius_of_bound (C : ℝ) {r : ℝ≥0} (h : ∀ n : ℕ, ‖p n‖ * (r : ℝ) ^ n ≤ C) : (r : ℝ≥0∞) ≤ p.radius :=
      le_iSup_of_le r <| le_iSup_of_le C <| le_iSup (fun _ => (r : ℝ≥0∞)) h ▶

on the branch and

[Elab.command] [3458114.000000] /-- If `‖pₙ‖ rⁿ` is bounded in `n`, then the radius of `p` is at least `r`. -/
    theorem le_radius_of_bound (C : ℝ) {r : ℝ≥0} (h : ∀ n : ℕ, ‖p n‖ * (r : ℝ) ^ n ≤ C) : (r : ℝ≥0∞) ≤ p.radius :=
      le_iSup_of_le r <| le_iSup_of_le C <| le_iSup (fun _ => (r : ℝ≥0∞)) h ▶

so indeed there's definitely something fishy going on. What is it? Start unfolding in both VS Code windows. Timings for almost everything are almost the same except that

  [step] [2751455.000000] expected type: Type (max u_3 u_2), term
      FormalMultilinearSeries 𝕜 E F ▶

has become

  [step] [3419812.000000] expected type: Type (max u_3 u_2), term
      FormalMultilinearSeries 𝕜 E F

and here the gap is even wider in relative terms, so we're on the right track. Unfold again. The big thing that stands out now is

 [Meta.synthInstance] [706260.000000] ✅️ ContinuousConstSMul 𝕜 E

which has become

    [Meta.synthInstance] [1068033.000000] ✅️ ContinuousConstSMul 𝕜 E ▶

and this is now more like a 40% slowdown. Continuing to dig we have that

 [] [80524.000000] ✅️ apply @NormedSpace.isBoundedSMul to IsBoundedSMul 𝕜 E

has become

 [] [292007.000000] ✅️ apply @NormSMulClass.toIsBoundedSMul to IsBoundedSMul 𝕜 E

etc etc. Keep going! This is the killer:

[] [35.000000] ✅️ MonoidWithZero.toMonoid =?= MonoidWithZero.toMonoid

on master vs

[] [34667.000000] ✅️ MonoidWithZero.toMonoid =?= MonoidWithZero.toMonoid

on the branch. So it looks like there are two monoid instances which are less defeq than before and that typeclass inference now explodes them on your branch. I don't have an immediate fix but this looks like something which it might be possible to fix (sorry, I have a meeting in 1 minute so need to stop). But this (on your branch) is never good:

[] [11343.000000] ✅️ Semiring.npow =?= Semiring.npow ▼

[Michael Stoll]

There seems to be a misplaced "```" in your message...

[Matthew Ballard]

When was this merged with master last?

[Eric Wieser]

Pretty recently I think. Merging master will invalidate our previous benchmarks unfortunately

[Matthew Ballard]

We've had significant changes to the instance graph in the interim which could possibly interact with these changes in new ways.

[David Loeffler]

I will merge latest master on this PR, and split off some changes that are
not relevant to the speed issues; but it might take me a day or so! —
Regards, David

[Matthew Ballard]

I merged master.

[Matthew Ballard]

I don't think de-tangling the order stuff helps much but perhaps IsSeminormedGroupand friends might

[Matthew Ballard]

One Zero
Another Zero

Two ways to get to the Zero for a docs#NontriviallyNormedField. They are defeq but not immediately so. Previously only the path through docs#NonUnitalNonAssocCommSemiring was seen because we were always looking in this context. But in the context ofNormSMulClass.toIsBoundedSMul we don't take that path to Zero. Lean has to check these are defeq a few times.

[Yuyang Zhao]

Decoupling algebraic typeclasses from Normed* is my next step to speed up searching in the algebraic typeclass hierarchy. But maybe not using Prop-valued typeclasses, rather something like !3#18462. Otherwise we would have to write [Norm E] [PseudoMetricSpace E] [AddCommGroup E] [IsNormedAddGroup E] for SeminormedAddCommGroup E.

[Yuyang Zhao]

If we have to use Prop-valued typeclasses, maybe we need two new typeclasses to avoid [Norm E] [(Pseudo)MetricSpace E].

[Kevin Buzzard]

I was coming to exactly this sort of conclusion for local fields, wondering if [Field K] [Preorder K] [UniformSpace K] plus some Prop-valued mixins was going to be the way to go

[Kevin Buzzard]

(in that theory we don't need the real numbers so the norm is replaced by a preorder and the metric by a uniformity. Here the preorder is defined by a <= b iff |a|<=|b| where |x| is a nonarchimedean valuation)

[Kevin Buzzard]

I left some comments about traces on Eric's PR. I've still not got to the bottom of things.

If the slowdown is actually about the exact moment that one drops the norm when moving from our "normed algebra" typeclass hierarchy to our algebra hierarchy (and more specifically about the fact that NonUnitalNormedCommRing->NonUnitalCommRing and SeminormedRing->Ring are different places to cross the border) then I would argue that this is evidence that there is a lot to be gained (not just in this PR but in mathlib in general) from decoupling our normed hierarchy from our algebra hierarchy, just as there was a lot to be gained from the recent decoupling of the algebra hierarchy from the order hierarchy. In fact the same argument would seem to suggest that we should even decouple commutativity of multiplication from the algebra heirarchy and have [Ring R] [IsCommutativeMul R] instead of [Ring R] and [CommRing R].

[Kevin Buzzard]

With current library design (if indeed it is designed as opposed to just being how it is by default) what is the logic behind where we are encouraging the border crossing? Should SeminormedRing.toRing also be low priority? here is what we currently have in mathlib: we have no fewer than 8 classes {NonUnital}{Semi}normed{Comm}Ring intertwined with 12 instances all flagged with the [lower instance priority] note.

[Kevin Buzzard]

IMG_20250413_222335365_HDR.jpg

I think that's what mathlib looks like currently, regarding {NonUnital/unital}{non-comm/Comm}{no norm/Seminorm/Norm}ed rings (so non-unital rings in the bottom left up to normed commutative rings in the top right, with seminormed rings in the middle). A red X means that the instance is present but has priority 100. The slightly curvy lines are NonUnitalNormedCommRing.toNonUnitalCommRing (i.e. skip the non-unital seminormed commutative ring) and NormedCommRing.toCommRing. A notable absentee is Seminormed Ring.toRing which presumably has default prio and which Matt explicitly flagged as perhaps causing a problem in the PR (note that SeminormedCommRing.toCommRing has prio 100). I don't know how to find the priority of SeminormedRing.toRing, I guess it could have prio lowered elsewhere.

What should the logic of the diagram be? Are we being inconsistent and paying for it now?

Is the picture supposed to be saying "Here are 12 classes but we really really really don't want you to deduce any of them from any of the others, except that you are allowed to deduce X from CommX"? Because that it what it says right now. It seems like a very weird set-up to me.

[Kevin Buzzard]

#24011 for an attempt to at least make the picture symmetric (i.e. "all lines exist and all but the ones dropping Comm have prio 100")

[Eric Wieser]

For what it's worth, in Lean 3 the rule was "every X.toY instance has priority 100, and only the concrete instances get the default priority"

[Eric Wieser]

When we ported that, it became "X.toY instances not implemented with extends get priority 100" because that was what mathport did and what Lean 4 supported at the time

[Eric Wieser]

My initial take is that those curvy lines in your diagram are bad and should be deleted

[Kevin Buzzard]

You can't delete NormedCommRing.toCommRing (the top curvy line) because NormedCommRing extends CommRing.

[Kevin Buzzard]

It's the normed to seminormed lines which "aren't really there" and we're adding them with code like

-- see Note [lower instance priority]
/-- A normed commutative ring is a seminormed commutative ring. -/
instance (priority := 100) NormedCommRing.toSeminormedCommRing [β : NormedCommRing α] :
    SeminormedCommRing α :=
  { β with }

[Eric Wieser]

Ah, I guess removing those lines is one of the things that (a redo of) #9642 would address

[Eric Wieser]

But I guess if we follow that road, we should also delete Semiring.toAddCommMonoid and make it go through unital/assoc classes

[Kevin Buzzard]

There is an undrawn curvy NormedRing.toRing line which has prio 1000 if I got my first ever piece of metacode right:

#eval Lean.Meta.getInstancePriority? ``NormedRing.toRing -- some 1000

so we made the 100 prio instance from NormedRing to SeminormedRing but if you're trying to get to Ring you can just go directly there at prio 1000.

[Kevin Buzzard]

I can't wait until Jireh tells us that he wants non-associative normed rings because then the number of classes in Mathlib/Analysis/Normed/Ring/Basic.lean goes up from 8 to 16. And then maybe Junyan will insist that we do it all for semirings (note: that's different to seminorms) so we can go up to 32.

[Kevin Buzzard]

Then it will be much harder to draw the diagram.

[Aaron Liu]

Kevin Buzzard said:

I can't wait until Jireh tells us that he wants non-associative normed rings because then the number of classes in Mathlib/Analysis/Normed/Ring/Basic.lean goes up from 8 to 16. And then maybe Junyan will insist that we do it all for semirings (note: that's different to seminorms) so we can go up to 32.

Maybe some of these should be mixins then

[Jireh Loreaux]

It probably won't be me, but what do you think a JB*-algebras is?

[Kevin Buzzard]

Well it's not so easy to make some of them mixins because in the world of rings they're not mixins and this is extending rings.

[Johan Commelin]

I'm looking forward to

variable [Zero R] [One R] [Add R] [Neg R] [Mul R]
variable [Topology R] [Uniformity R] [Dist R] [Norm R]
variable [IsNormedCommRing R]

[Johan Commelin]

Full disclosure: I'm not sure whether :up: is me being serious or joking.

[Edward van de Meent]

you sure we won't break it down into NormedMul and IsRing etc instead? :upside_down:

[Eric Wieser]

@Johan Commelin, you forgot IntCast R, NatCast R, SMul Int R, SMul Nat R, Pow R Nat, Sub R, NNDist R ...

[Aaron Liu]

Eric Wieser said:

Johan Commelin, you forgot IntCast R, NatCast R, SMul Int R, SMul Nat R, Pow R Nat, Sub R, NNDist R ...

Those can be added as needed, I know most theorems don't use a natpow

[David Loeffler]

This sounds like a catastrophic step backwards in terms of usability.

[Eric Wieser]

Aaron, only if you're willing to write ... [Pow R Nat] [IsRing R] [IsLawfulNatPow R] etc, which is now even worse.

[Aaron Liu]

I'm not saying this is a good idea

[Johan Commelin]

David Loeffler said:

This sounds like a catastrophic step backwards in terms of usability.

:100: So we would need good elaborator support before considering this approach.
But if it actually massively improves TC performance, then I think we should seriously consider how to make this a step forwards in terms of usability.

[Aaron Liu]

After seeing what happened with ordered algebra, I think this might also be a 40% drop in TC but no one's tried it yet because it massively hurts usability.

[Kevin Buzzard]

Eric raised the possibility of variable [Zero R] [One R] [Add R] [Neg R] [Mul R] ... a while ago (i.e. over a year ago). I am beginning to wonder whether Lean 4's typeclass inference system is pushing us towards such a design pattern.

Having spent many hours over the weekend trying and failing to speed up David's PR, I'm now wondering whether we should bite the bullet and merge it and just note that uncoupling norms from algebra will almost certainly give us the speedup back.

[Eric Wieser]

I have a few things I'd like to try over the next few days, but otherwise I agree merging soon is reasonable

[Jireh Loreaux]

I mentioned this in another thread (in the context of T2Space vs. R1Space + T0Space), but I think we need to make variable alias (or something like it) standard and usable in practice. The problem with variable? right now is that it does the replacement, and I would prefer it didn't. It would also make Mathlib much more familiar to new users (cf. there was a recent thread about HilbertSpace 𝕜 E and why that doesn't exist).

If we did this, then we could still write nice variablelines even if they get expanded to [SomeAlgbraicStructure] [SomeNormStructure] [SomeOrderStructure] (or even further) under the hood.

[Jireh Loreaux]

With the (not-so-)new behavior of variable and how they are included in declarations, this wouldn't be too much of a problem. The worst offenders might be things where you have a Module 𝕜 E, but the statement only references elements of E, and then you would need to include {𝕜}. I'm not sure how widespread an issue that would be.

[Kevin Buzzard]

I really pushed for VectorSpace in Lean 3 and eventually we gave it a go, but Lean 3 typeclass wasn't up to the job so it got reverted. If we get variable alias working then we could go back to this idea (and then it would save me telling generations of undergrads that Module is just French for vector space)

[Jireh Loreaux]

To be clear, I think we should make this happen regardless of whether we separate everything into atomic classes or not. Simply splitting the algebra, order, analysis hierarchies would be sufficient reason, not to mention Kevin's issue of making everything more readable for the uninitiated.

[Johan Commelin]

The main design question that I see is how you want to create new instances:

instance : Ring FooBar where
  zero := sorry
  one := sorry
  add := sorry
  ...

now has to become

instance : Zero FooBar where
  zero := sorry

instance : One FooBar where
  one := sorry

instance : Add FooBar where
  add := sorry

...

How should the elaborator treat

instance : HilbertSpace k E

[Sébastien Gouëzel]

Here is a design possibility just for variable declaration.

variable {k E : Type*} [[Module k E]]

goes through the typeclass assumptions of Module k E (here [Semiring k] [AddCommMonoid E]), checks for each of them if it is available as an instance, and otherwise declares it. So here it would declare under the hood [Semiring k] [AddCommMonoid E] [Module k E], but in

variable {k E : Type*} [NormedAddCommGroup E] [[Module k E]]

it would only declare [Semiring k] [Module k E].

Additionally, one would have a command

variable_alias (k E : Type*) [RClike k] [SeminormedAddCommGroup E] [InnerProductSpace k E] [CompleteSpace E] HilbertSpace

When declaring

variable {k E : Type*} [[HilbertSpace k E]]

it would do the same as above, i.e., go one by one though the typeclass assumptions in the variable_alias line, and declare them if they can not be synthetized from the context.

[Sébastien Gouëzel]

As for Johan's question, I would just forbid instance : HilbertSpace k E. To me, this should just be a mechanism for variable declaration. Ideally, it should work both in variable lines and in def or theorem statements, by the way.

And in an even more ideal world, when hovering over such a declaration one should get the list of the genuine typeclass assumptions that are generated through it.

[Johan Commelin]

Sébastien Gouëzel said:

As for Johan's question, I would just forbid instance : HilbertSpace k E. To me, this should just be a mechanism for variable declaration. Ideally, it should work both in variable lines and in def or theorem statements, by the way.

That is fine with me. Especially if the notation in the variable line makes it clear that we're not assuming an ordinary instance.

[Johan Commelin]

The tricky bit is

variable {k : Type*} [AddCommGroup k]

-- stuff happens here

variable {E : Type*} [[Module k E]]

Now we have [Semiring k] and we already have an existing [AddCommGroup k].

[Kim Morrison]

It seems that is an orthogonal problem, for which we are already desperately overdue a linter for! :-)

[Matthew Ballard]

Johan Commelin said:

The main design question that I see is how you want to create new instances:

instance : Ring FooBar where
  zero := sorry
  one := sorry
  add := sorry
  ...

instances which synthesizes the appropriate instance parameters from the environment and the data fields supplied by the user and then builds the Ring instance from those?

Also, I think the rule of thumb is to ask whether when you go hunting for an instance via a projection you are likely to succeed more often than not across in the library. Mathematically, Norm and TopologicalSpace seem to generally stand a good chance of appearing together so bundling them is reasonable. But Norm and Field is more niche to unbundling is better.

[Jireh Loreaux]

Sébastien Gouëzel said:

As for Johan's question, I would just forbid instance : HilbertSpace k E. To me, this should just be a mechanism for variable declaration. Ideally, it should work both in variable lines and in def or theorem statements, by the way.

And in an even more ideal world, when hovering over such a declaration one should get the list of the genuine typeclass assumptions that are generated through it.

Couldn't have communicated it better myself. Sébastien's proposal is exactly what I envision.

[Damiano Testa]

Kim Morrison said:

It seems that is an orthogonal problem, for which we are already desperately overdue a linter for! :-)

I had a linter that was flagging when a typeclass assumption in variable was syntesizable from the variables already present.

[Damiano Testa]

This happens everywhere, though...

[Damiano Testa]

Let me find the branch

[Damiano Testa]

#14731 is the linter.

[Matthew Ballard]

#24086 tries to avoid the path through toComm(Semi)Ring when possible. :fingers_crossed:

[Jireh Loreaux]

Damiano Testa said:

This happens everywhere, though...

It does? That seems like not something we want. I'm confused.

[Damiano Testa]

Let me revise this a little: it is not too widespread and I mention something in #mathlib4 > recyclable variables @ 💬.

[Damiano Testa]

I think that there are 168154 such situations, at least these are the ones that the linter notices.

[Eric Wieser]

Eric Wieser said:

I have a few things I'd like to try over the next few days, but otherwise I agree merging soon is reasonable

Soon was a lie, but I managed to shave off 1% (as a fraction of the overhead, not the total build time)