Elab to generalize type classes for theorems

Stream: mathlib4

[Eric Wieser]

Continuing from #lean4 > Elab to generalize type classes for theorems which discussed whether automated generalization was possible:

others are maybe not very useful

Some examples of this are thinks like generalizing [Ring R] [AddCommGroup M] [Module R M] to [Ring R] [AddCommMonoid M] [Module R M], since every module over a ring is necessarily also an AddCommGroup, and the generalization is just a distraction.

[Eric Wieser]

(The same is not true for [Semiring R] [AddCommGroup M], which actually can be useful)

[Ruben Van de Velde]

One might start with the ones that are just dropping commutativity, for example

[Ruben Van de Velde]

Maybe the main annoyance will be that it's harder to use variable

[Vlad Tsyrklevich]

Eric Wieser said:

since every module over a ring is necessarily also an AddCommGroup

Are you saying that M is always actually an AddCommGroup, or am I misunderstanding? If that's the case, should Module actually require an AddCommGroup?

[Vlad Tsyrklevich]

Ruben Van de Velde said:

Maybe the main annoyance will be that it's harder to use variable

That's one thing I have actually not gotten to yet. My current code only looks at type classes explicitly defined in the declaration, I do not yet look at those pulled in by variable

[Vlad Tsyrklevich]

However, building mathlib there are actually only a few places where it has complaints about uses of variable being shadowed, so at least up until now it doesn't seem to make it too messy

[Eric Wieser]

Vlad Tsyrklevich said:

Are you saying that M is always actually an AddCommGroup, or am I misunderstanding? If that's the case, should Module actually require an AddCommGroup?

I'm saying that the following are interesting:

• [Semiring R] [AddCommMonoid M] [Module R M] (a "semimodule")
• [Semiring R] [AddCommGroup M] [Module R M] (e.g a positive cone in a vector space)
• [Ring R] [AddCommGroup M] [Module R M] (a "module")

and this one is not:

• [Ring R] [AddCommMonoid M] [Module R M] (equivalent to a "module" mathematically, but with data fields absent)

[Kevin Buzzard]

Vlad Tsyrklevich said:

Are you saying that M is always actually an AddCommGroup, or am I misunderstanding? If that's the case, should Module actually require an AddCommGroup?

If R is a semiring and M is an AddCommMomoid then M can be an R-module. If R is a ring and M is an AddCommGroup then M can be an R-module and this is the set-up which is often used by mathematicians. The point is that if R is a ring (not a semiring) and M is an AddCommMonoid and if furthermore M is an R-module, then M is automatically an AddCommGroup, because negation on M can be defined by acting by -1 in the ring. So if you can't weaken the assumption on R from Ring to Semiring then weaking the hypothesis on M from group to monoid might just be causing problems rather than solving them, because they're still groups and it's now harder to see this because you're now going "the wrong way" in the typeclass inference graph.

[Vlad Tsyrklevich]

That makes sense. There could be some filters to try to match cases like this. If others see more cases that are not useful generalizations in that diff, that'd be helpful

[Kevin Buzzard]

If the total diff is going to be O(600 lines) then I would be tempted to just PR anyway, and link to this thread in the first message of the PR, and get people to check manually for stuff like this. Note that the second change (Mathlib/Algebra/Algebra/Basic.lean) is a bad module change, but the next few look fine to me. Stuff like Field -> DivisionRing, CommRing -> Semiring and Semiring -> MonoidWithZero look like great changes to me. It will be interesting to see what the results of benchmarking are.

[Edward van de Meent]

should part of this conversation move to #mathlib4 ? i imagine talking about specific suggestions by the tool will be more appropriate there, while talking about implementation of this kind of tool would (i think) still be appropriate here (edit: in #lean4)?

[Notification Bot]

12 messages were moved here from #lean4 > Elab to generalize type classes for theorems by Eric Wieser.

[Vlad Tsyrklevich]

Kevin Buzzard said:

If the total diff is going to be O(600 lines) then I would be tempted to just PR anyway, and link to this thread in the first message of the PR, and get people to check manually for stuff like this.

The current diff is over a commit that's ~2 weeks old so it's got plenty of merge conflicts already, but I'll keep that in mind for when I prepare the changes to upstream. Ideally, I'd like my code to be in a more complete state before preparing any derivative changes, though I'll probably have some small changes to split off before then.

[Eric Wieser]

I think you should make a PR anyway, even if it has conflicts

[Eric Wieser]

Then people can start extracting parts they like into spin-off PRs. You can always force-push over the original PR when you re-run

[Vlad Tsyrklevich]

I got caught up in a refactor and have not yet gotten to this, but will soon.

[Vlad Tsyrklevich]

I had a question about how to structure this to eventually upstream to Mathlib. I originally wrote the code as a command elab because that's what matched what I learned in Metaprogamming in Lean. Later I realized it could be a linter and that I could then use @[nolint] since at least one theorem requires it, but then after porting the code to use Lean's Linter architecture I realized that @[nolint] is specific to Batteries' linter architecture, which only supports MetaM. So now I have no idea if this should even be a Linter since it seems like it adds nothing and has some costs. At this point either approach is fine for me. Feedback welcome.

[Eric Wieser]

There are two types of linters; environment and syntax. Which one are you trying to explore, and why is MetaM an issue?

[Vlad Tsyrklevich]

Up until now I've worked on Syntax and I think that's the right way to go. That's what I meant with the MetaM comment since I thought that I would not be able to retrieve Syntax for declarations, but now I'm not sure if that's actually correct.

[Vlad Tsyrklevich]

Perhaps a related question: there is no equivalent for @[nolint] for linters in Mathlib (or perhaps just an extension of @[nolint] so both use the same attribute), instead a number of linters seem to use a number of scripts/nolints* files for the same purpose. Is there a principaled reason for this or is it just vestigial?

[Damiano Testa]

The way to silence a syntax linter is to use set_option linter.option false.

[Damiano Testa]

However, this normally is an indication that the exception is something that probably should not be linted in the first place, and it is ok to allow it.

[Vlad Tsyrklevich]

Aha, I had not seen this pattern before. So set_option linter.xyz false in seems to be kind of the idiomatic equivalent of @[nolint]

[Damiano Testa]

The nolints file are typically exceptions that should be resolved, in the sense that the linter is "right" in excepting them. Usually they are accumulated debt from introducing a linter late: you cannot/do not want to fix all the exceptions, but you still want to avoid introducing more exceptions in future code.

[Damiano Testa]

A good example of this is the docPrime linter: the idea is that every declaration that ends in ' should have an explanation of why it exists with this name, rather than something more descriptive.

[Damiano Testa]

However, when the linter was added, there were already over 4k exceptions.

[Damiano Testa]

So, those exceptions were engulfed in a giant nolints file and new declarations were no longer allowed to end in '.

[Damiano Testa]

If, for some reason, a future declaration was supposed to be allowed to end in ' and not have a doc-string, then set_option linter.docPrime false in would be the "correct" solution, instead of increasing the nolints file.

[Vlad Tsyrklevich]

That all makes sense and helps motivate how I should proceed, thanks!

[Vlad Tsyrklevich]

I've put up #22337 for review. It's branched off of the current master. I only included a subset of the generalizations (~350 in total). In particular I avoided any rewrites that would increase lines past >100 chars to avoid hitting linter warnings, and I also excluded all AddCommGroup -> AddCommMonoid changes for now.

[Ruben Van de Velde]

Looks like there's some interesting errors - probably you should fix those in a separate PR

[Ruben Van de Velde]

Also: cool!

[Vlad Tsyrklevich]

I investigated the batch of 30 unusedArguments linter failures and wanted to ask for some feedback. I'd not run the environment linters during development so I hadn't seen that in some cases generalization makes some instances unnecessary. For quick background, the way my linter works is very naive, simply trying to replace text for explicitly specified type classes instances in a theorem's declaration with it's parent type classes. It is not yet aware of instances pulled in from variables.

In 20/30 linter failures, this was cases that we would expect, things like generalizing [StarAddMonoid A]->[Star A] meaning we no longer need [AddMonoid A].
In 8/30 cases something more pernicious was happening, a theorem would use e.g. [Module R M] in the scope of variable {Module R M} block, and my linter would try to replace it with something more general and it would succeed because the implicit instance was being pulled in from the variable block. I changed my linter to reject generalizations when it caused a new parameter to be added to the theorem's type.
The final 2 cases are what I'm less sure about, these are cases where by weakening the instance's type class, we caused it to be implicitly synthesized instead, e.g. for

theorem finite_of_fg_torsion [AddCommGroup M] [Module ℤ M] [Module.Finite ℤ M]
    (hM : Module.IsTorsion ℤ M) : _root_.Finite M := by

deleting [Module ℤ M] just causes it to be implicitly synthesized using docs#AddCommGroup.toIntModule. This is not a generalization, but just replacing an explicit type class with an implicitly synthesized one. This seems like it may be undesirable, since it just makes the code less explicit. I'm not sure if it's also possible that the synthesized type class could also be different in a way that subtly changes the resulting statement of the theorem. I wanted to check if others agreed that I should teach my linter to avoid this case, before I try to figure out the best way to do so.

[Kevin Buzzard]

[Module \Z M] is a subsingleton (ie all instances are propositionally equal) but because that instance which you link to exists I think we must be discouraging users from creating another one, which makes me think that it's safe to delete. It might be a remnant of before docs#AddCommGroup had an inbuilt action of Int

[Ruben Van de Velde]

I think this actually un-generalises the theorem, in that it now no longer works if you already have a Module that doesn't come from AddCommGroup

[Kevin Buzzard]

But a Z-module which is a monoid is mathematically an AddCommGroup. And the theorem already asks for an AddCommGroup?

[Kevin Buzzard]

Given that docs#AddCommGroup.toIntModule exists it seems to me that the current set-up is as silly as a theorem asking for [Group G] [Monoid G]

[Kevin Buzzard]

We do have at least one ZSmul diamond in mathlib right now (see my unique open PR which Andrew Yang didn't think would fix the problem) but I can't imagine that we want a theorem which is specifically designed to work even if there are diamonds, I think we're supposed to fix the diamonds

[Vlad Tsyrklevich]

In case it's useful, the second example of this is a case of deleting [Module R₀ P.Cotangent] and instead using docs#Algebra.Extension.instModuleCotangent. Since it may be useful to delete some instances, perhaps I won't implement a change to filter them out yet, and instead I'll collect cases where this happens and see what people think when I have more examples, as this PR is only a subset of all generalizations found

[Kevin Buzzard]

Aah now this one isn't a subsingleton so deleting it might in theory actually change the meaning of some theorems, and if this happens in practice then it will probably change them to what the user actually meant to write :-)

[Eric Wieser]

Kevin Buzzard said:

but I can't imagine that we want a theorem which is specifically designed to work even if there are diamonds, I think we're supposed to fix the diamonds

At once point this actually was something we wanted, but this was before we introduced AddGroup.zsmul

[Vlad Tsyrklevich]

I have been finishing up some remaining edge case investigation in mathlib and just thought I'd share here. My linter currently tries to repeatedly replace a type class with a parent type class (note: only one at a time, if it has e.g. 3 parent type classes it won't try to replace it with 2/3). It will only report the most general type class, assuming generalization only follows a single parent in the tree. If there is a fork, it will report multiple "most general" type classes. This only occurs twice, once is because in docs#HahnSeries.embDomain_one it wants to replace NonAssocSemiring with either AddMonoidWithOne or MulZeroOneClass (what it actually wants is [Zero R] [One R] but the linter isn't smart enough for that.)

The other is docs#Ordinal.type_eq_zero_of_empty where IsWellOrder can be replaced by any of its parents, because IsEmpty means that it can be implicitly synthesized. My linter avoids reporting 'generalizations' if just deleting the entire class still causes the theorem to succeed to compile [1], and in this case because r does not have a type, it fails to synthesize IsWellOrder using docs#instIsWellOrderOfIsEmpty Adding a type to r silences the 'generalization'

[1] There is already a linter that reports if a type class is unused, so deleting it just means that it causes an explicit type class to be made implicit via synthesis or being pulled in from a variable block, and this should IMO be up to the discretion of the author.

[Vlad Tsyrklevich]

I've been somewhat hesitant to start looking at generalizing type classes inherited from variable blocks as these changes will be painful to automatically apply, I will probably hold off any investigation until I get more feedback on the current changes to ensure the current results are providing value.

[Vlad Tsyrklevich]

Going to use this thread a bit for non-PR review chat.

[Vlad Tsyrklevich]

One thing I realized the other day is that many possible generalizations are not expressed by parent type classes in the hierarchy, e.g. Semifield is not a parent of Field, T2Space is not a parent of T1Space, etc. I ran a build with the following additional parent relationships injected:

(Child, (Parents))

  (`Group, [`DivisionMonoid, `CancelMonoid]),
  (`AddGroup, [`SubtractionMonoid, `AddCancelMonoid]),
  (`CommGroup, [`CancelCommMonoid, `DivisionCommMonoid]),
  (`AddCommGroup, [`AddCancelCommMonoid, `SubtractionCommMonoid]),

  (`CommSemiring, [`NonUnitalCommSemiring, `CommMonoidWithZero]),
  (`CommRing, [`CommSemiring, `NonUnitalCommRing, `AddCommGroupWithOne]),
  (`DivisionRing, [`DivisionSemiring]),
  (`Field, [`Semifield]),
  (`NonUnitalCommRing, [`NonUnitalCommSemiring]),
  (`Ring, [`NonUnitalRing, `NonAssocRing]),

  (`NormedDivisionRing, [`NormedRing]),
  (`DenselyNormedField, [`NontriviallyNormedField]),
  (`NormedField, [`NormedDivisionRing]),
  (`NormedField, [`NormedCommRing]),

  (`T1Space, [`T0Space]),
  (`T2Space, [`T1Space]),
  (`T25Space, [`T2Space]),
  (`T3Space, [`T25Space]),
  (`T35Space, [`T3Space]),
  (`T4Space, [`T35Space]),
  (`T5Space, [`T4Space]),
  (`T6Space, [`T5Space]),
  (`CompletelyRegularSpace, [`RegularSpace]),
  (`PerfectlyNormalSpace, [`CompletelyNormalSpace]),
  (`CompletelyNormalSpace, [`NormalSpace]),
  (`PathConnectedSpace, [`ConnectedSpace]),
  (`IrreducibleSpace, [`ConnectedSpace]),
  (`PreirreducibleSpace, [`PreconnectedSpace]),
  (`R1Space, [`R0Space]),

For T*Space most of the results were junk, e.g. 'generalizing' a theorem about a T2Space to a T0Space, because T0Space + IsTopologicalRing recovers the Hausdorff property. In this case it, would be useful to not offer a generalization if the 'generalized' definition still allows you to synthesize the original type class. This seems obvious now, and in fact perhaps this offers a different way of filtering away useless generalizations, instead of writing code that specifically looks for the case where I have [Ring R] [AddCommMonoid M] [Module R M], maybe I just add an instance [Ring R] [AddCommMonoid M] [Module R M] : AddCommGroup M that's included only when the generalizer runs to make it clear AddCommGroup->AddCommMonoid does nothing.

[Kevin Buzzard]

I think instance [Ring R] [AddCommMonoid M] [Module R M] : AddCommGroup M is a recipe for diamonds. I thought we had it already in some form? Edit: docs#Module.addCommMonoidToAddCommGroup (not an instance)

[Vlad Tsyrklevich]

Yeah my idea was to only inject it when the generalizer is running, though maybe that's more trouble than it's worth