# Eta-equality for records: the case of semigroups

Consider the following definition of a semigroup:

Set Primitive Projections.

Record SG (A : Type) : Type := {
oper: A -> A -> A;
assoc :     forall x y z, oper x (oper y z) = oper (oper x y) z;
assoc_sym : forall x y z, oper (oper z y) x = oper z (oper y x)
}.


The field assoc_sym may appear useless because it is a trivial consequence of the field assoc. But it allows to define the opposite semigroup in such a way that opposite (opposite sg) and sg are definitionally equal.

Definition opposite [A : Type] (sg : SG A) : SG A := {|
oper := fun x y => oper A sg y x;
assoc := fun x y z => assoc_sym A sg x y z;
assoc_sym := fun x y z => assoc A sg x y z
|}.

Lemma involutive : forall A (sg : SG A), opposite (opposite sg) = sg.
Proof. reflexivity. Qed.


However in definitions of semigroups other than the opposite we would like Coq to automatically fill the field assoc_sym because we do not care about the chosen proof term. This can be done by providing a generic proof term for assoc_sym in the definition of SG:

Record SG (A : Type) : Type := {
oper: A -> A -> A;
assoc :     forall x y z, oper (oper x y) z = oper x (oper y z);
assoc_sym : forall x y z, oper z (oper y x) = oper (oper z y) x :=
fun x y z => eq_sym (assoc z y x)
}.


Then we can define the following semigroup without having to fill the assoc_sym field:

Definition trv : SG nat := {|
oper := fun x y => x + y;
|}.


Unfortunately, the generic proof term in SG makes the involutive equality not definitional and Coq does not allow the user to give an explicit proof term for assoc_sym because we have provided a generic one in SG:

Definition opposite [A : Type] (sg : SG A) : SG A := {|
oper := fun x y => oper A sg y x;
assoc := fun x y z => assoc_sym A sg x y z
|}.

Lemma involutive : forall A (sg : SG A), opposite (opposite sg) = sg.
Proof. Fail reflexivity. Abort.


Questions: Is there a way to tell Coq that I do not want to use the generic proof term in the definition of opposite? If this feature is not available, is there a generic proof term that would allow the involutive equality proof to be definitional?

The first thing I tried was to redefine eq_sym because it is opaque in the standard library.

Definition eq_sym [A : Type] [x y : A] (p : x = y) : y = x :=
match p in (_ = y) return (y = x) with eq_refl => eq_refl end.


But it does not help.

One approach is to do things the other way around: define SG with all the fields, without any one of them being defined. Then define an interface that will automatically fill in the fields that can be defined.

Require Import Nat Arith.

Set Primitive Projections.

Record SG (A : Type) : Type := {
oper: A -> A -> A;
assoc :     forall x y z, oper x (oper y z) = oper (oper x y) z;
assoc_sym : forall x y z, oper (oper z y) x = oper z (oper y x)
}.

Definition opposite [A : Type] (sg : SG A) : SG A := {|
oper := fun x y => oper A sg y x;
assoc := fun x y z => assoc_sym A sg x y z;
assoc_sym := fun x y z => assoc A sg x y z
|}.

Lemma involutive : forall A (sg : SG A), opposite (opposite sg) = sg.
Proof. reflexivity. Qed.

Definition SG_builder
{A : Type}
(oper : A -> A -> A)
(assoc : forall x y z, oper x (oper y z) = oper (oper x y) z) :
SG A.
Proof.
econstructor.
- eassumption.
- now symmetry.
Defined.

Definition trv : SG nat := SG_builder
(fun x y => x + y)

• Indeed, although I would argue that you do not define new instances of algebraic structures all that often so it is not too bad. A possibility if you really want to regain the notation is to define a structure pre_SG with only the oper and assoc fields, and have SG_builder {A : Type} (g : pre_SG A) : SG A. Oct 3, 2023 at 8:07