Zulip Chat Archive

Stream: general

Topic: ext + subsingletons

Reid Barton (Sep 26 2020 at 00:16):

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 (Sep 26 2020 at 00:53):

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

Scott Morrison (Sep 26 2020 at 01:15):

@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 (Sep 26 2020 at 01:15):

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

Pedro Minicz (Sep 26 2020 at 02:12):

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 (Sep 26 2020 at 02:15):

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 (Sep 26 2020 at 02:16):

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 (Sep 26 2020 at 03:21):

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

Last updated: Dec 20 2023 at 11:08 UTC