Zulip Chat Archive

Stream: general

Topic: building @[extensionality] lemmas for structures


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 13 2018 at 13:33):

shouldn't that obviously be a derive handler?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Aug 13 2018 at 13:34):

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

view this post on Zulip Mario Carneiro (Aug 13 2018 at 13:34):

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

view this post on Zulip 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. :-)

view this post on Zulip Mario Carneiro (Aug 13 2018 at 13:35):

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

view this post on Zulip Mario Carneiro (Aug 13 2018 at 13:35):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 13 2018 at 13:36):

I thought the thing after derive was just a label

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 13 2018 at 13:38):

yes

view this post on Zulip Mario Carneiro (Aug 13 2018 at 13:38):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 13 2018 at 13:42):

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

view this post on Zulip Mario Carneiro (Aug 13 2018 at 13:42):

it does that already

view this post on Zulip 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

view this post on Zulip Scott Morrison (Aug 13 2018 at 13:45):

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

view this post on Zulip Simon Hudon (Aug 13 2018 at 13:45):

Doesn't it?

view this post on Zulip Scott Morrison (Aug 13 2018 at 13:47):

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

view this post on Zulip 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.

view this post on Zulip 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 := ()

view this post on Zulip Simon Hudon (Aug 14 2018 at 18:11):

@Scott Morrison Any luck in building it?

view this post on Zulip 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