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;
assoc := Nat.add_assoc
|}.
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.
