diff options
Diffstat (limited to 'theories/Setoids/Setoid.v')
| -rw-r--r-- | theories/Setoids/Setoid.v | 61 |
1 files changed, 38 insertions, 23 deletions
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index d6975e91..e7fe82b2 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -6,38 +6,53 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Setoid.v 10765 2008-04-08 16:15:23Z msozeau $: i*) +(*i $Id: Setoid.v 11720 2008-12-28 07:12:15Z letouzey $: i*) 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. -(** Some tactics for manipulating Setoid Theory not officially - declared as Setoid. *) +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. -Ltac trans_st x := match goal with - | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => - apply (Seq_trans _ _ H) with x; auto - end. +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. -Ltac sym_st := match goal with - | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => - apply (Seq_sym _ _ H); auto - end. +(** Some tactics for manipulating Setoid Theory not officially + declared as Setoid. *) -Ltac refl_st := match goal with - | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => - apply (Seq_refl _ _ H); auto - end. +Ltac trans_st x := + idtac "trans_st on Setoid_Theory is OBSOLETE"; + idtac "use transitivity on Equivalence instead"; + match goal with + | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => + apply (Seq_trans _ _ H) with x; auto + end. + +Ltac sym_st := + idtac "sym_st on Setoid_Theory is OBSOLETE"; + idtac "use symmetry on Equivalence instead"; + match goal with + | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => + apply (Seq_sym _ _ H); auto + end. + +Ltac refl_st := + idtac "refl_st on Setoid_Theory is OBSOLETE"; + idtac "use reflexivity on Equivalence instead"; + match goal with + | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => + apply (Seq_refl _ _ H); auto + end. Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A). Proof. |