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: Oct 03 2023 at 21:01 UTC