Plug the new setoid implemtation in, leaving the original one commented

out. The semantics of the old setoid are faithfully simulated by the new
tactic, hence no scripts involving rewrite are modified. However,
parametric morphism declarations need to be changed, but there are only a
few in the standard library, notably in FSets. The declaration and the
introduction of variables in the script need to be tweaked a bit,
otherwise the proofs remain unchanged. 
Some fragile scripts not introducting their variable names explicitely
were broken. Requiring Setoid requires Program.Basics which sets stronger
implicit arguments on some constants, a few scripts benefit from that.
Ring/field have been ported but do not really use the new typeclass
architecture as well as they could. Performance should be mostly
unchanged, but will certainly improve in the near future. Size of the
vo's seems not to have changed at all.
It will certainly break some contribs using Setoid.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10631 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 78 insertions, 51 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index bf2602180..da302ea9d 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -101,6 +101,31 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
   "using" "relation" constr(rel) "by" tactic(t) :=
   setoidreplacein (rel x y) id ltac:t.
+
+
+Ltac red_subst_eq_morphism concl :=
+  match concl with
+    | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R'
+    | ?R ==> ?R' => red ; intros ; red_subst_eq_morphism R'
+    | _ => idtac
+  end.
+
+Ltac destruct_morphism :=
+  match goal with
+    | [ |- @Morphism ?A ?R ?m ] => constructor
+  end.
+
+Ltac reverse_arrows x :=
+  match x with
+    | @Logic.eq ?A ==> ?R' => revert_last ; reverse_arrows R'
+    | ?R ==> ?R' => do 3 revert_last ; reverse_arrows R'
+    | _ => idtac
+  end.
+
+Ltac add_morphism_tactic := (try destruct_morphism) ;
+  match goal with
+    | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y)
+  end.
   
 Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
 Proof with auto.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 87111b1a7..78962fd1b 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -660,48 +660,50 @@ Add Relation key E.eq
  transitivity proved by E.eq_trans 
  as KeySetoid.
 
-Add Relation t Equal 
- reflexivity proved by Equal_refl
- symmetry proved by Equal_sym
- transitivity proved by Equal_trans
+Implicit Arguments Equal [[elt]].
+
+Add Relation (t elt) Equal  
+ reflexivity proved by (@Equal_refl elt)
+ symmetry proved by (@Equal_sym elt)
+ transitivity proved by (@Equal_trans elt)
  as EqualSetoid.
 
-Add Morphism In with signature E.eq ==> Equal ==> iff as In_m.
+Add Morphism (@In elt) with signature E.eq ==> Equal ==> iff as In_m.
 Proof.
-unfold Equal; intros elt k k' Hk m m' Hm.
+unfold Equal; intros k k' Hk m m' Hm.
 rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition.
 Qed.
 
-Add Morphism MapsTo 
- with signature E.eq ==> @Logic.eq ==> Equal ==> iff as MapsTo_m.
+Add Morphism (@MapsTo elt)
+ with signature E.eq ==> Logic.eq ==> Equal ==> iff as MapsTo_m.
 Proof.
-unfold Equal; intros elt k k' Hk e m m' Hm.
+unfold Equal; intros k k' Hk e m m' Hm.
 rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm; 
  intuition.
 Qed.
 
-Add Morphism Empty with signature Equal ==> iff as Empty_m.
+Add Morphism (@Empty elt) with signature Equal ==> iff as Empty_m.
 Proof.
-unfold Empty; intros elt m m' Hm; intuition.
+unfold Empty; intros m m' Hm; intuition.
 rewrite <-Hm in H0; eauto.
 rewrite Hm in H0; eauto.
 Qed.
 
-Add Morphism is_empty with signature Equal ==> @Logic.eq as is_empty_m.
+Add Morphism (@is_empty elt) with signature Equal ==> Logic.eq as is_empty_m.
 Proof.
-intros elt m m' Hm.
+intros m m' Hm.
 rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition.
 Qed.
 
-Add Morphism mem with signature E.eq ==> Equal ==> @Logic.eq as mem_m.
+Add Morphism (@mem elt) with signature E.eq ==> Equal ==> Logic.eq as mem_m.
 Proof.
-intros elt k k' Hk m m' Hm.
+intros k k' Hk m m' Hm.
 rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition.
 Qed.
 
-Add Morphism find with signature E.eq ==> Equal ==> @Logic.eq as find_m.
+Add Morphism (@find elt) with signature E.eq ==> Equal ==> Logic.eq as find_m.
 Proof.
-intros elt k k' Hk m m' Hm.
+intros k k' Hk m m' Hm.
 generalize (find_mapsto_iff m k)(find_mapsto_iff m' k')
  (not_find_in_iff m k)(not_find_in_iff m' k'); 
 do 2 destruct find; auto; intros.
@@ -710,27 +712,27 @@ rewrite <- H1, Hk, Hm, H2; auto.
 symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto.
 Qed.
 
-Add Morphism add with signature 
- E.eq ==> @Logic.eq ==> Equal ==> Equal as add_m.
+Add Morphism (@add elt) with signature 
+ E.eq ==> Logic.eq ==> Equal ==> Equal as add_m.
 Proof.
-intros elt k k' Hk e m m' Hm y.
+intros k k' Hk e m m' Hm y.
 rewrite add_o, add_o; do 2 destruct eq_dec; auto.
 elim n; rewrite <-Hk; auto.
 elim n; rewrite Hk; auto.
 Qed.
 
-Add Morphism remove with signature
+Add Morphism (@remove elt) with signature
  E.eq ==> Equal ==> Equal as remove_m.
 Proof.
-intros elt k k' Hk m m' Hm y.
+intros k k' Hk m m' Hm y.
 rewrite remove_o, remove_o; do 2 destruct eq_dec; auto.
 elim n; rewrite <-Hk; auto.
 elim n; rewrite Hk; auto.
 Qed.
 
-Add Morphism map with signature @Logic.eq ==> Equal ==> Equal as map_m.
+Add Morphism (@map elt elt') with signature Logic.eq ==> Equal ==> Equal as map_m.
 Proof.
-intros elt elt' f m m' Hm y.
+intros f m m' Hm y.
 rewrite map_o, map_o, Hm; auto.
 Qed.
 
@@ -1102,7 +1104,7 @@ Module WProperties (E:DecidableType)(M:WSfun E).
 
  End Elt.
 
- Add Morphism cardinal with signature Equal ==> @Logic.eq as cardinal_m.
+ Add Morphism (@cardinal elt) with signature Equal ==> Logic.eq as cardinal_m.
  Proof. intros; apply Equal_cardinal; auto. Qed.
 
 End WProperties.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 8ee74649e..b0c8ee008 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -339,7 +339,7 @@ exact (H1 (refl_equal true) _ Ha).
 Qed.
 
 Add Morphism Empty with signature Equal ==> iff as Empty_m.
-Proof. 
+Proof.
 intros; do 2 rewrite is_empty_iff; rewrite H; intuition.
 Qed.
 
@@ -429,13 +429,13 @@ Add Relation t Subset
    the two previous lemmas, in order to allow conversion of 
    SubsetSetoid coming from separate Facts modules. See bug #1738. *)
 
-Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m.
+Instance In_s_m : Morphism (E.eq ==> Subset ++> impl) In | 1.
 Proof.
-unfold Subset, impl; intros; eauto with set.
+  do 2 red ; intros. unfold Subset, impl; intros; eauto with set.
 Qed.
 
 Add Morphism Empty with signature Subset --> impl as Empty_s_m.
-Proof. 
+Proof.
 unfold Subset, Empty, impl; firstorder.
 Qed.
 
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 866c3f620..c2bba9283 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -125,7 +125,7 @@ Module Raw (X: DecidableType).
   Lemma In_eq :
     forall (s : t) (x y : elt), X.eq x y -> In x s -> In y s.
   Proof.
-  intros s x y; do 2 setoid_rewrite InA_alt; firstorder eauto.
+  intros s x y; setoid_rewrite InA_alt; firstorder eauto.
   Qed.
   Hint Immediate In_eq.
 
diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
index db09c2ec7..e885d25bc 100644
--- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v
+++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
@@ -143,7 +143,7 @@ Hypothesis A0 : A 0.
 Hypothesis AS : forall n : NZ, A n <-> A (S n). (* Below, we use only -> direction *)
 
 Add Morphism A with signature NZeq ==> iff as A_morph.
-Proof A_wd.
+Proof. apply A_wd. Qed.
 
 Let B (n : Z) := A (Z_to_NZ n).
 
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 730d8a00f..084560de3 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -64,7 +64,7 @@ something like this. The same goes for "relation". *)
 Hypothesis A_wd : predicate_wd NZeq A.
 
 Add Morphism A with signature NZeq ==> iff as A_morph.
-Proof A_wd.
+Proof. apply A_wd. Qed.
 
 Theorem NZcentral_induction :
   forall z : NZ, A z ->
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 0708e060a..bc3600f9c 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -396,7 +396,7 @@ Variable A : NZ -> Prop.
 Hypothesis A_wd : predicate_wd NZeq A.
 
 Add Morphism A with signature NZeq ==> iff as A_morph.
-Proof A_wd.
+Proof. apply A_wd. Qed.
 
 Section Center.
 
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 0a3d1a586..27d9c72bd 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -81,7 +81,7 @@ function (by recursion) that maps 0 to false and the successor to true *)
 Definition if_zero (A : Set) (a b : A) (n : N) : A :=
   recursion a (fun _ _ => b) n.
 
-Add Morphism if_zero with signature @eq ==> @eq ==> Neq ==> @eq as if_zero_wd.
+Add Morphism (if_zero A) with signature (eq ==> eq ==> Neq ==> eq) as if_zero_wd.
 Proof.
 intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
 reflexivity. unfold fun2_eq; now intros. assumption.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 9ddaa9a2f..7b4645be3 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -407,7 +407,7 @@ Variable R : N -> N -> Prop.
 Hypothesis R_wd : relation_wd Neq Neq R.
 
 Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2.
-Proof R_wd.
+Proof. apply R_wd. Qed.
 
 Theorem le_ind_rel :
    (forall m : N, R 0 m) ->
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index e66bc8ebf..c063c7bc1 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -148,15 +148,15 @@ intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2.
 now symmetry.
 Qed.
 
-Add Relation (fun A B : Type => A -> B -> Prop) relations_eq
-  reflexivity proved by (fun A B : Type => proj1 (relations_eq_equiv A B))
-  symmetry proved by (fun A B : Type => proj2 (proj2 (relations_eq_equiv A B)))
-  transitivity proved by (fun A B : Type => proj1 (proj2 (relations_eq_equiv A B)))
+Add Relation (A -> B -> Prop) (@relations_eq A B)
+  reflexivity proved by (proj1 (relations_eq_equiv A B))
+  symmetry proved by (proj2 (proj2 (relations_eq_equiv A B)))
+  transitivity proved by (proj1 (proj2 (relations_eq_equiv A B)))
 as relations_eq_rel.
 
-Add Morphism well_founded with signature relations_eq ==> iff as well_founded_wd.
+Add Morphism (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd.
 Proof.
-unfold relations_eq, well_founded; intros A R1 R2 H;
+unfold relations_eq, well_founded; intros R1 R2 H;
 split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor;
 intros y H4; apply H3; [now apply <- H | now apply -> H].
 Qed.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 5199333ed..cde670075 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -200,7 +200,7 @@ Proof.
   unfold Qeq, Qopp; simpl.
   Open Scope Z_scope.
   intros.
-  replace (- Qnum x1 * ' Qden x2) with (- (Qnum x1 * ' Qden x2)) by ring.
+  replace (- Qnum x * ' Qden y) with (- (Qnum x * ' Qden y)) by ring.
   rewrite H in |- *;  ring.
   Close Scope Z_scope.
 Qed.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 8d76b4f4e..61b70ba68 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -83,9 +83,9 @@ Variable leA : A -> A -> Prop.
 Variable leB : B -> B -> Prop.
 
 Inductive le_AsB : A + B -> A + B -> Prop :=
-  | le_aa : forall x y:A, leA x y -> le_AsB (inl B x) (inl B y)
-  | le_ab : forall (x:A) (y:B), le_AsB (inl B x) (inr A y)
-  | le_bb : forall x y:B, leB x y -> le_AsB (inr A x) (inr A y).
+  | le_aa : forall x y:A, leA x y -> le_AsB (inl x) (inl y)
+  | le_ab : forall (x:A) (y:B), le_AsB (inl x) (inr y)
+  | le_bb : forall x y:B, leB x y -> le_AsB (inr x) (inr y).
 
 End Disjoint_Union. 
 
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index f93a12955..34bff6354 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -10,8 +10,8 @@
 
 Set Implicit Arguments.
 
-Require Export Setoid_tac.
-Require Export Setoid_Prop.
+Require Export Coq.Classes.Equivalence.
+Require Export Coq.Relations.Relation_Definitions.
 
 (** For backward compatibility *)
 
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 026a305b1..2f8ef8d11 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Relations.
+Require Import Coq.Relations.Relations.
 Require Import List.
 Require Import Multiset.
 Require Import Arith.
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index f6ce84f98..a86d19c09 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -21,7 +21,7 @@ Section Wf_Disjoint_Union.
 
   Notation Le_AsB := (le_AsB A B leA leB).
   
-  Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x).
+  Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl x).
   Proof.
     induction 1.
     apply Acc_intro; intros y H2.
@@ -30,7 +30,7 @@ Section Wf_Disjoint_Union.
   Qed.
 
   Lemma acc_B_sum :
-    well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x).
+    well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr x).
   Proof.
     induction 2.
     apply Acc_intro; intros y H3.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index de3b76e95..ff8033eeb 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -931,7 +931,7 @@ Module EqualityModulo (M:SomeNumber).
 
  Add Morphism Zopp : Zopp_eqm.
  Proof.
-  intros; change (-x1 == -x2) with (0-x1 == 0-x2).
+  intros; change (-x == -y) with (0-x == 0-y).
   rewrite H; red; auto.
  Qed.