Elab to generalize type classes for theorems

Stream: lean4

[Vlad Tsyrklevich]

I'm currently finishing up Metaprogramming in Lean and I'm thinking about projects to make use of it before I forget it all. One idea I had was for a command elaborator that overrides the default elab for theorem/lemma definitions, and tries to define the given theorem/lemma with more general type class assumptions (e.g. by replacing with a parent class in the hierarchy) and see if it succeeds. This seems like a kind of obvious idea that others may already have implemented, but searching around didn't reveal anything. Is anyone aware of such a thing?

[Kevin Buzzard]

There was this in Lean 3: https://www.youtube.com/watch?v=pudd4F749tE (Alex Best talk)

[Kim Morrison]

It would be amazing to have this in Lean4 again!

[Kim Morrison]

Also having a mode where this can be run at library-scale (e.g. just an option that can be set in the lakefile, that prints info messages on promising declarations) would be nice.

[Vlad Tsyrklevich]

Yeah, being able to use it on all of mathlib is my main idea. I’ll give it a shot and see how it goes

[Vlad Tsyrklevich]

Alex J. Best Nice talk! I learned things

[Asei Inoue]

nice idea!

[Vlad Tsyrklevich]

I've got something hacky working with lots of room for improvement. It already finds many possible generalizations, many seem like they may be nice-to-have, others are maybe not very useful, e.g. generalizing a type class for a single lemma deep in a theory where everything else only targets the more specific type is probably not going to help much. That's for the experts to judge though.

Here is an example of its results. This change builds, though obviously I do not propose it be reviewed in anything like this form. I am just sharing some early results in case anyone has feedback. I also had a question: is this change too big to put up a draft PR and try to run !bench on it? It requires a rebuild of the entirety of mathlib so I figure it may be a bad idea.

Some quick stats, the most common type classes generalized from:

  38 IsDedekindDomain
  44 PartialOrder
  46 AddMonoid
  58 Monoid
  65 CommRing
  72 Ring
  94 Semiring
 100 AddCommGroup
 116 Module

Most common generalized to:

  28 LE
  31 NonUnitalNonAssocSemiring
  38 IsDedekindRing
  41 Ring
  42 DistribMulAction
  46 Preorder
  54 MulOneClass
  66 AddZeroClass
  66 NonAssocSemiring
  71 Semiring
  82 AddCommMonoid
  96 SMul

Most common ordered as pairs specific->general

  11 CommSemiring -> Semiring
  12 MulAction -> SMul
  13 MonoidHomClass -> MulHomClass
  13 Semiring -> NonUnitalNonAssocSemiring
  14 NonAssocSemiring -> NonUnitalNonAssocSemiring
  14 TopologicalGroup -> ContinuousMul
  16 AddCommGroup -> AddGroup
  17 CommSemigroup -> CommMagma
  18 CommRing -> Semiring
  22 AddCommMonoid -> AddZeroClass
  23 Preorder -> LE
  24 Field -> DivisionRing
  36 PartialOrder -> Preorder
  37 CommRing -> Ring
  38 IsDedekindDomain -> IsDedekindRing
  42 AddMonoid -> AddZeroClass
  42 Module -> DistribMulAction
  42 Ring -> Semiring
  48 Monoid -> MulOneClass
  62 Semiring -> NonAssocSemiring
  64 Module -> SMul
  80 AddCommGroup -> AddCommMonoid

These are incomplete results as there are probably more generalizations/types of generalizations I could find, but sharing as an overview.

[Eric Wieser]

Vlad Tsyrklevich said:

I also had a question: is this change too big to put up a draft PR and try to run !bench on it? It requires a rebuild of the entirety of mathlib so I figure it may be a bad idea.

No, this happens all the time, and bench builds from scratch anyway so the size of the PR doesn't affect the cost.

[Kevin Buzzard]

This is awesome! I would honestly be tempted to just open a PR with this (if you can get it building).

[Notification Bot]

12 messages were moved from this topic to #mathlib4 > Elab to generalize type classes for theorems by Eric Wieser.

[Eric Wieser]

(I moved discussion about contributing to mathlib / mathlib typeclass-specific gotchas to #mathlib4)