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

2 files changed, 42 insertions, 28 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 9f9eca3c6..7665ac05b 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -832,8 +832,11 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
 
   (** * Conversions between maps and association lists. *)
 
+  Definition uncurry {U V W : Type} (f : U -> V -> W) : U*V -> W :=
+   fun p => f (fst p) (snd p).
+
   Definition of_list (l : list (key*elt)) :=
-    List.fold_right (fun p => add (fst p) (snd p)) (empty _) l.
+    List.fold_right (uncurry (@add _)) (empty _) l.
 
   Definition to_list := elements.
 
@@ -843,6 +846,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Proof.
   induction l as [|(k',e') l IH]; simpl; intros k e Hnodup.
   rewrite empty_mapsto_iff, InA_nil; intuition.
+  unfold uncurry; simpl.
   inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
   specialize (IH k e Hnodup'); clear Hnodup'.
   rewrite add_mapsto_iff, InA_cons, <- IH.
@@ -859,6 +863,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Proof.
   induction l as [|(k',e') l IH]; simpl; intros k Hnodup.
   apply empty_o.
+  unfold uncurry; simpl.
   inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
   specialize (IH k Hnodup'); clear Hnodup'.
   rewrite add_o, IH.
@@ -881,6 +886,14 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
 
   (** * Fold *)
 
+  (** Alternative specification via [fold_right] *)
+
+  Lemma fold_spec_right m (A:Type)(i:A)(f : key -> elt -> A -> A) :
+    fold f m i = List.fold_right (uncurry f) i (rev (elements m)).
+  Proof.
+   rewrite fold_1. symmetry. apply fold_left_rev_right.
+  Qed.
+
   (** ** Induction principles about fold contributed by S. Lescuyer *)
 
   (** In the following lemma, the step hypothesis is deliberately restricted
@@ -895,8 +908,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
       P m (fold f m i).
   Proof.
   intros A P f i m Hempty Hstep.
-  rewrite fold_1, <- fold_left_rev_right.
-  set (F:=fun (y : key * elt) (x : A) => f (fst y) (snd y) x).
+  rewrite fold_spec_right.
+  set (F:=uncurry f).
   set (l:=rev (elements m)).
   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)).
@@ -981,8 +994,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
      R (fold f m i) (fold g m j).
   Proof.
   intros A B R f g i j m Rempty Rstep.
-  do 2 rewrite fold_1, <- fold_left_rev_right.
-  set (l:=rev (elements m)).
+  rewrite 2 fold_spec_right. 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 with *).
@@ -1097,14 +1109,15 @@ 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.
-  intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
+  intros.
+  rewrite 2 fold_spec_right.
   assert (NoDupA eqk (rev (elements m1))) by (auto with *).
   assert (NoDupA eqk (rev (elements m2))) by (auto with *).
   apply fold_right_equivlistA_restr with (R:=complement eqk)(eqA:=eqke);
    auto with *.
   intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto.
   unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto.
-  intros (k,e) (k',e'); unfold eq_key; simpl; auto.
+  intros (k,e) (k',e'); unfold eq_key, uncurry; simpl; auto.
   rewrite <- NoDupA_altdef; auto.
   intros (k,e).
   rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H;
@@ -1114,8 +1127,9 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   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.
-  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 *.
+  intros.
+  rewrite 2 fold_spec_right.
+  set (f':=uncurry f).
   change (f k e (fold_right f' i (rev (elements m1))))
    with (f' (k,e) (fold_right f' i (rev (elements m1)))).
   assert (NoDupA eqk (rev (elements m1))) by (auto with *).
@@ -1124,7 +1138,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
    (R:=complement eqk)(eqA:=eqke)(eqB:=eqA); auto with *.
   intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. apply Comp; auto.
   unfold complement, eq_key_elt, eq_key; repeat red; intuition eauto.
-  unfold f'; intros (k1,e1) (k2,e2); unfold eq_key; simpl; auto.
+  unfold f'; intros (k1,e1) (k2,e2); unfold eq_key, uncurry; simpl; auto.
   rewrite <- NoDupA_altdef; auto.
   rewrite InA_rev, <- elements_mapsto_iff by (auto with *). firstorder.
   intros (a,b).
@@ -2128,8 +2142,7 @@ Module OrdProperties (M:S).
    eqA (fold f m1 i) (fold f m2 i).
   Proof.
   intros m1 m2 A eqA st f i Hf Heq.
-  do 2 rewrite fold_1.
-  do 2 rewrite <- fold_left_rev_right.
+  rewrite 2 fold_spec_right.
   apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.
   intros (k,e) (k',e') (Hk,He) a a' Ha; simpl in *; apply Hf; auto.
   apply eqlistA_rev. apply elements_Equal_eqlistA. auto.
@@ -2140,8 +2153,7 @@ Module OrdProperties (M:S).
    Above x m1 -> Add x e m1 m2 ->
    eqA (fold f m2 i) (f x e (fold f m1 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 *.
+  intros. rewrite 2 fold_spec_right. set (f':=uncurry f).
   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) (Hk,He) a1 a2 Ha; unfold f'; simpl in *. apply P; auto.
@@ -2156,8 +2168,7 @@ Module OrdProperties (M:S).
    Below x m1 -> Add x e m1 m2 ->
    eqA (fold f m2 i) (fold f m1 (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 *.
+  intros. rewrite 2 fold_spec_right. set (f':=uncurry f).
   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) (Hk,He) a1 a2 Ha; unfold f'; simpl in *; apply P; auto.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 80da1c5d8..1bad80615 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -335,6 +335,14 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
 
   Section Fold.
 
+  (** 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_1. symmetry. apply fold_left_rev_right.
+  Qed.
+
   Notation NoDup := (NoDupA E.eq).
   Notation InA := (InA E.eq).
 
@@ -351,8 +359,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
      P s (fold f s i).
   Proof.
   intros A P f i s Pempty Pstep.
-  rewrite fold_1, <- 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.
@@ -424,8 +431,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun 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, <- 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.
@@ -483,8 +489,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun 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
@@ -1086,8 +1091,7 @@ Module OrdProperties (M:S).
    Above 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.
+  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.
@@ -1103,11 +1107,11 @@ Module OrdProperties (M:S).
    Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)).
   Proof.
   intros.
-  do 2 rewrite M.fold_1.
+  rewrite 2 M.fold_1.
   set (g:=fun (a : A) (e : elt) => f e a).
   change (eqA (fold_left g (elements s') i) (fold_left g (x::elements s) i)).
   unfold g.
-  do 2 rewrite <- fold_left_rev_right.
+  rewrite <- 2 fold_left_rev_right.
   apply (@fold_right_eqlistA E.t E.eq A eqA st); auto.
   apply eqlistA_rev.
   apply elements_Add_Below; auto.
@@ -1124,8 +1128,7 @@ Module OrdProperties (M:S).
   Lemma fold_equal :
    forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i).
   Proof.
-  intros; do 2 rewrite M.fold_1.
-  do 2 rewrite <- fold_left_rev_right.
+  intros. 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.