leanprover-community
Replace manually defined extensionality lemmas by `@[ext]`
#1645 allows @[ext] to be applied to a structure to automatically derive the extensionality lemma. We should replace manually defined ext lemmas with the attribute. (The attribute should already be present on most of the lemmas themselves, so they'll be easy to find.)
I'm not sure how consistent we are overall with naming these sorts of things. ext, ext_iff, eq all show up, maybe more. We should make these consistent. (The attribute will help, obviously.)
In fact, @[ext] could be extended to generate the iff versions as well as the -> ones.
Are there examples of structures where it is harmful if @[ext] is applied?
I can't think of one. The only thing is that it might not be the right notion of extensionality for you
So in an alternative world the structure keyword would generate these by default, unless you prepend it with @[noext] to indicate that you want to write your own "right notion" of extensionality.
If we could change the meaning of structure, I'd be in favor with redefining it the way you say but I don't want to start redefining basic structures for something that an attribute does perfectly well.
Also, having a new structure keyword asks you to remember to use a different keyword in order to get the ext declaration. It's not exactly what I'd call a default behavior.
Exactly: we don't live in that alternative world :grinning: I'm happy to use @[ext].
Currently, e.g., monoid_hom.ext uses ⦃f g : M →* N⦄ as arguments. Do I understand correctly that the new @[ext] structure monoid_hom would generate a lemma with (f g : M →* N)? Another difference between the manually defined and autogenerated lemmas would be usage of to_fun vs coe_fn. BTW, do you require extensional or = equality on function fields?
