eta law for structures

Stream: general

[Jannis Limperg]

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]

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

[Simon Hudon]

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]

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

[Reid Barton]

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

[Simon Hudon]

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]

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

[Simon Hudon]

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

[Scott Morrison]

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

[Simon Hudon]

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.