MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right

 In fact, this formula "fold ... = fold_right ... (rev (elements))"
 was already frequently used, but without ever stating it explicitely.
 Instead, we were always chaining two rewrites each time.

 Thanks to A. Appel for mentionning this question of fold_right vs.
 fold_left in the spec of fold.

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

1 files changed, 14 insertions, 11 deletions

diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v
index 9cd28e171..0f24d76a9 100644
--- a/theories/MSets/MSetProperties.v
+++ b/theories/MSets/MSetProperties.v
@@ -337,6 +337,14 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   Notation NoDup := (NoDupA E.eq).
   Notation InA := (InA E.eq).
 
+  (** Alternative specification via [fold_right] *)
+
+  Lemma fold_spec_right (s:t)(A:Type)(i:A)(f : elt -> A -> A) :
+    fold f s i = List.fold_right f i (rev (elements s)).
+  Proof.
+   rewrite fold_spec. symmetry. apply fold_left_rev_right.
+  Qed.
+
   (** ** Induction principles for fold (contributed by S. Lescuyer) *)
 
   (** In the following lemma, the step hypothesis is deliberately restricted
@@ -350,8 +358,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
      P s (fold f s i).
   Proof.
   intros A P f i s Pempty Pstep.
-  rewrite fold_1; unfold flip; rewrite <- fold_left_rev_right.
-  set (l:=rev (elements s)).
+  rewrite fold_spec_right. set (l:=rev (elements s)).
   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.
@@ -423,8 +430,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
      R (fold f s i) (fold g s j).
   Proof.
   intros A B R f g i j s Rempty Rstep.
-  do 2 (rewrite fold_1; unfold flip; rewrite <- fold_left_rev_right).
-  set (l:=rev (elements s)).
+  rewrite 2 fold_spec_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 with *).
   clearbody l; clear Rstep s.
@@ -482,8 +488,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   split; intros.
   rewrite elements_iff; do 2 rewrite InA_alt.
   split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition.
-  rewrite fold_left_rev_right.
-  apply fold_1.
+  apply fold_spec_right.
   Qed.
 
   (** An alternate (and previous) specification for [fold] was based on
@@ -1093,8 +1098,7 @@ Module OrdProperties (M:Sets).
    Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
   Proof.
   intros.
-  rewrite !FM.fold_1.
-  unfold flip; rewrite <-!fold_left_rev_right.
+  rewrite 2 fold_spec_right.
   change (f x (fold_right f i (rev (elements s)))) with
     (fold_right f i (rev (x::nil)++rev (elements s))).
   apply (@fold_right_eqlistA E.t E.eq A eqA st); auto with *.
@@ -1110,7 +1114,7 @@ Module OrdProperties (M:Sets).
    Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)).
   Proof.
   intros.
-  rewrite !FM.fold_1.
+  rewrite !fold_spec.
   change (eqA (fold_left (flip f) (elements s') i)
               (fold_left (flip f) (x::elements s) i)).
   unfold flip; rewrite <-!fold_left_rev_right.
@@ -1131,8 +1135,7 @@ Module OrdProperties (M:Sets).
    forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
   Proof.
   intros.
-  rewrite !FM.fold_1.
-  unfold flip; rewrite <- !fold_left_rev_right.
+  rewrite 2 fold_spec_right.
   apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
   apply eqlistA_rev.
   apply sort_equivlistA_eqlistA; auto with set.