Zulip Chat Archive

Stream: general

Topic: eta law for structures


view this post on Zulip Jannis Limperg (May 29 2020 at 15:52):

Given a structure

structure S : Type :=
(x : X)
(y : Y)
...

we have the eta law for S:

lemma S.eta (s : S) : s = s.x, s.y, ...⟩

Does Lean already provide this anywhere (generically, for any structure)?

view this post on Zulip Kevin Buzzard (May 29 2020 at 17:19):

I doubt it, because for structures like the complex numbers it is proved explicitly very early on

view this post on Zulip Simon Hudon (May 29 2020 at 18:10):

It shouldn't be too hard to automate. Already, we have ext laws for structures and simps laws as well. You can prove an eta rule by cases s and then you apply the automatically generated ext rule

view this post on Zulip Reid Barton (May 29 2020 at 18:26):

If you use cases s then it will already be true by rfl.

view this post on Zulip Reid Barton (May 29 2020 at 18:26):

Do we really have a way to autogenerate ext lemmas? I missed that!

view this post on Zulip Simon Hudon (May 29 2020 at 18:32):

Yes, it's the same attribute. You tag your structure with ext and you get two ext lemmas: one implication and one logical equivalence

view this post on Zulip Simon Hudon (May 29 2020 at 18:32):

(I had to look up the doc string to make sure I didn't imagine that the change happened)

view this post on Zulip Simon Hudon (May 29 2020 at 18:33):

(and git blame tells me that I was the one to implement it. I keep forgetting :P)

view this post on Zulip Scott Morrison (May 30 2020 at 03:23):

I wonder if the @[ext] annotation should just at the eta lemma while it's at it.

view this post on Zulip Simon Hudon (May 30 2020 at 03:26):

That would be a good idea. Would could also make the structure and inductive keywords extendible so that we can specify parts of the inductive compiler. This way, every structure would get ext and eta lemmas without us having to annotate them.


Last updated: May 11 2021 at 13:22 UTC