building @[extensionality] lemmas for structures

Stream: general

[Scott Morrison]

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]

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]

shouldn't that obviously be a derive handler?

[Scott Morrison]

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]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Simon Hudon]

@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]

I thought the thing after derive was just a label

[Scott Morrison]

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?

[Mario Carneiro]

yes

[Mario Carneiro]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

it does that already

[Simon Hudon]

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

[Scott Morrison]

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

[Simon Hudon]

Doesn't it?

[Scott Morrison]

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

[Simon Hudon]

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]

@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]

@Scott Morrison Any luck in building it?

[Scott Morrison]

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