HomClasses and tooling

Stream: mathlib4

[Eric Rodriguez]

On #6045, I migrated some lemmas to use MonoidHomClass as opposed to specifically typed such lemmas. This caused some breakage, and @Yaël Dillies asked me to revert this, so that Lean works more smoothly. I was opposed to this, because I personally feel that the added flexibility is really great. However, they do have a great point that often these lemmata break more than just elaboration and often slow down proofs. I guess the main point of this thread is to start a discussion on this, and see what the way forward should be in many respects.

One idea I had here was to write a metaprogram that can generate such lemmas - that is, when a lemma is tagged with @[MNFA], (short for My New Fancy Attribute), anything with an instance of XHomClass gets its own automatically generated lemma that is fully type-correct, e.g.:

class FooHomClass := ...
--- two instances - RingHom and Homeomorph

@[MNFA] lemma eq_id (f : F) : f = id := sorry
-- would produce two lemmas `RingHom.eq_id` and  `Homeomorph.eq_id`.

This gets complicated by the fact that lemmas can be defined before instances of XClass are defined, and also the complexities of XClass applying sometimes.

Another is just to give in and manually write duplicates for common cases. I think this is what Yael is advocating for.

I'm personally fine with sticking with just HomClasses and hoping that we can squirrel down this behaviour into something that can be remotely fixable in core.

[Riccardo Brasca]

Do you think this was already the case in Lean3?

[Yaël Dillies]

Yes it was.

[Yaël Dillies]

All I'm saying really is that it's acceptable to have structure-specific lemmas where hom classes lemmas do not elaborate properly. Gladly, the most common hom classes lemmas (map_add, map_pow, ...) do elaborate properly.

I'm not advocating for full duplication.

[Riccardo Brasca]

Sure, I am not saying duplication is a big problem, I am just curious if we can rather solve the elaboration problems.

[Eric Wieser]

It looks to me like this PR changes not only the lemmas, but the definitions too?

[Eric Wieser]

In particular, docs#IsLocalRingHom now works on RingHomClass. This is possibly problematic, because now you need lemmas to translate between IsLocalRingHom f and IsLocalRingHom ↑f for every RingHomClass f

[Eric Rodriguez]

It actually works on MonoidHomClass. There is an instance for f ringhomclass -> f as a ring hom, but nothing else - I'm not sure why other translations would be necessary

[Eric Rodriguez]

And that was pretty much done to sate old code