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".

2 files changed, 78 insertions, 7 deletions

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.