feat(extensionality): rename to ext; generate ext rules for structures

[cipher1024]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[semorrison]

What does this do?

[semorrison]

(Perhaps we should update the PR template so it prominently asks for a summary, before the checklist.)

[digama0]

@semorrison Tell me I'm crazy, but didn't you use a tactic like this one in the category theory library? See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Equivalent.20of.20subtype.2Eeq.20for.20structures.3F/near/179768896

[digama0]

@cipher1024 Why the name change in this tactic? This is just @[extensionality] theorem T.ext, automatically derived. I would prefer the name @[derive extensionality] if possible.

[semorrison]

Nope, I'd asked for it, but never got around to writing it. Good things come to those who wait! (Well, not usually.)

[robertylewis]

@cipher1024 Why the name change in this tactic? This is just @[extensionality] theorem T.ext, automatically derived. I would prefer the name @[derive extensionality] if possible.

This was my gut response too, but right now derive is used specifically for type class instances. (Also the interface for a derive handler is slightly different.) Here's a half-baked idea: what about modifying @[extensionality] itself, so it can be applied either to a lemma like now, or to a structure, in which case it generates the relevant lemma?

[robertylewis]

Independent of the above: are we consistent in the library about using type.ext and type.eq? I just checked subtype, which uses the first for the iff version and the second for the -> version. Maybe this tactic could generate both. It should apply the extensionality attribute to the proper one, which I think is the -> one?

[jcommelin]

I think there are also a lot of ext and ext_iff pairs in the library.

[digama0]

subtype.eq is different from the convention, but it's in core so 🤷‍♂️ .

[cipher1024]

I didn't think of it. I'll use .ext. Also, I like the idea of merging this with ext.

[semorrison]

While we're renaming things, how about we shorten the `@[extensionality]` tag to just `@[ext]`? This will then match the name of the tactic that uses these lemmas.

…

On Tue, Nov 5, 2019 at 2:37 AM Simon Hudon ***@***.***> wrote: I didn't think of it. I'll use .ext. Also, I like the idea of merging this with ext. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#1645?email_source=notifications&email_token=AADUWBGXF57GRU76JZ7K4BLQSA6RZA5CNFSM4JIPGAS2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEC7VL2Y#issuecomment-549410283>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AADUWBDOJDQ6STIJJTZFXETQSA6RZANCNFSM4JIPGASQ> .

[cipher1024]

I agree

[bryangingechen]

Would it make sense to let [extensionality] work as well, for backwards compatibility?

[cipher1024]

I don't think that's a good idea. The change is very easy to make and having a synonym for an attribute is going to be messy and ugly.

[robertylewis]

Looks good! Could you update the doc string for the ext attribute and its entry in tactics.md?

[robertylewis]

Looks good! I think there are two related tasks remaining: replacing manually defined ext lemmas with the attribute, and cleaning up naming issues. (We should uniformly use ext, ext_iff, eq, etc.) I'll make an issue for this, it's material for another PR.

[bryangingechen]

Looks like [skip ci] on the last commit message keeps mergify from doing its thing. Did a merge to get this rolling again.