## Stream: general

### Topic: eta law for structures

#### 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)?

#### 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

#### 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

#### Reid Barton (May 29 2020 at 18:26):

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

#### Reid Barton (May 29 2020 at 18:26):

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

#### 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

#### 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)

#### 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)

#### 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.

#### 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