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

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

.)

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

Super, thanks! :+1:

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 `*`

)?

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.

Sometimes, people redefine `prod`

(`*`

) and maybe write it `×`

.

Last updated: Oct 03 2023 at 21:01 UTC