Merge SetoidList2 into SetoidList.

This file contains low-level stuff for FSets/FMaps. Switching it to
the new version (the one using Equivalence and so on instead of
eq_refl/eq_sym/eq_trans and so on) only leads to a few changes in
FSets/FMaps that are minor and probably invisible to standard users.

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

9 files changed, 136 insertions, 152 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index c457a83c4..c6252de9c 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1325,7 +1325,7 @@ Proof.
  apply Hl; auto.
  constructor.
  apply Hr; eauto.
- apply (InA_InfA (PX.eqke_refl (elt:=elt))); intros (y',e') H6.
+ apply InA_InfA with (eqA:=eqke); auto with *. intros (y',e') H6.
  destruct (elements_aux_mapsto r acc y' e'); intuition.
  red; simpl; eauto.
  red; simpl; eauto.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 5565c048c..1d4bb8f11 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -571,7 +571,7 @@ Qed.
 (** First, [Equal] is [Equiv] with Leibniz on elements. *)
 
 Lemma Equal_Equiv : forall (m m' : t elt),
-  Equal m m' <-> Equiv (@Logic.eq elt) m m'.
+  Equal m m' <-> Equiv Logic.eq m m'.
 Proof.
 intros. rewrite Equal_mapsto_iff. split; intros.
 split.
@@ -760,6 +760,16 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Notation eqke := (@eq_key_elt elt).
   Notation eqk := (@eq_key elt).
 
+  Instance eqk_equiv : Equivalence eqk.
+  Proof. split; repeat red; eauto. Qed.
+
+  Instance eqke_equiv : Equivalence eqke.
+  Proof.
+   unfold eq_key_elt; split; repeat red; firstorder.
+   eauto with *.
+   congruence.
+  Qed.
+
   (** Complements about InA, NoDupA and findA *)
 
   Lemma InA_eqke_eqk : forall k1 k2 e1 e2 l,
@@ -787,12 +797,12 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   intros. symmetry.
   unfold eqb.
   rewrite <- findA_NoDupA, InA_rev, findA_NoDupA
-   by eauto using NoDupA_rev; eauto.
+   by (eauto using NoDupA_rev with *); eauto.
   case_eq (findA (eqb k) (rev l)); auto.
   intros e.
   unfold eqb.
   rewrite <- findA_NoDupA, InA_rev, findA_NoDupA
-   by eauto using NoDupA_rev.
+   by (eauto using NoDupA_rev with *).
   intro Eq; rewrite Eq; auto.
   Qed.
 
@@ -893,9 +903,9 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   assert (Hstep' : forall k e a m' m'', InA eqke (k,e) l -> ~In k m' ->
              Add k e m' m'' -> P m' a -> P m'' (F (k,e) a)).
    intros k e a m' m'' H ? ? ?; eapply Hstep; eauto.
-   revert H; unfold l; rewrite InA_rev, elements_mapsto_iff; auto.
+   revert H; unfold l; rewrite InA_rev, elements_mapsto_iff; auto with *.
   assert (Hdup : NoDupA eqk l).
-   unfold l. apply NoDupA_rev; try red; unfold eq_key ; eauto.
+   unfold l. apply NoDupA_rev; try red; unfold eq_key ; eauto with *.
    apply elements_3w.
   assert (Hsame : forall k, find k m = findA (eqb k) l).
    intros k. unfold l. rewrite elements_o, findA_rev; auto.
@@ -977,7 +987,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   set (l:=rev (elements m)).
   assert (Rstep' : forall k e a b, InA eqke (k,e) l ->
     R a b -> R (f k e a) (g k e b)) by
-    (intros; apply Rstep; auto; rewrite elements_mapsto_iff, <- InA_rev; auto).
+    (intros; apply Rstep; auto; rewrite elements_mapsto_iff, <- InA_rev; auto with *).
   clearbody l; clear Rstep m.
   induction l; simpl; auto.
   apply Rstep'; auto.
@@ -1087,66 +1097,49 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Lemma fold_Equal : forall m1 m2 i, Equal m1 m2 ->
    eqA (fold f m1 i) (fold f m2 i).
   Proof.
-  assert (eqke_refl : forall p, eqke p p).
-   red; auto.
-  assert (eqke_sym : forall p p', eqke p p' -> eqke p' p).
-   intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition.
-  assert (eqke_trans : forall p p' p'', eqke p p' -> eqke p' p'' -> eqke p p'').
-   intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl.
-   intuition; eauto; congruence.
   intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
   apply fold_right_equivlistA_restr with
-    (R:=fun p p' => ~eqk p p') (eqA:=eqke) (eqB:=eqA); auto.
-  intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; simpl in *; apply Comp; auto.
-  unfold eq_key; auto.
-  intros (k1,e1) (k2,e2) (k3,e3). unfold eq_key_elt, eq_key; simpl.
-   intuition eauto.
+    (R:=fun p p' => ~eqk p p') (eqA:=eqke) (eqB:=eqA); auto with *.
+  intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto.
+  unfold eq_key, eq_key_elt; repeat red. intuition eauto.
   intros (k,e) (k',e'); unfold eq_key; simpl; auto.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply ForallList2_equiv1 with (eqA:=eqk); try red ; unfold eq_key ; eauto.
-  apply NoDupA_rev; try red ; unfold eq_key; eauto. apply elements_3w.
+  apply NoDupA_rev; auto with *; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply NoDupA_rev; auto with *; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply ForallL2_equiv1 with (eqA:=eqk); try red ; unfold eq_key ; eauto with *.
+  apply NoDupA_rev; try red ; unfold eq_key; eauto with *. apply elements_3w.
   red; intros.
-  do 2 rewrite InA_rev.
-  destruct x; do 2 rewrite <- elements_mapsto_iff.
-  do 2 rewrite find_mapsto_iff.
-  rewrite H; split; auto.
+  rewrite 2 InA_rev by auto with *.
+  destruct x; rewrite <- 2 elements_mapsto_iff by auto with *.
+  rewrite 2 find_mapsto_iff by auto with *.
+  rewrite H. split; auto.
   Qed.
 
   Lemma fold_Add : forall m1 m2 k e i, ~In k m1 -> Add k e m1 m2 ->
    eqA (fold f m2 i) (f k e (fold f m1 i)).
   Proof.
-  assert (eqke_refl : forall p, eqke p p).
-   red; auto.
-  assert (eqke_sym : forall p p', eqke p p' -> eqke p' p).
-   intros (x1,x2) (y1,y2); unfold eq_key_elt; simpl; intuition.
-  assert (eqke_trans : forall p p' p'', eqke p p' -> eqke p' p'' -> eqke p p'').
-   intros (x1,x2) (y1,y2) (z1,z2); unfold eq_key_elt; simpl.
-   intuition; eauto; congruence.
   intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
   set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
   change (f k e (fold_right f' i (rev (elements m1))))
    with (f' (k,e) (fold_right f' i (rev (elements m1)))).
   apply fold_right_add_restr with
-    (R:=fun p p'=>~eqk p p')(eqA:=eqke)(eqB:=eqA); auto.
-  intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *. apply Comp; auto.
+    (R:=fun p p'=>~eqk p p')(eqA:=eqke)(eqB:=eqA); auto with *.
+  intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. apply Comp; auto.
 
-  unfold eq_key; auto.
-  intros (k1,e1) (k2,e2) (k3,e3). unfold eq_key_elt, eq_key; simpl.
-   intuition eauto.
+  unfold eq_key_elt, eq_key; repeat red; intuition eauto.
   unfold f'; intros (k1,e1) (k2,e2); unfold eq_key; simpl; auto.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
-  apply ForallList2_equiv1 with (eqA:=eqk); try red; unfold eq_key ; eauto.
-  apply NoDupA_rev; try red; eauto. apply elements_3w.
-  rewrite InA_rev.
+  apply NoDupA_rev; auto with *; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply NoDupA_rev; auto with *; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply ForallL2_equiv1 with (eqA:=eqk); try red; unfold eq_key ; eauto with *.
+  apply NoDupA_rev; try red; eauto with *. apply elements_3w.
+  rewrite InA_rev; auto with *.
   contradict H.
   exists e.
   rewrite elements_mapsto_iff; auto.
   intros a.
-  rewrite InA_cons; do 2 rewrite InA_rev;
-  destruct a as (a,b); do 2 rewrite <- elements_mapsto_iff.
-  do 2 rewrite find_mapsto_iff; unfold eq_key_elt; simpl.
+  destruct a as (a,b).
+  rewrite InA_cons, 2 InA_rev, <- 2 elements_mapsto_iff,
+   2 find_mapsto_iff by (auto with *).
+  unfold eq_key_elt; simpl.
   rewrite H0.
   rewrite add_o.
   destruct (eq_dec k a); intuition.
@@ -1545,9 +1538,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   set (f:=fun (_:key)(_:elt)=>S).
   setoid_replace (fold f m 0) with (fold f m1 (fold f m2 0)).
   rewrite <- cardinal_fold.
-  intros. apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto.
-  apply Partition_fold with (eqA:=eq); try red; auto.
-  compute; auto.
+  apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto.
+  apply Partition_fold with (eqA:=eq); repeat red; auto.
   Qed.
 
   Lemma Partition_partition : forall m m1 m2, Partition m m1 m2 ->
@@ -1777,8 +1769,7 @@ Module OrdProperties (M:S).
   Lemma sort_equivlistA_eqlistA : forall l l' : list (key*elt),
    sort ltk l -> sort ltk l' -> equivlistA eqke l l' -> eqlistA eqke l l'.
   Proof.
-  apply SortA_equivlistA_eqlistA; eauto;
-  unfold O.eqke, O.ltk; simpl; intuition; eauto.
+  apply SortA_equivlistA_eqlistA; eauto with *.
   Qed.
 
   Ltac clean_eauto := unfold O.eqke, O.ltk; simpl; intuition; eauto.
@@ -1802,7 +1793,7 @@ Module OrdProperties (M:S).
    destruct (E.compare x y); intuition; try discriminate; ME.order.
   Qed.
 
-  Lemma gtb_compat : forall p, compat_bool eqke (gtb p).
+  Lemma gtb_compat : forall p, Proper (eqke==>eq) (gtb p).
   Proof.
    red; intros (x,e) (a,e') (b,e'') H; red in H; simpl in *; destruct H.
    generalize (gtb_1 (x,e) (a,e'))(gtb_1 (x,e) (b,e''));
@@ -1817,7 +1808,7 @@ Module OrdProperties (M:S).
    rewrite <- H2; auto.
   Qed.
 
-  Lemma leb_compat : forall p, compat_bool eqke (leb p).
+  Lemma leb_compat : forall p, Proper (eqke==>eq) (leb p).
   Proof.
    red; intros x a b H.
    unfold leb; f_equal; apply gtb_compat; auto.
@@ -1829,7 +1820,7 @@ Module OrdProperties (M:S).
     elements m = elements_lt p m ++ elements_ge p m.
   Proof.
   unfold elements_lt, elements_ge, leb; intros.
-  apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto with map.
+  apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto with *.
   intros; destruct x; destruct y; destruct p.
   rewrite gtb_1 in H; unfold O.ltk in H; simpl in *.
   assert (~ltk (t1,e0) (k,e1)).
@@ -1843,14 +1834,14 @@ Module OrdProperties (M:S).
                  (elements_lt (x,e) m ++ (x,e):: elements_ge (x,e) m).
   Proof.
   intros; unfold elements_lt, elements_ge.
-  apply sort_equivlistA_eqlistA; auto with map.
-  apply (@SortA_app _ eqke); auto with map.
-  apply (@filter_sort _ eqke); auto with map; clean_eauto.
+  apply sort_equivlistA_eqlistA; auto with *.
+  apply (@SortA_app _ eqke); auto with *.
+  apply (@filter_sort _ eqke); auto with *; clean_eauto.
   constructor; auto with map.
-  apply (@filter_sort _ eqke); auto with map; clean_eauto.
-  rewrite (@InfA_alt _ eqke); auto with map; try (clean_eauto; fail).
+  apply (@filter_sort _ eqke); auto with *; clean_eauto.
+  rewrite (@InfA_alt _ eqke); auto with *; try (clean_eauto; fail).
   intros.
-  rewrite filter_InA in H1; auto with map; destruct H1.
+  rewrite filter_InA in H1; auto with *; destruct H1.
   rewrite leb_1 in H2.
   destruct y; unfold O.ltk in *; simpl in *.
   rewrite <- elements_mapsto_iff in H1.
@@ -1858,24 +1849,22 @@ Module OrdProperties (M:S).
    contradict H.
    exists e0; apply MapsTo_1 with t0; auto.
   ME.order.
-  apply (@filter_sort _ eqke); auto with map; clean_eauto.
+  apply (@filter_sort _ eqke); auto with *; clean_eauto.
   intros.
-  rewrite filter_InA in H1; auto with map; destruct H1.
+  rewrite filter_InA in H1; auto with *; destruct H1.
   rewrite gtb_1 in H3.
   destruct y; destruct x0; unfold O.ltk in *; simpl in *.
   inversion_clear H2.
   red in H4; simpl in *; destruct H4.
   ME.order.
-  rewrite filter_InA in H4; auto with map; destruct H4.
+  rewrite filter_InA in H4; auto with *; destruct H4.
   rewrite leb_1 in H4.
   unfold O.ltk in *; simpl in *; ME.order.
   red; intros a; destruct a.
-  rewrite InA_app_iff; rewrite InA_cons.
-  do 2 (rewrite filter_InA; auto with map).
-  do 2 rewrite <- elements_mapsto_iff.
-  rewrite leb_1; rewrite gtb_1.
-  rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
-  rewrite add_mapsto_iff.
+  rewrite InA_app_iff, InA_cons, 2 filter_InA,
+    <-2 elements_mapsto_iff, leb_1, gtb_1,
+    find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
+    add_mapsto_iff by (auto with *).
   unfold O.eqke, O.ltk; simpl.
   destruct (E.compare t0 x); intuition.
   right; split; auto; ME.order.
@@ -1892,8 +1881,8 @@ Module OrdProperties (M:S).
      eqlistA eqke (elements m') (elements m ++ (x,e)::nil).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto with map.
-  apply (@SortA_app _ eqke); auto with map.
+  apply sort_equivlistA_eqlistA; auto with *.
+  apply (@SortA_app _ eqke); auto with *.
   intros.
   inversion_clear H2.
   destruct x0; destruct y.
@@ -1903,11 +1892,10 @@ Module OrdProperties (M:S).
   apply H; firstorder.
   inversion H3.
   red; intros a; destruct a.
-  rewrite InA_app_iff; rewrite InA_cons; rewrite InA_nil.
-  do 2 rewrite <- elements_mapsto_iff.
-  rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
-  rewrite add_mapsto_iff; unfold O.eqke; simpl.
-  intuition.
+  rewrite InA_app_iff, InA_cons, InA_nil, <- 2 elements_mapsto_iff,
+   find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
+   add_mapsto_iff by (auto with *).
+  unfold O.eqke; simpl. intuition.
   destruct (E.eq_dec x t0); auto.
   exfalso.
   assert (In t0 m).
@@ -1921,9 +1909,9 @@ Module OrdProperties (M:S).
      eqlistA eqke (elements m') ((x,e)::elements m).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto with map.
+  apply sort_equivlistA_eqlistA; auto with *.
   change (sort ltk (((x,e)::nil) ++ elements m)).
-  apply (@SortA_app _ eqke); auto with map.
+  apply (@SortA_app _ eqke); auto with *.
   intros.
   inversion_clear H1.
   destruct y; destruct x0.
@@ -1933,11 +1921,10 @@ Module OrdProperties (M:S).
   apply H; firstorder.
   inversion H3.
   red; intros a; destruct a.
-  rewrite InA_cons.
-  do 2 rewrite <- elements_mapsto_iff.
-  rewrite find_mapsto_iff; rewrite (H0 t0); rewrite <- find_mapsto_iff.
-  rewrite add_mapsto_iff; unfold O.eqke; simpl.
-  intuition.
+  rewrite InA_cons, <- 2 elements_mapsto_iff,
+    find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
+    add_mapsto_iff by (auto with *).
+  unfold O.eqke; simpl. intuition.
   destruct (E.eq_dec x t0); auto.
   exfalso.
   assert (In t0 m).
@@ -1950,7 +1937,7 @@ Module OrdProperties (M:S).
    Equal m m' -> eqlistA eqke (elements m) (elements m').
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto with map.
+  apply sort_equivlistA_eqlistA; auto with *.
   red; intros.
   destruct x; do 2 rewrite <- elements_mapsto_iff.
   do 2 rewrite find_mapsto_iff; rewrite H; split; auto.
@@ -2052,11 +2039,8 @@ Module OrdProperties (M:S).
   inversion_clear H1.
   red in H2; destruct H2; simpl in *; ME.order.
   inversion_clear H4.
-  rewrite (@InfA_alt _ eqke) in H3; eauto.
+  rewrite (@InfA_alt _ eqke) in H3; eauto with *.
   apply (H3 (y,x0)); auto.
-  unfold lt_key; simpl; intuition; eauto.
-  intros (x1,x2) (y1,y2) (z1,z2); compute; intuition; eauto.
-  intros (x1,x2) (y1,y2) (z1,z2); compute; intuition; eauto.
   Qed.
 
   Lemma min_elt_MapsTo :
@@ -2156,7 +2140,7 @@ Module OrdProperties (M:S).
   do 2 rewrite fold_1.
   do 2 rewrite <- fold_left_rev_right.
   apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
-  intros (k,e) (k',e') a a' (Hk,He) Ha; simpl in *; apply Hf; auto.
+  intros (k,e) (k',e') (Hk,He) a a' Ha; simpl in *; apply Hf; auto.
   apply eqlistA_rev. apply elements_Equal_eqlistA. auto.
   Qed.
 
@@ -2169,7 +2153,7 @@ Module OrdProperties (M:S).
   set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
   transitivity (fold_right f' i (rev (elements m1 ++ (x,e)::nil))).
   apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
-  intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *. apply P; auto.
+  intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *. apply P; auto.
   apply eqlistA_rev.
   apply elements_Add_Above; auto.
   rewrite distr_rev; simpl.
@@ -2185,7 +2169,7 @@ Module OrdProperties (M:S).
   set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
   transitivity (fold_right f' i (rev (((x,e)::nil)++elements m1))).
   apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
-  intros (k1,e1) (k2,e2) a1 a2 (Hk,He) Ha; unfold f'; simpl in *; apply P; auto.
+  intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *; apply P; auto.
   apply eqlistA_rev.
   simpl; apply elements_Add_Below; auto.
   rewrite distr_rev; simpl.
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index da5b35874..f5ee8b23f 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -584,6 +584,10 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p').
 
+  Global Instance eqk_equiv : Equivalence eq_key.
+  Global Instance eqke_equiv : Equivalence eq_key_elt.
+  Global Instance ltk_strorder : StrictOrder lt_key.
+
   Lemma mem_find :
     forall m x, mem x m = match find x m with None => false | _ => true end.
   Proof.
@@ -764,8 +768,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   simpl; auto.
   destruct o; simpl; intros.
   (* Some *)
-  apply (SortA_app (eqA:=eq_key_elt)); auto.
-  compute; intuition.
+  apply (SortA_app (eqA:=eq_key_elt)); auto with *.
   constructor; auto.
   apply In_InfA; intros.
   destruct y0.
@@ -784,8 +787,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   eapply xelements_bits_lt_1; eauto.
   eapply xelements_bits_lt_2; eauto.
   (* None *)
-  apply (SortA_app (eqA:=eq_key_elt)); auto.
-  compute; intuition.
+  apply (SortA_app (eqA:=eq_key_elt)); auto with *.
   intros x0 y0.
   do 2 rewrite InA_alt.
   intros (y1,(Hy1,H)) (y2,(Hy2,H0)).
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 36964ad01..08071ec56 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -1698,9 +1698,9 @@ Lemma L_eq_cons :
 Proof.
  unfold L.eq, L.Equal in |- *; intuition.
  inversion_clear H1; generalize (H0 a); clear H0; intuition.
- apply InA_eqA with x; eauto.
+ apply InA_eqA with x; eauto with *.
  inversion_clear H1; generalize (H0 a); clear H0; intuition.
- apply InA_eqA with y; eauto.
+ apply InA_eqA with y; eauto with *.
 Qed.
 Hint Resolve L_eq_cons.
 
@@ -2000,7 +2000,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  rewrite partition_in_2, filter_in; intuition.
  rewrite H2; auto.
  destruct (f a); auto.
- red; intros; f_equal.
+ repeat red; intros; f_equal.
  rewrite (H _ _ H0); auto.
  Qed.
 
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 796db9f8f..1b1bae352 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -133,7 +133,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
    forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}),
    compat_P E.eq P -> compat_bool E.eq (fdec Pdec).
   Proof.
-    unfold compat_P, compat_bool, fdec in |- *; intros.
+    unfold compat_P, compat_bool, Proper, respectful, fdec in |- *; intros.
     generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder.
   Qed.
 
@@ -217,7 +217,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
     intros s1 s2; simpl in |- *.
     intros; assert (compat_bool E.eq (fdec Pdec)); auto.
     intros; assert (compat_bool E.eq (fun x => negb (fdec Pdec x))).
-    generalize H2; unfold compat_bool in |- *; intuition;
+    generalize H2; unfold compat_bool, Proper, respectful in |- *; intuition;
      apply (f_equal negb); auto.
     intuition.
     generalize H4; unfold For_all, Equal in |- *; intuition.
@@ -662,7 +662,8 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
    forall f : elt -> bool,
    compat_bool E.eq f -> compat_P E.eq (fun x => f x = true).
   Proof.
-     unfold compat_bool, compat_P in |- *; intros; rewrite <- H1; firstorder.
+     unfold compat_bool, compat_P, Proper, respectful, impl; intros;
+      rewrite <- H1; firstorder.
   Qed.
 
   Hint Resolve compat_P_aux.
@@ -768,7 +769,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
     intro p; case p; clear p; intros s1 s2 H C.
     generalize (H (compat_P_aux C)); clear H; intro H.
     assert (D : compat_bool E.eq (fun x => negb (f x))).
-    generalize C; unfold compat_bool in |- *; intros; apply (f_equal negb);
+    generalize C; unfold compat_bool, Proper, respectful; intros; apply (f_equal negb);
      auto.
     simpl in |- *; unfold Equal in |- *; intuition.
     apply filter_3; firstorder.
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index c95aa8025..ec0c6a559 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -592,11 +592,11 @@ Section Bool.
 (** Properties of [filter] *)
 
 Variable f:elt->bool.
-Variable Comp: compat_bool E.eq f.
+Variable Comp: Proper (E.eq==>Logic.eq) f.
 
-Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
+Let Comp' : Proper (E.eq==>Logic.eq) (fun x =>negb (f x)).
 Proof.
-unfold compat_bool in *; intros; f_equal; auto.
+repeat red; intros; f_equal; auto.
 Qed.
 
 Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.
@@ -695,7 +695,7 @@ Proof.
 clear Comp' Comp f.
 intros.
 assert (compat_bool E.eq (fun x => orb (f x) (g x))).
-  unfold compat_bool; intros.
+  unfold compat_bool, Proper, respectful; intros.
   rewrite (H x y H1);  rewrite (H0 x y H1); auto.
 unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto.
 assert (f a || g a = true <-> f a = true \/ g a = true).
@@ -785,7 +785,7 @@ Variable Comp: compat_bool E.eq f.
 
 Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
 Proof.
-unfold compat_bool in *; intros; f_equal; auto.
+unfold compat_bool, Proper, respectful in *; intros; f_equal; auto.
 Qed.
 
 Lemma exists_mem_1:
@@ -841,16 +841,16 @@ Notation compat_opL := (compat_op E.eq Logic.eq).
 Notation transposeL := (transpose Logic.eq).
 
 Lemma sum_plus :
-  forall f g, compat_nat E.eq f -> compat_nat E.eq g ->
+  forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
     forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.
 Proof.
 unfold sum.
 intros f g Hf Hg.
-assert (fc : compat_opL (fun x:elt =>plus (f x))).  auto.
+assert (fc : compat_opL (fun x:elt =>plus (f x))).  red; auto.
 assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega.
-assert (gc : compat_opL (fun x:elt => plus (g x))). auto.
+assert (gc : compat_opL (fun x:elt => plus (g x))). red; auto.
 assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega.
-assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). auto.
+assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). repeat red; auto.
 assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
 assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
 intros s;pattern s; apply set_rec.
@@ -869,8 +869,8 @@ Proof.
 unfold sum; intros f Hf.
 assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
 assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))).
- red; intros.
- rewrite (Hf x x' H); auto.
+ repeat red; intros.
+ rewrite (Hf _ _ H); auto.
 assert (ct : transposeL (fun x => plus (if f x then 1 else 0))).
  red; intros; omega.
 intros s;pattern s; apply set_rec.
@@ -912,17 +912,18 @@ transitivity (f x (fold f s0 i)).
 apply fold_add with (eqA:=eqA); auto with set.
 transitivity (g x (fold f s0 i)); auto with set.
 transitivity (g x (fold g s0 i)); auto with set.
+apply gc; auto with *.
 symmetry; apply fold_add with (eqA:=eqA); auto.
 do 2 rewrite fold_empty; reflexivity.
 Qed.
 
 Lemma sum_compat :
-  forall f g, compat_nat E.eq f -> compat_nat E.eq g ->
+  forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
   forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
 intros.
-unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto.
-red; intros; omega.
-red; intros; omega.
+unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with *.
+intros x x' Hx y y' Hy. rewrite Hx, Hy; auto.
+intros x x' Hx y y' Hy. rewrite Hx, Hy; auto.
 Qed.
 
 End Sum.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 412b6f5c5..bd1472330 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -478,7 +478,7 @@ Lemma filter_ext : forall f f', compat_bool E.eq f -> (forall x, f x = f' x) ->
 Proof.
 intros f f' Hf Hff' s s' Hss' x. do 2 (rewrite filter_iff; auto).
 rewrite Hff', Hss'; intuition.
-red; intros; rewrite <- 2 Hff'; auto.
+repeat red; intros; rewrite <- 2 Hff'; auto.
 Qed.
 
 Lemma filter_subset : forall f, compat_bool E.eq f ->
diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v
index bc2b7b64e..782dccae3 100644
--- a/theories/FSets/FSetFullAVL.v
+++ b/theories/FSets/FSetFullAVL.v
@@ -1067,7 +1067,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  rewrite partition_in_2, filter_in; intuition.
  rewrite H2; auto.
  destruct (f a); auto.
- red; intros; f_equal.
+ repeat red; intros; f_equal.
  rewrite (H _ _ H0); auto.
  Qed.
 
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 032f0c1b3..84c26dacd 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -21,7 +21,7 @@ Require Import DecidableTypeEx FSetFacts FSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Hint Unfold transpose compat_op.
+Hint Unfold transpose compat_op Proper respectful.
 Hint Extern 1 (Equivalence _) => constructor; congruence.
 
 (** First, a functor for Weak Sets in functorial version. *)
@@ -358,9 +358,9 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   assert (Pstep' : forall x a s' s'', InA x l -> ~In x s' -> Add x s' s'' ->
            P s' a -> P s'' (f x a)).
    intros; eapply Pstep; eauto.
-   rewrite elements_iff, <- InA_rev; auto.
+   rewrite elements_iff, <- InA_rev; auto with *.
   assert (Hdup : NoDup l) by
-    (unfold l; eauto using elements_3w, NoDupA_rev).
+    (unfold l; eauto using elements_3w, NoDupA_rev with *).
   assert (Hsame : forall x, In x s <-> InA x l) by
     (unfold l; intros; rewrite elements_iff, InA_rev; intuition).
   clear Pstep; clearbody l; revert s Hsame; induction l.
@@ -429,7 +429,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   do 2 rewrite fold_1, <- fold_left_rev_right.
   set (l:=rev (elements s)).
   assert (Rstep' : forall x a b, InA x l -> R a b -> R (f x a) (g x b)) by
-    (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto).
+    (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto with *).
   clearbody l; clear Rstep s.
   induction l; simpl; auto.
   Qed.
@@ -481,8 +481,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
         fold f s i = fold_right f i l.
   Proof.
   intros; exists (rev (elements s)); split.
-  apply NoDupA_rev; auto with set.
-  exact E.eq_trans.
+  apply NoDupA_rev; auto with *.
   split; intros.
   rewrite elements_iff; do 2 rewrite InA_alt.
   split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition.
@@ -517,8 +516,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2)));
     destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))).
   rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.
-  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto.
-  eauto.
+  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto with *.
   rewrite <- Hl1; auto.
   intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1;
    rewrite (H2 a); intuition.
@@ -547,7 +545,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   intros.
   apply fold_rel with (R:=fun u v => eqA u (f x v)); intros.
   reflexivity.
-  transitivity (f x0 (f x b)); auto.
+  transitivity (f x0 (f x b)); auto. apply Comp; auto with *.
   Qed.
 
   (** ** Fold is a morphism *)
@@ -556,6 +554,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
    eqA (fold f s i) (fold f s i').
   Proof.
   intros. apply fold_rel with (R:=eqA); auto.
+   intros; apply Comp; auto with *.
   Qed.
 
   Lemma fold_equal :
@@ -910,7 +909,7 @@ Module OrdProperties (M:S).
   Lemma sort_equivlistA_eqlistA : forall l l' : list elt,
    sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l'.
   Proof.
-  apply SortA_equivlistA_eqlistA; eauto.
+  apply SortA_equivlistA_eqlistA; eauto with *.
   Qed.
 
   Definition gtb x y := match E.compare x y with GT _ => true | _ => false end.
@@ -929,7 +928,7 @@ Module OrdProperties (M:S).
    intros; unfold leb, gtb; destruct (E.compare x y); intuition; try discriminate; ME.order.
   Qed.
 
-  Lemma gtb_compat : forall x, compat_bool E.eq (gtb x).
+  Lemma gtb_compat : forall x, Proper (E.eq==>Logic.eq) (gtb x).
   Proof.
    red; intros x a b H.
    generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto.
@@ -943,7 +942,7 @@ Module OrdProperties (M:S).
    rewrite <- H1; auto.
   Qed.
 
-  Lemma leb_compat : forall x, compat_bool E.eq (leb x).
+  Lemma leb_compat : forall x, Proper (E.eq==>Logic.eq) (leb x).
   Proof.
    red; intros x a b H; unfold leb.
    f_equal; apply gtb_compat; auto.
@@ -954,8 +953,7 @@ Module OrdProperties (M:S).
    elements s = elements_lt x s ++ elements_ge x s.
   Proof.
   unfold elements_lt, elements_ge, leb; intros.
-  eapply (@filter_split _ E.eq); trivial with set; auto with set.
-   ME.order. ME.order. ME.order.
+  eapply (@filter_split _ E.eq _ E.lt); auto with *.
   intros.
   rewrite gtb_1 in H.
   assert (~E.lt y x).
@@ -969,34 +967,32 @@ Module OrdProperties (M:S).
   Proof.
   intros; unfold elements_ge, elements_lt.
   apply sort_equivlistA_eqlistA; auto with set.
-  apply (@SortA_app _ E.eq); auto.
-  apply (@filter_sort _ E.eq); auto with set; eauto with set.
+  apply (@SortA_app _ E.eq); auto with *.
+  apply (@filter_sort _ E.eq); auto with *.
   constructor; auto.
-  apply (@filter_sort _ E.eq); auto with set; eauto with set.
-  rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with set).
+  apply (@filter_sort _ E.eq); auto with *.
+  rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with *).
   intros.
-  rewrite filter_InA in H1; auto; destruct H1.
+  rewrite filter_InA in H1; auto with *; destruct H1.
   rewrite leb_1 in H2.
   rewrite <- elements_iff in H1.
   assert (~E.eq x y).
    contradict H; rewrite H; auto.
   ME.order.
   intros.
-  rewrite filter_InA in H1; auto; destruct H1.
+  rewrite filter_InA in H1; auto with *; destruct H1.
   rewrite gtb_1 in H3.
   inversion_clear H2.
   ME.order.
-  rewrite filter_InA in H4; auto; destruct H4.
+  rewrite filter_InA in H4; auto with *; destruct H4.
   rewrite leb_1 in H4.
   ME.order.
   red; intros a.
-  rewrite InA_app_iff; rewrite InA_cons.
-  do 2 (rewrite filter_InA; auto).
-  do 2 rewrite <- elements_iff.
-  rewrite leb_1; rewrite gtb_1.
-  rewrite (H0 a); intuition.
+  rewrite InA_app_iff, InA_cons, !filter_InA, <-elements_iff,
+   leb_1, gtb_1, (H0 a) by auto with *.
+  intuition.
   destruct (E.compare a x); intuition.
-  right; right; split; auto.
+  right; right; split; auto with *.
   ME.order.
   Qed.
 
@@ -1008,15 +1004,15 @@ Module OrdProperties (M:S).
      eqlistA E.eq (elements s') (elements s ++ x::nil).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto with set.
-  apply (@SortA_app _ E.eq); auto with set.
+  apply sort_equivlistA_eqlistA; auto with *.
+  apply (@SortA_app _ E.eq); auto with *.
   intros.
   inversion_clear H2.
   rewrite <- elements_iff in H1.
   apply ME.lt_eq with x; auto.
   inversion H3.
   red; intros a.
-  rewrite InA_app_iff; rewrite InA_cons; rewrite InA_nil.
+  rewrite InA_app_iff, InA_cons, InA_nil by auto with *.
   do 2 rewrite <- elements_iff; rewrite (H0 a); intuition.
   Qed.
 
@@ -1025,9 +1021,9 @@ Module OrdProperties (M:S).
      eqlistA E.eq (elements s') (x::elements s).
   Proof.
   intros.
-  apply sort_equivlistA_eqlistA; auto with set.
+  apply sort_equivlistA_eqlistA; auto with *.
   change (sort E.lt ((x::nil) ++ elements s)).
-  apply (@SortA_app _ E.eq); auto with set.
+  apply (@SortA_app _ E.eq); auto with *.
   intros.
   inversion_clear H1.
   rewrite <- elements_iff in H2.