## Stream: Coq users

### Topic: η for records

#### James Wood (Feb 24 2022 at 14:01):

Why does the following proof fail? In particular, I think it should succeed even without type-directed normalisation, because `swap z` is always a record expression, and this should trigger η-expansion of `xy`. Note that I really care about the equation holding judgementally.

``````Record times {A B : Type} : Type := {
prl : A;
prr : B;
}.
Arguments times A B : clear implicits.

Definition swap {A B} (xy : times A B) : times B A := {|
prl := xy.(prr);
prr := xy.(prl);
|}.

Fail Definition swap_involutive {A B} (xy : times A B) : swap (swap xy) = xy := eq_refl.
``````

#### James Wood (Feb 24 2022 at 14:04):

(Just for sanity, the error message is indeed `cannot unify "swap (swap xy)" and "xy"`.)

#### Théo Winterhalter (Feb 24 2022 at 14:10):

Eta for records isn't activated by default.

``````Set Primitive Projections.

Record times {A B : Type} : Type := {
prl : A;
prr : B;
}.
Arguments times A B : clear implicits.

Definition swap {A B} (xy : times A B) : times B A := {|
prl := xy.(prr);
prr := xy.(prl);
|}.

Definition swap_involutive {A B} (xy : times A B) : swap (swap xy) = xy.
Proof.
reflexivity.
Qed.
``````

#### James Wood (Feb 24 2022 at 14:14):

Super, thanks! :+1:

#### James Wood (Feb 24 2022 at 14:16):

Am I right in thinking that I need to define my own products to get η-laws (i.e, I won't get the same with the default `*`)?

#### Théo Winterhalter (Feb 24 2022 at 14:17):

You're correct. The option only applies to definitions made afterwards. There is no way to turn an old record into a record with primitive projections sadly.

#### Théo Winterhalter (Feb 24 2022 at 14:18):

Sometimes, people redefine `prod` (`*`) and maybe write it `×`.

Last updated: Jun 18 2024 at 09:02 UTC