From 589effd34254f5082e522821de9af93e54cdaf86 Mon Sep 17 00:00:00 2001 From: msozeau Date: Thu, 4 Sep 2008 10:47:27 +0000 Subject: Improve typeclasses eauto using the dnet for local assumptions too, and select only relevant hypotheses in it, slightly cutting the search space. Makes setoid_rewrite less sensitive to the number of hypothesis (~ 5% time improvment on the stdlib). This currently prevents resolution with constants which reduce to classes, hence the modifications in Setoids.Setoid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11360 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Setoids/Setoid.v | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) (limited to 'theories/Setoids') 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. *) -- cgit v1.2.3