## Stream: general

### Topic: building @[extensionality] lemmas for structures

#### Scott Morrison (Aug 13 2018 at 13:07):

Hi @Simon Hudon, I'm wondering if you've thought recently about building @[extensionality] lemmas for structures automatically. I know we had some discussion about this a long time ago (gitter?), and some attempts at a congr_struct tactic.

#### Simon Hudon (Aug 13 2018 at 13:32):

Hi Scott! No, I haven't thought of it but I think it shouldn't be hard. We could invoke it with @[make_extentionality] to distinguish from the lemma itself.

#### Mario Carneiro (Aug 13 2018 at 13:33):

shouldn't that obviously be a derive handler?

#### Scott Morrison (Aug 13 2018 at 13:33):

From memory the problems quickly arose when there were dependent fields. First there's the question of whether to use rewrites or heqs.

#### Scott Morrison (Aug 13 2018 at 13:34):

But I think correctly building the statements for later fields, in either approach, seemed hardish.

#### Mario Carneiro (Aug 13 2018 at 13:34):

can't you just use congr to generate the lemma?

#### Scott Morrison (Aug 13 2018 at 13:34):

At the time I knew almost nothing about writing tactics, and haven't thought much about it since, however. :-)

#### Mario Carneiro (Aug 13 2018 at 13:35):

However, I don't usually find that extensionality lemmas are automatable

#### Mario Carneiro (Aug 13 2018 at 13:35):

since they are often mathematically nontrivial, e.g. units A only depends on the first component

#### Simon Hudon (Aug 13 2018 at 13:35):

@Mario Carneiro I also thought about making it a derive handler but I think it has to be a type class for that, no?

#### Mario Carneiro (Aug 13 2018 at 13:36):

I thought the thing after derive was just a label

#### Scott Morrison (Aug 13 2018 at 13:36):

You mean ... make a metavariable of type a = b, actually run the cases a, cases b, congr tactic, then inspect the goals, take those as arguments for your declaration, and have the proof by cases a, cases b, congr ; assumption?

yes

#### Mario Carneiro (Aug 13 2018 at 13:38):

or more directly, just generate the congr_lemma and inspect its type

#### Scott Morrison (Aug 13 2018 at 13:41):

I see. We'd need a cleanup phase that decides when fields are propositional and omits those heqs.

#### Mario Carneiro (Aug 13 2018 at 13:42):

no, that's why I am suggesting you use the congr_lemma

#### Simon Hudon (Aug 13 2018 at 13:44):

Looking at the code for derive_attr, I think you're right Mario and it is of course a much better way

#### Scott Morrison (Aug 13 2018 at 13:45):

oh, okay: why doesn't congr do that then?

Doesn't it?

#### Scott Morrison (Aug 13 2018 at 13:47):

I just tried on category_theory.functor, and got goals for the propositional fields.

#### Simon Hudon (Aug 13 2018 at 13:50):

I'm surprised. You can clean them up I think using match_eq / match_heq and then using is_proof on the results.

#### Simon Hudon (Aug 13 2018 at 13:58):

@Mario Carneiro The annoying thing with derive is that it parses a pexpr and does some basic name resolution. We may get around it by defining a dummy like def extensionality := ()

#### Simon Hudon (Aug 14 2018 at 18:11):

@Scott Morrison Any luck in building it?

#### Scott Morrison (Aug 14 2018 at 22:42):

Sorry, haven't got back to it. Writing ext lemmas by hand is annoying but not critical. :-)

Last updated: May 14 2021 at 12:18 UTC