diff options
Diffstat (limited to 'theories/Setoids')
| -rw-r--r-- | theories/Setoids/Setoid.v | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 8f59c048f..28d8feeae 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -12,14 +12,20 @@ Require Export Coq.Classes.SetoidTactics. (** For backward compatibility *) -Definition Setoid_Theory := @Equivalence. -Definition Build_Setoid_Theory := @Build_Equivalence. -Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x := - Eval compute in reflexivity. -Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x := - Eval compute in symmetry. -Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z := - Eval compute in transitivity. +Definition Setoid_Theory := @Equivalence. +Definition Build_Setoid_Theory := @Build_Equivalence. + +Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x. + unfold Setoid_Theory. intros ; reflexivity. +Defined. + +Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x. + unfold Setoid_Theory. intros ; symmetry ; assumption. +Defined. + +Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z. + unfold Setoid_Theory. intros ; transitivity y ; assumption. +Defined. (** Some tactics for manipulating Setoid Theory not officially declared as Setoid. *) |