Duplication/repetitive code in various `Equiv`s

Stream: mathlib4

[Michael Rothgang]

This is a somewhat newbie question about mathlib's library design; feel free to move if there's a better stream.

I'm creating a new Equiv (ContinuousAffineEquiv, #11341). Here and in previous PRs, I noticed that adding basic API is lots of repetitive boilerplate: lots of Equivs (including PartialEquiv, PartialHomeomorph, Diffeomorph, LocalHomeomorph) have very similar code, e.g.

• refl, symm and trans "instances" (mind you, these are defs, not instances)
• the same lemmas about them: symm_refl, symm_symm, trans_refl, refl_trans, symm_apply, apply_symm_apply, symm_apply_symm, etc.

The latter is a long list which I never remember. Basically, I open a related file (if there are several: repeat for all of them), copy-paste the relevant section and adapt or delete lemmas accordingly. If there are several files, look if the second file contains new lemmas.
It's somewhat tedious, and of course every Equiv has a slightly different set of lemmas and in different order. I understand this is natural as mathlib grew organically over time, I can deal with it, but I wonder if there's a better way.

• Would it make sense to standardise these lemmas - e.g., in a particular order or to a particular set of lemmas?
• Is there a way to avoid the duplication? Do we need all of these lemmas?
• Do you have particular tricks to make writing this API more efficient/less tedious?

[Anatole Dedecker]

I agree with this, and Equivs are not the only occurence of such things. We probably don't want something too strict for now (looking at how much @[simps] we need to generate by hand, full automation is not the way to go) but having a template file would be a great way to start. If you or anyone else wants to create a page on the website describing this that would be great!

[Joseph Myers]

I think there have been previous discussions of various possible approaches for having type-generic refl, symm and trans that work for EquivLike classes in general to reduce such duplication. I wonder if we should set up notation typeclasses for refl, symm and trans (and then use the notation everywhere), plus typeclasses for when that notation, together with a family of EquivLike classes, satisfies the axioms of a groupoid. (I don't know how well such typeclasses would work with Lean's typeclass search / elaboration, however.)

[Kim Morrison]

The category theoretic Iso is there waiting for you. :-) It is not as universe polymorphic, but :woman_shrugging:.

[Johan Commelin]

@Edward van de Meent recently created such a template

[Eric Wieser]

I think the answer here is probably to have the generalization live outside of Lean's type theory, but as meta code that generates declarations

[Edward van de Meent]

i don't have a template for Equiv (yet), but i do have one for Hom...

[Edward van de Meent]

for that, see this message

[Edward van de Meent]

the trouble is that there are multiple ways to create Equiv classes, however. because you can say "this equivalence is [X] Equivalence that is also [Y] equivalence", or you can say it is "[Z] Equivalence that has [W] property", and either one generates not quite the same thing...

[Yaël Dillies]

@Anne Baanen's docs#EquivLike was supposed to be the solution to this duplication, but it induces a significant amount of technical pain itself.

[Edward van de Meent]

which reminds me, it would appear the docs suggest extending EquivLike when defining MyEquivClass, however for example MulEquivClass takes it as a parameter instead... what is the policy for this?

[Edward van de Meent]

because it leads to a bit of juggling when creating an instance for your new class

[Johan Commelin]

This was a recent refactor, and apparently not all the docs have been updated...

[Johan Commelin]

Taking a parameter is the new way to go

[Edward van de Meent]

ah :melting_face:

[Edward van de Meent]

i guess i have work to do :smiling_face_with_tear:

[Anne Baanen]

Related work by @Yury G. Kudryashov: #2202, https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/RFC.3A.20bundled.20sets.20.236442