ext + subsingletons

Stream: general

[Reid Barton]

Is there a particular reason that ext on a structure does not try to use subsingleton instances to eliminate unnecessary hypotheses from the generated lemma? (It only checks for Prop.)

[Pedro Minicz]

ext only uses lemmas annotated with @[ext], afik.

[Scott Morrison]

@Pedro Minicz, Reid is talking about something slightly different. Annotating a structure with @[ext] runs some metaprogram that actually constructs the extensionality lemmas that the tactic ext will later use (somewhat confusing!). Reid is asking for that metaprogram to be smarter.

[Scott Morrison]

(It's possible that @[ext] on a structure should actually have a different name, like @[generate_ext_lemma].)

[Pedro Minicz]

Oh, interesting. I was unaware of the @[ext] annotations in structures. I don't think it is necessary to change the name. I tend to prefer uniformity, even if at the cost of a tiny bit of ambiguity.

[Pedro Minicz]

Looking at the code for derive_struct_ext_lemma it already seems to have a lot going so. So maybe adding subsingleton wouldn't make it much more complex, relatively speaking.

[Pedro Minicz]

Do we have this kind of functionality implemented as more general functions in the tactic framework? For example, a "clean this lemma" function, to be called by multiple lemma generating tactics?

[Scott Morrison]

Sometimes... often resuable parts end up in tactic.core.