- Extensions of FMap(Weak)Facts:

fold properties and induction principles for (weak) maps.

- Simplification in SetoidList: 
the two important results fold_right_equivlistA and fold_right_add are
now proved without using removeA and hence do not depend anymore on a
decidable equality (good for maps and their arbitrary datas).  In
fact, removeA is not used at all anymore, but I leave it here (mostly),
since it can't hurt.



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

5 files changed, 434 insertions, 205 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 9a23a398e0..b119f27ce7 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -566,6 +566,10 @@ Module Properties (M: S).
  Section Elt. 
   Variable elt:Set.
 
+  Notation eqke := (@eqke elt).
+  Notation eqk := (@eqk elt).
+  Notation ltk := (@ltk elt).
+
   Definition cardinal (m:t elt) := length (elements m).
 
   Definition Equal (m m':t elt) := forall y, find y m = find y m'.
@@ -595,13 +599,21 @@ Module Properties (M: S).
   rewrite H in H0; destruct H0 as (_,H0); inversion H0.
   Qed.
 
-  Notation eqke := (@eqke elt).
-  Notation eqk := (@eqk elt).
-  Notation ltk := (@ltk elt).
+  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.
+  Qed.
+
+  Ltac clean_eauto := unfold O.eqke, O.ltk; simpl; intuition; eauto.
 
   Definition gtb (p p':key*elt) := match E.compare (fst p) (fst p') with GT _ => true | _ => false end.
   Definition leb p := fun p' => negb (gtb p p'). 
 
+  Definition elements_lt p m := List.filter (gtb p) (elements m).
+  Definition elements_ge p m := List.filter (leb p) (elements m).
+
   Lemma gtb_1 : forall p p', gtb p p' = true <-> ltk p' p.
   Proof.
    intros (x,e) (y,e'); unfold gtb, O.ltk; simpl.
@@ -638,10 +650,9 @@ Module Properties (M: S).
   Hint Resolve gtb_compat leb_compat elements_3.
 
   Lemma elements_split : forall p m, 
-    elements m = 
-    List.filter (gtb p) (elements m) ++ List.filter (leb p) (elements m).
+    elements m = elements_lt p m ++ elements_ge p m.
   Proof.
-  unfold leb; intros.
+  unfold elements_lt, elements_ge, leb; intros.
   apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto.
   intros; destruct x; destruct y; destruct p.
   rewrite gtb_1 in H; unfold O.ltk in H; simpl in *.
@@ -651,21 +662,11 @@ Module Properties (M: S).
   unfold O.ltk in *; simpl in *; ME.order.
   Qed.
 
-  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.
-  Qed.
-
-  Ltac clean_eauto := unfold O.eqke, O.ltk; simpl; intuition; eauto.
-
   Lemma elements_Add : forall m m' x e, ~In x m -> Add x e m m' -> 
     eqlistA eqke (elements m') 
-      (List.filter (gtb (x,e)) (elements m) ++ 
-       (x,e)::List.filter (leb (x,e)) (elements m)).
+                 (elements_lt (x,e) m ++ (x,e):: elements_ge (x,e) m).
   Proof.
-  intros.
+  intros; unfold elements_lt, elements_ge.
   apply sort_equivlistA_eqlistA; auto.
   apply (@SortA_app _ eqke); auto.
   apply (@filter_sort _ eqke); auto; clean_eauto.
@@ -710,7 +711,7 @@ Module Properties (M: S).
   right; split; auto; ME.order.
   Qed.
 
-  Lemma elements_eqlistA_max : forall m m' x e, 
+  Lemma elements_Add_Above : forall m m' x e, 
    Above x m -> Add x e m m' -> 
      eqlistA eqke (elements m') (elements m ++ (x,e)::nil).
   Proof.
@@ -739,7 +740,7 @@ Module Properties (M: S).
   ME.order.
   Qed.
 
-  Lemma elements_eqlistA_min : forall m m' x e, 
+  Lemma elements_Add_Below : forall m m' x e, 
    Below x m -> Add x e m m' -> 
      eqlistA eqke (elements m') ((x,e)::elements m).
   Proof.
@@ -829,6 +830,13 @@ Module Properties (M: S).
   symmetry; apply elements_split; auto.
   Qed.
 
+  Lemma cardinal_Equal : forall m m', Equal m m' -> cardinal m = cardinal m'.
+  Proof.
+  unfold cardinal; intros.
+  apply eqlistA_length with (eqA:=eqke).
+  apply elements_Equal_eqlistA; auto.
+  Qed.
+
   End Cardinal.
 
   Section Min_Max_Elt.
@@ -925,11 +933,11 @@ Module Properties (M: S).
   inversion_clear H1.
   red in H2; destruct H2; simpl in *; ME.order.
   inversion_clear H4.
-  rewrite (@InfA_alt _ (@eqke elt)) in H3; eauto.
+  rewrite (@InfA_alt _ eqke) in H3; eauto.
   apply (H3 (y,x0)); auto.
   unfold lt_key; simpl; intuition; eauto.
-  unfold eqke, lt_key; simpl; intuition; eauto.
-  unfold eqke, 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 : 
@@ -1036,41 +1044,82 @@ Module Properties (M: S).
 
   Section Fold_properties.
 
+  Lemma fold_Empty : forall s (A:Set)(f:key->elt->A->A)(i:A),
+   Empty s -> fold f s i = i.
+  Proof.
+  intros.
+  rewrite fold_1.
+  rewrite elements_Empty in H; rewrite H; simpl; auto.
+  Qed.
+
   Lemma fold_Equal : forall s1 s2 (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
    (f:key->elt->A->A)(i:A), 
-   compat_op (@O.eqke _) eqA (fun y =>f (fst y) (snd y)) -> 
+   compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> 
    Equal s1 s2 -> 
    eqA (fold f s1 i) (fold f s2 i).
   Proof.
   intros.
   do 2 rewrite fold_1.
   do 2 rewrite <- fold_left_rev_right.
-  apply fold_right_eqlistA with (eqA:=@O.eqke _) (eqB:=eqA); auto.
+  apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
   apply eqlistA_rev.
   apply elements_Equal_eqlistA; auto.
   Qed.
 
   Lemma fold_Add : forall s1 s2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
    (f:key->elt->A->A)(i:A), 
-   compat_op (@O.eqke _) eqA (fun y =>f (fst y) (snd y)) -> 
+   compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> 
    transpose eqA (fun y =>f (fst y) (snd y)) -> 
    ~In x s1 -> Add x e s1 s2 -> 
    eqA (fold f s2 i) (f x e (fold f s1 i)).
   Proof.
   intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
-  set (f':=fun (y:key*elt) x0 => f (fst y) (snd y) x0) in *.
+  set (f':=fun y x0 => f (fst y) (snd y) x0) in *.
   change (f x e (fold_right f' i (rev (elements s1))))
    with (f' (x,e) (fold_right f' i (rev (elements s1)))).
-  trans_st (fold_right f' i (rev ((filter (gtb (x, e)) (elements s1) ++
-                              (x, e) :: filter (leb (x, e)) (elements s1))))).
-  apply fold_right_eqlistA with (eqA:=@eqke _) (eqB:=eqA); auto.
+  trans_st (fold_right f' i 
+              (rev (elements_lt (x, e) s1 ++ (x,e) :: elements_ge (x, e) s1))).
+  apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
   apply eqlistA_rev.
   apply elements_Add; auto.
   rewrite distr_rev; simpl.
   rewrite app_ass; simpl.
-  pattern (elements s1) at 3; rewrite (elements_split (x,e) s1).
+  rewrite (elements_split (x,e) s1).
+  rewrite distr_rev; simpl.
+  apply fold_right_commutes with (eqA:=eqke) (eqB:=eqA); auto.
+  Qed.
+
+  Lemma fold_Add_Above : forall s1 s2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
+   (f:key->elt->A->A)(i:A), 
+   compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> 
+   Above x s1 -> Add x e s1 s2 -> 
+   eqA (fold f s2 i) (f x e (fold f s1 i)).
+  Proof.
+  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 *.
+  trans_st (fold_right f' i (rev (elements s1 ++ (x,e)::nil))).
+  apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
+  apply eqlistA_rev.
+  apply elements_Add_Above; auto.
+  rewrite distr_rev; simpl.
+  refl_st.
+  Qed.
+
+  Lemma fold_Add_Below : forall s1 s2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
+   (f:key->elt->A->A)(i:A), 
+   compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> 
+   Below x s1 -> Add x e s1 s2 -> 
+   eqA (fold f s2 i) (fold f s1 (f x e i)).
+  Proof.
+  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 *.
+  trans_st (fold_right f' i (rev (((x,e)::nil)++elements s1))).
+  apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
+  apply eqlistA_rev.
+  simpl; apply elements_Add_Below; auto.
   rewrite distr_rev; simpl.
-  apply fold_right_commutes with (eqA:=@eqke _) (eqB:=eqA); auto.
+  rewrite fold_right_app.
+  refl_st.
   Qed.
 
   End Fold_properties.
diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v
index ccd29be882..180df008ef 100644
--- a/theories/FSets/FMapWeakFacts.v
+++ b/theories/FSets/FMapWeakFacts.v
@@ -552,3 +552,198 @@ Qed.
 End BoolSpec.
 
 End Facts.
+
+
+Module Properties (M: S).
+ Module F:=Facts M. 
+ Import F.
+ Import M.
+
+ Section Elt. 
+  Variable elt:Set.
+
+  Definition cardinal (m:t elt) := length (elements m).
+
+  Definition Equal (m m':t elt) := forall y, find y m = find y m'.
+  Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m).
+
+  Notation eqke := (@eq_key_elt elt).
+  Notation eqk := (@eq_key elt).
+
+  Lemma elements_Empty : forall m:t elt, Empty m <-> elements m = nil.
+  Proof.
+  intros.
+  unfold Empty.
+  split; intros.
+  assert (forall a, ~ List.In a (elements m)).
+   red; intros.
+   apply (H (fst a) (snd a)).
+   rewrite elements_mapsto_iff.
+   rewrite InA_alt; exists a; auto.
+   split; auto; split; auto.
+  destruct (elements m); auto.
+  elim (H0 p); simpl; auto.
+  red; intros.
+  rewrite elements_mapsto_iff in H0.
+  rewrite InA_alt in H0; destruct H0.
+  rewrite H in H0; destruct H0 as (_,H0); inversion H0.
+  Qed.
+
+  Lemma fold_Empty : forall m (A:Set)(f:key->elt->A->A)(i:A),
+   Empty m -> fold f m i = i.
+  Proof.
+  intros.
+  rewrite fold_1.
+  rewrite elements_Empty in H; rewrite H; simpl; auto.
+  Qed.
+
+  Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l.
+  Proof.
+  induction 1; auto.
+  constructor; auto.
+  swap H.
+  destruct x as (x,y).
+  rewrite InA_alt in *; destruct H1 as ((a,b),((H1,H2),H3)); simpl in *.
+  exists (a,b); auto.
+  Qed.
+
+  Lemma fold_Equal : forall m1 m2 (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
+   (f:key->elt->A->A)(i:A), 
+   compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> 
+   transpose eqA (fun y => f (fst y) (snd y)) -> 
+   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 with (eqA:=eqke) (eqB:=eqA); auto.
+  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3.
+  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3.
+  red; intros.
+  do 2 rewrite InA_rev.
+  destruct x; do 2 rewrite <- elements_mapsto_iff.
+  do 2 rewrite find_mapsto_iff.
+  rewrite H1; split; auto.
+  Qed.
+
+  Lemma fold_Add : forall m1 m2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
+   (f:key->elt->A->A)(i:A), 
+   compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> 
+   transpose eqA (fun y =>f (fst y) (snd y)) -> 
+   ~In x m1 -> Add x e m1 m2 -> 
+   eqA (fold f m2 i) (f x 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 x e (fold_right f' i (rev (elements m1))))
+   with (f' (x,e) (fold_right f' i (rev (elements m1)))).
+  apply fold_right_add with (eqA:=eqke)(eqB:=eqA); auto.
+  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3.
+  apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3.
+  rewrite InA_rev.
+  swap H1.
+  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.
+  rewrite H2.
+  rewrite add_o.
+  destruct (E.eq_dec x a); intuition.
+  inversion H3; auto.
+  f_equal; auto.
+  elim H1.
+  exists b; apply MapsTo_1 with a; auto.
+  elim n; auto.
+  Qed.
+
+  Lemma cardinal_fold : forall m, cardinal m = fold (fun _ _ => S) m 0.
+  Proof.
+  intros; unfold cardinal; rewrite fold_1.
+  symmetry; apply fold_left_length; auto.
+  Qed.
+ 
+  Lemma Equal_cardinal : forall m m', Equal m m' -> cardinal m = cardinal m'.
+  Proof.
+  intros; do 2 rewrite cardinal_fold.
+  apply fold_Equal with (eqA:=@eq _); auto.
+  constructor; auto; congruence.
+  red; auto.
+  red; auto.
+  Qed.
+
+  Lemma cardinal_1 : forall m, Empty m -> cardinal m = 0.
+  Proof.
+  intros; unfold cardinal; rewrite elements_Empty in H; rewrite H; simpl; auto.
+  Qed.
+
+  Lemma cardinal_2 :
+    forall m m' x e, ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m).
+  Proof.
+  intros; do 2 rewrite cardinal_fold.
+  change S with ((fun _ _ => S) x e).
+  apply fold_Add; auto.
+  constructor; intros; auto; congruence.
+  red; simpl; auto.
+  red; simpl; auto.
+  Qed.
+
+  Lemma cardinal_inv_1 : forall m, cardinal m = 0 -> Empty m. 
+  Proof. 
+  unfold cardinal; intros m H a e.
+  rewrite elements_mapsto_iff.    
+  destruct (elements m); simpl in *.
+  red; inversion 1.
+  inversion H.
+  Qed.
+  Hint Resolve cardinal_inv_1.
+
+  Lemma cardinal_inv_2 :
+   forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }.
+  Proof. 
+  unfold cardinal; intros.
+  generalize (elements_mapsto_iff m).
+  destruct (elements m); try discriminate. 
+  exists p; auto.
+  rewrite H0; destruct p; simpl; auto.
+  constructor; red; auto.
+  Qed.
+
+  Lemma map_induction :
+   forall P : t elt -> Type,
+   (forall m, Empty m -> P m) ->
+   (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') ->
+   forall m, P m.
+  Proof.
+  intros; remember (cardinal m) as n; revert m Heqn; induction n; intros.
+  apply X; apply cardinal_inv_1; auto.
+
+  destruct (cardinal_inv_2 (sym_eq Heqn)) as ((x,e),H0); simpl in *.
+  assert (Add x e (remove x m) m).
+   red; intros.
+   rewrite add_o; rewrite remove_o; destruct (E.eq_dec x y); eauto.
+  apply X0 with (remove x m) x e; auto.
+  apply IHn; auto.
+  assert (S n = S (cardinal (remove x m))).
+   rewrite Heqn; eapply cardinal_2; eauto.
+  inversion H1; auto.
+  Qed.
+
+ End Elt.
+
+End Properties.
+
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 4039e5bbbc..2070cf815b 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -459,6 +459,13 @@ Module Properties (M: S).
 
   Section Elements.
 
+  (* First, a specialized version of SortA_equivlistA_eqlistA: *)
+  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.
+  Qed.
+
   Lemma elements_Empty : forall s, Empty s <-> elements s = nil.
   Proof.
   intros.
@@ -480,6 +487,9 @@ Module Properties (M: S).
   Definition gtb x y := match E.compare x y with GT _ => true | _ => false end.
   Definition leb x := fun y => negb (gtb x y).
 
+  Definition elements_lt x s := List.filter (gtb x) (elements s).
+  Definition elements_ge x s := List.filter (leb x) (elements s).
+
   Lemma gtb_1 : forall x y, gtb x y = true <-> E.lt y x.
   Proof.
    intros; unfold gtb; destruct (E.compare x y); intuition; try discriminate; ME.order.
@@ -512,9 +522,9 @@ Module Properties (M: S).
   Hint Resolve gtb_compat leb_compat.
 
   Lemma elements_split : forall x s, 
-   elements s = List.filter (gtb x) (elements s) ++ List.filter (leb x) (elements s).
+   elements s = elements_lt x s ++ elements_ge x s.
   Proof.
-  unfold leb; intros.
+  unfold elements_lt, elements_ge, leb; intros.
   eapply (@filter_split _ E.eq); eauto. ME.order. ME.order. ME.order.
   intros.
   rewrite gtb_1 in H.
@@ -523,18 +533,10 @@ Module Properties (M: S).
   ME.order.
   Qed.
 
-  (* a specialized version of SortA_equivlistA_eqlistA: *)
-  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.
-  Qed.
-
   Lemma elements_Add : forall s s' x, ~In x s -> Add x s s' -> 
-    eqlistA E.eq (elements s') 
-      (List.filter (gtb x) (elements s) ++ x::List.filter (leb x) (elements s)).
+    eqlistA E.eq (elements s') (elements_lt x s ++ x :: elements_ge x s). 
   Proof.
-  intros.
+  intros; unfold elements_ge, elements_lt.
   apply sort_equivlistA_eqlistA; auto.
   apply (@SortA_app _ E.eq); auto.
   apply (@filter_sort _ E.eq); auto; eauto.
@@ -567,7 +569,7 @@ Module Properties (M: S).
   ME.order.
   Qed.
 
-  Lemma elements_eqlistA_max : forall s s' x, 
+  Lemma elements_Add_Above : forall s s' x, 
    Above x s -> Add x s s' -> 
      eqlistA E.eq (elements s') (elements s ++ x::nil).
   Proof.
@@ -584,7 +586,7 @@ Module Properties (M: S).
   do 2 rewrite <- elements_iff; rewrite (H0 a); intuition.
   Qed.
 
-  Lemma elements_eqlistA_min : forall s s' x, 
+  Lemma elements_Add_Below : forall s s' x, 
    Below x s -> Add x s s' -> 
      eqlistA E.eq (elements s') (x::elements s).
   Proof.
@@ -784,14 +786,13 @@ Module Properties (M: S).
    ~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
   Proof.
   intros; do 2 rewrite M.fold_1; do 2 rewrite <- fold_left_rev_right.
-  trans_st (fold_right f i (rev ((List.filter (gtb x) (elements s) ++
-                                 x :: List.filter (leb x) (elements s))))).
+  trans_st (fold_right f i (rev (elements_lt x s ++ x :: elements_ge x s))).
   apply fold_right_eqlistA with (eqA:=E.eq) (eqB:=eqA); auto.
   apply eqlistA_rev.
   apply elements_Add; auto.
   rewrite distr_rev; simpl.
   rewrite app_ass; simpl.
-  pattern (elements s) at 3; rewrite (elements_split x s).
+  rewrite (elements_split x s).
   rewrite distr_rev; simpl.
   apply fold_right_commutes with (eqA:=E.eq) (eqB:=eqA); auto.
   Qed.
@@ -812,7 +813,7 @@ Module Properties (M: S).
   apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
   rewrite <- distr_rev.
   apply eqlistA_rev.
-  apply elements_eqlistA_max; auto.
+  apply elements_Add_Above; auto.
   Qed.
 
   Lemma fold_4 :
@@ -829,7 +830,7 @@ Module Properties (M: S).
   do 2 rewrite <- fold_left_rev_right.
   apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
   apply eqlistA_rev.
-  apply elements_eqlistA_min; auto.
+  apply elements_Add_Below; auto.
   Qed.
 
   End Fold_Basic.
diff --git a/theories/FSets/FSetWeakProperties.v b/theories/FSets/FSetWeakProperties.v
index 12a180298d..169543e320 100644
--- a/theories/FSets/FSetWeakProperties.v
+++ b/theories/FSets/FSetWeakProperties.v
@@ -493,9 +493,9 @@ Module Properties (M: S).
   rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.
   apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto.
   eauto.
-  exact eq_dec.
   rewrite <- Hl1; auto.
-  intros; rewrite <- Hl1; rewrite <- Hl'1; auto.
+  intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1; 
+   rewrite (H2 a); intuition.
   Qed.
 
   (** Similar specifications for [cardinal]. *)
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index ab470f2ae3..301a09f25a 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -124,6 +124,35 @@ exists (a::l1); exists y; exists l2; auto.
 split; simpl; f_equal; auto.
 Qed.
 
+Lemma InA_app : forall l1 l2 x,
+ InA x (l1 ++ l2) -> InA x l1 \/ InA x l2.
+Proof.
+ induction l1; simpl in *; intuition.
+ inversion_clear H; auto.
+ elim (IHl1 l2 x H0); auto.
+Qed.
+
+Lemma InA_app_iff : forall l1 l2 x,
+ InA x (l1 ++ l2) <-> InA x l1 \/ InA x l2.
+Proof.
+ split.
+ apply InA_app.
+ destruct 1; generalize H; do 2 rewrite InA_alt.
+ destruct 1 as (y,(H1,H2)); exists y; split; auto.
+ apply in_or_app; auto.
+ destruct 1 as (y,(H1,H2)); exists y; split; auto.
+ apply in_or_app; auto.
+Qed.
+
+Lemma InA_rev : forall p m, 
+ InA p (rev m) <-> InA p m.
+Proof.
+ intros; do 2 rewrite InA_alt.
+ split; intros (y,H); exists y; intuition.
+ rewrite In_rev; auto.
+ rewrite <- In_rev; auto.
+Qed.
+
 (** Results concerning lists modulo [eqA] and [ltA] *)
 
 Variable ltA : A -> A -> Prop.
@@ -188,6 +217,26 @@ intros; eapply SortA_InfA_InA; eauto.
 apply InA_InfA.
 Qed.
 
+Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
+Proof.
+ induction l1; simpl; auto.
+ inversion_clear 1; auto.
+Qed.
+
+Lemma SortA_app :
+ forall l1 l2, SortA l1 -> SortA l2 ->
+ (forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
+ SortA (l1 ++ l2).
+Proof.
+ induction l1; simpl in *; intuition.
+ inversion_clear H.
+ constructor; auto.
+ apply InfA_app; auto.
+ destruct l2; auto.
+Qed.
+
+Section NoDupA.
+
 Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
 Proof.
  simple induction l; auto.
@@ -220,7 +269,6 @@ intros.
 apply (H1 x); auto.
 Qed.
 
-
 Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l).
 Proof.
 induction l.
@@ -241,46 +289,37 @@ rewrite In_rev; auto.
 inversion H4.
 Qed.
 
-Lemma InA_app : forall l1 l2 x,
- InA x (l1 ++ l2) -> InA x l1 \/ InA x l2.
+Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l').
 Proof.
- induction l1; simpl in *; intuition.
- inversion_clear H; auto.
- elim (IHl1 l2 x H0); auto.
+ induction l; simpl in *; inversion_clear 1; auto.
+ constructor; eauto.
+ swap H0.
+ rewrite InA_app_iff in *; rewrite InA_cons; intuition.
 Qed.
 
-Lemma InA_app_iff : forall l1 l2 x,
- InA x (l1 ++ l2) <-> InA x l1 \/ InA x l2.
+Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l').
 Proof.
- split.
- apply InA_app.
- destruct 1; generalize H; do 2 rewrite InA_alt.
- destruct 1 as (y,(H1,H2)); exists y; split; auto.
- apply in_or_app; auto.
- destruct 1 as (y,(H1,H2)); exists y; split; auto.
- apply in_or_app; auto.
+ induction l; simpl in *; inversion_clear 1; auto.
+ constructor; eauto.
+ assert (H2:=IHl _ _ H1).
+ inversion_clear H2.
+ rewrite InA_cons.
+ red; destruct 1.
+ apply H0.
+ rewrite InA_app_iff in *; rewrite InA_cons; auto.
+ apply H; auto.
+ constructor.
+ swap H0.
+ rewrite InA_app_iff in *; rewrite InA_cons; intuition.
+ eapply NoDupA_split; eauto.
 Qed.
 
-Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
-Proof.
- induction l1; simpl; auto.
- inversion_clear 1; auto.
-Qed.
-
-Lemma SortA_app :
- forall l1 l2, SortA l1 -> SortA l2 ->
- (forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
- SortA (l1 ++ l2).
-Proof.
- induction l1; simpl in *; intuition.
- inversion_clear H.
- constructor; auto.
- apply InfA_app; auto.
- destruct l2; auto.
-Qed.
+End NoDupA.
 
 (** Some results about [eqlistA] *)
 
+Section EqlistA.
+
 Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'.
 Proof.
 induction 1; auto; simpl; congruence.
@@ -342,8 +381,12 @@ assert (H8 : InA x (a::l)) by auto; inversion_clear H8; auto.
 elim (@ltA_not_eqA a0 x); eauto.
 Qed.
 
+End EqlistA.
+
 (** A few things about [filter] *)
 
+Section Filter.
+
 Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
 Proof.
 induction l; simpl; auto.
@@ -387,6 +430,8 @@ case_eq (f a); auto; intros.
 rewrite H3 in H; auto; try discriminate.
 Qed.
 
+End Filter.
+
 Section Fold.
 
 Variable B:Set.
@@ -423,7 +468,64 @@ refl_st.
 trans_st (f a (f x (fold_right f i (s1++s2)))).
 Qed.
 
-Section Remove_And_More_Fold.
+Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y -> 
+ NoDupA (x::l) -> NoDupA (l1++y::l2) -> 
+ equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
+Proof.
+ intros; intro a.
+ generalize (H2 a).
+ repeat rewrite InA_app_iff.
+ do 2 rewrite InA_cons.
+ inversion_clear H0.
+ assert (SW:=NoDupA_swap H1).
+ inversion_clear SW.
+ rewrite InA_app_iff in H0.
+ split; intros.
+ assert (~eqA a x).
+  swap H3; apply InA_eqA with a; auto.
+ assert (~eqA a y).
+  swap H8; eauto.
+ intuition.
+ assert (eqA a x \/ InA a l) by intuition.
+ destruct H8; auto.
+ elim H0.
+ destruct H7; [left|right]; eapply InA_eqA; eauto.
+Qed. 
+
+Lemma fold_right_equivlistA :
+  forall s s', NoDupA s -> NoDupA s' ->
+  equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
+Proof.
+ simple induction s.
+ destruct s'; simpl.
+ intros; refl_st; auto.
+ unfold equivlistA; intros.
+ destruct (H1 a).
+ assert (X : InA a nil); auto; inversion X.
+ intros x l Hrec s' N N' E; simpl in *.
+ assert (InA x s').
+  rewrite <- (E x); auto.
+ destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))).
+ subst s'.
+ trans_st (f x (fold_right f i (s1++s2))).
+ apply Comp; auto.
+ apply Hrec; auto.
+ inversion_clear N; auto.
+ eapply NoDupA_split; eauto.
+ eapply equivlistA_NoDupA_split; eauto.
+ trans_st (f y (fold_right f i (s1++s2))).
+ apply Comp; auto; refl_st.
+ sym_st; apply fold_right_commutes.
+Qed.
+
+Lemma fold_right_add :
+  forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s ->
+  equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
+Proof.   
+ intros; apply (@fold_right_equivlistA s' (x::s)); auto.
+Qed.
+
+Section Remove.
 
 Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
 
@@ -501,125 +603,7 @@ inversion_clear H1; auto.
 elim H2; auto.
 Qed.
 
-Let addlistA x l l' := forall y, InA y l' <-> eqA x y \/ InA y l.
-
-Lemma removeA_add :
-  forall s s' x x', NoDupA s -> NoDupA (x' :: s') ->
-  ~ eqA x x' -> ~ InA x s -> 
-  addlistA x s (x' :: s') -> addlistA x (removeA x' s) s'.
-Proof.
-unfold addlistA; intros.
-inversion_clear H0.
-rewrite removeA_InA; auto.
-split; intros.
-destruct (eqA_dec x y); auto; intros.
-right; split; auto.
-destruct (H3 y); clear H3.
-destruct H6; intuition.
-swap H4; apply InA_eqA with y; auto.
-destruct H0.
-assert (InA y (x' :: s')) by (rewrite H3; auto).
-inversion_clear H6; auto.
-elim H1; apply eqA_trans with y; auto.
-destruct H0.
-assert (InA y (x' :: s')) by (rewrite H3; auto).
-inversion_clear H7; auto.
-elim H6; auto.
-Qed.
-
-Lemma removeA_fold_right_0 :
-  forall s x, ~InA x s ->
-  eqB (fold_right f i s) (fold_right f i (removeA x s)).
-Proof.
- simple induction s; simpl; intros.
- refl_st.
- destruct (eqA_dec x a); simpl; intros.
- absurd_hyp e; auto.
- apply Comp; auto. 
-Qed.   
-
-Lemma removeA_fold_right :
-  forall s x, NoDupA s -> InA x s ->
-  eqB (fold_right f i s) (f x (fold_right f i (removeA x s))).
-Proof.
- simple induction s; simpl.  
- inversion_clear 2.
- intros.
- inversion_clear H0.
- destruct (eqA_dec x a); simpl; intros.
- apply Comp; auto. 
- apply removeA_fold_right_0; auto.
- swap H2; apply InA_eqA with x; auto.
- inversion_clear H1. 
- destruct n; auto.
- trans_st (f a (f x (fold_right f i (removeA x l)))).
-Qed.   
-
-Lemma fold_right_equivlistA :
-  forall s s', NoDupA s -> NoDupA s' ->
-  equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
-Proof.
- simple induction s.
- destruct s'; simpl.
- intros; refl_st; auto.
- unfold equivlistA; intros.
- destruct (H1 a).
- assert (X : InA a nil); auto; inversion X.
- intros x l Hrec s' N N' E; simpl in *.
- trans_st (f x (fold_right f i (removeA x s'))).
- apply Comp; auto.
- apply Hrec; auto.
- inversion N; auto.
- apply removeA_NoDupA; auto; apply eqA_trans.
- apply removeA_equivlistA; auto.
- inversion_clear N; auto.
- sym_st.
- apply removeA_fold_right; auto.
- unfold equivlistA in E.
- rewrite <- E; auto.
-Qed.
-
-Lemma fold_right_add :
-  forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s ->
-  addlistA x s s' -> eqB (fold_right f i s') (f x (fold_right f i s)).
-Proof.   
- simple induction s'.
- unfold addlistA; intros.
- destruct (H2 x); clear H2.
- assert (X : InA x nil); auto; inversion X.
- intros x' l' Hrec s x N N' IN EQ; simpl.
- (* if x=x' *)
- destruct (eqA_dec x x').
- apply Comp; auto.
- apply fold_right_equivlistA; auto.
- inversion_clear N'; trivial.
- unfold equivlistA; unfold addlistA in EQ; intros.
- destruct (EQ x0); clear EQ.
- split; intros.
- destruct H; auto.
- inversion_clear N'.
- destruct H2; apply InA_eqA with x0; auto.
- apply eqA_trans with x; auto.
- assert (X:InA x0 (x' :: l')); auto; inversion_clear X; auto.
- destruct IN; apply InA_eqA with x0; auto.
- apply eqA_trans with x'; auto.
- (* else x<>x' *)   
- trans_st (f x' (f x (fold_right f i (removeA x' s)))).
- apply Comp; auto.
- apply Hrec; auto.
- apply removeA_NoDupA; auto; apply eqA_trans.
- inversion_clear N'; auto.
- rewrite removeA_InA; intuition.
- apply removeA_add; auto.
- trans_st (f x (f x' (fold_right f i (removeA x' s)))).
- apply Comp; auto.
- sym_st.
- apply removeA_fold_right; auto.
- destruct (EQ x'). 
- destruct H; auto; destruct n; auto.
-Qed.
-
-End Remove_And_More_Fold.
+End Remove.
 
 End Fold.