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

4 files changed, 102 insertions, 85 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 *) 
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 74b2812231..ab470f2ae3 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -387,8 +387,43 @@ case_eq (f a); auto; intros.
 rewrite H3 in H; auto; try discriminate.
 Qed.
 
+Section Fold.
+
+Variable B:Set.
+Variable eqB:B->B->Prop.
+
+(** Compatibility of a two-argument function with respect to two equalities. *)
+Definition compat_op (f : A -> B -> B) :=
+  forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y').
+
+(** Two-argument functions that allow to reorder their arguments. *)
+Definition transpose (f : A -> B -> B) :=
+  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). 
+
+Variable st:Setoid_Theory _ eqB.
+Variable f:A->B->B.
+Variable i:B.
+Variable Comp:compat_op f.
+
+Lemma fold_right_eqlistA : 
+   forall s s', eqlistA s s' -> 
+   eqB (fold_right f i s) (fold_right f i s').
+Proof.
+induction 1; simpl; auto.
+refl_st.
+Qed.
+
+Variable Ass:transpose f.
+
+Lemma fold_right_commutes : forall s1 s2 x, 
+  eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
+Proof.
+induction s1; simpl; auto; intros.
+refl_st.
+trans_st (f a (f x (fold_right f i (s1++s2)))).
+Qed.
 
-Section Remove.
+Section Remove_And_More_Fold.
 
 Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
 
@@ -492,26 +527,6 @@ inversion_clear H7; auto.
 elim H6; auto.
 Qed.
 
-
-Section Fold.
-
-Variable B:Set.
-Variable eqB:B->B->Prop.
-
-(** Compatibility of a two-argument function with respect to two equalities. *)
-Definition compat_op (f : A -> B -> B) :=
-  forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y').
-
-(** Two-argument functions that allow to reorder their arguments. *)
-Definition transpose (f : A -> B -> B) :=
-  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). 
-
-Variable st:Setoid_Theory _ eqB.
-Variable f:A->B->B.
-Variable Comp:compat_op f.
-Variable Ass:transpose f.
-Variable i:B.
-
 Lemma removeA_fold_right_0 :
   forall s x, ~InA x s ->
   eqB (fold_right f i s) (fold_right f i (removeA x s)).
@@ -564,15 +579,6 @@ Proof.
  rewrite <- E; auto.
 Qed.
 
-(* for this one, the transpose hyp is not required *)
-Lemma fold_right_eqlistA : 
-   forall s s', eqlistA s s' -> 
-   eqB (fold_right f i s) (fold_right f i s').
-Proof.
-induction 1; simpl; auto.
-refl_st.
-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)).
@@ -613,9 +619,9 @@ Proof.
  destruct H; auto; destruct n; auto.
 Qed.
 
-End Fold.
+End Remove_And_More_Fold.
 
-End Remove.
+End Fold.
 
 End Type_with_equality.