Introducing MMaps, a modernized FMaps.

 NB: this is work-in-progress, there is currently only one
 provided implementation (MMapWeakList).

 In the same spirit as MSets w.r.t FSets, the main difference between
 MMaps and former FMaps is the use of a new version of OrderedType
 (see Orders.v instead of obsolete OrderedType.v).

 We also try to benefit more from recent notions such as Proper.

 For most function specifications, the style has changed : we now use
 equations over "find" instead of "MapsTo" predicates, whenever possible
 (cf. Maps in Compcert for a source of inspiration). Former specs are
 now derived in FMapFacts, so this is mostly a matter of taste.

 Two changes inspired by the current Maps of OCaml:
 - "elements" is now "bindings"
 - "map2" is now "merge" (and its function argument also receives a key).

 We now use a maximal implicit argument for "empty".

11 files changed, 3697 insertions, 252 deletions

diff --git a/Makefile.common b/Makefile.common
index e54861961..07df8bb15 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -288,6 +288,7 @@ STRINGSVO:=$(call cat_vo_itarget, theories/Strings)
 SETSVO:=$(call cat_vo_itarget, theories/Sets)
 FSETSVO:=$(call cat_vo_itarget, theories/FSets)
 MSETSVO:=$(call cat_vo_itarget, theories/MSets)
+MMAPSVO:=$(call cat_vo_itarget, theories/MMaps)
 RELATIONSVO:=$(call cat_vo_itarget, theories/Relations)
 WELLFOUNDEDVO:=$(call cat_vo_itarget, theories/Wellfounded)
 REALSVO:=$(call cat_vo_itarget, theories/Reals)
@@ -303,7 +304,7 @@ THEORIESVO:=\
   $(RELATIONSVO) $(WELLFOUNDEDVO) $(SETOIDSVO) \
   $(LISTSVO) $(STRINGSVO) \
   $(PARITHVO) $(NARITHVO) $(ZARITHVO) \
-  $(SETSVO) $(FSETSVO) $(MSETSVO) \
+  $(SETSVO) $(FSETSVO) $(MSETSVO) $(MMAPSVO) \
   $(REALSVO)  $(SORTINGVO) $(QARITHVO) \
   $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO)
 
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index b57c3f046..c95fb4d5c 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -613,18 +613,18 @@ induction s1; simpl; auto; intros.
 Qed.
 
 Lemma fold_right_equivlistA_restr2 :
-  forall s s' (i j:B) (heqij: eqB i j),
+  forall s s' i j,
     NoDupA s -> NoDupA s' -> ForallOrdPairs R s ->
-               eqB i j -> 
-  equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s').
+    equivlistA s s' -> eqB i j ->
+    eqB (fold_right f i s) (fold_right f j s').
 Proof.
  simple induction s.
  destruct s'; simpl.
  intros. assumption.
  unfold equivlistA; intros.
- destruct (H3 a).
+ destruct (H2 a).
  assert (InA a nil) by auto; inv.
- intros x l Hrec s' i j heqij N N' F eqij E; simpl in *.
+ intros x l Hrec s' i j N N' F E eqij; simpl in *.
  assert (InA x s') by (rewrite <- (E x); auto).
  destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))).
  subst s'.
@@ -649,7 +649,6 @@ Proof.
      red; intros; rewrite E; auto.
 Qed.
 
-
 Lemma fold_right_add_restr2 :
   forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s ->
   equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)).
diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v
index afc7c25bd..cea3e839f 100644
--- a/theories/Lists/SetoidPermutation.v
+++ b/theories/Lists/SetoidPermutation.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import SetoidList.
+Require Import Permutation SetoidList.
 (* Set Universe Polymorphism. *)
 
 Set Implicit Arguments.
@@ -123,4 +123,76 @@ Proof.
     apply equivlistA_NoDupA_split with x y; intuition.
 Qed.
 
+Lemma Permutation_eqlistA_commute l₁ l₂ l₃ :
+ eqlistA eqA l₁ l₂ -> Permutation l₂ l₃ ->
+ exists l₂', Permutation l₁ l₂' /\ eqlistA eqA l₂' l₃.
+Proof.
+ intros E P. revert l₁ E.
+ induction P; intros.
+ - inversion_clear E. now exists nil.
+ - inversion_clear E.
+   destruct (IHP l0) as (l0',(P',E')); trivial. clear IHP.
+   exists (x0::l0'). split; auto.
+ - inversion_clear E. inversion_clear H0.
+   exists (x1::x0::l1). now repeat constructor.
+ - clear P1 P2.
+   destruct (IHP1 _ E) as (l₁',(P₁,E₁)).
+   destruct (IHP2 _ E₁) as (l₂',(P₂,E₂)).
+   exists l₂'. split; trivial. econstructor; eauto.
+Qed.
+
+Lemma PermutationA_decompose l₁ l₂ :
+ PermutationA l₁ l₂ ->
+ exists l, Permutation l₁ l /\ eqlistA eqA l l₂.
+Proof.
+ induction 1.
+ - now exists nil.
+ - destruct IHPermutationA as (l,(P,E)). exists (x₁::l); auto.
+ - exists (x::y::l). split. constructor. reflexivity.
+ - destruct IHPermutationA1 as (l₁',(P,E)).
+   destruct IHPermutationA2 as (l₂',(P',E')).
+   destruct (@Permutation_eqlistA_commute l₁' l₂ l₂') as (l₁'',(P'',E''));
+    trivial.
+   exists l₁''. split. now transitivity l₁'. now transitivity l₂'.
+Qed.
+
+Lemma Permutation_PermutationA l₁ l₂ :
+ Permutation l₁ l₂ -> PermutationA l₁ l₂.
+Proof.
+ induction 1.
+ - constructor.
+ - now constructor.
+ - apply permA_swap.
+ - econstructor; eauto.
+Qed.
+
+Lemma eqlistA_PermutationA l₁ l₂ :
+ eqlistA eqA l₁ l₂ -> PermutationA l₁ l₂.
+Proof.
+ induction 1; now constructor.
+Qed.
+
+Lemma NoDupA_equivlistA_decompose l1 l2 :
+  NoDupA eqA l1 -> NoDupA eqA l2 -> equivlistA eqA l1 l2 ->
+  exists l, Permutation l1 l /\ eqlistA eqA l l2.
+Proof.
+ intros. apply PermutationA_decompose.
+ now apply NoDupA_equivlistA_PermutationA.
+Qed.
+
+Lemma PermutationA_preserves_NoDupA l₁ l₂ :
+ PermutationA l₁ l₂ -> NoDupA eqA l₁ -> NoDupA eqA l₂.
+Proof.
+ induction 1; trivial.
+ - inversion_clear 1; constructor; auto.
+   apply PermutationA_equivlistA in H0. contradict H2.
+   now rewrite H, H0.
+ - inversion_clear 1. inversion_clear H1. constructor.
+   + contradict H. inversion_clear H; trivial.
+     elim H0. now constructor.
+   + constructor; trivial.
+     contradict H0. now apply InA_cons_tl.
+ - eauto.
+Qed.
+
 End Permutation.
diff --git a/theories/MMaps/MMapFacts.v b/theories/MMaps/MMapFacts.v
new file mode 100644
index 000000000..69066a7b6
--- /dev/null
+++ b/theories/MMaps/MMapFacts.v
@@ -0,0 +1,2434 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(** * Finite maps library *)
+
+(** This functor derives additional facts from [MMapInterface.S]. These
+  facts are mainly the specifications of [MMapInterface.S] written using
+  different styles: equivalence and boolean equalities.
+*)
+
+Require Import Bool Equalities Orders OrdersFacts OrdersLists.
+Require Import Morphisms Permutation SetoidPermutation.
+Require Export MMapInterface.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Lemma eq_bool_alt b b' : b=b' <-> (b=true <-> b'=true).
+Proof.
+ destruct b, b'; intuition.
+Qed.
+
+Lemma eq_option_alt {elt}(o o':option elt) :
+ o=o' <-> (forall e, o=Some e <-> o'=Some e).
+Proof.
+split; intros.
+- now subst.
+- destruct o, o'; rewrite ?H; auto.
+  symmetry; now apply H.
+Qed.
+
+Lemma option_map_some {A B}(f:A->B) o :
+ option_map f o <> None <-> o <> None.
+Proof.
+ destruct o; simpl. now split. split; now destruct 1.
+Qed.
+
+(** * Properties about weak maps *)
+
+Module WProperties_fun (E:DecidableType)(Import M:WSfun E).
+
+Definition Empty {elt}(m : t elt) := forall x e, ~MapsTo x e m.
+
+(** A few things about E.eq *)
+
+Lemma eq_refl x : E.eq x x. Proof. apply E.eq_equiv. Qed.
+Lemma eq_sym x y : E.eq x y -> E.eq y x. Proof. apply E.eq_equiv. Qed.
+Lemma eq_trans x y z : E.eq x y -> E.eq y z -> E.eq x z.
+Proof. apply E.eq_equiv. Qed.
+Hint Immediate eq_refl eq_sym : map.
+Hint Resolve eq_trans eq_equivalence E.eq_equiv : map.
+
+Definition eqb x y := if E.eq_dec x y then true else false.
+
+Lemma eqb_eq x y : eqb x y = true <-> E.eq x y.
+Proof.
+ unfold eqb; case E.eq_dec; now intuition.
+Qed.
+
+Lemma eqb_sym x y : eqb x y = eqb y x.
+Proof.
+ apply eq_bool_alt. rewrite !eqb_eq. split; apply E.eq_equiv.
+Qed.
+
+(** Initial results about MapsTo and In *)
+
+Lemma mapsto_fun {elt} m x (e e':elt) :
+  MapsTo x e m -> MapsTo x e' m -> e=e'.
+Proof.
+rewrite <- !find_spec. congruence.
+Qed.
+
+Lemma in_find {elt} (m : t elt) x : In x m <-> find x m <> None.
+Proof.
+ unfold In. split.
+ - intros (e,H). rewrite <-find_spec in H. congruence.
+ - destruct (find x m) as [e|] eqn:H.
+   + exists e. now apply find_spec.
+   + now destruct 1.
+Qed.
+
+Lemma not_in_find {elt} (m : t elt) x : ~In x m <-> find x m = None.
+Proof.
+ rewrite in_find. split; auto.
+ intros; destruct (find x m); trivial. now destruct H.
+Qed.
+
+Notation in_find_iff := in_find (only parsing).
+Notation not_find_in_iff := not_in_find (only parsing).
+
+(** * [Equal] is a setoid equality. *)
+
+Infix "==" := Equal (at level 30).
+
+Lemma Equal_refl {elt} (m : t elt) : m == m.
+Proof. red; reflexivity. Qed.
+
+Lemma Equal_sym {elt} (m m' : t elt) : m == m' -> m' == m.
+Proof. unfold Equal; auto. Qed.
+
+Lemma Equal_trans {elt} (m m' m'' : t elt) :
+ m == m' -> m' == m'' -> m == m''.
+Proof. unfold Equal; congruence. Qed.
+
+Instance Equal_equiv {elt} : Equivalence (@Equal elt).
+Proof.
+constructor; [exact Equal_refl | exact Equal_sym | exact Equal_trans].
+Qed.
+
+Arguments Equal {elt} m m'.
+
+Instance MapsTo_m {elt} :
+  Proper (E.eq==>Logic.eq==>Equal==>iff) (@MapsTo elt).
+Proof.
+intros k k' Hk e e' <- m m' Hm. rewrite <- Hk.
+now rewrite <- !find_spec, Hm.
+Qed.
+
+Instance In_m {elt} :
+  Proper (E.eq==>Equal==>iff) (@In elt).
+Proof.
+intros k k' Hk m m' Hm. unfold In.
+split; intros (e,H); exists e; revert H;
+ now rewrite Hk, <- !find_spec, Hm.
+Qed.
+
+Instance find_m {elt} : Proper (E.eq==>Equal==>Logic.eq) (@find elt).
+Proof.
+intros k k' Hk m m' <-.
+rewrite eq_option_alt. intros. now rewrite !find_spec, Hk.
+Qed.
+
+Instance mem_m {elt} : Proper (E.eq==>Equal==>Logic.eq) (@mem elt).
+Proof.
+intros k k' Hk m m' Hm. now rewrite eq_bool_alt, !mem_spec, Hk, Hm.
+Qed.
+
+Instance Empty_m {elt} : Proper (Equal==>iff) (@Empty elt).
+Proof.
+intros m m' Hm. unfold Empty. now setoid_rewrite Hm.
+Qed.
+
+Instance is_empty_m {elt} : Proper (Equal ==> Logic.eq) (@is_empty elt).
+Proof.
+intros m m' Hm. rewrite eq_bool_alt, !is_empty_spec.
+ now setoid_rewrite Hm.
+Qed.
+
+Instance add_m {elt} : Proper (E.eq==>Logic.eq==>Equal==>Equal) (@add elt).
+Proof.
+intros k k' Hk e e' <- m m' Hm y.
+destruct (E.eq_dec k y) as [H|H].
+- rewrite <-H, add_spec1. now rewrite Hk, add_spec1.
+- rewrite !add_spec2; trivial. now rewrite <- Hk.
+Qed.
+
+Instance remove_m {elt} : Proper (E.eq==>Equal==>Equal) (@remove elt).
+Proof.
+intros k k' Hk m m' Hm y.
+destruct (E.eq_dec k y) as [H|H].
+- rewrite <-H, remove_spec1. now rewrite Hk, remove_spec1.
+- rewrite !remove_spec2; trivial. now rewrite <- Hk.
+Qed.
+
+Instance map_m {elt elt'} :
+  Proper ((Logic.eq==>Logic.eq)==>Equal==>Equal) (@map elt elt').
+Proof.
+intros f f' Hf m m' Hm y. rewrite !map_spec, Hm.
+destruct (find y m'); simpl; trivial. f_equal. now apply Hf.
+Qed.
+
+Instance mapi_m {elt elt'} :
+  Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Equal) (@mapi elt elt').
+Proof.
+intros f f' Hf m m' Hm y.
+destruct (mapi_spec f m y) as (x,(Hx,->)).
+destruct (mapi_spec f' m' y) as (x',(Hx',->)).
+rewrite <- Hm. destruct (find y m); trivial. simpl.
+f_equal. apply Hf; trivial. now rewrite Hx, Hx'.
+Qed.
+
+Instance merge_m {elt elt' elt''} :
+ Proper ((E.eq==>Logic.eq==>Logic.eq==>Logic.eq)==>Equal==>Equal==>Equal)
+  (@merge elt elt' elt'').
+Proof.
+intros f f' Hf m1 m1' Hm1 m2 m2' Hm2 y.
+destruct (find y m1) as [e1|] eqn:H1.
+- apply find_spec in H1.
+  assert (H : In y m1 \/ In y m2) by (left; now exists e1).
+  destruct (merge_spec1 f H) as (y1,(Hy1,->)).
+  rewrite Hm1,Hm2 in H.
+  destruct (merge_spec1 f' H) as (y2,(Hy2,->)).
+  rewrite <- Hm1, <- Hm2. apply Hf; trivial. now transitivity y.
+- destruct (find y m2) as [e2|] eqn:H2.
+  + apply find_spec in H2.
+    assert (H : In y m1 \/ In y m2) by (right; now exists e2).
+    destruct (merge_spec1 f H) as (y1,(Hy1,->)).
+    rewrite Hm1,Hm2 in H.
+    destruct (merge_spec1 f' H) as (y2,(Hy2,->)).
+    rewrite <- Hm1, <- Hm2. apply Hf; trivial. now transitivity y.
+  + apply not_in_find in H1. apply not_in_find in H2.
+    assert (H : ~In y (merge f m1 m2)).
+    { intro H. apply merge_spec2 in H. intuition. }
+    apply not_in_find in H. rewrite H.
+    symmetry. apply not_in_find. intro H'.
+    apply merge_spec2 in H'. rewrite <- Hm1, <- Hm2 in H'.
+    intuition.
+Qed.
+
+(* Later: compatibility for cardinal, fold, ... *)
+
+(** ** Earlier specifications (cf. FMaps) *)
+
+Section OldSpecs.
+Variable elt: Type.
+Implicit Type m: t elt.
+Implicit Type x y z: key.
+Implicit Type e: elt.
+
+Lemma MapsTo_1 m x y e : E.eq x y -> MapsTo x e m -> MapsTo y e m.
+Proof.
+ now intros ->.
+Qed.
+
+Lemma find_1 m x e : MapsTo x e m -> find x m = Some e.
+Proof. apply find_spec. Qed.
+
+Lemma find_2 m x e : find x m = Some e -> MapsTo x e m.
+Proof. apply find_spec. Qed.
+
+Lemma mem_1 m x : In x m -> mem x m = true.
+Proof. apply mem_spec. Qed.
+
+Lemma mem_2 m x : mem x m = true -> In x m.
+Proof. apply mem_spec. Qed.
+
+Lemma empty_1 : Empty (@empty elt).
+Proof.
+ intros x e. now rewrite <- find_spec, empty_spec.
+Qed.
+
+Lemma is_empty_1 m : Empty m -> is_empty m = true.
+Proof.
+ unfold Empty; rewrite is_empty_spec. setoid_rewrite <- find_spec.
+ intros H x. specialize (H x).
+ destruct (find x m) as [e|]; trivial.
+ now destruct (H e).
+Qed.
+
+Lemma is_empty_2 m : is_empty m = true -> Empty m.
+Proof.
+ rewrite is_empty_spec. intros H x e. now rewrite <- find_spec, H.
+Qed.
+
+Lemma add_1 m x y e : E.eq x y -> MapsTo y e (add x e m).
+Proof.
+ intros <-. rewrite <-find_spec. apply add_spec1.
+Qed.
+
+Lemma add_2 m x y e e' :
+  ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
+Proof.
+ intro. now rewrite <- !find_spec, add_spec2.
+Qed.
+
+Lemma add_3 m x y e e' :
+  ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
+Proof.
+ intro. rewrite <- !find_spec, add_spec2; trivial.
+Qed.
+
+Lemma remove_1 m x y : E.eq x y -> ~ In y (remove x m).
+Proof.
+ intros <-. apply not_in_find. apply remove_spec1.
+Qed.
+
+Lemma remove_2 m x y e :
+  ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
+Proof.
+ intro. now rewrite <- !find_spec, remove_spec2.
+Qed.
+
+Lemma remove_3bis m x y e :
+  find y (remove x m) = Some e -> find y m = Some e.
+Proof.
+ destruct (E.eq_dec x y) as [<-|H].
+ - now rewrite remove_spec1.
+ - now rewrite remove_spec2.
+Qed.
+
+Lemma remove_3 m x y e : MapsTo y e (remove x m) -> MapsTo y e m.
+Proof.
+ rewrite <-!find_spec. apply remove_3bis.
+Qed.
+
+Lemma bindings_1 m x e :
+  MapsTo x e m -> InA eq_key_elt (x,e) (bindings m).
+Proof. apply bindings_spec1. Qed.
+
+Lemma bindings_2 m x e :
+  InA eq_key_elt (x,e) (bindings m) -> MapsTo x e m.
+Proof. apply bindings_spec1. Qed.
+
+Lemma bindings_3w m : NoDupA eq_key (bindings m).
+Proof. apply bindings_spec2w. Qed.
+
+Lemma cardinal_1 m : cardinal m = length (bindings m).
+Proof. apply cardinal_spec. Qed.
+
+Lemma fold_1 m (A : Type) (i : A) (f : key -> elt -> A -> A) :
+  fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i.
+Proof. apply fold_spec. Qed.
+
+Lemma equal_1 m m' cmp : Equivb cmp m m' -> equal cmp m m' = true.
+Proof. apply equal_spec. Qed.
+
+Lemma equal_2 m m' cmp : equal cmp m m' = true -> Equivb cmp m m'.
+Proof. apply equal_spec. Qed.
+
+End OldSpecs.
+
+Lemma map_1 {elt elt'}(m: t elt)(x:key)(e:elt)(f:elt->elt') :
+  MapsTo x e m -> MapsTo x (f e) (map f m).
+Proof.
+ rewrite <- !find_spec, map_spec. now intros ->.
+Qed.
+
+Lemma map_2 {elt elt'}(m: t elt)(x:key)(f:elt->elt') :
+  In x (map f m) -> In x m.
+Proof.
+ rewrite !in_find, map_spec. apply option_map_some.
+Qed.
+
+Lemma mapi_1 {elt elt'}(m: t elt)(x:key)(e:elt)(f:key->elt->elt') :
+  MapsTo x e m ->
+  exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
+Proof.
+ destruct (mapi_spec f m x) as (y,(Hy,Eq)).
+ intro H. exists y; split; trivial.
+ rewrite <-find_spec in *. now rewrite Eq, H.
+Qed.
+
+Lemma mapi_2 {elt elt'}(m: t elt)(x:key)(f:key->elt->elt') :
+  In x (mapi f m) -> In x m.
+Proof.
+ destruct (mapi_spec f m x) as (y,(Hy,Eq)).
+ rewrite !in_find. intro H; contradict H. now rewrite Eq, H.
+Qed.
+
+(** The ancestor [map2] of the current [merge] was dealing with functions
+    on datas only, not on keys. *)
+
+Definition map2 {elt elt' elt''} (f:option elt->option elt'->option elt'')
+ := merge (fun _ => f).
+
+Lemma map2_1 {elt elt' elt''}(m: t elt)(m': t elt')
+      (x:key)(f:option elt->option elt'->option elt'') :
+  In x m \/ In x m' ->
+  find x (map2 f m m') = f (find x m) (find x m').
+Proof.
+ intros. unfold map2.
+ now destruct (merge_spec1 (fun _ => f) H) as (y,(_,->)).
+Qed.
+
+Lemma map2_2 {elt elt' elt''}(m: t elt)(m': t elt')
+      (x:key)(f:option elt->option elt'->option elt'') :
+  In x (map2 f m m') -> In x m \/ In x m'.
+Proof. apply merge_spec2. Qed.
+
+Hint Immediate MapsTo_1 mem_2 is_empty_2
+     map_2 mapi_2 add_3 remove_3 find_2 : map.
+Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1
+     remove_2 find_1 fold_1 map_1 mapi_1 mapi_2 : map.
+
+(** ** Specifications written using equivalences *)
+
+Section IffSpec.
+Variable elt: Type.
+Implicit Type m: t elt.
+Implicit Type x y z: key.
+Implicit Type e: elt.
+
+Lemma in_iff m x y : E.eq x y -> (In x m <-> In y m).
+Proof. now intros ->. Qed.
+
+Lemma mapsto_iff m x y e : E.eq x y -> (MapsTo x e m <-> MapsTo y e m).
+Proof. now intros ->. Qed.
+
+Lemma mem_in_iff m x : In x m <-> mem x m = true.
+Proof. symmetry. apply mem_spec. Qed.
+
+Lemma not_mem_in_iff m x : ~In x m <-> mem x m = false.
+Proof.
+rewrite mem_in_iff; destruct (mem x m); intuition.
+Qed.
+
+Lemma mem_find m x : mem x m = true <-> find x m <> None.
+Proof.
+ rewrite <- mem_in_iff. apply in_find.
+Qed.
+
+Lemma not_mem_find m x : mem x m = false <-> find x m = None.
+Proof.
+ rewrite <- not_mem_in_iff. apply not_in_find.
+Qed.
+
+Lemma In_dec m x : { In x m } + { ~ In x m }.
+Proof.
+ generalize (mem_in_iff m x).
+ destruct (mem x m); [left|right]; intuition.
+Qed.
+
+Lemma find_mapsto_iff m x e : MapsTo x e m <-> find x m = Some e.
+Proof. symmetry. apply find_spec. Qed.
+
+Lemma equal_iff m m' cmp : Equivb cmp m m' <-> equal cmp m m' = true.
+Proof. symmetry. apply equal_spec. Qed.
+
+Lemma empty_mapsto_iff x e : MapsTo x e empty <-> False.
+Proof.
+rewrite <- find_spec, empty_spec. now split.
+Qed.
+
+Lemma not_in_empty x : ~In x (@empty elt).
+Proof.
+intros (e,H). revert H. apply empty_mapsto_iff.
+Qed.
+
+Lemma empty_in_iff x : In x (@empty elt) <-> False.
+Proof.
+split; [ apply not_in_empty | destruct 1 ].
+Qed.
+
+Lemma is_empty_iff m : Empty m <-> is_empty m = true.
+Proof. split; [apply is_empty_1 | apply is_empty_2 ]. Qed.
+
+Lemma add_mapsto_iff m x y e e' :
+  MapsTo y e' (add x e m) <->
+     (E.eq x y /\ e=e') \/
+     (~E.eq x y /\ MapsTo y e' m).
+Proof.
+split.
+- intros H. destruct (E.eq_dec x y); [left|right]; split; trivial.
+  + symmetry. apply (mapsto_fun H); auto with map.
+  + now apply add_3 with x e.
+- destruct 1 as [(H,H')|(H,H')]; subst; auto with map.
+Qed.
+
+Lemma add_mapsto_new m x y e e' : ~In x m ->
+  MapsTo y e' (add x e m) <-> (E.eq x y /\ e=e') \/ MapsTo y e' m.
+Proof.
+ intros.
+ rewrite add_mapsto_iff. intuition.
+ right; split; trivial. contradict H. exists e'. now rewrite H.
+Qed.
+
+Lemma in_add m x y e : In y m -> In y (add x e m).
+Proof.
+ destruct (E.eq_dec x y) as [<-|H'].
+ - now rewrite !in_find, add_spec1.
+ - now rewrite !in_find, add_spec2.
+Qed.
+
+Lemma add_in_iff m x y e : In y (add x e m) <-> E.eq x y \/ In y m.
+Proof.
+split.
+- intros H. destruct (E.eq_dec x y); [now left|right].
+  rewrite in_find, add_spec2 in H; trivial. now apply in_find.
+- intros [<-|H].
+  + exists e. now apply add_1.
+  + now apply in_add.
+Qed.
+
+Lemma add_neq_mapsto_iff m x y e e' :
+ ~ E.eq x y -> (MapsTo y e' (add x e m) <-> MapsTo y e' m).
+Proof.
+split; [apply add_3|apply add_2]; auto.
+Qed.
+
+Lemma add_neq_in_iff m x y e :
+ ~ E.eq x y -> (In y (add x e m)  <-> In y m).
+Proof.
+split; intros (e',H0); exists e'.
+- now apply add_3 with x e.
+- now apply add_2.
+Qed.
+
+Lemma remove_mapsto_iff m x y e :
+  MapsTo y e (remove x m) <-> ~E.eq x y /\ MapsTo y e m.
+Proof.
+split; [split|destruct 1].
+- intro E. revert H. now rewrite <-E, <- find_spec, remove_spec1.
+- now apply remove_3 with x.
+- now apply remove_2.
+Qed.
+
+Lemma remove_in_iff m x y : In y (remove x m) <-> ~E.eq x y /\ In y m.
+Proof.
+unfold In; split; [ intros (e,H) | intros (E,(e,H)) ].
+- apply remove_mapsto_iff in H. destruct H; split; trivial.
+  now exists e.
+- exists e. now apply remove_2.
+Qed.
+
+Lemma remove_neq_mapsto_iff : forall m x y e,
+ ~ E.eq x y -> (MapsTo y e (remove x m)  <-> MapsTo y e m).
+Proof.
+split; [apply remove_3|apply remove_2]; auto.
+Qed.
+
+Lemma remove_neq_in_iff : forall m x y,
+ ~ E.eq x y -> (In y (remove x m) <-> In y m).
+Proof.
+split; intros (e',H0); exists e'.
+- now apply remove_3 with x.
+- now apply remove_2.
+Qed.
+
+Lemma bindings_mapsto_iff m x e :
+ MapsTo x e m <-> InA eq_key_elt (x,e) (bindings m).
+Proof. symmetry. apply bindings_spec1. Qed.
+
+Lemma bindings_in_iff m x :
+ In x m <-> exists e, InA eq_key_elt (x,e) (bindings m).
+Proof.
+unfold In; split; intros (e,H); exists e; now apply bindings_spec1.
+Qed.
+
+End IffSpec.
+
+Lemma map_mapsto_iff {elt elt'} m x b (f : elt -> elt') :
+ MapsTo x b (map f m) <-> exists a, b = f a /\ MapsTo x a m.
+Proof.
+rewrite <-find_spec, map_spec. setoid_rewrite <- find_spec.
+destruct (find x m); simpl; split.
+- injection 1. now exists e.
+- intros (a,(->,H)). now injection H as ->.
+- discriminate.
+- intros (a,(_,H)); discriminate.
+Qed.
+
+Lemma map_in_iff {elt elt'} m x (f : elt -> elt') :
+ In x (map f m) <-> In x m.
+Proof.
+rewrite !in_find, map_spec. apply option_map_some.
+Qed.
+
+Lemma mapi_in_iff {elt elt'} m x (f:key->elt->elt') :
+ In x (mapi f m) <-> In x m.
+Proof.
+rewrite !in_find. destruct (mapi_spec f m x) as (y,(_,->)).
+apply option_map_some.
+Qed.
+
+(** Unfortunately, we don't have simple equivalences for [mapi]
+  and [MapsTo]. The only correct one needs compatibility of [f]. *)
+
+Lemma mapi_inv {elt elt'} m x b (f : key -> elt -> elt') :
+ MapsTo x b (mapi f m) ->
+ exists a y, E.eq y x /\ b = f y a /\ MapsTo x a m.
+Proof.
+rewrite <- find_spec. setoid_rewrite <- find_spec.
+destruct (mapi_spec f m x) as (y,(E,->)).
+destruct (find x m); simpl.
+- injection 1 as <-. now exists e, y.
+- discriminate.
+Qed.
+
+Lemma mapi_spec' {elt elt'} (f:key->elt->elt') :
+ Proper (E.eq==>Logic.eq==>Logic.eq) f ->
+ forall m x,
+   find x (mapi f m) = option_map (f x) (find x m).
+Proof.
+ intros. destruct (mapi_spec f m x) as (y,(Hy,->)).
+ destruct (find x m); simpl; trivial.
+ now rewrite Hy.
+Qed.
+
+Lemma mapi_1bis {elt elt'} m x e (f:key->elt->elt') :
+ Proper (E.eq==>Logic.eq==>Logic.eq) f ->
+ MapsTo x e m -> MapsTo x (f x e) (mapi f m).
+Proof.
+intros. destruct (mapi_1 f H0) as (y,(->,H2)). trivial.
+Qed.
+
+Lemma mapi_mapsto_iff {elt elt'} m x b (f:key->elt->elt') :
+ Proper (E.eq==>Logic.eq==>Logic.eq) f ->
+ (MapsTo x b (mapi f m) <-> exists a, b = f x a /\ MapsTo x a m).
+Proof.
+rewrite <-find_spec. setoid_rewrite <-find_spec.
+intros Pr. rewrite mapi_spec' by trivial.
+destruct (find x m); simpl; split.
+- injection 1 as <-. now exists e.
+- intros (a,(->,H)). now injection H as <-.
+- discriminate.
+- intros (a,(_,H)). discriminate.
+Qed.
+
+(** Things are even worse for [merge] : we don't try to state any
+ equivalence, see instead boolean results below. *)
+
+(** Useful tactic for simplifying expressions like
+   [In y (add x e (remove z m))] *)
+
+Ltac map_iff :=
+ repeat (progress (
+  rewrite add_mapsto_iff || rewrite add_in_iff ||
+  rewrite remove_mapsto_iff || rewrite remove_in_iff ||
+  rewrite empty_mapsto_iff || rewrite empty_in_iff ||
+  rewrite map_mapsto_iff || rewrite map_in_iff ||
+  rewrite mapi_in_iff)).
+
+(** ** Specifications written using boolean predicates *)
+
+Section BoolSpec.
+
+Lemma mem_find_b {elt}(m:t elt)(x:key) :
+  mem x m = if find x m then true else false.
+Proof.
+apply eq_bool_alt. rewrite mem_find. destruct (find x m).
+- now split.
+- split; (discriminate || now destruct 1).
+Qed.
+
+Variable elt elt' elt'' : Type.
+Implicit Types m : t elt.
+Implicit Types x y z : key.
+Implicit Types e : elt.
+
+Lemma mem_b m x y : E.eq x y -> mem x m = mem y m.
+Proof. now intros ->. Qed.
+
+Lemma find_o m x y : E.eq x y -> find x m = find y m.
+Proof. now intros ->. Qed.
+
+Lemma empty_o x : find x (@empty elt) = None.
+Proof. apply empty_spec. Qed.
+
+Lemma empty_a x : mem x (@empty elt) = false.
+Proof. apply not_mem_find. apply empty_spec. Qed.
+
+Lemma add_eq_o m x y e :
+ E.eq x y -> find y (add x e m) = Some e.
+Proof.
+ intros <-. apply add_spec1.
+Qed.
+
+Lemma add_neq_o m x y e :
+ ~ E.eq x y -> find y (add x e m) = find y m.
+Proof. apply add_spec2. Qed.
+Hint Resolve add_neq_o : map.
+
+Lemma add_o m x y e :
+ find y (add x e m) = if E.eq_dec x y then Some e else find y m.
+Proof.
+destruct (E.eq_dec x y); auto with map.
+Qed.
+
+Lemma add_eq_b m x y e :
+ E.eq x y -> mem y (add x e m) = true.
+Proof.
+intros <-. apply mem_spec, add_in_iff. now left.
+Qed.
+
+Lemma add_neq_b m x y e :
+ ~E.eq x y -> mem y (add x e m) = mem y m.
+Proof.
+intros. now rewrite !mem_find_b, add_neq_o.
+Qed.
+
+Lemma add_b m x y e :
+ mem y (add x e m) = eqb x y || mem y m.
+Proof.
+rewrite !mem_find_b, add_o. unfold eqb.
+now destruct (E.eq_dec x y).
+Qed.
+
+Lemma remove_eq_o m x y :
+ E.eq x y -> find y (remove x m) = None.
+Proof. intros ->. apply remove_spec1. Qed.
+
+Lemma remove_neq_o m x y :
+ ~ E.eq x y -> find y (remove x m) = find y m.
+Proof. apply remove_spec2. Qed.
+
+Hint Resolve remove_eq_o remove_neq_o : map.
+
+Lemma remove_o m x y :
+ find y (remove x m) = if E.eq_dec x y then None else find y m.
+Proof.
+destruct (E.eq_dec x y); auto with map.
+Qed.
+
+Lemma remove_eq_b m x y :
+ E.eq x y -> mem y (remove x m) = false.
+Proof.
+intros <-. now rewrite mem_find_b, remove_eq_o.
+Qed.
+
+Lemma remove_neq_b m x y :
+ ~ E.eq x y -> mem y (remove x m) = mem y m.
+Proof.
+intros. now rewrite !mem_find_b, remove_neq_o.
+Qed.
+
+Lemma remove_b m x y :
+ mem y (remove x m) = negb (eqb x y) && mem y m.
+Proof.
+rewrite !mem_find_b, remove_o; unfold eqb.
+now destruct (E.eq_dec x y).
+Qed.
+
+Lemma map_o m x (f:elt->elt') :
+ find x (map f m) = option_map f (find x m).
+Proof. apply map_spec. Qed.
+
+Lemma map_b m x (f:elt->elt') :
+ mem x (map f m) = mem x m.
+Proof.
+rewrite !mem_find_b, map_o. now destruct (find x m).
+Qed.
+
+Lemma mapi_b m x (f:key->elt->elt') :
+ mem x (mapi f m) = mem x m.
+Proof.
+apply eq_bool_alt; rewrite !mem_spec. apply mapi_in_iff.
+Qed.
+
+Lemma mapi_o m x (f:key->elt->elt') :
+ Proper (E.eq==>Logic.eq==>Logic.eq) f ->
+ find x (mapi f m) = option_map (f x) (find x m).
+Proof. intros; now apply mapi_spec'. Qed.
+
+Lemma merge_spec1' (f:key->option elt->option elt'->option elt'') :
+ Proper (E.eq==>Logic.eq==>Logic.eq==>Logic.eq) f ->
+ forall (m:t elt)(m':t elt') x,
+   In x m \/ In x m' ->
+   find x (merge f m m') = f x (find x m) (find x m').
+Proof.
+ intros Hf m m' x H.
+ now destruct (merge_spec1 f H) as (y,(->,->)).
+Qed.
+
+Lemma merge_spec1_none (f:key->option elt->option elt'->option elt'') :
+ (forall x, f x None None = None) ->
+ forall (m: t elt)(m': t elt') x,
+ exists y, E.eq y x /\ find x (merge f m m') = f y (find x m) (find x m').
+Proof.
+intros Hf m m' x.
+destruct (find x m) as [e|] eqn:Hm.
+- assert (H : In x m \/ In x m') by (left; exists e; now apply find_spec).
+  destruct (merge_spec1 f H) as (y,(Hy,->)).
+  exists y; split; trivial. now rewrite Hm.
+- destruct (find x m') as [e|] eqn:Hm'.
+  + assert (H : In x m \/ In x m') by (right; exists e; now apply find_spec).
+    destruct (merge_spec1 f H) as (y,(Hy,->)).
+    exists y; split; trivial. now rewrite Hm, Hm'.
+  + exists x. split. reflexivity. rewrite Hf.
+    apply not_in_find. intro H.
+    apply merge_spec2 in H. apply not_in_find in Hm. apply not_in_find in Hm'.
+    intuition.
+Qed.
+
+Lemma merge_spec1'_none (f:key->option elt->option elt'->option elt'') :
+ Proper (E.eq==>Logic.eq==>Logic.eq==>Logic.eq) f ->
+ (forall x, f x None None = None) ->
+ forall (m: t elt)(m': t elt') x,
+  find x (merge f m m') = f x (find x m) (find x m').
+Proof.
+ intros Hf Hf' m m' x.
+ now destruct (merge_spec1_none Hf' m m' x) as (y,(->,->)).
+Qed.
+
+Lemma bindings_o : forall m x,
+ find x m = findA (eqb x) (bindings m).
+Proof.
+intros. rewrite eq_option_alt. intro e.
+rewrite <- find_mapsto_iff, bindings_mapsto_iff.
+unfold eqb.
+rewrite <- findA_NoDupA; dintuition; try apply bindings_3w; eauto.
+Qed.
+
+Lemma bindings_b : forall m x,
+ mem x m = existsb (fun p => eqb x (fst p)) (bindings m).
+Proof.
+intros.
+apply eq_bool_alt.
+rewrite mem_spec, bindings_in_iff, existsb_exists.
+split.
+- intros (e,H).
+  rewrite InA_alt in H.
+  destruct H as ((k,e'),((H1,H2),H')); simpl in *; subst e'.
+  exists (k, e); split; trivial. simpl. now apply eqb_eq.
+- intros ((k,e),(H,H')); simpl in *. apply eqb_eq in H'.
+  exists e. rewrite InA_alt. exists (k,e). now repeat split.
+Qed.
+
+End BoolSpec.
+
+Section Equalities.
+Variable elt:Type.
+
+(** A few basic equalities *)
+
+Lemma eq_empty (m: t elt) : m == empty <-> is_empty m = true.
+Proof.
+ unfold Equal. rewrite is_empty_spec. now setoid_rewrite empty_spec.
+Qed.
+
+Lemma add_id (m: t elt) x e : add x e m == m <-> find x m = Some e.
+Proof.
+ split.
+ - intros H. rewrite <- (H x). apply add_spec1.
+ - intros H y. rewrite !add_o. now destruct E.eq_dec as [<-|E].
+Qed.
+
+Lemma add_add_1 (m: t elt) x e :
+ add x e (add x e m) == add x e m.
+Proof.
+ intros y. rewrite !add_o. destruct E.eq_dec; auto.
+Qed.
+
+Lemma add_add_2 (m: t elt) x x' e e' :
+ ~E.eq x x' -> add x e (add x' e' m) == add x' e' (add x e m).
+Proof.
+ intros H y. rewrite !add_o.
+ do 2 destruct E.eq_dec; auto.
+ elim H. now transitivity y.
+Qed.
+
+Lemma remove_id (m: t elt) x : remove x m == m <-> ~In x m.
+Proof.
+ rewrite not_in_find. split.
+ - intros H. rewrite <- (H x). apply remove_spec1.
+ - intros H y. rewrite !remove_o. now destruct E.eq_dec as [<-|E].
+Qed.
+
+Lemma remove_remove_1 (m: t elt) x :
+ remove x (remove x m) == remove x m.
+Proof.
+ intros y. rewrite !remove_o. destruct E.eq_dec; auto.
+Qed.
+
+Lemma remove_remove_2 (m: t elt) x x' :
+ remove x (remove x' m) == remove x' (remove x m).
+Proof.
+ intros y. rewrite !remove_o. do 2 destruct E.eq_dec; auto.
+Qed.
+
+Lemma remove_add_1 (m: t elt) x e :
+  remove x (add x e m) == remove x m.
+Proof.
+ intro y. rewrite !remove_o, !add_o. now destruct E.eq_dec.
+Qed.
+
+Lemma remove_add_2 (m: t elt) x x' e :
+  ~E.eq x x' -> remove x' (add x e m) == add x e (remove x' m).
+Proof.
+ intros H y. rewrite !remove_o, !add_o.
+ do 2 destruct E.eq_dec; auto.
+ - elim H; now transitivity y.
+ - symmetry. now apply remove_eq_o.
+ - symmetry. now apply remove_neq_o.
+Qed.
+
+Lemma add_remove_1 (m: t elt) x e :
+  add x e (remove x m) == add x e m.
+Proof.
+ intro y. rewrite !add_o, !remove_o. now destruct E.eq_dec.
+Qed.
+
+(** Another characterisation of [Equal] *)
+
+Lemma Equal_mapsto_iff : forall m1 m2 : t elt,
+ 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),
+  m == m' <-> Equiv Logic.eq m m'.
+Proof.
+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]
+    are related. *)
+
+Section Cmp.
+Variable eq_elt : elt->elt->Prop.
+Variable cmp : elt->elt->bool.
+
+Definition compat_cmp :=
+ forall e e', cmp e e' = true <-> eq_elt e e'.
+
+Lemma Equiv_Equivb : compat_cmp ->
+ forall m m', Equiv eq_elt m m' <-> Equivb cmp m m'.
+Proof.
+ unfold Equivb, Equiv, Cmp; intuition.
+ red in H; rewrite H; eauto.
+ red in H; rewrite <-H; eauto.
+Qed.
+End Cmp.
+
+(** Composition of the two last results: relation between [Equal]
+    and [Equivb]. *)
+
+Lemma Equal_Equivb : forall cmp,
+ (forall e e', cmp e e' = true <-> e = e') ->
+ forall (m m':t elt), m == m' <-> Equivb cmp m m'.
+Proof.
+ intros; rewrite Equal_Equiv.
+ apply Equiv_Equivb; auto.
+Qed.
+
+Lemma Equal_Equivb_eqdec :
+ forall eq_elt_dec : (forall e e', { e = e' } + { e <> e' }),
+ let cmp := fun e e' => if eq_elt_dec e e' then true else false in
+ forall (m m':t elt), m == m' <-> Equivb cmp m m'.
+Proof.
+intros; apply Equal_Equivb.
+unfold cmp; clear cmp; intros.
+destruct eq_elt_dec; now intuition.
+Qed.
+
+End Equalities.
+
+(** * Results about [fold], [bindings], induction principles... *)
+
+Section Elt.
+  Variable elt:Type.
+
+  Definition Add x (e:elt) m m' := m' == (add x e m).
+
+  Notation eqke := (@eq_key_elt elt).
+  Notation eqk := (@eq_key elt).
+
+  Instance eqk_equiv : Equivalence eqk.
+  Proof. unfold eq_key. destruct E.eq_equiv. constructor; eauto. Qed.
+
+  Instance eqke_equiv : Equivalence eqke.
+  Proof.
+   unfold eq_key_elt; split; repeat red; intuition; simpl in *;
+    etransitivity; eauto.
+  Qed.
+
+  (** Complements about InA, NoDupA and findA *)
+
+  Lemma InA_eqke_eqk k k' e e' l :
+    E.eq k k' -> InA eqke (k,e) l -> InA eqk (k',e') l.
+  Proof.
+  intros Hk. rewrite 2 InA_alt.
+  intros ((k'',e'') & (Hk'',He'') & H); simpl in *; subst e''.
+  exists (k'',e); split; auto. red; simpl. now transitivity k.
+  Qed.
+
+  Lemma NoDupA_incl {A} (R R':relation A) :
+   (forall x y, R x y -> R' x y) ->
+   forall l, NoDupA R' l -> NoDupA R l.
+  Proof.
+  intros Incl.
+  induction 1 as [ | a l E _ IH ]; constructor; auto.
+  contradict E. revert E. rewrite 2 InA_alt. firstorder.
+  Qed.
+
+  Lemma NoDupA_eqk_eqke l : NoDupA eqk l -> NoDupA eqke l.
+  Proof.
+  apply NoDupA_incl. now destruct 1.
+  Qed.
+
+  Lemma findA_rev l k : NoDupA eqk l ->
+    findA (eqb k) l = findA (eqb k) (rev l).
+  Proof.
+  intros H. apply eq_option_alt. intros e. unfold eqb.
+  rewrite <- !findA_NoDupA, InA_rev; eauto with map. reflexivity.
+  change (NoDupA eqk (rev l)). apply NoDupA_rev; auto using eqk_equiv.
+  Qed.
+
+  (** * Bindings *)
+
+  Lemma bindings_Empty (m:t elt) : Empty m <-> bindings m = nil.
+  Proof.
+  unfold Empty. split; intros H.
+  - assert (H' : forall a, ~ List.In a (bindings m)).
+    { intros (k,e) H'. apply (H k e).
+      rewrite bindings_mapsto_iff, InA_alt.
+      exists (k,e); repeat split; auto with map. }
+    destruct (bindings m) as [|p l]; trivial.
+    destruct (H' p); simpl; auto.
+  - intros x e. rewrite bindings_mapsto_iff, InA_alt.
+    rewrite H. now intros (y,(E,H')).
+  Qed.
+
+  Lemma bindings_empty : bindings (@empty elt) = nil.
+  Proof.
+  rewrite <-bindings_Empty; apply empty_1.
+  Qed.
+
+  (** * 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 :=
+    List.fold_right (uncurry (@add _)) (@empty elt).
+
+  Definition to_list := bindings.
+
+  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.
+  - unfold uncurry; simpl.
+    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 (E.eq_dec k k'); [left|right]; split; auto with map.
+    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.
+  unfold uncurry; simpl.
+  inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].
+  specialize (IH k Hnodup'); clear Hnodup'.
+  rewrite add_o, IH, eqb_sym. unfold eqb; now destruct E.eq_dec.
+  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 <- bindings_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, bindings_o; auto.
+  apply bindings_3w.
+  Qed.
+
+  (** * 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 (bindings 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
+      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_spec_right.
+  set (F:=uncurry f).
+  set (l:=rev (bindings 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, bindings_mapsto_iff; auto with *. }
+  assert (Hdup : NoDupA eqk l).
+  { unfold l. apply NoDupA_rev; try red; unfold eq_key ; eauto with *.
+    apply bindings_3w. }
+  assert (Hsame : forall k, find k m = findA (eqb k) l).
+  { intros k. unfold l. rewrite bindings_o, findA_rev; auto.
+    apply bindings_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 with map.
+    + inversion_clear Hdup. contradict H. destruct H as (e',He').
+      apply InA_eqke_eqk with k e'; auto with map.
+      rewrite <- of_list_1; auto.
+    + intro k'. rewrite Hsame, add_o, of_list_1b. simpl.
+      rewrite eqb_sym. unfold eqb. now destruct E.eq_dec.
+      inversion_clear Hdup; auto with map.
+    + 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.
+  rewrite 2 fold_spec_right. set (l:=rev (bindings 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)).
+  { intros; apply Rstep; auto.
+    rewrite bindings_mapsto_iff, <- InA_rev; auto with map. }
+  clearbody l; clear Rstep m.
+  induction l; simpl; auto.
+  apply Rstep'; auto.
+  destruct a; simpl; rewrite InA_cons; left; red; auto with map.
+  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.
+  apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto.
+  Qed.
+
+  (** [fold] can be used to reconstruct the same initial set. *)
+
+  Lemma fold_identity : forall m : t elt, Equal (fold (@add _) m empty) m.
+  Proof.
+  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'.
+  red in Heq. rewrite Hadd, 2 add_o, Heq; auto.
+  Qed.
+
+  Section Fold_More.
+
+  (** ** Additional properties of fold *)
+
+  (** When a function [f] is compatible and allows transpositions, we can
+      compute [fold f] in any order. *)
+
+  Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
+
+  Lemma fold_Empty (f:key->elt->A->A) :
+   forall m i, Empty m -> eqA (fold f m i) i.
+  Proof.
+  intros. apply fold_rec_nodep with (P:=fun a => eqA a i).
+  reflexivity.
+  intros. elim (H k e); auto.
+  Qed.
+
+  Lemma fold_init (f:key->elt->A->A) :
+   Proper (E.eq==>eq==>eqA==>eqA) f ->
+   forall m i i', eqA i i' -> eqA (fold f m i) (fold f m i').
+  Proof.
+  intros Hf m i i' Hi. apply fold_rel with (R:=eqA); auto.
+  intros. now apply Hf.
+  Qed.
+
+  (** Transpositions of f (a.k.a diamond property).
+      Could we swap two sequential calls to f, i.e. do we have:
+
+        f k e (f k' e' a) == f k' e' (f k e a)
+
+      First, we do no need this equation for all keys, but only
+      when k and k' aren't equal, as suggested by Pierre Castéran.
+      Think for instance of [f] being [M.add] : in general, we don't have
+      [M.add k e (M.add k e' m) == 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.
+      NB: without this condition, this condition would be
+      [SetoidList.transpose2].
+
+      Secondly, instead of the equation above, we now use a statement
+      with more basic equalities, allowing to prove [fold_commutes] even
+      when [f] isn't a morphism.
+      NB: When [f] is a morphism, [Diamond f] gives back the equation above.
+*)
+
+  Definition Diamond (f:key->elt->A->A) :=
+    forall k k' e e' a b b', ~E.eq k k' ->
+      eqA (f k e a) b -> eqA (f k' e' a) b' -> eqA (f k e b') (f k' e' b).
+
+  Lemma fold_commutes (f:key->elt->A->A) :
+   Diamond f ->
+   forall i m k e, ~In k m ->
+   eqA (fold f m (f k e i)) (f k e (fold f m i)).
+  Proof.
+  intros Hf i m k e H.
+  apply fold_rel with (R:= fun a b => eqA a (f k e b)); auto.
+  - reflexivity.
+  - intros k' e' b a Hm E.
+    apply Hf with a; try easy.
+    contradict H; rewrite <- H. now exists e'.
+  Qed.
+
+  Hint Resolve NoDupA_eqk_eqke NoDupA_rev bindings_3w : map.
+
+  Lemma fold_Proper (f:key->elt->A->A) :
+   Proper (E.eq==>eq==>eqA==>eqA) f ->
+   Diamond f ->
+   Proper (Equal==>eqA==>eqA) (fold f).
+  Proof.
+  intros Hf Hf' m1 m2 Hm i j Hi.
+  rewrite 2 fold_spec_right.
+  assert (NoDupA eqk (rev (bindings m1))) by (auto with * ).
+  assert (NoDupA eqk (rev (bindings m2))) by (auto with * ).
+  apply fold_right_equivlistA_restr2 with (R:=complement eqk)(eqA:=eqke)
+  ; auto with *.
+  - intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *. now apply Hf.
+  - unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto with map.
+  - intros (k,e) (k',e') z z' h h'; unfold eq_key, uncurry;simpl; auto.
+    rewrite h'. eapply Hf'; now eauto.
+  - rewrite <- NoDupA_altdef; auto.
+  - intros (k,e).
+    rewrite 2 InA_rev, <- 2 bindings_mapsto_iff, 2 find_mapsto_iff, Hm;
+      auto with *.
+  Qed.
+
+  Lemma fold_Equal (f:key->elt->A->A) :
+   Proper (E.eq==>eq==>eqA==>eqA) f ->
+   Diamond f ->
+   forall m1 m2 i,
+   Equal m1 m2 ->
+   eqA (fold f m1 i) (fold f m2 i).
+  Proof.
+   intros. now apply fold_Proper.
+  Qed.
+
+  Lemma fold_Add (f:key->elt->A->A) :
+   Proper (E.eq==>eq==>eqA==>eqA) f ->
+   Diamond f ->
+   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 Hf Hf' m1 m2 k e i Hm1 Hm2.
+  rewrite 2 fold_spec_right.
+  set (f':=uncurry f).
+  change (f k e (fold_right f' i (rev (bindings m1))))
+   with (f' (k,e) (fold_right f' i (rev (bindings m1)))).
+  assert (NoDupA eqk (rev (bindings m1))) by (auto with * ).
+  assert (NoDupA eqk (rev (bindings m2))) by (auto with * ).
+  apply fold_right_add_restr with
+   (R:=complement eqk)(eqA:=eqke); auto with *.
+  - intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. now apply Hf.
+  - unfold complement, eq_key_elt, eq_key; repeat red; intuition eauto with map.
+  - intros (k1,e1) (k2,e2) z1 z2; unfold eq_key, f', uncurry; simpl.
+    eapply Hf'; now eauto.
+  - rewrite <- NoDupA_altdef; auto.
+  - rewrite InA_rev, <- bindings_mapsto_iff by (auto with * ). firstorder.
+  - intros (a,b).
+    rewrite InA_cons, 2 InA_rev, <- 2 bindings_mapsto_iff,
+    2 find_mapsto_iff by (auto with * ).
+    unfold eq_key_elt; simpl.
+    rewrite Hm2, !find_spec, add_mapsto_new; intuition.
+  Qed.
+
+  Lemma fold_add (f:key->elt->A->A) :
+   Proper (E.eq==>eq==>eqA==>eqA) f ->
+   Diamond f ->
+   forall m k e i, ~In k m ->
+   eqA (fold f (add k e m) i) (f k e (fold f m i)).
+  Proof.
+  intros. now apply fold_Add.
+  Qed.
+
+  End Fold_More.
+
+  (** * Cardinal *)
+
+  Lemma cardinal_fold (m : t elt) :
+   cardinal m = fold (fun _ _ => S) m 0.
+  Proof.
+  rewrite cardinal_1, fold_1.
+  symmetry; apply fold_left_length; auto.
+  Qed.
+
+  Lemma cardinal_Empty : forall m : t elt,
+   Empty m <-> cardinal m = 0.
+  Proof.
+  intros.
+  rewrite cardinal_1, bindings_Empty.
+  destruct (bindings m); intuition; discriminate.
+  Qed.
+
+  Lemma Equal_cardinal (m m' : t elt) :
+    Equal m m' -> cardinal m = cardinal m'.
+  Proof.
+  intro. rewrite 2 cardinal_fold.
+  apply fold_Equal with (eqA:=eq); try congruence; auto with map.
+  Qed.
+
+  Lemma cardinal_0 (m : t elt) : Empty m -> cardinal m = 0.
+  Proof.
+  intros; rewrite <- cardinal_Empty; auto.
+  Qed.
+
+  Lemma cardinal_S m m' x e :
+    ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m).
+  Proof.
+  intros. rewrite 2 cardinal_fold.
+  change S with ((fun _ _ => S) x e).
+  apply fold_Add with (eqA:=eq); try congruence; auto with map.
+  Qed.
+
+  Lemma cardinal_inv_1 : forall m : t elt,
+   cardinal m = 0 -> Empty m.
+  Proof.
+  intros; rewrite cardinal_Empty; auto.
+  Qed.
+  Hint Resolve cardinal_inv_1 : map.
+
+  Lemma cardinal_inv_2 :
+   forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }.
+  Proof.
+  intros; rewrite M.cardinal_spec in *.
+  generalize (bindings_mapsto_iff m).
+  destruct (bindings m); try discriminate.
+  exists p; auto.
+  rewrite H0; destruct p; simpl; auto.
+  constructor; red; auto with map.
+  Qed.
+
+  Lemma cardinal_inv_2b :
+   forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }.
+  Proof.
+  intros.
+  generalize (@cardinal_inv_2 m); destruct cardinal.
+  elim H;auto.
+  eauto.
+  Qed.
+
+  Lemma not_empty_mapsto (m : t elt) :
+    ~Empty m -> exists k e, MapsTo k e m.
+  Proof.
+  intro.
+  destruct (@cardinal_inv_2b m) as ((k,e),H').
+  contradict H. now apply cardinal_inv_1.
+  exists k; now exists e.
+  Qed.
+
+  Lemma not_empty_in (m:t elt) :
+    ~Empty m -> exists k, In k m.
+  Proof.
+  intro. destruct (not_empty_mapsto H) as (k,Hk).
+  now exists k.
+  Qed.
+
+  (** * Additional notions over maps *)
+
+  Definition Disjoint (m m' : t elt) :=
+   forall k, ~(In k m /\ In k m').
+
+  Definition Partition (m m1 m2 : t elt) :=
+    Disjoint m1 m2 /\
+    (forall k e, MapsTo k e m <-> MapsTo k e m1 \/ MapsTo k e m2).
+
+  (** * 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.
+
+  Definition for_all (f : key -> elt -> bool)(m : t elt) :=
+   fold (fun k e b => if f k e then b else false) m true.
+
+  Definition exists_ (f : key -> elt -> bool)(m : t elt) :=
+   fold (fun k e b => if f k e then true else b) m false.
+
+  Definition partition (f : key -> elt -> bool)(m : t elt) :=
+   (filter f m, filter (fun k e => negb (f k e)) m).
+
+  (** [update] adds to [m1] all the bindings of [m2]. It can be seen as
+     an [union] operator which gives priority to its 2nd argument
+     in case of binding conflit. *)
+
+  Definition update (m1 m2 : t elt) := fold (@add _) m2 m1.
+
+  (** [restrict] keeps from [m1] only the bindings whose key is in [m2].
+      It can be seen as an [inter] operator, with priority to its 1st argument
+      in case of binding conflit. *)
+
+  Definition restrict (m1 m2 : t elt) := filter (fun k _ => mem k m2) m1.
+
+  (** [diff] erases from [m1] all bindings whose key is in [m2]. *)
+
+  Definition diff (m1 m2 : t elt) := filter (fun k _ => negb (mem k m2)) m1.
+
+  (** Properties of these abbreviations *)
+
+  Lemma filter_iff (f : key -> elt -> bool) :
+    Proper (E.eq==>eq==>eq) f ->
+    forall m k e,
+      MapsTo k e (filter f m) <-> MapsTo k e m /\ f k e = true.
+  Proof.
+  unfold filter.
+  set (f':=fun k e m => if f k e then add k e m else m).
+  intros Hf m. pattern m, (fold f' m empty). apply fold_rec.
+
+  - intros m' Hm' k e. rewrite empty_mapsto_iff. intuition.
+    elim (Hm' k e); auto.
+
+  - intros k e acc m1 m2 Hke Hn Hadd IH k' e'.
+    change (Equal m2 (add k e m1)) in Hadd; rewrite Hadd.
+    unfold f'; simpl.
+    rewrite add_mapsto_new by trivial.
+    case_eq (f k e); intros Hfke; simpl;
+     rewrite ?add_mapsto_iff, IH; clear IH; intuition.
+    + rewrite <- Hfke; apply Hf; auto with map.
+    + right. repeat split; trivial. contradict Hn. rewrite Hn. now exists e'.
+    + assert (f k e = f k' e') by (apply Hf; auto). congruence.
+  Qed.
+
+  Lemma for_all_filter f m :
+   for_all f m = is_empty (filter (fun k e => negb (f k e)) m).
+  Proof.
+   unfold for_all, filter.
+   eapply fold_rel with (R:=fun x y => x = is_empty y).
+   - symmetry. apply is_empty_iff. apply empty_1.
+   - intros; subst. destruct (f k e); simpl; trivial.
+     symmetry. apply not_true_is_false. rewrite is_empty_spec.
+     intros H'. specialize (H' k). now rewrite add_spec1 in H'.
+  Qed.
+
+  Lemma exists_filter f m :
+   exists_ f m = negb (is_empty (filter f m)).
+  Proof.
+   unfold for_all, filter.
+   eapply fold_rel with (R:=fun x y => x = negb (is_empty y)).
+   - symmetry. rewrite negb_false_iff. apply is_empty_iff. apply empty_1.
+   - intros; subst. destruct (f k e); simpl; trivial.
+     symmetry. rewrite negb_true_iff. apply not_true_is_false.
+     rewrite is_empty_spec.
+     intros H'. specialize (H' k). now rewrite add_spec1 in H'.
+  Qed.
+
+  Lemma for_all_iff f m :
+   Proper (E.eq==>eq==>eq) f ->
+   (for_all f m = true <-> (forall k e, MapsTo k e m -> f k e = true)).
+  Proof.
+  intros Hf.
+  rewrite for_all_filter.
+  rewrite <- is_empty_iff. unfold Empty.
+  split; intros H k e; specialize (H k e);
+   rewrite filter_iff in * by solve_proper; intuition.
+  - destruct (f k e); auto.
+  - now rewrite H0 in H2.
+  Qed.
+
+  Lemma exists_iff f m :
+   Proper (E.eq==>eq==>eq) f ->
+   (exists_ f m = true <->
+     (exists k e, MapsTo k e m /\ f k e = true)).
+  Proof.
+  intros Hf.
+  rewrite exists_filter. rewrite negb_true_iff.
+  rewrite <- not_true_iff_false, <- is_empty_iff.
+  split.
+  - intros H. apply not_empty_mapsto in H. now setoid_rewrite filter_iff in H.
+  - unfold Empty. setoid_rewrite filter_iff; trivial. firstorder.
+  Qed.
+
+  Lemma Disjoint_alt : forall m m',
+   Disjoint m m' <->
+   (forall k e e', MapsTo k e m -> MapsTo k e' m' -> False).
+  Proof.
+  unfold Disjoint; split.
+  intros H k v v' H1 H2.
+  apply H with k; split.
+  exists v; trivial.
+  exists v'; trivial.
+  intros H k ((v,Hv),(v',Hv')).
+  eapply H; eauto.
+  Qed.
+
+  Section Partition.
+  Variable f : key -> elt -> bool.
+  Hypothesis Hf : Proper (E.eq==>eq==>eq) f.
+
+  Lemma partition_iff_1 : forall m m1 k e,
+   m1 = fst (partition f m) ->
+   (MapsTo k e m1 <-> MapsTo k e m /\ f k e = true).
+  Proof.
+  unfold partition; simpl; intros. subst m1.
+  apply filter_iff; auto.
+  Qed.
+
+  Lemma partition_iff_2 : forall m m2 k e,
+   m2 = snd (partition f m) ->
+   (MapsTo k e m2 <-> MapsTo k e m /\ f k e = false).
+  Proof.
+  unfold partition; simpl; intros. subst m2.
+  rewrite filter_iff.
+  split; intros (H,H'); split; auto.
+  destruct (f k e); simpl in *; auto.
+  rewrite H'; auto.
+  repeat red; intros. f_equal. apply Hf; auto.
+  Qed.
+
+  Lemma partition_Partition : forall m m1 m2,
+   partition f m = (m1,m2) -> Partition m m1 m2.
+  Proof.
+  intros. split.
+  rewrite Disjoint_alt. intros k e e'.
+  rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2)
+   by (rewrite H; auto).
+  intros (U,V) (W,Z). rewrite <- (mapsto_fun U W) in Z; congruence.
+  intros k e.
+  rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2)
+   by (rewrite H; auto).
+  destruct (f k e); intuition.
+  Qed.
+
+  End Partition.
+
+  Lemma Partition_In : forall m m1 m2 k,
+   Partition m m1 m2 -> In k m -> {In k m1}+{In k m2}.
+  Proof.
+  intros m m1 m2 k Hm Hk.
+  destruct (In_dec m1 k) as [H|H]; [left|right]; auto.
+  destruct Hm as (Hm,Hm').
+  destruct Hk as (e,He); rewrite Hm' in He; destruct He.
+  elim H; exists e; auto.
+  exists e; auto.
+  Defined.
+
+  Lemma Disjoint_sym : forall m1 m2, Disjoint m1 m2 -> Disjoint m2 m1.
+  Proof.
+  intros m1 m2 H k (H1,H2). elim (H k); auto.
+  Qed.
+
+  Lemma Partition_sym : forall m m1 m2,
+   Partition m m1 m2 -> Partition m m2 m1.
+  Proof.
+  intros m m1 m2 (H,H'); split.
+  apply Disjoint_sym; auto.
+  intros; rewrite H'; intuition.
+  Qed.
+
+  Lemma Partition_Empty : forall m m1 m2, Partition m m1 m2 ->
+   (Empty m <-> (Empty m1 /\ Empty m2)).
+  Proof.
+  intros m m1 m2 (Hdisj,Heq). split.
+  intro He.
+  split; intros k e Hke; elim (He k e); rewrite Heq; auto.
+  intros (He1,He2) k e Hke. rewrite Heq in Hke. destruct Hke.
+  elim (He1 k e); auto.
+  elim (He2 k e); auto.
+  Qed.
+
+  Lemma Partition_Add :
+    forall m m' x e , ~In x m -> Add x e m m' ->
+    forall m1 m2, Partition m' m1 m2 ->
+     exists m3, (Add x e m3 m1 /\ Partition m m3 m2 \/
+                 Add x e m3 m2 /\ Partition m m1 m3).
+  Proof.
+  unfold Partition. intros m m' x e Hn Hadd m1 m2 (Hdisj,Hor).
+  assert (Heq : Equal m (remove x m')).
+  { change (Equal m' (add x e m)) in Hadd. rewrite Hadd.
+    intro k. rewrite remove_o, add_o.
+    destruct E.eq_dec as [He|Hne]; auto.
+    rewrite <- He, <- not_find_in_iff; auto. }
+  assert (H : MapsTo x e m').
+  { change (Equal m' (add x e m)) in Hadd; rewrite Hadd.
+    apply add_1; auto with map. }
+  rewrite Hor in H; destruct H.
+
+  - (* first case : x in m1 *)
+    exists (remove x m1); left. split; [|split].
+    + (* add *)
+      change (Equal m1 (add x e (remove x m1))).
+      intro k.
+      rewrite add_o, remove_o.
+      destruct E.eq_dec as [He|Hne]; auto.
+      rewrite <- He; apply find_1; auto.
+    + (* disjoint *)
+      intros k (H1,H2). elim (Hdisj k). split; auto.
+      rewrite remove_in_iff in H1; destruct H1; auto.
+    + (* mapsto *)
+      intros k' e'.
+      rewrite Heq, 2 remove_mapsto_iff, Hor.
+      intuition.
+      elim (Hdisj x); split; [exists e|exists e']; auto.
+      apply MapsTo_1 with k'; auto with map.
+
+  - (* second case : x in m2 *)
+    exists (remove x m2); right. split; [|split].
+    + (* add *)
+      change (Equal m2 (add x e (remove x m2))).
+      intro k.
+      rewrite add_o, remove_o.
+      destruct E.eq_dec as [He|Hne]; auto.
+      rewrite <- He; apply find_1; auto.
+    + (* disjoint *)
+      intros k (H1,H2). elim (Hdisj k). split; auto.
+      rewrite remove_in_iff in H2; destruct H2; auto.
+    + (* mapsto *)
+      intros k' e'.
+      rewrite Heq, 2 remove_mapsto_iff, Hor.
+      intuition.
+      elim (Hdisj x); split; [exists e'|exists e]; auto.
+      apply MapsTo_1 with k'; auto with map.
+  Qed.
+
+  Lemma Partition_fold :
+   forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A),
+   Proper (E.eq==>eq==>eqA==>eqA) f ->
+   Diamond eqA f ->
+   forall m m1 m2 i,
+   Partition m m1 m2 ->
+   eqA (fold f m i) (fold f m1 (fold f m2 i)).
+  Proof.
+  intros A eqA st f Comp Tra.
+  induction m as [m Hm|m m' IH k e Hn Hadd] using map_induction.
+
+  - intros m1 m2 i Hp. rewrite (fold_Empty (eqA:=eqA)); auto.
+    rewrite (Partition_Empty Hp) in Hm. destruct Hm.
+    rewrite 2 (fold_Empty (eqA:=eqA)); auto. reflexivity.
+
+  - intros m1 m2 i Hp.
+    destruct (Partition_Add Hn Hadd Hp) as (m3,[(Hadd',Hp')|(Hadd',Hp')]).
+    + (* fst case: m3 is (k,e)::m1 *)
+      assert (~In k m3).
+      { contradict Hn. destruct Hn as (e',He').
+        destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. }
+      transitivity (f k e (fold f m i)).
+      apply fold_Add with (eqA:=eqA); auto.
+      symmetry.
+      transitivity (f k e (fold f m3 (fold f m2 i))).
+      apply fold_Add with (eqA:=eqA); auto.
+      apply Comp; auto with map.
+      symmetry; apply IH; auto.
+    + (* snd case: m3 is (k,e)::m2 *)
+      assert (~In k m3).
+      { contradict Hn. destruct Hn as (e',He').
+        destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. }
+      assert (~In k m1).
+      { contradict Hn. destruct Hn as (e',He').
+        destruct Hp' as (Hp1,Hp2). exists e'. rewrite Hp2; auto. }
+      transitivity (f k e (fold f m i)).
+      apply fold_Add with (eqA:=eqA); auto.
+      transitivity (f k e (fold f m1 (fold f m3 i))).
+      apply Comp; auto using IH with map.
+      transitivity (fold f m1 (f k e (fold f m3 i))).
+      symmetry.
+      apply fold_commutes with (eqA:=eqA); auto.
+      apply fold_init with (eqA:=eqA); auto.
+      symmetry.
+      apply fold_Add with (eqA:=eqA); auto.
+  Qed.
+
+  Lemma Partition_cardinal : forall m m1 m2, Partition m m1 m2 ->
+   cardinal m = cardinal m1 + cardinal m2.
+  Proof.
+  intros.
+  rewrite (cardinal_fold m), (cardinal_fold m1).
+  set (f:=fun (_:key)(_:elt)=>S).
+  setoid_replace (fold f m 0) with (fold f m1 (fold f m2 0)).
+  rewrite <- cardinal_fold.
+  apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto.
+  apply Partition_fold with (eqA:=eq); compute; auto with map. congruence.
+  Qed.
+
+  Lemma Partition_partition : forall m m1 m2, Partition m m1 m2 ->
+    let f := fun k (_:elt) => mem k m1 in
+   Equal m1 (fst (partition f m)) /\ Equal m2 (snd (partition f m)).
+  Proof.
+  intros m m1 m2 Hm f.
+  assert (Hf : Proper (E.eq==>eq==>eq) f).
+   intros k k' Hk e e' _; unfold f; rewrite Hk; auto.
+  set (m1':= fst (partition f m)).
+  set (m2':= snd (partition f m)).
+  split; rewrite Equal_mapsto_iff; intros k e.
+  rewrite (@partition_iff_1 f Hf m m1') by auto.
+  unfold f.
+  rewrite <- mem_in_iff.
+  destruct Hm as (Hm,Hm').
+  rewrite Hm'.
+  intuition.
+  exists e; auto.
+  elim (Hm k); split; auto; exists e; auto.
+  rewrite (@partition_iff_2 f Hf m m2') by auto.
+  unfold f.
+  rewrite <- not_mem_in_iff.
+  destruct Hm as (Hm,Hm').
+  rewrite Hm'.
+  intuition.
+  elim (Hm k); split; auto; exists e; auto.
+  elim H1; exists e; auto.
+  Qed.
+
+  Lemma update_mapsto_iff : forall m m' k e,
+   MapsTo k e (update m m') <->
+    (MapsTo k e m' \/ (MapsTo k e m /\ ~In k m')).
+  Proof.
+  unfold update.
+  intros m m'.
+  pattern m', (fold (@add _) m' m). apply fold_rec.
+
+  - intros m0 Hm0 k e.
+    assert (~In k m0) by (intros (e0,He0); apply (Hm0 k e0); auto).
+    intuition.
+    elim (Hm0 k e); auto.
+
+  - intros k e m0 m1 m2 _ Hn Hadd IH k' e'.
+    change (Equal m2 (add k e m1)) in Hadd.
+    rewrite Hadd, 2 add_mapsto_iff, IH, add_in_iff. clear IH. intuition.
+  Qed.
+
+  Lemma update_dec : forall m m' k e, MapsTo k e (update m m') ->
+   { MapsTo k e m' } + { MapsTo k e m /\ ~In k m'}.
+  Proof.
+  intros m m' k e H. rewrite update_mapsto_iff in H.
+  destruct (In_dec m' k) as [H'|H']; [left|right]; intuition.
+  elim H'; exists e; auto.
+  Defined.
+
+  Lemma update_in_iff : forall m m' k,
+   In k (update m m') <-> In k m \/ In k m'.
+  Proof.
+  intros m m' k. split.
+  intros (e,H); rewrite update_mapsto_iff in H.
+  destruct H; [right|left]; exists e; intuition.
+  destruct (In_dec m' k) as [H|H].
+  destruct H as (e,H). intros _; exists e.
+  rewrite update_mapsto_iff; left; auto.
+  destruct 1 as [H'|H']; [|elim H; auto].
+  destruct H' as (e,H'). exists e.
+  rewrite update_mapsto_iff; right; auto.
+  Qed.
+
+  Lemma diff_mapsto_iff : forall m m' k e,
+   MapsTo k e (diff m m') <-> MapsTo k e m /\ ~In k m'.
+  Proof.
+  intros m m' k e.
+  unfold diff.
+  rewrite filter_iff.
+  intuition.
+  rewrite mem_1 in *; auto; discriminate.
+  intros ? ? Hk _ _ _; rewrite Hk; auto.
+  Qed.
+
+  Lemma diff_in_iff : forall m m' k,
+   In k (diff m m') <-> In k m /\ ~In k m'.
+  Proof.
+  intros m m' k. split.
+  intros (e,H); rewrite diff_mapsto_iff in H.
+  destruct H; split; auto. exists e; auto.
+  intros ((e,H),H'); exists e; rewrite diff_mapsto_iff; auto.
+  Qed.
+
+  Lemma restrict_mapsto_iff : forall m m' k e,
+   MapsTo k e (restrict m m') <-> MapsTo k e m /\ In k m'.
+  Proof.
+  intros m m' k e.
+  unfold restrict.
+  rewrite filter_iff.
+  intuition.
+  intros ? ? Hk _ _ _; rewrite Hk; auto.
+  Qed.
+
+  Lemma restrict_in_iff : forall m m' k,
+   In k (restrict m m') <-> In k m /\ In k m'.
+  Proof.
+  intros m m' k. split.
+  intros (e,H); rewrite restrict_mapsto_iff in H.
+  destruct H; split; auto. exists e; auto.
+  intros ((e,H),H'); exists e; rewrite restrict_mapsto_iff; auto.
+  Qed.
+
+  (** specialized versions analyzing only keys (resp. bindings) *)
+
+  Definition filter_dom (f : key -> bool) := filter (fun k _ => f k).
+  Definition filter_range (f : elt -> bool) := filter (fun _ => f).
+  Definition for_all_dom (f : key -> bool) := for_all (fun k _ => f k).
+  Definition for_all_range (f : elt -> bool) := for_all (fun _ => f).
+  Definition exists_dom (f : key -> bool) := exists_ (fun k _ => f k).
+  Definition exists_range (f : elt -> bool) := exists_ (fun _ => f).
+  Definition partition_dom (f : key -> bool) := partition (fun k _ => f k).
+  Definition partition_range (f : elt -> bool) := partition (fun _ => f).
+
+ End Elt.
+
+ Instance cardinal_m {elt} : Proper (Equal ==> Logic.eq) (@cardinal elt).
+ Proof. intros m m'. apply Equal_cardinal. Qed.
+
+ Instance Disjoint_m {elt} : Proper (Equal ==> Equal ==> iff) (@Disjoint elt).
+ Proof.
+  intros m1 m1' Hm1 m2 m2' Hm2. unfold Disjoint. split; intros.
+  rewrite <- Hm1, <- Hm2; auto.
+  rewrite Hm1, Hm2; auto.
+ Qed.
+
+ Instance Partition_m {elt} :
+   Proper (Equal ==> Equal ==> Equal ==> iff) (@Partition elt).
+ Proof.
+  intros m1 m1' Hm1 m2 m2' Hm2 m3 m3' Hm3. unfold Partition.
+  rewrite <- Hm2, <- Hm3.
+  split; intros (H,H'); split; auto; intros.
+  rewrite <- Hm1, <- Hm2, <- Hm3; auto.
+  rewrite Hm1, Hm2, Hm3; auto.
+ Qed.
+
+(*
+ Instance filter_m0 {elt} (f:key->elt->bool) :
+   Proper (E.eq==>Logic.eq==>Logic.eq) f ->
+   Proper (Equal==>Equal) (filter f).
+ Proof.
+  intros Hf m m' Hm. apply Equal_mapsto_iff. intros.
+  now rewrite !filter_iff, Hm.
+ Qed.
+*)
+
+ Instance filter_m {elt} :
+   Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Equal) (@filter elt).
+ Proof.
+  intros f f' Hf m m' Hm. unfold filter.
+  rewrite 2 fold_spec_right.
+  set (l := rev (bindings m)).
+  set (l' := rev (bindings m')).
+  set (op := fun (f:key->elt->bool) =>
+             uncurry (fun k e acc => if f k e then add k e acc else acc)).
+  change (Equal (fold_right (op f) empty l) (fold_right (op f') empty l')).
+  assert (Hl : NoDupA eq_key l).
+  { apply NoDupA_rev. apply eqk_equiv. apply bindings_spec2w. }
+  assert (Hl' : NoDupA eq_key l').
+  { apply NoDupA_rev. apply eqk_equiv. apply bindings_spec2w. }
+  assert (H : PermutationA eq_key_elt l l').
+  { apply NoDupA_equivlistA_PermutationA.
+    - apply eqke_equiv.
+    - now apply NoDupA_eqk_eqke.
+    - now apply NoDupA_eqk_eqke.
+    - intros (k,e); unfold l, l'. rewrite 2 InA_rev, 2 bindings_spec1.
+      rewrite Equal_mapsto_iff in Hm. apply Hm. }
+  destruct (PermutationA_decompose (eqke_equiv _) H) as (l0,(P,E)).
+  transitivity (fold_right (op f) empty l0).
+  - apply fold_right_equivlistA_restr2
+     with (eqA:=Logic.eq)(R:=complement eq_key); auto with *.
+    + intros p p' <- acc acc' Hacc.
+      destruct p as (k,e); unfold op, uncurry; simpl.
+      destruct (f k e); now rewrite Hacc.
+    + intros (k,e) (k',e') z z'.
+      unfold op, complement, uncurry, eq_key; simpl.
+      intros Hk Hz.
+      destruct (f k e), (f k' e'); rewrite <- Hz; try reflexivity.
+      now apply add_add_2.
+    + apply NoDupA_incl with eq_key; trivial. intros; subst; now red.
+    + apply PermutationA_preserves_NoDupA with l; auto with *.
+      apply Permutation_PermutationA; auto with *.
+      apply NoDupA_incl with eq_key; trivial. intros; subst; now red.
+    + apply NoDupA_altdef. apply NoDupA_rev. apply eqk_equiv.
+      apply bindings_spec2w.
+    + apply PermutationA_equivlistA; auto with *.
+      apply Permutation_PermutationA; auto with *.
+  - clearbody l'. clear l Hl Hl' H P m m' Hm.
+    induction E.
+    + reflexivity.
+    + simpl. destruct x as (k,e), x' as (k',e').
+      unfold op, uncurry at 1 3; simpl.
+      destruct H; simpl in *. rewrite <- (Hf _ _ H _ _ H0).
+      destruct (f k e); trivial. now f_equiv.
+ Qed.
+
+ Instance for_all_m {elt} :
+   Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Logic.eq) (@for_all elt).
+ Proof.
+ intros f f' Hf m m' Hm. rewrite 2 for_all_filter.
+ (* Strange: we cannot rewrite Hm here... *)
+ f_equiv. f_equiv; trivial.
+ intros k k' Hk e e' He. f_equal. now apply Hf.
+ Qed.
+
+ Instance exists_m {elt} :
+   Proper ((E.eq==>Logic.eq==>Logic.eq)==>Equal==>Logic.eq) (@exists_ elt).
+ Proof.
+ intros f f' Hf m m' Hm. rewrite 2 exists_filter.
+ f_equal. now apply is_empty_m, filter_m.
+ Qed.
+
+ Fact diamond_add {elt} : Diamond Equal (@add elt).
+ Proof.
+  intros k k' e e' a b b' Hk <- <-. now apply add_add_2.
+ Qed.
+
+ Instance update_m {elt} : Proper (Equal ==> Equal ==> Equal) (@update elt).
+ Proof.
+  intros m1 m1' Hm1 m2 m2' Hm2.
+  unfold update.
+  apply fold_Proper; auto using diamond_add with *.
+ Qed.
+
+ Instance restrict_m {elt} : Proper (Equal==>Equal==>Equal) (@restrict elt).
+ Proof.
+  intros m1 m1' Hm1 m2 m2' Hm2 y.
+  unfold restrict.
+  apply eq_option_alt. intros e.
+  rewrite !find_spec, !filter_iff, Hm1, Hm2. reflexivity.
+  clear. intros x x' Hx e e' He. now rewrite Hx.
+  clear. intros x x' Hx e e' He. now rewrite Hx.
+ Qed.
+
+ Instance diff_m {elt} : Proper (Equal==>Equal==>Equal) (@diff elt).
+ Proof.
+  intros m1 m1' Hm1 m2 m2' Hm2 y.
+  unfold diff.
+  apply eq_option_alt. intros e.
+  rewrite !find_spec, !filter_iff, Hm1, Hm2. reflexivity.
+  clear. intros x x' Hx e e' He. now rewrite Hx.
+  clear. intros x x' Hx e e' He. now rewrite Hx.
+ Qed.
+
+End WProperties_fun.
+
+(** * Same Properties for self-contained weak maps and for full maps *)
+
+Module WProperties (M:WS) := WProperties_fun M.E M.
+Module Properties := WProperties.
+
+(** * Properties specific to maps with ordered keys *)
+
+Module OrdProperties (M:S).
+ Module Import ME := OrderedTypeFacts M.E.
+ Module Import O:=KeyOrderedType M.E.
+ Module Import P:=Properties M.
+ Import M.
+
+ Section Elt.
+  Variable elt:Type.
+
+  Definition Above x (m:t elt) := forall y, In y m -> E.lt y x.
+  Definition Below x (m:t elt) := forall y, In y m -> E.lt x y.
+
+  Section Bindings.
+
+  Lemma sort_equivlistA_eqlistA : forall l l' : list (key*elt),
+   sort ltk l -> sort ltk l' -> equivlistA eqke l l' -> eqlistA eqke l l'.
+  Proof.
+  apply SortA_equivlistA_eqlistA; eauto with *.
+  Qed.
+
+  Ltac klean := unfold O.eqke, O.ltk, RelCompFun in *; simpl in *.
+  Ltac keauto := klean; intuition; eauto.
+
+  Definition gtb (p p':key*elt) :=
+    match E.compare (fst p) (fst p') with Gt => true | _ => false end.
+  Definition leb p := fun p' => negb (gtb p p').
+
+  Definition bindings_lt p m := List.filter (gtb p) (bindings m).
+  Definition bindings_ge p m := List.filter (leb p) (bindings m).
+
+  Lemma gtb_1 : forall p p', gtb p p' = true <-> ltk p' p.
+  Proof.
+   intros (x,e) (y,e'); unfold gtb; klean.
+   case E.compare_spec; intuition; try discriminate; ME.order.
+  Qed.
+
+  Lemma leb_1 : forall p p', leb p p' = true <-> ~ltk p' p.
+  Proof.
+   intros (x,e) (y,e'); unfold leb, gtb; klean.
+   case E.compare_spec; intuition; try discriminate; ME.order.
+  Qed.
+
+  Instance gtb_compat : forall p, Proper (eqke==>eq) (gtb p).
+  Proof.
+   red; intros (x,e) (a,e') (b,e'') H; red in H; simpl in *; destruct H.
+   generalize (gtb_1 (x,e) (a,e'))(gtb_1 (x,e) (b,e''));
+    destruct (gtb (x,e) (a,e')); destruct (gtb (x,e) (b,e'')); klean; auto.
+   - intros. symmetry; rewrite H2. rewrite <-H, <-H1; auto.
+   - intros. rewrite H1. rewrite H, <- H2; auto.
+  Qed.
+
+  Instance leb_compat : forall p, Proper (eqke==>eq) (leb p).
+  Proof.
+   intros x a b H. unfold leb; f_equal; apply gtb_compat; auto.
+  Qed.
+
+  Hint Resolve gtb_compat leb_compat bindings_spec2 : map.
+
+  Lemma bindings_split : forall p m,
+    bindings m = bindings_lt p m ++ bindings_ge p m.
+  Proof.
+  unfold bindings_lt, bindings_ge, leb; intros.
+  apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto with *.
+  intros; destruct x; destruct y; destruct p.
+  rewrite gtb_1 in H; klean.
+  apply not_true_iff_false in H0. rewrite gtb_1 in H0. klean. ME.order.
+  Qed.
+
+  Lemma bindings_Add : forall m m' x e, ~In x m -> Add x e m m' ->
+    eqlistA eqke (bindings m')
+                 (bindings_lt (x,e) m ++ (x,e):: bindings_ge (x,e) m).
+  Proof.
+  intros; unfold bindings_lt, bindings_ge.
+  apply sort_equivlistA_eqlistA; auto with *.
+  - apply (@SortA_app _ eqke); auto with *.
+    + apply (@filter_sort _ eqke); auto with *; keauto.
+    + constructor; auto with map.
+      * apply (@filter_sort _ eqke); auto with *; keauto.
+      * rewrite (@InfA_alt _ eqke); auto with *; try (keauto; fail).
+        { intros.
+          rewrite filter_InA in H1; auto with *; destruct H1.
+          rewrite leb_1 in H2.
+          destruct y; klean.
+          rewrite <- bindings_mapsto_iff in H1.
+          assert (~E.eq x t0).
+          { contradict H.
+            exists e0; apply MapsTo_1 with t0; auto.
+            ME.order. }
+          ME.order. }
+        { apply (@filter_sort _ eqke); auto with *; keauto. }
+    + intros.
+      rewrite filter_InA in H1; auto with *; destruct H1.
+      rewrite gtb_1 in H3.
+      destruct y; destruct x0; klean.
+      inversion_clear H2.
+      * red in H4; klean; destruct H4; simpl in *. ME.order.
+      * rewrite filter_InA in H4; auto with *; destruct H4.
+        rewrite leb_1 in H4. klean; ME.order.
+  - intros (k,e').
+    rewrite InA_app_iff, InA_cons, 2 filter_InA,
+      <-2 bindings_mapsto_iff, leb_1, gtb_1,
+      find_mapsto_iff, (H0 k), <- find_mapsto_iff,
+      add_mapsto_iff by (auto with * ).
+    change (eqke (k,e') (x,e)) with (E.eq k x /\ e' = e).
+    klean.
+    split.
+    + intros [(->,->)|(Hk,Hm)].
+      * right; now left.
+      * destruct (lt_dec k x); intuition.
+    + intros [(Hm,LT)|[(->,->)|(Hm,EQ)]].
+      * right; split; trivial; ME.order.
+      * now left.
+      * destruct (eq_dec x k) as [Hk|Hk].
+        elim H. exists e'. now rewrite Hk.
+        right; auto.
+  Qed.
+
+  Lemma bindings_Add_Above : forall m m' x e,
+   Above x m -> Add x e m m' ->
+     eqlistA eqke (bindings m') (bindings m ++ (x,e)::nil).
+  Proof.
+  intros.
+  apply sort_equivlistA_eqlistA; auto with *.
+  apply (@SortA_app _ eqke); auto with *.
+  intros.
+  inversion_clear H2.
+  destruct x0; destruct y.
+  rewrite <- bindings_mapsto_iff in H1.
+  destruct H3; klean.
+  rewrite H2.
+  apply H; firstorder.
+  inversion H3.
+  red; intros a; destruct a.
+  rewrite InA_app_iff, InA_cons, InA_nil, <- 2 bindings_mapsto_iff,
+   find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
+   add_mapsto_iff by (auto with *).
+  change (eqke (t0,e0) (x,e)) with (E.eq t0 x /\ e0 = e).
+  intuition.
+  destruct (E.eq_dec x t0) as [Heq|Hneq]; auto.
+  exfalso.
+  assert (In t0 m) by (exists e0; auto).
+  generalize (H t0 H1).
+  ME.order.
+  Qed.
+
+  Lemma bindings_Add_Below : forall m m' x e,
+   Below x m -> Add x e m m' ->
+     eqlistA eqke (bindings m') ((x,e)::bindings m).
+  Proof.
+  intros.
+  apply sort_equivlistA_eqlistA; auto with *.
+  change (sort ltk (((x,e)::nil) ++ bindings m)).
+  apply (@SortA_app _ eqke); auto with *.
+  intros.
+  inversion_clear H1.
+  destruct y; destruct x0.
+  rewrite <- bindings_mapsto_iff in H2.
+  destruct H3; klean.
+  rewrite H1.
+  apply H; firstorder.
+  inversion H3.
+  red; intros a; destruct a.
+  rewrite InA_cons, <- 2 bindings_mapsto_iff,
+    find_mapsto_iff, (H0 t0), <- find_mapsto_iff,
+    add_mapsto_iff by (auto with * ).
+  change (eqke (t0,e0) (x,e)) with (E.eq t0 x /\ e0 = e).
+  intuition.
+  destruct (E.eq_dec x t0) as [Heq|Hneq]; auto.
+  exfalso.
+  assert (In t0 m) by (exists e0; auto).
+  generalize (H t0 H1).
+  ME.order.
+  Qed.
+
+  Lemma bindings_Equal_eqlistA : forall (m m': t elt),
+   Equal m m' -> eqlistA eqke (bindings m) (bindings m').
+  Proof.
+  intros.
+  apply sort_equivlistA_eqlistA; auto with *.
+  red; intros.
+  destruct x; do 2 rewrite <- bindings_mapsto_iff.
+  do 2 rewrite find_mapsto_iff; rewrite H; split; auto.
+  Qed.
+
+  End Bindings.
+
+  Section Min_Max_Elt.
+
+  (** We emulate two [max_elt] and [min_elt] functions. *)
+
+  Fixpoint max_elt_aux (l:list (key*elt)) := match l with
+    | nil => None
+    | (x,e)::nil => Some (x,e)
+    | (x,e)::l => max_elt_aux l
+    end.
+  Definition max_elt m := max_elt_aux (bindings m).
+
+  Lemma max_elt_Above :
+   forall m x e, max_elt m = Some (x,e) -> Above x (remove x m).
+  Proof.
+  red; intros.
+  rewrite remove_in_iff in H0.
+  destruct H0.
+  rewrite bindings_in_iff in H1.
+  destruct H1.
+  unfold max_elt in *.
+  generalize (bindings_spec2 m).
+  revert x e H y x0 H0 H1.
+  induction (bindings m).
+  simpl; intros; try discriminate.
+  intros.
+  destruct a; destruct l; simpl in *.
+  injection H; clear H; intros; subst.
+  inversion_clear H1.
+  red in H; simpl in *; intuition.
+  now elim H0.
+  inversion H.
+  change (max_elt_aux (p::l) = Some (x,e)) in H.
+  generalize (IHl x e H); clear IHl; intros IHl.
+  inversion_clear H1; [ | inversion_clear H2; eauto ].
+  red in H3; simpl in H3; destruct H3.
+  destruct p as (p1,p2).
+  destruct (E.eq_dec p1 x) as [Heq|Hneq].
+  rewrite <- Heq; auto.
+   inversion_clear H2.
+   inversion_clear H5.
+   red in H2; simpl in H2; ME.order.
+  transitivity p1; auto.
+   inversion_clear H2.
+   inversion_clear H5.
+   red in H2; simpl in H2; ME.order.
+  eapply IHl; eauto with *.
+  econstructor; eauto.
+  red; eauto with *.
+  inversion H2; auto.
+  Qed.
+
+  Lemma max_elt_MapsTo :
+   forall m x e, max_elt m = Some (x,e) -> MapsTo x e m.
+  Proof.
+  intros.
+  unfold max_elt in *.
+  rewrite bindings_mapsto_iff.
+  induction (bindings m).
+  simpl; try discriminate.
+  destruct a; destruct l; simpl in *.
+  injection H; intros; subst; constructor; red; auto with *.
+  constructor 2; auto.
+  Qed.
+
+  Lemma max_elt_Empty :
+   forall m, max_elt m = None -> Empty m.
+  Proof.
+  intros.
+  unfold max_elt in *.
+  rewrite bindings_Empty.
+  induction (bindings m); auto.
+  destruct a; destruct l; simpl in *; try discriminate.
+  assert (H':=IHl H); discriminate.
+  Qed.
+
+  Definition min_elt m : option (key*elt) := match bindings m with
+   | nil => None
+   | (x,e)::_ => Some (x,e)
+  end.
+
+  Lemma min_elt_Below :
+   forall m x e, min_elt m = Some (x,e) -> Below x (remove x m).
+  Proof.
+  unfold min_elt, Below; intros.
+  rewrite remove_in_iff in H0; destruct H0.
+  rewrite bindings_in_iff in H1.
+  destruct H1.
+  generalize (bindings_spec2 m).
+  destruct (bindings m).
+  try discriminate.
+  destruct p; injection H; intros; subst.
+  inversion_clear H1.
+  red in H2; destruct H2; simpl in *; ME.order.
+  inversion_clear H4.
+  rewrite (@InfA_alt _ eqke) in H3; eauto with *.
+  apply (H3 (y,x0)); auto.
+  Qed.
+
+  Lemma min_elt_MapsTo :
+   forall m x e, min_elt m = Some (x,e) -> MapsTo x e m.
+  Proof.
+  intros.
+  unfold min_elt in *.
+  rewrite bindings_mapsto_iff.
+  destruct (bindings m).
+  simpl; try discriminate.
+  destruct p; simpl in *.
+  injection H; intros; subst; constructor; red; auto with *.
+  Qed.
+
+  Lemma min_elt_Empty :
+   forall m, min_elt m = None -> Empty m.
+  Proof.
+  intros.
+  unfold min_elt in *.
+  rewrite bindings_Empty.
+  destruct (bindings m); auto.
+  destruct p; simpl in *; discriminate.
+  Qed.
+
+  End Min_Max_Elt.
+
+  Section Induction_Principles.
+
+  Lemma map_induction_max :
+   forall P : t elt -> Type,
+   (forall m, Empty m -> P m) ->
+   (forall m m', P m -> forall x e, Above 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.
+
+  case_eq (max_elt m); intros.
+  destruct p.
+  assert (Add k e (remove k m) m).
+  { apply max_elt_MapsTo, find_spec, add_id in H.
+    unfold Add. symmetry. now rewrite add_remove_1. }
+  apply X0 with (remove k m) k e; auto with map.
+  apply IHn.
+  assert (S n = S (cardinal (remove k m))).
+  { rewrite Heqn.
+    eapply cardinal_S; eauto with map. }
+  inversion H1; auto.
+  eapply max_elt_Above; eauto.
+
+  apply X; apply max_elt_Empty; auto.
+  Qed.
+
+  Lemma map_induction_min :
+   forall P : t elt -> Type,
+   (forall m, Empty m -> P m) ->
+   (forall m m', P m -> forall x e, Below 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.
+
+  case_eq (min_elt m); intros.
+  destruct p.
+  assert (Add k e (remove k m) m).
+  { apply min_elt_MapsTo, find_spec, add_id in H.
+    unfold Add. symmetry. now rewrite add_remove_1. }
+  apply X0 with (remove k m) k e; auto.
+  apply IHn.
+  assert (S n = S (cardinal (remove k m))).
+  { rewrite Heqn.
+    eapply cardinal_S; eauto with map. }
+  inversion H1; auto.
+  eapply min_elt_Below; eauto.
+
+  apply X; apply min_elt_Empty; auto.
+  Qed.
+
+  End Induction_Principles.
+
+  Section Fold_properties.
+
+  (** The following lemma has already been proved on Weak Maps,
+      but with one additionnal hypothesis (some [transpose] fact). *)
+
+  Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence  eqA)
+   (f:key->elt->A->A)(i:A),
+   Proper (E.eq==>eq==>eqA==>eqA) f ->
+   Equal m1 m2 ->
+   eqA (fold f m1 i) (fold f m2 i).
+  Proof.
+  intros m1 m2 A eqA st f i Hf Heq.
+  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 bindings_Equal_eqlistA. auto.
+  Qed.
+
+  Lemma fold_Add_Above : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
+   (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>eq==>eqA==>eqA) f),
+   Above x m1 -> Add x e m1 m2 ->
+   eqA (fold f m2 i) (f x e (fold f m1 i)).
+  Proof.
+  intros. rewrite 2 fold_spec_right. set (f':=uncurry f).
+  transitivity (fold_right f' i (rev (bindings 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.
+  apply eqlistA_rev.
+  apply bindings_Add_Above; auto.
+  rewrite distr_rev; simpl.
+  reflexivity.
+  Qed.
+
+  Lemma fold_Add_Below : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
+   (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>eq==>eqA==>eqA) f),
+   Below x m1 -> Add x e m1 m2 ->
+   eqA (fold f m2 i) (fold f m1 (f x e i)).
+  Proof.
+  intros. rewrite 2 fold_spec_right. set (f':=uncurry f).
+  transitivity (fold_right f' i (rev (((x,e)::nil)++bindings 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.
+  apply eqlistA_rev.
+  simpl; apply bindings_Add_Below; auto.
+  rewrite distr_rev; simpl.
+  rewrite fold_right_app.
+  reflexivity.
+  Qed.
+
+  End Fold_properties.
+
+ End Elt.
+
+End OrdProperties.
diff --git a/theories/MMaps/MMapInterface.v b/theories/MMaps/MMapInterface.v
new file mode 100644
index 000000000..05c5e5d8f
--- /dev/null
+++ b/theories/MMaps/MMapInterface.v
@@ -0,0 +1,292 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(** * Finite map library *)
+
+(** This file proposes interfaces for finite maps *)
+
+Require Export Bool Equalities Orders SetoidList.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** When compared with Ocaml Map, this signature has been split in
+    several parts :
+
+   - The first parts [WSfun] and [WS] propose signatures for weak
+     maps, which are maps with no ordering on the key type nor the
+     data type.  [WSfun] and [WS] are almost identical, apart from the
+     fact that [WSfun] is expressed in a functorial way whereas [WS]
+     is self-contained. For obtaining an instance of such signatures,
+     a decidable equality on keys in enough (see for example
+     [FMapWeakList]). These signatures contain the usual operators
+     (add, find, ...). The only function that asks for more is
+     [equal], whose first argument should be a comparison on data.
+
+   - Then comes [Sfun] and [S], that extend [WSfun] and [WS] to the
+     case where the key type is ordered. The main novelty is that
+     [bindings] is required to produce sorted lists.
+
+   - Finally, [Sord] extends [S] with a complete comparison function. For
+     that, the data type should have a decidable total ordering as well.
+
+   If unsure, what you're looking for is probably [S]: apart from [Sord],
+   all other signatures are subsets of [S].
+
+   Some additional differences with Ocaml:
+
+    - no [iter] function, useless since Coq is purely functional
+    - [option] types are used instead of [Not_found] exceptions
+
+*)
+
+
+Definition Cmp {elt:Type}(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
+
+(** ** Weak signature for maps
+
+    No requirements for an ordering on keys nor elements, only decidability
+    of equality on keys. First, a functorial signature: *)
+
+Module Type WSfun (E : DecidableType).
+
+  Definition key := E.t.
+  Hint Transparent key.
+
+  Definition eq_key {elt} (p p':key*elt) := E.eq (fst p) (fst p').
+
+  Definition eq_key_elt {elt} (p p':key*elt) :=
+      E.eq (fst p) (fst p') /\ (snd p) = (snd p').
+
+  Parameter t : Type -> Type.
+  (** the abstract type of maps *)
+
+  Section Ops.
+
+    Parameter empty : forall {elt}, t elt.
+    (** The empty map. *)
+
+    Variable elt:Type.
+
+    Parameter is_empty : t elt -> bool.
+    (** Test whether a map is empty or not. *)
+
+    Parameter add : key -> elt -> t elt -> t elt.
+    (** [add x y m] returns a map containing the same bindings as [m],
+	plus a binding of [x] to [y]. If [x] was already bound in [m],
+	its previous binding disappears. *)
+
+    Parameter find : key -> t elt -> option elt.
+    (** [find x m] returns the current binding of [x] in [m],
+	or [None] if no such binding exists. *)
+
+    Parameter remove : key -> t elt -> t elt.
+    (** [remove x m] returns a map containing the same bindings as [m],
+	except for [x] which is unbound in the returned map. *)
+
+    Parameter mem : key -> t elt -> bool.
+    (** [mem x m] returns [true] if [m] contains a binding for [x],
+	and [false] otherwise. *)
+
+    Parameter bindings : t elt -> list (key*elt).
+    (** [bindings m] returns an assoc list corresponding to the bindings
+        of [m], in any order. *)
+
+    Parameter cardinal : t elt -> nat.
+    (** [cardinal m] returns the number of bindings in [m]. *)
+
+    Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A.
+    (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)],
+	where [k1] ... [kN] are the keys of all bindings in [m]
+	(in any order), and [d1] ... [dN] are the associated data. *)
+
+    Parameter equal : (elt -> elt -> bool) -> t elt -> t elt -> bool.
+    (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are equal,
+      that is, contain equal keys and associate them with equal data.
+      [cmp] is the equality predicate used to compare the data associated
+      with the keys. *)
+
+    Variable elt' elt'' : Type.
+
+    Parameter map : (elt -> elt') -> t elt -> t elt'.
+    (** [map f m] returns a map with same domain as [m], where the associated
+	value a of all bindings of [m] has been replaced by the result of the
+	application of [f] to [a]. Since Coq is purely functional, the order
+        in which the bindings are passed to [f] is irrelevant. *)
+
+    Parameter mapi : (key -> elt -> elt') -> t elt -> t elt'.
+    (** Same as [map], but the function receives as arguments both the
+	key and the associated value for each binding of the map. *)
+
+    Parameter merge : (key -> option elt -> option elt' -> option elt'') ->
+                      t elt -> t elt' ->  t elt''.
+    (** [merge f m m'] creates a new map whose bindings belong to the ones
+        of either [m] or [m']. The presence and value for a key [k] is
+        determined by [f k e e'] where [e] and [e'] are the (optional)
+        bindings of [k] in [m] and [m']. *)
+
+  End Ops.
+  Section Specs.
+
+    Variable elt:Type.
+
+    Parameter MapsTo : key -> elt -> t elt -> Prop.
+
+    Definition In (k:key)(m: t elt) : Prop := exists e:elt, MapsTo k e m.
+
+    Global Declare Instance MapsTo_compat :
+      Proper (E.eq==>Logic.eq==>Logic.eq==>iff) MapsTo.
+
+    Variable m m' : t elt.
+    Variable x y : key.
+    Variable e : elt.
+
+    Parameter find_spec : find x m = Some e <-> MapsTo x e m.
+    Parameter mem_spec : mem x m = true <-> In x m.
+    Parameter empty_spec : find x (@empty elt) = None.
+    Parameter is_empty_spec : is_empty m = true <-> forall x, find x m = None.
+    Parameter add_spec1 : find x (add x e m) = Some e.
+    Parameter add_spec2 : ~E.eq x y -> find y (add x e m) = find y m.
+    Parameter remove_spec1 : find x (remove x m) = None.
+    Parameter remove_spec2 : ~E.eq x y -> find y (remove x m) = find y m.
+
+    (** Specification of [bindings] *)
+    Parameter bindings_spec1 :
+      InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m.
+    (** When compared with ordered maps, here comes the only
+        property that is really weaker: *)
+    Parameter bindings_spec2w : NoDupA eq_key (bindings m).
+
+    (** Specification of [cardinal] *)
+    Parameter cardinal_spec : cardinal m = length (bindings m).
+
+    (** Specification of [fold] *)
+    Parameter fold_spec :
+      forall {A} (i : A) (f : key -> elt -> A -> A),
+      fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i.
+
+    (** Equality of maps *)
+
+    (** Caveat: there are at least three distinct equality predicates on maps.
+      - The simpliest (and maybe most natural) way is to consider keys up to
+        their equivalence [E.eq], but elements up to Leibniz equality, in
+        the spirit of [eq_key_elt] above. This leads to predicate [Equal].
+      - Unfortunately, this [Equal] predicate can't be used to describe
+        the [equal] function, since this function (for compatibility with
+        ocaml) expects a boolean comparison [cmp] that may identify more
+        elements than Leibniz. So logical specification of [equal] is done
+        via another predicate [Equivb]
+      - This predicate [Equivb] is quite ad-hoc with its boolean [cmp],
+        it can be generalized in a [Equiv] expecting a more general
+        (possibly non-decidable) equality predicate on elements *)
+
+    Definition Equal (m m':t elt) := forall y, find y m = find y m'.
+    Definition Equiv (eq_elt:elt->elt->Prop) m m' :=
+      (forall k, In k m <-> In k m') /\
+      (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
+    Definition Equivb (cmp: elt->elt->bool) := Equiv (Cmp cmp).
+
+    (** Specification of [equal] *)
+    Parameter equal_spec : forall cmp : elt -> elt -> bool,
+      equal cmp m m' = true <-> Equivb cmp m m'.
+
+  End Specs.
+  Section SpecMaps.
+
+    Variables elt elt' elt'' : Type.
+
+    Parameter map_spec : forall (f:elt->elt') m x,
+      find x (map f m) = option_map f (find x m).
+
+    Parameter mapi_spec : forall (f:key->elt->elt') m x,
+      exists y:key, E.eq y x /\ find x (mapi f m) = option_map (f y) (find x m).
+
+    Parameter merge_spec1 :
+      forall (f:key->option elt->option elt'->option elt'') m m' x,
+      In x m \/ In x m' ->
+      exists y:key, E.eq y x /\
+                    find x (merge f m m') = f y (find x m) (find x m').
+
+    Parameter merge_spec2 :
+      forall (f:key -> option elt->option elt'->option elt'') m m' x,
+      In x (merge f m m') -> In x m \/ In x m'.
+
+  End SpecMaps.
+End WSfun.
+
+(** ** Static signature for Weak Maps
+
+    Similar to [WSfun] but expressed in a self-contained way. *)
+
+Module Type WS.
+  Declare Module E : DecidableType.
+  Include WSfun E.
+End WS.
+
+
+
+(** ** Maps on ordered keys, functorial signature *)
+
+Module Type Sfun (E : OrderedType).
+  Include WSfun E.
+
+  Definition lt_key {elt} (p p':key*elt) := E.lt (fst p) (fst p').
+
+  (** Additional specification of [bindings] *)
+
+  Parameter bindings_spec2 : forall {elt}(m : t elt), sort lt_key (bindings m).
+
+  (** Remark: since [fold] is specified via [bindings], this stronger
+   specification of [bindings] has an indirect impact on [fold],
+   which can now be proved to receive bindings in increasing order. *)
+
+End Sfun.
+
+
+(** ** Maps on ordered keys, self-contained signature *)
+
+Module Type S.
+  Declare Module E : OrderedType.
+  Include Sfun E.
+End S.
+
+
+
+(** ** Maps with ordering both on keys and datas *)
+
+Module Type Sord.
+
+  Declare Module Data : OrderedType.
+  Declare Module MapS : S.
+  Import MapS.
+
+  Definition t := MapS.t Data.t.
+
+  Include HasEq <+ HasLt <+ IsEq <+ IsStrOrder.
+
+  Definition cmp e e' :=
+    match Data.compare e e' with Eq => true | _ => false end.
+
+  Parameter eq_spec : forall m m', eq m m' <-> Equivb cmp m m'.
+
+  Parameter compare : t -> t -> comparison.
+
+  Parameter compare_spec : forall m1 m2, CompSpec eq lt m1 m2 (compare m1 m2).
+
+End Sord.
+
+
+(* TODO: provides filter + partition *)
+
+(* TODO: provide split
+   Parameter split : key -> t elt -> t elt * option elt * t elt.
+
+   Parameter split_spec k m :
+     split k m = (filter (fun x -> E.compare x k) m, find k m, filter ...)
+
+   min_binding, max_binding, choose ?
+*)
diff --git a/theories/MMaps/MMapWeakList.v b/theories/MMaps/MMapWeakList.v
new file mode 100644
index 000000000..656c61e11
--- /dev/null
+++ b/theories/MMaps/MMapWeakList.v
@@ -0,0 +1,687 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(** * Finite map library *)
+
+(** This file proposes an implementation of the non-dependant interface
+ [MMapInterface.WS] using lists of pairs, unordered but without redundancy. *)
+
+Require Import MMapInterface EqualitiesFacts.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Lemma Some_iff {A} (a a' : A) : Some a = Some a' <-> a = a'.
+Proof. split; congruence. Qed.
+
+Module Raw (X:DecidableType).
+
+Module Import PX := KeyDecidableType X.
+
+Definition key := X.t.
+Definition t (elt:Type) := list (X.t * elt).
+
+Ltac dec := match goal with
+ | |- context [ X.eq_dec ?x ?x ] =>
+   let E := fresh "E" in destruct (X.eq_dec x x) as [E|E]; [ | now elim E]
+ | H : X.eq ?x ?y |- context [ X.eq_dec ?x ?y ] =>
+   let E := fresh "E" in destruct (X.eq_dec x y) as [_|E]; [ | now elim E]
+ | H : ~X.eq ?x ?y |- context [ X.eq_dec ?x ?y ] =>
+   let E := fresh "E" in destruct (X.eq_dec x y) as [E|_]; [ now elim H | ]
+ | |- context [ X.eq_dec ?x ?y ] =>
+   let E := fresh "E" in destruct (X.eq_dec x y) as [E|E]
+end.
+
+Section Elt.
+
+Variable elt : Type.
+Notation NoDupA := (@NoDupA _ eqk).
+
+(** * [find] *)
+
+Fixpoint find (k:key) (s: t elt) : option elt :=
+  match s with
+   | nil => None
+   | (k',x)::s' => if X.eq_dec k k' then Some x else find k s'
+  end.
+
+Lemma find_spec : forall m (Hm:NoDupA m) x e,
+  find x m = Some e <-> MapsTo x e m.
+Proof.
+ unfold PX.MapsTo.
+ induction m as [ | (k,e) m IH]; simpl.
+ - split; inversion 1.
+ - intros Hm k' e'. rewrite InA_cons.
+   change (eqke (k',e') (k,e)) with (X.eq k' k /\ e' = e).
+   inversion_clear Hm. dec.
+   + rewrite Some_iff; intuition.
+     elim H. apply InA_eqk with (k',e'); auto.
+   + rewrite IH; intuition.
+Qed.
+
+(** * [mem] *)
+
+Fixpoint mem (k : key) (s : t elt) : bool :=
+  match s with
+   | nil => false
+   | (k',_) :: l => if X.eq_dec k k' then true else mem k l
+  end.
+
+Lemma mem_spec : forall m (Hm:NoDupA m) x, mem x m = true <-> In x m.
+Proof.
+ induction m as [ | (k,e) m IH]; simpl; intros Hm x.
+ - split. discriminate. inversion_clear 1. inversion H0.
+ - inversion_clear Hm. rewrite PX.In_cons; simpl.
+   rewrite <- IH by trivial.
+   dec; intuition.
+Qed.
+
+(** * [empty] *)
+
+Definition empty : t elt := nil.
+
+Lemma empty_spec x : find x empty = None.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma empty_NoDup : NoDupA empty.
+Proof.
+ unfold empty; auto.
+Qed.
+
+(** * [is_empty] *)
+
+Definition is_empty (l : t elt) : bool := if l then true else false.
+
+Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None.
+Proof.
+ destruct m; simpl; intuition; try discriminate.
+ specialize (H a).
+ revert H. now dec.
+Qed.
+
+(* Not part of the exported specifications, used later for [merge]. *)
+
+Lemma find_eq : forall m (Hm:NoDupA m) x x',
+   X.eq x x' -> find x m = find x' m.
+Proof.
+ induction m; simpl; auto; destruct a; intros.
+ inversion_clear Hm.
+ rewrite (IHm H1 x x'); auto.
+ dec; dec; trivial.
+ elim E0. now transitivity x.
+ elim E. now transitivity x'.
+Qed.
+
+(** * [add] *)
+
+Fixpoint add (k : key) (x : elt) (s : t elt) : t elt :=
+  match s with
+   | nil => (k,x) :: nil
+   | (k',y) :: l => if X.eq_dec k k' then (k,x)::l else (k',y)::add k x l
+  end.
+
+Lemma add_spec1 m x e : find x (add x e m) = Some e.
+Proof.
+ induction m as [ | (k,e') m IH]; simpl.
+ - now dec.
+ - dec; simpl; now dec.
+Qed.
+
+Lemma add_spec2 m x y e : ~X.eq x y -> find y (add x e m) = find y m.
+Proof.
+ intros N.
+ assert (N' : ~X.eq y x) by now contradict N.
+ induction m as [ | (k,e') m IH]; simpl.
+ - dec; trivial.
+ - repeat (dec; simpl); trivial. elim N. now transitivity k.
+Qed.
+
+Lemma add_InA : forall m x y e e',
+  ~ X.eq x y -> InA eqk (y,e) (add x e' m) -> InA eqk (y,e) m.
+Proof.
+ induction m as [ | (k,e') m IH]; simpl; intros.
+ - inversion_clear H0. elim H. symmetry; apply H1. inversion_clear H1.
+ - revert H0; dec; rewrite !InA_cons.
+   + rewrite E. intuition.
+   + intuition. right; eapply IH; eauto.
+Qed.
+
+Lemma add_NoDup : forall m (Hm:NoDupA m) x e, NoDupA (add x e m).
+Proof.
+ induction m as [ | (k,e') m IH]; simpl; intros Hm x e.
+ - constructor; auto. now inversion 1.
+ - inversion_clear Hm. dec; constructor; auto.
+   + contradict H. apply InA_eqk with (x,e); auto.
+   + contradict H; apply add_InA with x e; auto.
+Qed.
+
+(** * [remove] *)
+
+Fixpoint remove (k : key) (s : t elt) : t elt :=
+  match s with
+   | nil => nil
+   | (k',x) :: l => if X.eq_dec k k' then l else (k',x) :: remove k l
+  end.
+
+Lemma remove_spec1 m (Hm: NoDupA m) x : find x (remove x m) = None.
+Proof.
+ induction m as [ | (k,e') m IH]; simpl; trivial.
+ inversion_clear Hm.
+ repeat (dec; simpl); auto.
+ destruct (find x m) eqn:F; trivial.
+ apply find_spec in F; trivial.
+ elim H. apply InA_eqk with (x,e); auto.
+Qed.
+
+Lemma remove_spec2 m (Hm: NoDupA m) x y : ~X.eq x y ->
+  find y (remove x m) = find y m.
+Proof.
+ induction m as [ | (k,e') m IH]; simpl; trivial; intros E.
+ inversion_clear Hm.
+ repeat (dec; simpl); auto.
+ elim E. now transitivity k.
+Qed.
+
+Lemma remove_InA : forall m (Hm:NoDupA m) x y e,
+  InA eqk (y,e) (remove x m) -> InA eqk (y,e) m.
+Proof.
+ induction m as [ | (k,e') m IH]; simpl; trivial; intros.
+ inversion_clear Hm.
+ revert H; dec; rewrite !InA_cons; intuition.
+ right; eapply H; eauto.
+Qed.
+
+Lemma remove_NoDup : forall m (Hm:NoDupA m) x, NoDupA (remove x m).
+Proof.
+ induction m.
+ simpl; intuition.
+ intros.
+ inversion_clear Hm.
+ destruct a as (x',e').
+ simpl; case (X.eq_dec x x'); auto.
+ constructor; auto.
+ contradict H; apply remove_InA with x; auto.
+Qed.
+
+(** * [bindings] *)
+
+Definition bindings (m: t elt) := m.
+
+Lemma bindings_spec1 m x e : InA eqke (x,e) (bindings m) <-> MapsTo x e m.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma bindings_spec2w m (Hm:NoDupA m) : NoDupA (bindings m).
+Proof.
+ trivial.
+Qed.
+
+(** * [fold] *)
+
+Fixpoint fold (A:Type)(f:key->elt->A->A)(m:t elt) (acc : A) :  A :=
+  match m with
+   | nil => acc
+   | (k,e)::m' => fold f m' (f k e acc)
+  end.
+
+Lemma fold_spec : forall m (A:Type)(i:A)(f:key->elt->A->A),
+  fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i.
+Proof.
+ induction m as [ | (k,e) m IH]; simpl; auto.
+Qed.
+
+(** * [equal] *)
+
+Definition check (cmp : elt -> elt -> bool)(k:key)(e:elt)(m': t elt) :=
+  match find k m' with
+   | None => false
+   | Some e' => cmp e e'
+  end.
+
+Definition submap (cmp : elt -> elt -> bool)(m m' : t elt) : bool :=
+  fold (fun k e b => andb (check cmp k e m') b) m true.
+
+Definition equal (cmp : elt -> elt -> bool)(m m' : t elt) : bool :=
+  andb (submap cmp m m') (submap (fun e' e => cmp e e') m' m).
+
+Definition Submap (cmp:elt->elt->bool) m m' :=
+  (forall k, In k m -> In k m') /\
+  (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).
+
+Definition Equivb (cmp:elt->elt->bool) m m' :=
+  (forall k, In k m <-> In k m') /\
+  (forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).
+
+Lemma submap_1 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp,
+  Submap cmp m m' -> submap cmp m m' = true.
+Proof.
+ unfold Submap, submap.
+ induction m.
+ simpl; auto.
+ destruct a; simpl; intros.
+ destruct H.
+ inversion_clear Hm.
+ assert (H3 : In t0 m').
+ { apply H; exists e; auto with *. }
+ destruct H3 as (e', H3).
+ assert (H4 : find t0 m' = Some e') by now apply find_spec.
+ unfold check at 2. rewrite H4.
+ rewrite (H0 t0); simpl; auto with *.
+ eapply IHm; auto.
+ split; intuition.
+ apply H.
+ destruct H6 as (e'',H6); exists e''; auto.
+ apply H0 with k; auto.
+Qed.
+
+Lemma submap_2 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp,
+  submap cmp m m' = true -> Submap cmp m m'.
+Proof.
+ unfold Submap, submap.
+ induction m.
+ simpl; auto.
+ intuition.
+ destruct H0; inversion H0.
+ inversion H0.
+
+ destruct a; simpl; intros.
+ inversion_clear Hm.
+ rewrite andb_b_true in H.
+ assert (check cmp t0 e m' = true).
+  clear H1 H0 Hm' IHm.
+  set (b:=check cmp t0 e m') in *.
+  generalize H; clear H; generalize b; clear b.
+  induction m; simpl; auto; intros.
+  destruct a; simpl in *.
+  destruct (andb_prop _ _ (IHm _ H)); auto.
+ rewrite H2 in H.
+ destruct (IHm H1 m' Hm' cmp H); auto.
+ unfold check in H2.
+ case_eq (find t0 m'); [intros e' H5 | intros H5];
+  rewrite H5 in H2; try discriminate.
+ split; intros.
+ destruct H6 as (e0,H6); inversion_clear H6.
+ compute in H7; destruct H7; subst.
+ exists e'.
+ apply PX.MapsTo_eq with t0; auto with *.
+ apply find_spec; auto.
+ apply H3.
+ exists e0; auto.
+ inversion_clear H6.
+ compute in H8; destruct H8; subst.
+ assert (H8 : MapsTo t0 e'0 m'). { eapply PX.MapsTo_eq; eauto. }
+ apply find_spec in H8; trivial. congruence.
+ apply H4 with k; auto.
+Qed.
+
+(** Specification of [equal] *)
+
+Lemma equal_spec : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp,
+  equal cmp m m' = true <-> Equivb cmp m m'.
+Proof.
+ unfold Equivb, equal.
+ split.
+ - intros.
+   destruct (andb_prop _ _ H); clear H.
+   generalize (submap_2 Hm Hm' H0).
+   generalize (submap_2 Hm' Hm H1).
+   firstorder.
+ - intuition.
+   apply andb_true_intro; split; apply submap_1; unfold Submap; firstorder.
+Qed.
+End Elt.
+Section Elt2.
+Variable elt elt' : Type.
+
+(** * [map] and [mapi] *)
+
+Fixpoint map (f:elt -> elt') (m:t elt) : t elt' :=
+  match m with
+   | nil => nil
+   | (k,e)::m' => (k,f e) :: map f m'
+  end.
+
+Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' :=
+  match m with
+   | nil => nil
+   | (k,e)::m' => (k,f k e) :: mapi f m'
+  end.
+
+(** Specification of [map] *)
+
+Lemma map_spec (f:elt->elt')(m:t elt)(x:key) :
+  find x (map f m) = option_map f (find x m).
+Proof.
+ induction m as [ | (k,e) m IH]; simpl; trivial.
+ dec; simpl; trivial.
+Qed.
+
+Lemma map_NoDup m (Hm : NoDupA (@eqk elt) m)(f:elt->elt') :
+  NoDupA (@eqk elt') (map f m).
+Proof.
+ induction m; simpl; auto.
+ intros.
+ destruct a as (x',e').
+ inversion_clear Hm.
+ constructor; auto.
+ contradict H.
+ clear IHm H0.
+ induction m; simpl in *; auto.
+ inversion H.
+ destruct a; inversion H; auto.
+Qed.
+
+(** Specification of [mapi] *)
+
+Lemma mapi_spec (f:key->elt->elt')(m:t elt)(x:key) :
+  exists y, X.eq y x /\ find x (mapi f m) = option_map (f y) (find x m).
+Proof.
+ induction m as [ | (k,e) m IH]; simpl; trivial.
+ - now exists x.
+ - dec; simpl.
+   + now exists k.
+   + destruct IH as (y,(Hy,H)). now exists y.
+Qed.
+
+Lemma mapi_NoDup : forall m (Hm : NoDupA (@eqk elt) m)(f: key->elt->elt'),
+  NoDupA (@eqk elt') (mapi f m).
+Proof.
+ induction m; simpl; auto.
+ intros.
+ destruct a as (x',e').
+ inversion_clear Hm; auto.
+ constructor; auto.
+ contradict H.
+ clear IHm H0.
+ induction m; simpl in *; auto.
+ inversion_clear H.
+ destruct a; inversion_clear H; auto.
+Qed.
+
+End Elt2.
+
+Lemma mapfst_InA {elt}(m:t elt) x :
+ InA X.eq x (List.map fst m) <-> In x m.
+Proof.
+ induction m as [| (k,e) m IH]; simpl; auto.
+ - split; inversion 1. inversion H0.
+ - rewrite InA_cons, In_cons. simpl. now rewrite IH.
+Qed.
+
+Lemma mapfst_NoDup {elt}(m:t elt) :
+ NoDupA X.eq (List.map fst m) <-> NoDupA eqk m.
+Proof.
+ induction m as [| (k,e) m IH]; simpl.
+ - split; constructor.
+ - split; inversion_clear 1; constructor; try apply IH; trivial.
+   + contradict H0. rewrite mapfst_InA. eapply In_alt'; eauto.
+   + rewrite mapfst_InA. contradict H0. now apply In_alt'.
+Qed.
+
+Lemma filter_NoDup f (m:list key) :
+ NoDupA X.eq m -> NoDupA X.eq (List.filter f m).
+Proof.
+ induction 1; simpl.
+ - constructor.
+ - destruct (f x); trivial. constructor; trivial.
+   contradict H. rewrite InA_alt in *. destruct H as (y,(Hy,H)).
+   exists y; split; trivial. now rewrite filter_In in H.
+Qed.
+
+Lemma NoDupA_unique_repr (l:list key) x y :
+ NoDupA X.eq l -> X.eq x y -> List.In x l -> List.In y l -> x = y.
+Proof.
+ intros H E Hx Hy.
+ induction H; simpl in *.
+ - inversion Hx.
+ - intuition; subst; trivial.
+   elim H. apply InA_alt. now exists y.
+   elim H. apply InA_alt. now exists x.
+Qed.
+
+Section Elt3.
+
+Variable elt elt' elt'' : Type.
+
+Definition restrict (m:t elt)(k:key) :=
+ match find k m with
+ | None => true
+ | Some _ => false
+ end.
+
+Definition domains (m:t elt)(m':t elt') :=
+ List.map fst m ++ List.filter (restrict m) (List.map fst m').
+
+Lemma domains_InA m m' (Hm : NoDupA eqk m) x :
+ InA X.eq x (domains m m') <-> In x m \/ In x m'.
+Proof.
+ unfold domains.
+ assert (Proper (X.eq==>eq) (restrict m)).
+ { intros k k' Hk. unfold restrict. now rewrite (find_eq Hm Hk). }
+ rewrite InA_app_iff, filter_InA, !mapfst_InA; intuition.
+ unfold restrict.
+ destruct (find x m) eqn:F.
+ - left. apply find_spec in F; trivial. now exists e.
+ - now right.
+Qed.
+
+Lemma domains_NoDup m m' : NoDupA eqk m -> NoDupA eqk m' ->
+ NoDupA X.eq (domains m m').
+Proof.
+ intros Hm Hm'. unfold domains.
+ apply NoDupA_app; auto with *.
+ - now apply mapfst_NoDup.
+ - now apply filter_NoDup, mapfst_NoDup.
+ - intros x.
+   rewrite mapfst_InA. intros (e,H).
+   apply find_spec in H; trivial.
+   rewrite InA_alt. intros (y,(Hy,H')).
+   rewrite (find_eq Hm Hy) in H.
+   rewrite filter_In in H'. destruct H' as (_,H').
+   unfold restrict in H'. now rewrite H in H'.
+Qed.
+
+Fixpoint fold_keys (f:key->option elt'') l :=
+  match l with
+    | nil => nil
+    | k::l =>
+      match f k with
+        | Some e => (k,e)::fold_keys f l
+        | None => fold_keys f l
+      end
+  end.
+
+Lemma fold_keys_In f l x e :
+  List.In (x,e) (fold_keys f l) <-> List.In x l /\ f x = Some e.
+Proof.
+ induction l as [|k l IH]; simpl.
+ - intuition.
+ - destruct (f k) eqn:F; simpl; rewrite IH; clear IH; intuition;
+   try left; congruence.
+Qed.
+
+Lemma fold_keys_NoDup f l :
+  NoDupA X.eq l -> NoDupA eqk (fold_keys f l).
+Proof.
+ induction 1; simpl.
+ - constructor.
+ - destruct (f x); trivial.
+   constructor; trivial. contradict H.
+   apply InA_alt in H. destruct H as ((k,e'),(E,H)).
+   rewrite fold_keys_In in H.
+   apply InA_alt. exists k. now split.
+Qed.
+
+Variable f : key -> option elt -> option elt' -> option elt''.
+
+Definition merge m m' : t elt'' :=
+ fold_keys (fun k => f k (find k m) (find k m')) (domains m m').
+
+Lemma merge_NoDup m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m') :
+  NoDupA (@eqk elt'') (merge m m').
+Proof.
+ now apply fold_keys_NoDup, domains_NoDup.
+Qed.
+
+Lemma merge_spec1 m (Hm:NoDupA eqk m) m' (Hm':NoDupA eqk m') x :
+  In x m \/ In x m' ->
+  exists y:key, X.eq y x /\
+                find x (merge m m') = f y (find x m) (find x m').
+Proof.
+ assert (Hmm' : NoDupA eqk (merge m m')) by now apply merge_NoDup.
+ rewrite <- domains_InA; trivial.
+ rewrite InA_alt. intros (y,(Hy,H)).
+ exists y; split; [easy|].
+ rewrite (find_eq Hm Hy), (find_eq Hm' Hy).
+ destruct (f y (find y m) (find y m')) eqn:F.
+ - apply find_spec; trivial.
+   red. apply InA_alt. exists (y,e). split. now split.
+   unfold merge. apply fold_keys_In. now split.
+ - destruct (find x (merge m m')) eqn:F'; trivial.
+   rewrite <- F; clear F. symmetry.
+   apply find_spec in F'; trivial.
+   red in F'. rewrite InA_alt in F'.
+   destruct F' as ((y',e'),(E,F')).
+   unfold merge in F'; rewrite fold_keys_In in F'.
+   destruct F' as (H',F').
+   compute in E; destruct E as (Hy',<-).
+   replace y with y'; trivial.
+   apply (@NoDupA_unique_repr (domains m m')); auto.
+   now apply domains_NoDup.
+   now transitivity x.
+Qed.
+
+Lemma merge_spec2 m (Hm:NoDupA eqk m) m' (Hm':NoDupA eqk m') x :
+  In x (merge m m') -> In x m \/ In x m'.
+Proof.
+ rewrite <- domains_InA; trivial.
+ intros (e,H). red in H. rewrite InA_alt in H. destruct H as ((k,e'),(E,H)).
+ unfold merge in H; rewrite fold_keys_In in H. destruct H as (H,_).
+ apply InA_alt. exists k. split; trivial. now destruct E.
+Qed.
+
+End Elt3.
+End Raw.
+
+
+Module Make (X: DecidableType) <: WS with Module E:=X.
+ Module Raw := Raw X.
+
+ Module E := X.
+ Definition key := E.t.
+ Definition eq_key {elt} := @Raw.PX.eqk elt.
+ Definition eq_key_elt {elt} := @Raw.PX.eqke elt.
+
+ Record t_ (elt:Type) := Mk
+  {this :> Raw.t elt;
+   nodup : NoDupA Raw.PX.eqk this}.
+ Definition t := t_.
+
+ Definition empty {elt} : t elt := Mk (Raw.empty_NoDup elt).
+
+Section Elt.
+ Variable elt elt' elt'':Type.
+ Implicit Types m : t elt.
+ Implicit Types x y : key.
+ Implicit Types e : elt.
+
+ Definition find x m : option elt := Raw.find x m.(this).
+ Definition mem x m : bool := Raw.mem x m.(this).
+ Definition is_empty m : bool := Raw.is_empty m.(this).
+ Definition add x e m : t elt := Mk (Raw.add_NoDup m.(nodup) x e).
+ Definition remove x m : t elt := Mk (Raw.remove_NoDup m.(nodup) x).
+ Definition map f m : t elt' := Mk (Raw.map_NoDup m.(nodup) f).
+ Definition mapi (f:key->elt->elt') m : t elt' :=
+   Mk (Raw.mapi_NoDup m.(nodup) f).
+ Definition merge f m (m':t elt') : t elt'' :=
+   Mk (Raw.merge_NoDup f m.(nodup) m'.(nodup)).
+ Definition bindings m : list (key*elt) := Raw.bindings m.(this).
+ Definition cardinal m := length m.(this).
+ Definition fold {A}(f:key->elt->A->A) m (i:A) : A := Raw.fold f m.(this) i.
+ Definition equal cmp m m' : bool := Raw.equal cmp m.(this) m'.(this).
+ Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e m.(this).
+ Definition In x m : Prop := Raw.PX.In x m.(this).
+
+ Definition Equal m m' := forall y, find y m = find y m'.
+ Definition Equiv (eq_elt:elt->elt->Prop) m m' :=
+         (forall k, In k m <-> In k m') /\
+         (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
+ Definition Equivb cmp m m' : Prop := Raw.Equivb cmp m.(this) m'.(this).
+
+ Instance MapsTo_compat :
+   Proper (E.eq==>Logic.eq==>Logic.eq==>iff) MapsTo.
+ Proof.
+   intros x x' Hx e e' <- m m' <-. unfold MapsTo. now rewrite Hx.
+ Qed.
+
+ Lemma find_spec m : forall x e, find x m = Some e <-> MapsTo x e m.
+ Proof. exact (Raw.find_spec m.(nodup)). Qed.
+
+ Lemma mem_spec m : forall x, mem x m = true <-> In x m.
+ Proof. exact (Raw.mem_spec m.(nodup)). Qed.
+
+ Lemma empty_spec : forall x, find x empty = None.
+ Proof. exact (Raw.empty_spec _). Qed.
+
+ Lemma is_empty_spec m : is_empty m = true <-> (forall x, find x m = None).
+ Proof. exact (Raw.is_empty_spec m.(this)). Qed.
+
+ Lemma add_spec1 m : forall x e, find x (add x e m) = Some e.
+ Proof. exact (Raw.add_spec1 m.(this)). Qed.
+ Lemma add_spec2 m : forall x y e, ~E.eq x y -> find y (add x e m) = find y m.
+ Proof. exact (Raw.add_spec2 m.(this)). Qed.
+
+ Lemma remove_spec1 m : forall x, find x (remove x m) = None.
+ Proof. exact (Raw.remove_spec1 m.(nodup)). Qed.
+ Lemma remove_spec2 m : forall x y, ~E.eq x y -> find y (remove x m) = find y m.
+ Proof. exact (Raw.remove_spec2 m.(nodup)). Qed.
+
+ Lemma bindings_spec1 m : forall x e,
+   InA eq_key_elt (x,e) (bindings m) <-> MapsTo x e m.
+ Proof. exact (Raw.bindings_spec1 m.(this)). Qed.
+ Lemma bindings_spec2w m : NoDupA eq_key (bindings m).
+ Proof. exact (Raw.bindings_spec2w m.(nodup)). Qed.
+
+ Lemma cardinal_spec m : cardinal m = length (bindings m).
+ Proof. reflexivity. Qed.
+
+ Lemma fold_spec m : forall (A : Type) (i : A) (f : key -> elt -> A -> A),
+        fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i.
+ Proof. exact (Raw.fold_spec m.(this)). Qed.
+
+ Lemma equal_spec m m' : forall cmp, equal cmp m m' = true <-> Equivb cmp m m'.
+ Proof. exact (Raw.equal_spec m.(nodup) m'.(nodup)). Qed.
+
+End Elt.
+
+ Lemma map_spec {elt elt'} (f:elt->elt') m :
+   forall x, find x (map f m) = option_map f (find x m).
+ Proof. exact (Raw.map_spec f m.(this)). Qed.
+
+ Lemma mapi_spec {elt elt'} (f:key->elt->elt') m :
+   forall x, exists y,
+     E.eq y x /\ find x (mapi f m) = option_map (f y) (find x m).
+ Proof. exact (Raw.mapi_spec f m.(this)). Qed.
+
+ Lemma merge_spec1 {elt elt' elt''}
+  (f:key->option elt->option elt'->option elt'') m m' :
+  forall x,
+   In x m \/ In x m' ->
+   exists y, E.eq y x /\ find x (merge f m m') = f y (find x m) (find x m').
+ Proof. exact (Raw.merge_spec1 f m.(nodup) m'.(nodup)). Qed.
+
+ Lemma merge_spec2 {elt elt' elt''}
+  (f:key->option elt->option elt'->option elt'') m m' :
+  forall x,
+   In x (merge f m m') -> In x m \/ In x m'.
+ Proof. exact (Raw.merge_spec2 m.(nodup) m'.(nodup)). Qed.
+
+End Make.
diff --git a/theories/MMaps/MMaps.v b/theories/MMaps/MMaps.v
new file mode 100644
index 000000000..93d117817
--- /dev/null
+++ b/theories/MMaps/MMaps.v
@@ -0,0 +1,18 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+
+Require Export Orders OrdersEx OrdersAlt.
+Require Export Equalities.
+Require Export MMapInterface.
+Require Export MMapFacts.
+Require Export MMapWeakList.
+(*
+Require Export MMapList.
+Require Export MMapPositive.
+*)
\ No newline at end of file
diff --git a/theories/MMaps/vo.itarget b/theories/MMaps/vo.itarget
new file mode 100644
index 000000000..875d7bb22
--- /dev/null
+++ b/theories/MMaps/vo.itarget
@@ -0,0 +1,4 @@
+MMapInterface.vo
+MMapFacts.vo
+MMapWeakList.vo
+MMaps.vo
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index 11d94c119..b394cf48d 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -8,132 +8,170 @@
 
 Require Import Equalities Bool SetoidList RelationPairs.
 
-(** * Keys and datas used in FMap *)
+(** * Keys and datas used in MMap *)
 
-Module KeyDecidableType(Import D:DecidableType).
+Module KeyDecidableType(D:DecidableType).
 
- Section Elt.
- Variable elt : Type.
- Notation key:=t.
+ Local Open Scope signature_scope.
+ Local Notation key := D.t.
 
-  Local Open Scope signature_scope.
+ Definition eqk {elt} : relation (key*elt) := D.eq @@1.
+ Definition eqke {elt} : relation (key*elt) := D.eq * Logic.eq.
 
-  Definition eqk : relation (key*elt) := eq @@1.
-  Definition eqke : relation (key*elt) := eq * Logic.eq.
-  Hint Unfold eqk eqke.
+ Hint Unfold eqk eqke.
 
-  (* eqke is stricter than eqk *)
+ (** eqk, eqke are equalities *)
 
-  Global Instance eqke_eqk : subrelation eqke eqk.
-  Proof. firstorder. Qed.
+ Instance eqk_equiv {elt} : Equivalence (@eqk elt) := _.
 
-  (* eqk, eqke are equalities, ltk is a strict order *)
+ Instance eqke_equiv {elt} : Equivalence (@eqke elt) := _.
 
-  Global Instance eqk_equiv : Equivalence eqk := _.
+ (** eqke is stricter than eqk *)
 
-  Global Instance eqke_equiv : Equivalence eqke := _.
+ Instance eqke_eqk {elt} : subrelation (@eqke elt) (@eqk elt).
+ Proof. firstorder. Qed.
 
-  (* Additionnal facts *)
+ (** Alternative definitions of eqke and eqk *)
 
-  Lemma InA_eqke_eqk :
-     forall x m, InA eqke x m -> InA eqk x m.
-  Proof.
-    unfold eqke, RelProd; induction 1; firstorder.
-  Qed.
-  Hint Resolve InA_eqke_eqk.
+ Lemma eqke_def {elt} k k' (e e':elt) :
+  eqke (k,e) (k',e') = (D.eq k k' /\ e = e').
+ Proof. reflexivity. Defined.
 
-  Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
-  Proof.
-   intros. rewrite <- H; auto.
-  Qed.
+ Lemma eqke_def' {elt} (p q:key*elt) :
+  eqke p q = (D.eq (fst p) (fst q) /\ snd p = snd q).
+ Proof. reflexivity. Defined.
 
-  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
-  Definition In k m := exists e:elt, MapsTo k e m.
+ Lemma eqke_1 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> D.eq k k'.
+ Proof. now destruct 1. Qed.
 
-  Hint Unfold MapsTo In.
+ Lemma eqke_2 {elt} k k' (e e':elt) : eqke (k,e) (k',e') -> e=e'.
+ Proof. now destruct 1. Qed.
 
-  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
+ Lemma eqk_def {elt} k k' (e e':elt) : eqk (k,e) (k',e') = D.eq k k'.
+ Proof. reflexivity. Defined.
 
-  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
-  Proof.
-  firstorder.
-  exists x; auto.
-  induction H.
-  destruct y; compute in H.
-  exists e; left; auto.
-  destruct IHInA as [e H0].
-  exists e; auto.
-  Qed.
-
-  Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
-  Proof.
+ Lemma eqk_def' {elt} (p q:key*elt) : eqk p q = D.eq (fst p) (fst q).
+ Proof. reflexivity. Qed.
+
+ Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'.
+ Proof. trivial. Qed.
+
+ Hint Resolve eqke_1 eqke_2 eqk_1.
+
+ (* Additionnal facts *)
+
+ Lemma InA_eqke_eqk {elt} p (m:list (key*elt)) :
+   InA eqke p m -> InA eqk p m.
+ Proof.
+  induction 1; firstorder.
+ Qed.
+ Hint Resolve InA_eqke_eqk.
+
+ Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) :
+  InA eqk p m -> exists q, eqk p q /\ InA eqke q m.
+ Proof.
+  induction 1; firstorder.
+ Qed.
+
+ Lemma InA_eqk {elt} p q (m:list (key*elt)) :
+   eqk p q -> InA eqk p m -> InA eqk q m.
+ Proof.
+  now intros <-.
+ Qed.
+
+ Definition MapsTo {elt} (k:key)(e:elt):= InA eqke (k,e).
+ Definition In {elt} k m := exists e:elt, MapsTo k e m.
+
+ Hint Unfold MapsTo In.
+
+ (* Alternative formulations for [In k l] *)
+
+ Lemma In_alt {elt} k (l:list (key*elt)) :
+   In k l <-> exists e, InA eqk (k,e) l.
+ Proof.
+  unfold In, MapsTo.
+  split; intros (e,H).
+  - exists e; auto.
+  - apply InA_eqk_eqke in H. destruct H as ((k',e'),(E,H)).
+    compute in E. exists e'. now rewrite E.
+ Qed.
+
+ Lemma In_alt' {elt} (l:list (key*elt)) k e :
+   In k l <-> InA eqk (k,e) l.
+ Proof.
+  rewrite In_alt. firstorder. eapply InA_eqk; eauto. now compute.
+ Qed.
+
+ Lemma In_alt2 {elt} k (l:list (key*elt)) :
+   In k l <-> Exists (fun p => D.eq k (fst p)) l.
+ Proof.
   unfold In, MapsTo.
   setoid_rewrite Exists_exists; setoid_rewrite InA_alt.
   firstorder.
   exists (snd x), x; auto.
-  Qed.
-
-  Lemma In_nil : forall k, In k nil <-> False.
-  Proof.
-  intros; rewrite In_alt2; apply Exists_nil.
-  Qed.
-
-  Lemma In_cons : forall k p l,
-   In k (p::l) <-> eq k (fst p) \/ In k l.
-  Proof.
-  intros; rewrite !In_alt2, Exists_cons; intuition.
-  Qed.
-
-  Global Instance MapsTo_compat :
-   Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
-  Proof.
+ Qed.
+
+ Lemma In_nil {elt} k : In k (@nil (key*elt)) <-> False.
+ Proof.
+  rewrite In_alt2; apply Exists_nil.
+ Qed.
+
+ Lemma In_cons {elt} k p (l:list (key*elt)) :
+   In k (p::l) <-> D.eq k (fst p) \/ In k l.
+ Proof.
+  rewrite !In_alt2, Exists_cons; intuition.
+ Qed.
+
+ Instance MapsTo_compat {elt} :
+   Proper (D.eq==>Logic.eq==>equivlistA eqke==>iff) (@MapsTo elt).
+ Proof.
   intros x x' Hx e e' He l l' Hl. unfold MapsTo.
   rewrite Hx, He, Hl; intuition.
-  Qed.
+ Qed.
 
-  Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
-  Proof.
+ Instance In_compat {elt} : Proper (D.eq==>equivlistA eqk==>iff) (@In elt).
+ Proof.
   intros x x' Hx l l' Hl. rewrite !In_alt.
   setoid_rewrite Hl. setoid_rewrite Hx. intuition.
-  Qed.
-
-  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
-  Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed.
+ Qed.
 
-  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
-  Proof. intros l x y EQ. rewrite <- EQ; auto. Qed.
+ Lemma MapsTo_eq {elt} (l:list (key*elt)) x y e :
+   D.eq x y -> MapsTo x e l -> MapsTo y e l.
+ Proof. now intros <-. Qed.
 
-  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
-  Proof.
-    intros; invlist In; invlist MapsTo. compute in * |- ; intuition.
-    right; exists x; auto.
-  Qed.
+ Lemma In_eq {elt} (l:list (key*elt)) x y :
+   D.eq x y -> In x l -> In y l.
+ Proof. now intros <-. Qed.
 
-  Lemma In_inv_2 : forall k k' e e' l,
-      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
-  Proof.
-   intros; invlist InA; intuition.
-  Qed.
+ Lemma In_inv {elt} k k' e (l:list (key*elt)) :
+   In k ((k',e) :: l) -> D.eq k k' \/ In k l.
+ Proof.
+  intros (e',H). red in H. rewrite InA_cons, eqke_def in H.
+  intuition. right. now exists e'.
+ Qed.
 
-  Lemma In_inv_3 : forall x x' l,
-      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
-  Proof.
-   intros; invlist InA; compute in * |- ; intuition.
-  Qed.
+ Lemma In_inv_2 {elt} k k' e e' (l:list (key*elt)) :
+   InA eqk (k, e) ((k', e') :: l) -> ~ D.eq k k' -> InA eqk (k, e) l.
+ Proof.
+  rewrite InA_cons, eqk_def. intuition.
+ Qed.
 
- End Elt.
+ Lemma In_inv_3 {elt} x x' (l:list (key*elt)) :
+   InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
+ Proof.
+  rewrite InA_cons. destruct 1 as [H|H]; trivial. destruct 1.
+  eauto with *.
+ Qed.
 
- Hint Unfold eqk eqke.
  Hint Extern 2 (eqke ?a ?b) => split.
  Hint Resolve InA_eqke_eqk.
- Hint Unfold MapsTo In.
  Hint Resolve In_inv_2 In_inv_3.
 
 End KeyDecidableType.
 
 
-(** * PairDecidableType 
-   
+(** * PairDecidableType
+
    From two decidable types, we can build a new DecidableType
    over their cartesian product. *)
 
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index 059992f5b..4d49ac84e 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -6,51 +6,47 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Export RelationPairs SetoidList Orders.
+Require Export RelationPairs SetoidList Orders EqualitiesFacts.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
 (** * Specialization of results about lists modulo. *)
 
-Module OrderedTypeLists (Import O:OrderedType).
+Module OrderedTypeLists (O:OrderedType).
 
-Section ForNotations.
-
-Notation In:=(InA eq).
-Notation Inf:=(lelistA lt).
-Notation Sort:=(sort lt).
-Notation NoDup:=(NoDupA eq).
+Local Notation In:=(InA O.eq).
+Local Notation Inf:=(lelistA O.lt).
+Local Notation Sort:=(sort O.lt).
+Local Notation NoDup:=(NoDupA O.eq).
 
 Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
 Proof. intros. rewrite <- H; auto. Qed.
 
 Lemma ListIn_In : forall l x, List.In x l -> In x l.
-Proof. exact (In_InA eq_equiv). Qed.
+Proof. exact (In_InA O.eq_equiv). Qed.
 
-Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_ltA lt_strorder). Qed.
+Lemma Inf_lt : forall l x y, O.lt x y -> Inf y l -> Inf x l.
+Proof. exact (InfA_ltA O.lt_strorder). Qed.
 
-Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_eqA eq_equiv lt_compat). Qed.
+Lemma Inf_eq : forall l x y, O.eq x y -> Inf y l -> Inf x l.
+Proof. exact (InfA_eqA O.eq_equiv O.lt_compat). Qed.
 
-Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
-Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
+Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> O.lt a x.
+Proof. exact (SortA_InfA_InA O.eq_equiv O.lt_strorder O.lt_compat). Qed.
 
-Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l.
-Proof. exact (@In_InfA t lt). Qed.
+Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> O.lt x y) -> Inf x l.
+Proof. exact (@In_InfA O.t O.lt). Qed.
 
-Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l.
-Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed.
+Lemma In_Inf : forall l x, (forall y, In y l -> O.lt x y) -> Inf x l.
+Proof. exact (InA_InfA O.eq_equiv (ltA:=O.lt)). Qed.
 
 Lemma Inf_alt :
- forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)).
-Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed.
+ forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> O.lt x y)).
+Proof. exact (InfA_alt O.eq_equiv O.lt_strorder O.lt_compat). Qed.
 
 Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
-Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat) . Qed.
-
-End ForNotations.
+Proof. exact (SortA_NoDupA O.eq_equiv O.lt_strorder O.lt_compat) . Qed.
 
 Hint Resolve ListIn_In Sort_NoDup Inf_lt.
 Hint Immediate In_eq Inf_lt.
@@ -58,140 +54,66 @@ Hint Immediate In_eq Inf_lt.
 End OrderedTypeLists.
 
 
+(** * Results about keys and data as manipulated in MMaps. *)
 
+Module KeyOrderedType(O:OrderedType).
+ Include KeyDecidableType(O). (* provides eqk, eqke *)
 
+ Local Notation key:=O.t.
+ Local Open Scope signature_scope.
 
-(** * Results about keys and data as manipulated in FMaps. *)
-
-
-Module KeyOrderedType(Import O:OrderedType).
- Module Import MO:=OrderedTypeLists(O).
-
- Section Elt.
- Variable elt : Type.
- Notation key:=t.
-
-  Local Open Scope signature_scope.
-
-  Definition eqk : relation (key*elt) := eq @@1.
-  Definition eqke : relation (key*elt) := eq * Logic.eq.
-  Definition ltk : relation (key*elt) := lt @@1.
-
-  Hint Unfold eqk eqke ltk.
+ Definition ltk {elt} : relation (key*elt) := O.lt @@1.
 
-  (* eqke is stricter than eqk *)
+ Hint Unfold ltk.
 
-  Global Instance eqke_eqk : subrelation eqke eqk.
-  Proof. firstorder. Qed.
+ (* ltk is a strict order *)
 
-  (* eqk, eqke are equalities, ltk is a strict order *)
+ Instance ltk_strorder {elt} : StrictOrder (@ltk elt) := _.
 
-  Global Instance eqk_equiv : Equivalence eqk := _.
+ Instance ltk_compat {elt} : Proper (eqk==>eqk==>iff) (@ltk elt).
+ Proof. unfold eqk, ltk; auto with *. Qed.
 
-  Global Instance eqke_equiv : Equivalence eqke := _.
+ Instance ltk_compat' {elt} : Proper (eqke==>eqke==>iff) (@ltk elt).
+ Proof. eapply subrelation_proper; eauto with *. Qed.
 
-  Global Instance ltk_strorder : StrictOrder ltk := _.
+ (* Additionnal facts *)
 
-  Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
-  Proof. unfold eqk, ltk; auto with *. Qed.
+ Instance pair_compat {elt} : Proper (O.eq==>Logic.eq==>eqke) (@pair key elt).
+ Proof. apply pair_compat. Qed.
 
-  (* Additionnal facts *)
-
-  Global Instance pair_compat : Proper (eq==>Logic.eq==>eqke) (@pair key elt).
-  Proof. apply pair_compat. Qed.
+ Section Elt.
+  Variable elt : Type.
+  Implicit Type p q : key*elt.
+  Implicit Type l m : list (key*elt).
 
-  Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'.
+  Lemma ltk_not_eqk p q : ltk p q -> ~ eqk p q.
   Proof.
-  intros e e' LT EQ; rewrite EQ in LT.
+  intros LT EQ; rewrite EQ in LT.
   elim (StrictOrder_Irreflexive _ LT).
   Qed.
 
-  Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'.
+  Lemma ltk_not_eqke p q : ltk p q -> ~eqke p q.
   Proof.
-  intros e e' LT EQ; rewrite EQ in LT.
+  intros LT EQ; rewrite EQ in LT.
   elim (StrictOrder_Irreflexive _ LT).
   Qed.
 
-  Lemma InA_eqke_eqk :
-     forall x m, InA eqke x m -> InA eqk x m.
-  Proof.
-    unfold eqke, RelProd; induction 1; firstorder.
-  Qed.
-  Hint Resolve InA_eqke_eqk.
-
-  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
-  Definition In k m := exists e:elt, MapsTo k e m.
   Notation Sort := (sort ltk).
   Notation Inf := (lelistA ltk).
 
-  Hint Unfold MapsTo In.
-
-  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
-
-  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
-  Proof.
-  firstorder.
-  exists x; auto.
-  induction H.
-  destruct y; compute in H.
-  exists e; left; auto.
-  destruct IHInA as [e H0].
-  exists e; auto.
-  Qed.
+  Lemma Inf_eq l x x' : eqk x x' -> Inf x' l -> Inf x l.
+  Proof. now intros <-. Qed.
 
-  Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
-  Proof.
-  unfold In, MapsTo.
-  setoid_rewrite Exists_exists; setoid_rewrite InA_alt.
-  firstorder.
-  exists (snd x), x; auto.
-  Qed.
-
-  Lemma In_nil : forall k, In k nil <-> False.
-  Proof.
-  intros; rewrite In_alt2; apply Exists_nil.
-  Qed.
-
-  Lemma In_cons : forall k p l,
-   In k (p::l) <-> eq k (fst p) \/ In k l.
-  Proof.
-  intros; rewrite !In_alt2, Exists_cons; intuition.
-  Qed.
-
-  Global Instance MapsTo_compat :
-   Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
-  Proof.
-  intros x x' Hx e e' He l l' Hl. unfold MapsTo.
-  rewrite Hx, He, Hl; intuition.
-  Qed.
-
-  Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
-  Proof.
-  intros x x' Hx l l' Hl. rewrite !In_alt.
-  setoid_rewrite Hl. setoid_rewrite Hx. intuition.
-  Qed.
-
-  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
-  Proof. intros l x y e EQ. rewrite <- EQ; auto. Qed.
-
-  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
-  Proof. intros l x y EQ. rewrite <- EQ; auto. Qed.
-
-  Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
-  Proof. intros l x x' H. rewrite H; auto. Qed.
-
-  Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
+  Lemma Inf_lt l x x' : ltk x x' -> Inf x' l -> Inf x l.
   Proof. apply InfA_ltA; auto with *. Qed.
 
   Hint Immediate Inf_eq.
   Hint Resolve Inf_lt.
 
-  Lemma Sort_Inf_In :
-      forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
+  Lemma Sort_Inf_In l p q : Sort l -> Inf q l -> InA eqk p l -> ltk q p.
   Proof. apply SortA_InfA_InA; auto with *. Qed.
 
-  Lemma Sort_Inf_NotIn :
-      forall l k e, Sort l -> Inf (k,e) l ->  ~In k l.
+  Lemma Sort_Inf_NotIn l k e : Sort l -> Inf (k,e) l ->  ~In k l.
   Proof.
     intros; red; intros.
     destruct H1 as [e' H2].
@@ -200,57 +122,34 @@ Module KeyOrderedType(Import O:OrderedType).
     repeat red; reflexivity.
   Qed.
 
-  Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l.
+  Lemma Sort_NoDupA l : Sort l -> NoDupA eqk l.
   Proof. apply SortA_NoDupA; auto with *. Qed.
 
-  Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
+  Lemma Sort_In_cons_1 l p q : Sort (p::l) -> InA eqk q l -> ltk p q.
   Proof.
    intros; invlist sort; eapply Sort_Inf_In; eauto.
   Qed.
 
-  Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) ->
-      ltk e e' \/ eqk e e'.
+  Lemma Sort_In_cons_2 l p q : Sort (p::l) -> InA eqk q (p::l) ->
+      ltk p q \/ eqk p q.
   Proof.
     intros; invlist InA; auto with relations.
     left; apply Sort_In_cons_1 with l; auto with relations.
   Qed.
 
-  Lemma Sort_In_cons_3 :
-    forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k.
+  Lemma Sort_In_cons_3 x l k e :
+    Sort ((k,e)::l) -> In x l -> ~O.eq x k.
   Proof.
     intros; invlist sort; red; intros.
     eapply Sort_Inf_NotIn; eauto using In_eq.
   Qed.
 
-  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
-  Proof.
-    intros; invlist In; invlist MapsTo. compute in * |- ; intuition.
-    right; exists x; auto.
-  Qed.
-
-  Lemma In_inv_2 : forall k k' e e' l,
-      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
-  Proof.
-   intros; invlist InA; intuition.
-  Qed.
-
-  Lemma In_inv_3 : forall x x' l,
-      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
-  Proof.
-   intros; invlist InA; compute in * |- ; intuition.
-  Qed.
-
  End Elt.
 
- Hint Unfold eqk eqke ltk.
- Hint Extern 2 (eqke ?a ?b) => split.
  Hint Resolve ltk_not_eqk ltk_not_eqke.
- Hint Resolve InA_eqke_eqk.
- Hint Unfold MapsTo In.
  Hint Immediate Inf_eq.
  Hint Resolve Inf_lt.
  Hint Resolve Sort_Inf_NotIn.
- Hint Resolve In_inv_2 In_inv_3.
 
 End KeyOrderedType.
 
diff --git a/theories/theories.itarget b/theories/theories.itarget
index 3a87d8cf1..4519070e4 100644
--- a/theories/theories.itarget
+++ b/theories/theories.itarget
@@ -3,6 +3,7 @@ Bool/vo.otarget
 Classes/vo.otarget
 FSets/vo.otarget
 MSets/vo.otarget
+MMaps/vo.otarget
 Structures/vo.otarget
 Init/vo.otarget
 Lists/vo.otarget