Skip to main content
Proof Assistants Beta

Return to Question

added 6 characters in body
Source Link
Jon
Jon
  • 75
  • 5

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

Questions: Is there a way to tell Coq that weI 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.

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

Questions Is there a way to tell Coq that we 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 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.

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.

added 6 characters in body
Source Link
Jon
Jon
  • 75
  • 5

Questions Is there a way to tell Coq that we 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?

Questions Is there a way to tell Coq that we 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 to be definitional?

Questions Is there a way to tell Coq that we 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?

Source Link
Jon
Jon
  • 75
  • 5

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 for defining 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 we 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 to be definitional?