FMap: fold_rec + more permissive transpose hyp + various cleanup

The induction principles for fold are due to S. Lescuyer
The better transpose hyp is a suggestion by P. Casteran

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

1 files changed, 377 insertions, 144 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 4b4d2549f..f52d292de 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -32,6 +32,15 @@ Proof.
  destruct b; destruct b'; intuition.
 Qed.
 
+Lemma eq_option_alt : forall (elt:Type)(o o':option elt),
+ o=o' <-> (forall e, o=Some e <-> o'=Some e).
+Proof.
+split; intros.
+subst; split; auto.
+destruct o; destruct o'; try rewrite H; auto.
+symmetry; rewrite <- H; auto.
+Qed.
+
 Lemma MapsTo_fun : forall (elt:Type) m x (e e':elt), 
   MapsTo x e m -> MapsTo x e' m -> e=e'.
 Proof.
@@ -85,14 +94,10 @@ Qed.
 
 Lemma not_find_in_iff : forall m x, ~In x m <-> find x m = None.
 Proof.
-intros.
-generalize (find_mapsto_iff m x); destruct (find x m).
-split; intros; try discriminate.
-destruct H0.
-exists e; rewrite H; auto.
-split; auto.
-intros; intros (e,H1).
-rewrite H in H1; discriminate.
+split; intros.
+rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff.
+split; try discriminate. intro H'; elim H; exists e; auto.
+intros (e,He); rewrite find_mapsto_iff,H in He; discriminate.
 Qed.
 
 Lemma in_find_iff : forall m x, In x m <-> find x m <> None.
@@ -334,21 +339,14 @@ Qed.
 
 Lemma find_o : forall m x y, E.eq x y -> find x m = find y m.
 Proof.
-intros.
-generalize (find_mapsto_iff m x) (find_mapsto_iff m y) (fun e => MapsTo_iff m e H).
-destruct (find x m); destruct (find y m); intros.
-rewrite <- H0; rewrite H2; rewrite H1; auto.
-symmetry; rewrite <- H1; rewrite <- H2; rewrite H0; auto.
-rewrite <- H0; rewrite H2; rewrite H1; auto.
-auto.
+intros. rewrite eq_option_alt. intro e. rewrite <- 2 find_mapsto_iff.
+apply MapsTo_iff; auto.
 Qed.
 
 Lemma empty_o : forall x, find x (empty elt) = None.
 Proof.
-intros.
-case_eq (find x (empty elt)); intros; auto.
-generalize (find_2 H).
-rewrite empty_mapsto_iff; intuition.
+intros. rewrite eq_option_alt. intro e.
+rewrite <- find_mapsto_iff, empty_mapsto_iff; now intuition.
 Qed.
 
 Lemma empty_a : forall x, mem x (empty elt) = false.
@@ -368,15 +366,12 @@ Qed.
 Lemma add_neq_o : forall m x y e, 
  ~ E.eq x y -> find y (add x e m) = find y m. 
 Proof.
-intros.
-case_eq (find y m); intros; auto with map.
-case_eq (find y (add x e m)); intros; auto with map.
-rewrite <- H0; symmetry.
-apply find_1; apply add_3 with x e; auto with map.
+intros. rewrite eq_option_alt. intro e'. rewrite <- 2 find_mapsto_iff.
+apply add_neq_mapsto_iff; auto.
 Qed.
 Hint Resolve add_neq_o : map.
 
-Lemma add_o : forall m x y e, 
+Lemma add_o : forall m x y e,
  find y (add x e m) = if eq_dec x y then Some e else find y m.
 Proof.
 intros; destruct (eq_dec x y); auto with map.
@@ -404,45 +399,38 @@ Qed.
 Lemma remove_eq_o : forall m x y, 
  E.eq x y -> find y (remove x m) = None.
 Proof.
-intros.
-generalize (remove_1 (m:=m) H).
-generalize (find_mapsto_iff (remove x m) y).
-destruct (find y (remove x m)); auto.
-destruct 2.
-exists e; rewrite H0; auto.
+intros. rewrite eq_option_alt. intro e.
+rewrite <- find_mapsto_iff, remove_mapsto_iff; now intuition.
 Qed.
 Hint Resolve remove_eq_o : map.
 
-Lemma remove_neq_o : forall m x y, 
- ~ E.eq x y -> find y (remove x m) = find y m. 
+Lemma remove_neq_o : forall m x y,
+ ~ E.eq x y -> find y (remove x m) = find y m.
 Proof.
-intros.
-case_eq (find y m); intros; auto with map.
-case_eq (find y (remove x m)); intros; auto with map.
-rewrite <- H0; symmetry.
-apply find_1; apply remove_3 with x; auto with map.
+intros. rewrite eq_option_alt. intro e.
+rewrite <- find_mapsto_iff, remove_neq_mapsto_iff; now intuition.
 Qed.
 Hint Resolve remove_neq_o : map.
 
-Lemma remove_o : forall m x y, 
+Lemma remove_o : forall m x y,
  find y (remove x m) = if eq_dec x y then None else find y m.
 Proof.
 intros; destruct (eq_dec x y); auto with map.
 Qed.
 
-Lemma remove_eq_b : forall m x y, 
+Lemma remove_eq_b : forall m x y,
  E.eq x y -> mem y (remove x m) = false.
 Proof.
 intros; rewrite mem_find_b; rewrite remove_eq_o; auto.
 Qed.
 
-Lemma remove_neq_b : forall m x y, 
+Lemma remove_neq_b : forall m x y,
  ~ E.eq x y -> mem y (remove x m) = mem y m.
 Proof.
 intros; do 2 rewrite mem_find_b; rewrite remove_neq_o; auto.
 Qed.
 
-Lemma remove_b : forall m x y, 
+Lemma remove_b : forall m x y,
  mem y (remove x m) = negb (eqb x y) && mem y m.
 Proof.
 intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb.
@@ -506,7 +494,7 @@ Qed.
 Lemma map2_1bis : forall (m: t elt)(m': t elt') x 
  (f:option elt->option elt'->option elt''), 
  f None None = None -> 
- find x (map2 f m m') = f (find x m) (find x m').       
+ find x (map2 f m m') = f (find x m) (find x m').
 Proof.
 intros.
 case_eq (find x m); intros.
@@ -525,23 +513,16 @@ rewrite (find_1 H4) in H0; discriminate.
 rewrite (find_1 H4) in H1; discriminate.
 Qed.
 
-Lemma elements_o : forall m x, 
+Lemma elements_o : forall m x,
  find x m = findA (eqb x) (elements m).
 Proof.
-intros.
-assert (forall e, find x m = Some e <-> InA (eq_key_elt (elt:=elt)) (x,e) (elements m)).
- intros; rewrite <- find_mapsto_iff; apply elements_mapsto_iff.
-assert (H0:=elements_3w m).
-generalize (fun e => @findA_NoDupA _ _ _ E.eq_sym E.eq_trans eq_dec (elements m) x e H0).
-fold (eqb x).
-destruct (find x m); destruct (findA (eqb x) (elements m)); 
- simpl; auto; intros.
-symmetry; rewrite <- H1; rewrite <- H; auto.
-symmetry; rewrite <- H1; rewrite <- H; auto.
-rewrite H; rewrite H1; auto.
-Qed.
-
-Lemma elements_b : forall m x, 
+intros. rewrite eq_option_alt. intro e.
+rewrite <- find_mapsto_iff, elements_mapsto_iff.
+unfold eqb.
+rewrite <- findA_NoDupA; intuition; try apply elements_3w; eauto.
+Qed.
+
+Lemma elements_b : forall m x,
  mem x m = existsb (fun p => eqb x (fst p)) (elements m).
 Proof.
 intros.
@@ -568,30 +549,41 @@ Qed.
 
 End BoolSpec.
 
-Section Equalities. 
+Section Equalities.
 
 Variable elt:Type.
 
+ (** Another characterisation of [Equal] *)
+
+Lemma Equal_mapsto_iff : forall m1 m2 : t elt,
+ Equal m1 m2 <-> (forall k e, MapsTo k e m1 <-> MapsTo k e m2).
+Proof.
+intros m1 m2. split; [intros Heq k e|intros Hiff].
+rewrite 2 find_mapsto_iff, Heq. split; auto.
+intro k. rewrite eq_option_alt. intro e.
+rewrite <- 2 find_mapsto_iff; auto.
+Qed.
+
 (** * Relations between [Equal], [Equiv] and [Equivb]. *)
 
 (** First, [Equal] is [Equiv] with Leibniz on elements. *)
 
-Lemma Equal_Equiv : forall (m m' : t elt), 
+Lemma Equal_Equiv : forall (m m' : t elt),
   Equal m m' <-> Equiv (@Logic.eq elt) m m'.
 Proof.
- unfold Equal, Equiv; split; intros.
- split; intros.
- rewrite in_find_iff, in_find_iff, H; intuition.
- rewrite find_mapsto_iff in H0,H1; congruence.
- destruct H.
- specialize (H y).
- specialize (H0 y).
- do 2 rewrite in_find_iff in H.
- generalize (find_mapsto_iff m y)(find_mapsto_iff m' y).
- do 2 destruct find; auto; intros.
- f_equal; apply H0; [rewrite H1|rewrite H2]; auto.
- destruct H as [H _]; now elim H.
- destruct H as [_ H]; now elim H.
+intros. rewrite Equal_mapsto_iff. split; intros.
+split.
+split; intros (e,Hin); exists e; [rewrite <- H|rewrite H]; auto.
+intros; apply MapsTo_fun with m k; auto; rewrite H; auto.
+split; intros H'.
+destruct H.
+assert (Hin : In k m') by (rewrite <- H; exists e; auto).
+destruct Hin as (e',He').
+rewrite (H0 k e e'); auto.
+destruct H.
+assert (Hin : In k m) by (rewrite H; exists e; auto).
+destruct Hin as (e',He').
+rewrite <- (H0 k e' e); auto.
 Qed.
 
 (** [Equivb] and [Equiv] and equivalent when [eq_elt] and [cmp]
@@ -668,7 +660,8 @@ Add Parametric Relation (elt : Type) : (t elt) Equal
  transitivity proved by (@Equal_trans elt)
  as EqualSetoid.
 
-Add Parametric Morphism elt : (@In elt) with signature E.eq ==> Equal ==> iff as In_m.
+Add Parametric Morphism elt : (@In elt)
+ with signature E.eq ==> Equal ==> iff as In_m.
 Proof.
 unfold Equal; intros k k' Hk m m' Hm.
 rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition.
@@ -678,42 +671,41 @@ Add Parametric Morphism elt : (@MapsTo elt)
  with signature E.eq ==> @Logic.eq _ ==> Equal ==> iff as MapsTo_m.
 Proof.
 unfold Equal; intros k k' Hk e m m' Hm.
-rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm; 
+rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm;
  intuition.
 Qed.
 
-Add Parametric Morphism elt : (@Empty elt) with signature Equal ==> iff as Empty_m.
+Add Parametric Morphism elt : (@Empty elt)
+ with signature Equal ==> iff as Empty_m.
 Proof.
 unfold Empty; intros m m' Hm; intuition.
 rewrite <-Hm in H0; eauto.
 rewrite Hm in H0; eauto.
 Qed.
 
-Add Parametric Morphism elt : (@is_empty elt) with signature Equal ==> @Logic.eq _ as is_empty_m.
+Add Parametric Morphism elt : (@is_empty elt)
+ with signature Equal ==> @Logic.eq _ as is_empty_m.
 Proof.
 intros m m' Hm.
 rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition.
 Qed.
 
-Add Parametric Morphism elt : (@mem elt) with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m.
+Add Parametric Morphism elt : (@mem elt)
+ with signature E.eq ==> Equal ==> @Logic.eq _ as mem_m.
 Proof.
 intros k k' Hk m m' Hm.
 rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition.
 Qed.
 
-Add Parametric Morphism elt : (@find elt) with signature E.eq ==> Equal ==> @Logic.eq _ as find_m.
+Add Parametric Morphism elt : (@find elt)
+ with signature E.eq ==> Equal ==> @Logic.eq _ as find_m.
 Proof.
-intros k k' Hk m m' Hm.
-generalize (find_mapsto_iff m k)(find_mapsto_iff m' k')
- (not_find_in_iff m k)(not_find_in_iff m' k'); 
-do 2 destruct find; auto; intros.
-rewrite <- H, Hk, Hm, H0; auto.
-rewrite <- H1, Hk, Hm, H2; auto.
-symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto.
+intros k k' Hk m m' Hm. rewrite eq_option_alt. intro e.
+rewrite <- 2 find_mapsto_iff, Hk, Hm. split; auto.
 Qed.
 
-Add Parametric Morphism elt : (@add elt) with signature 
- E.eq ==> @Logic.eq _ ==> Equal ==> Equal as add_m.
+Add Parametric Morphism elt : (@add elt)
+ with signature E.eq ==> @Logic.eq _ ==> Equal ==> Equal as add_m.
 Proof.
 intros k k' Hk e m m' Hm y.
 rewrite add_o, add_o; do 2 destruct eq_dec; auto.
@@ -721,8 +713,8 @@ elim n; rewrite <-Hk; auto.
 elim n; rewrite Hk; auto.
 Qed.
 
-Add Parametric Morphism elt : (@remove elt) with signature
- E.eq ==> Equal ==> Equal as remove_m.
+Add Parametric Morphism elt : (@remove elt)
+ with signature E.eq ==> Equal ==> Equal as remove_m.
 Proof.
 intros k k' Hk m m' Hm y.
 rewrite remove_o, remove_o; do 2 destruct eq_dec; auto.
@@ -730,7 +722,8 @@ elim n; rewrite <-Hk; auto.
 elim n; rewrite Hk; auto.
 Qed.
 
-Add Parametric Morphism elt elt' : (@map elt elt') with signature @Logic.eq _ ==> Equal ==> Equal as map_m.
+Add Parametric Morphism elt elt' : (@map elt elt')
+ with signature @Logic.eq _ ==> Equal ==> Equal as map_m.
 Proof.
 intros f m m' Hm y.
 rewrite map_o, map_o, Hm; auto.
@@ -748,16 +741,16 @@ End WFacts_fun.
 Module WFacts (M:S) := WFacts_fun M.E M.
 Module Facts := WFacts.
 
-(** * Additional Properties for weak maps 
- 
+(** * Additional Properties for weak maps
+
     Results about [fold], [elements], induction principles...
 *)
 
 Module WProperties_fun (E:DecidableType)(M:WSfun E).
- Module Import F:=WFacts_fun E M. 
+ Module Import F:=WFacts_fun E M.
  Import M.
 
- Section Elt. 
+ Section Elt.
   Variable elt:Type.
 
   Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m).
@@ -765,6 +758,44 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Notation eqke := (@eq_key_elt elt).
   Notation eqk := (@eq_key elt).
 
+  (** Complements about InA, NoDupA and findA *)
+
+  Lemma InA_eqke_eqk : forall k1 k2 e1 e2 l,
+    E.eq k1 k2 -> InA eqke (k1,e1) l -> InA eqk (k2,e2) l.
+  Proof.
+  intros k1 k2 e1 e2 l Hk. rewrite 2 InA_alt.
+  intros ((k',e') & (Hk',He') & H); simpl in *.
+  exists (k',e'); split; auto.
+  red; simpl; eauto.
+  Qed.
+
+  Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l.
+  Proof.
+  induction 1; auto.
+  constructor; auto.
+  destruct x as (k,e).
+  eauto using InA_eqke_eqk.
+  Qed.
+
+  Lemma findA_rev : forall l k, NoDupA eqk l ->
+    findA (eqb k) l = findA (eqb k) (rev l).
+  Proof.
+  intros.
+  case_eq (findA (eqb k) l).
+  intros. symmetry.
+  unfold eqb.
+  rewrite <- findA_NoDupA, InA_rev, findA_NoDupA
+   by eauto using NoDupA_rev; eauto.
+  case_eq (findA (eqb k) (rev l)); auto.
+  intros e.
+  unfold eqb.
+  rewrite <- findA_NoDupA, InA_rev, findA_NoDupA
+   by eauto using NoDupA_rev.
+  intro Eq; rewrite Eq; auto.
+  Qed.
+
+  (** * Elements *)
+
   Lemma elements_Empty : forall m:t elt, Empty m <-> elements m = nil.
   Proof.
   intros.
@@ -789,29 +820,234 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   rewrite <-elements_Empty; apply empty_1.
   Qed.
 
-  Lemma fold_Empty : forall m (A:Type)(f:key->elt->A->A)(i:A),
-   Empty m -> fold f m i = i.
+  (** * Conversions between maps and association lists. *)
+
+  Definition of_list (l : list (key*elt)) :=
+    List.fold_right (fun p => add (fst p) (snd p)) (empty _) l.
+
+  Definition to_list := elements.
+
+  Lemma of_list_1 : forall l k e,
+    NoDupA eqk l ->
+    (MapsTo k e (of_list l) <-> InA eqke (k,e) l).
+  Proof.
+  induction l as [|(k',e') l IH]; simpl; intros k e Hnodup.
+  rewrite empty_mapsto_iff, InA_nil; intuition.
+  inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
+  specialize (IH k e Hnodup'); clear Hnodup'.
+  rewrite add_mapsto_iff, InA_cons, <- IH.
+  unfold eq_key_elt at 1; simpl.
+  split; destruct 1 as [H|H]; try (intuition;fail).
+  destruct (eq_dec k k'); [left|right]; split; auto.
+  contradict Hnotin.
+  apply InA_eqke_eqk with k e; intuition.
+  Qed.
+
+  Lemma of_list_1b : forall l k,
+    NoDupA eqk l ->
+    find k (of_list l) = findA (eqb k) l.
+  Proof.
+  induction l as [|(k',e') l IH]; simpl; intros k Hnodup.
+  apply empty_o.
+  inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
+  specialize (IH k Hnodup'); clear Hnodup'.
+  rewrite add_o, IH.
+  unfold eqb; do 2 destruct eq_dec; auto; elim n; eauto.
+  Qed.
+
+  Lemma of_list_2 : forall l, NoDupA eqk l ->
+    equivlistA eqke l (to_list (of_list l)).
+  Proof.
+  intros l Hnodup (k,e).
+  rewrite <- elements_mapsto_iff, of_list_1; intuition.
+  Qed.
+
+  Lemma of_list_3 : forall s, Equal (of_list (to_list s)) s.
+  Proof.
+  intros s k.
+  rewrite of_list_1b, elements_o; auto.
+  apply elements_3w.
+  Qed.
+
+  (** * Fold *)
+
+  (** ** Induction principles about fold contributed by S. Lescuyer *)
+
+  (** In the following lemma, the step hypothesis is deliberately restricted
+      to the precise map m we are considering. *)
+
+  Lemma fold_rec :
+    forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A),
+     forall (i:A)(m:t elt),
+      (forall m, Empty m -> P m i) ->
+      (forall k e a m' m'', MapsTo k e m -> ~In k m' ->
+         Add k e m' m'' -> P m' a -> P m'' (f k e a)) ->
+      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).
+  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)).
+   intros k e a m' m'' H ? ? ?; eapply Hstep; eauto.
+   revert H; unfold l; rewrite InA_rev, elements_mapsto_iff; auto.
+  assert (Hdup : NoDupA eqk l).
+   unfold l. apply NoDupA_rev; try red; eauto. apply elements_3w.
+  assert (Hsame : forall k, find k m = findA (eqb k) l).
+   intros k. unfold l. rewrite elements_o, findA_rev; auto.
+   apply elements_3w.
+  clearbody l. clearbody F. clear Hstep f. revert m Hsame. induction l.
+  (* empty *)
+  intros m Hsame; simpl.
+  apply Hempty. intros k e.
+  rewrite find_mapsto_iff, Hsame; simpl; discriminate.
+  (* step *)
+  intros m Hsame; destruct a as (k,e); simpl.
+  apply Hstep' with (of_list l); auto.
+   rewrite InA_cons; left; red; auto.
+   inversion_clear Hdup. contradict H. destruct H as (e',He').
+   apply InA_eqke_eqk with k e'; auto.
+   rewrite <- of_list_1; auto.
+   intro k'. rewrite Hsame, add_o, of_list_1b. simpl.
+   unfold eqb. do 2 destruct eq_dec; auto; elim n; eauto.
+   inversion_clear Hdup; auto.
+  apply IHl.
+   intros; eapply Hstep'; eauto.
+   inversion_clear Hdup; auto.
+   intros; apply of_list_1b. inversion_clear Hdup; auto.
+  Qed.
+
+  (** Same, with [empty] and [add] instead of [Empty] and [Add]. In this
+      case, [P] must be compatible with equality of sets *)
+
+  Theorem fold_rec_bis :
+    forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A),
+     forall (i:A)(m:t elt),
+     (forall m m' a, Equal m m' -> P m a -> P m' a) ->
+     (P (empty _) i) ->
+     (forall k e a m', MapsTo k e m -> ~In k m' ->
+       P m' a -> P (add k e m') (f k e a)) ->
+     P m (fold f m i).
+  Proof.
+  intros A P f i m Pmorphism Pempty Pstep.
+  apply fold_rec; intros.
+  apply Pmorphism with (empty _); auto. intro k. rewrite empty_o.
+  case_eq (find k m0); auto; intros e'; rewrite <- find_mapsto_iff.
+  intro H'; elim (H k e'); auto.
+  apply Pmorphism with (add k e m'); try intro; auto.
+  Qed.
+
+  Lemma fold_rec_nodep :
+    forall (A:Type)(P : A -> Type)(f : key -> elt -> A -> A)(i:A)(m:t elt),
+     P i -> (forall k e a, MapsTo k e m -> P a -> P (f k e a)) ->
+     P (fold f m i).
+  Proof.
+  intros; apply fold_rec_bis with (P:=fun _ => P); auto.
+  Qed.
+
+  (** [fold_rec_weak] is a weaker principle than [fold_rec_bis] :
+      the step hypothesis must here be applicable anywhere.
+      At the same time, it looks more like an induction principle,
+      and hence can be easier to use. *)
+
+  Lemma fold_rec_weak :
+    forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A)(i:A),
+    (forall m m' a, Equal m m' -> P m a -> P m' a) ->
+    P (empty _) i ->
+    (forall k e a m, ~In k m -> P m a -> P (add k e m) (f k e a)) ->
+    forall m, P m (fold f m i).
+  Proof.
+  intros; apply fold_rec_bis; auto.
+  Qed.
+
+  Lemma fold_rel :
+    forall (A B:Type)(R : A -> B -> Type)
+     (f : key -> elt -> A -> A)(g : key -> elt -> B -> B)(i : A)(j : B)
+     (m : t elt),
+     R i j ->
+     (forall k e a b, MapsTo k e m -> R a b -> R (f k e a) (g k e b)) ->
+     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)).
+  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).
+  clearbody l; clear Rstep m.
+  induction l; simpl; auto.
+  apply Rstep'; auto.
+  destruct a; simpl; rewrite InA_cons; left; red; auto.
+  Qed.
+
+  (** From the induction principle on [fold], we can deduce some general
+      induction principles on maps. *)
+
+  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. apply (@fold_rec _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto.
+  Qed.
+
+  Lemma map_induction_bis :
+   forall P : t elt -> Type,
+   (forall m m', Equal m m' -> P m -> P m') ->
+   P (empty _) ->
+   (forall x e m, ~In x m -> P m -> P (add x e m)) ->
+   forall m, P m.
   Proof.
   intros.
-  rewrite fold_1.
-  rewrite elements_Empty in H; rewrite H; simpl; auto.
+  apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto.
   Qed.
 
-  Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l.
+  (** [fold] can be used to reconstruct the same initial set. *)
+
+  Lemma fold_identity : forall m : t elt, Equal (fold (@add _) m (empty _)) m.
   Proof.
-  induction 1; auto.
-  constructor; auto.
-  contradict H.
-  destruct x as (x,y).
-  rewrite InA_alt in *; destruct H as ((a,b),((H1,H2),H3)); simpl in *.
-  exists (a,b); auto.
+  intros.
+  apply fold_rec with (P:=fun m acc => Equal acc m); auto with map.
+  intros m' Heq k'.
+  rewrite empty_o.
+  case_eq (find k' m'); auto; intros e'; rewrite <- find_mapsto_iff.
+  intro; elim (Heq k' e'); auto.
+  intros k e a m' m'' _ _ Hadd Heq k'.
+  rewrite Hadd, 2 add_o, Heq; auto.
   Qed.
 
-  Lemma fold_Equal : forall m1 m2 (A:Type)(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 -> 
+  (** ** Additional properties of fold *)
+
+  (** When a function [f] is compatible and allows transpositions, we can
+      compute [fold f] in any order. *)
+
+  (** As noticed by P. Casteran, asking for the general [SetoidList.transpose]
+      here is too restrictive. Think for instance of [f] being [M.add] :
+      in general, [M.add k e (M.add k e' m)] is not equivalent to
+      [M.add k e' (M.add k e m)]. Fortunately, we will never encounter this
+      situation during a real [fold], since the keys received by this [fold]
+      are unique. Hence we can ask the transposition property to hold only
+      for non-equal keys.
+
+      This idea could be push slightly further, by asking the transposition
+      property to hold only for (non-equal) keys living in the map given to
+      [fold]. Please contact us if you need such a version.
+
+      FSets could also benefit from a restricted [transpose], but for this
+      case the gain is unclear. *)
+
+  Definition transpose_neqkey (A:Type)(eqA:A->A->Prop)(f:key->elt->A->A) :=
+    forall k k' e e' a, ~E.eq k k' ->
+      eqA (f k e (f k' e' a)) (f k' e' (f k e a)).
+
+  Lemma fold_Equal :
+   forall m1 m2 (A:Type)(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_neqkey eqA f ->
+   Equal m1 m2 ->
    eqA (fold f m1 i) (fold f m2 i).
   Proof.
   assert (eqke_refl : forall p, eqke p p).
@@ -822,9 +1058,16 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
    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 fold_right_equivlistA_restr with
+    (R:=fun p p' => ~eqk p p') (eqA:=eqke) (eqB:=eqA); auto.
+  unfold eq_key; auto.
+  intros (k1,e1) (k2,e2) (k3,e3). unfold eq_key_elt, eq_key; simpl.
+   intuition eauto.
+  intros (k,e) (k',e'); unfold eq_key; simpl; auto.
   apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
   apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply ForallList2_equiv1 with (eqA:=eqk); try red; eauto.
+  apply NoDupA_rev; try red; eauto. apply elements_3w.
   red; intros.
   do 2 rewrite InA_rev.
   destruct x; do 2 rewrite <- elements_mapsto_iff.
@@ -832,11 +1075,12 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   rewrite H1; split; auto.
   Qed.
 
-  Lemma fold_Add : forall m1 m2 x e (A:Type)(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 -> 
+  Lemma fold_Add :
+   forall m1 m2 x e (A:Type)(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_neqkey eqA f ->
+   ~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).
@@ -850,15 +1094,22 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   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 fold_right_add_restr with
+    (R:=fun p p'=>~eqk p p')(eqA:=eqke)(eqB:=eqA); auto.
+  unfold eq_key; auto.
+  intros (k1,e1) (k2,e2) (k3,e3). unfold eq_key_elt, eq_key; simpl.
+   intuition eauto.
+  unfold f'; intros (k1,e1) (k2,e2); unfold eq_key; simpl; auto.
   apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
   apply NoDupA_rev; auto; apply NoDupA_eqk_eqke; apply elements_3w.
+  apply ForallList2_equiv1 with (eqA:=eqk); try red; eauto.
+  apply NoDupA_rev; try red; eauto. apply elements_3w.
   rewrite InA_rev.
   contradict H1.
   exists e.
   rewrite elements_mapsto_iff; auto.
   intros a.
-  rewrite InA_cons; do 2 rewrite InA_rev; 
+  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.
@@ -871,22 +1122,24 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   elim n; auto.
   Qed.
 
-  Lemma cardinal_fold : forall m : t elt, 
+  (** * Cardinal *)
+
+  Lemma cardinal_fold : forall m : t elt,
    cardinal m = fold (fun _ _ => S) m 0.
   Proof.
   intros; rewrite cardinal_1, fold_1.
   symmetry; apply fold_left_length; auto.
   Qed.
 
-  Lemma cardinal_Empty : forall m : t elt, 
+  Lemma cardinal_Empty : forall m : t elt,
    Empty m <-> cardinal m = 0.
   Proof.
   intros.
   rewrite cardinal_1, elements_Empty.
   destruct (elements m); intuition; discriminate.
   Qed.
- 
-  Lemma Equal_cardinal : forall m m' : t elt, 
+
+  Lemma Equal_cardinal : forall m m' : t elt,
     Equal m m' -> cardinal m = cardinal m'.
   Proof.
   intros; do 2 rewrite cardinal_fold.
@@ -939,27 +1192,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   eauto.
   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 (eq_dec x y); eauto with map.
-  apply X0 with (remove x m) x e; auto with map.
-  apply IHn; auto with map.
-  assert (S n = S (cardinal (remove x m))).
-   rewrite Heqn; eapply cardinal_2; eauto with map.
-  inversion H1; auto with map.
-  Qed.
-
-  (** * Let's emulate some functions not present in the interface *)
+  (** * Emulation of some functions lacking in the interface *)
 
   Definition filter (f : key -> elt -> bool)(m : t elt) := 
    fold (fun k e m => if f k e then add k e m else m) m (empty _).