additional properties for FMap (and slight rework of SetoidList and FSetProperties)

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

3 files changed, 64 insertions, 53 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 115f75dc4d..9a23a398e0 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -568,6 +568,7 @@ Module Properties (M: S).
 
   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).
 
   Definition Above x (m:t elt) := forall y, In y m -> E.lt y x.
@@ -768,6 +769,16 @@ Module Properties (M: S).
   ME.order.
   Qed.
 
+  Lemma elements_Equal_eqlistA : forall (m m': t elt), 
+   Equal m m' -> eqlistA eqke (elements m) (elements m').
+  Proof.
+  intros.
+  apply sort_equivlistA_eqlistA; auto.
+  red; intros.
+  destruct x; do 2 rewrite <- elements_mapsto_iff.
+  do 2 rewrite find_mapsto_iff; rewrite H; split; auto.
+  Qed.
+
   End Elements.
 
   Section Cardinal.
@@ -1022,6 +1033,48 @@ Module Properties (M: S).
   Qed.
 
   End Induction_Principles.
+
+  Section Fold_properties.
+
+  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)) -> 
+   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 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)) -> 
+   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 *.
+  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.
+  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 distr_rev; simpl.
+  apply fold_right_commutes with (eqA:=@eqke _) (eqB:=eqA); auto.
+  Qed.
+
+  End Fold_properties.
+
  End Elt.
 
 End Properties.
diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v
index af8dccf536..ccd29be882 100644
--- a/theories/FSets/FMapWeakFacts.v
+++ b/theories/FSets/FMapWeakFacts.v
@@ -508,51 +508,6 @@ rewrite (find_1 H4) in H0; discriminate.
 rewrite (find_1 H4) in H1; discriminate.
 Qed.
 
-Fixpoint findA (A B:Set)(f : A -> bool) (l:list (A*B)) : option B := 
- match l with  
-  | nil => None 
-  | (a,b)::l => if f a then Some b else findA f l
- end.
-
-Lemma findA_NoDupA : 
- forall (A B:Set)
- (eqA:A->A->Prop)
- (eqA_sym: forall a b, eqA a b -> eqA b a)
- (eqA_trans: forall a b c, eqA a b -> eqA b c -> eqA a c)
- (eqA_dec : forall a a', { eqA a a' }+{~eqA a a' }) 
- (l:list (A*B))(x:A)(e:B),  
- NoDupA (fun p p' => eqA (fst p) (fst p')) l -> 
- (InA (fun p p' => eqA (fst p) (fst p') /\ snd p = snd p') (x,e) l <->
-  findA (fun y:A => if eqA_dec x y then true else false) l = Some e).
-Proof.
-induction l; simpl; intros.
-split; intros; try discriminate.
-inversion H0.
-destruct a as (y,e').
-inversion_clear H.
-split; intros.
-inversion_clear H.
-simpl in *; destruct H2; subst e'.
-destruct (eqA_dec x y); intuition.
-destruct (eqA_dec x y); simpl.
-destruct H0.
-generalize e0 H2 eqA_trans eqA_sym; clear.
-induction l.
-inversion 2.
-inversion_clear 2; intros; auto.
-destruct a.
-compute in H; destruct H.
-subst b.
-constructor 1; auto.
-simpl.
-apply eqA_trans with x; auto.
-rewrite <- IHl; auto.
-destruct (eqA_dec x y); simpl in *.
-inversion H; clear H; intros; subst e'; auto.
-constructor 2.
-rewrite IHl; auto.
-Qed.
-
 Lemma elements_o : forall m x, 
  find x m = findA (eqb x) (elements m).
 Proof.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 21ca1120c6..4039e5bbbc 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -783,14 +783,17 @@ Module Properties (M: S).
    transpose eqA f ->
    ~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
   Proof.
-  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.
-  exact eq_dec.
-  rewrite <- Hl1; auto.
-  intros; rewrite <- Hl1; rewrite <- Hl'1; auto.
+  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))))).
+  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 distr_rev; simpl.
+  apply fold_right_commutes with (eqA:=E.eq) (eqB:=eqA); auto.
   Qed.
 
   (** More properties of [fold] : behavior with respect to Above/Below *)