etoffage des notions de permutations (a la fois List.Permutation et Permutation.permutation)

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

4 files changed, 695 insertions, 19 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 71f8346d3..105340635 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -147,6 +147,14 @@ Section Facts.
     unfold not in |- *; intros a H; inversion_clear H.
   Qed.
 
+  Lemma In_split : forall x (l:list A), In x l -> exists l1, exists l2, l = l1++x::l2.
+  Proof.
+  induction l; simpl; destruct 1.
+  subst a; auto.
+  exists (@nil A); exists l; auto.
+  destruct (IHl H) as (l1,(l2,H0)).
+  exists (a::l1); exists l2; simpl; f_equal; auto.
+  Qed.
 
   (** Inversion *)
   Theorem in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l.
@@ -154,7 +162,6 @@ Section Facts.
     intros a b l H; inversion_clear H; auto.
   Qed.
 
-
   (** Decidability of [In] *)
   Theorem In_dec :
     (forall x y:A, {x = y} + {x <> y}) ->
@@ -753,6 +760,22 @@ Section ListOps.
       apply Permutation_trans with (l' := y :: x :: l' ++ l); constructor.
       apply Permutation_trans with (l' := x :: l ++ l'); auto.
     Qed.
+  
+    Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
+      Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
+    Proof.
+    intros l l1; revert l.
+    induction l1.
+    simpl.
+    intros; apply perm_skip; auto.
+    simpl; intros.
+    apply perm_trans with (a0::a::l1++l2).
+    apply perm_skip; auto.
+    apply perm_trans with (a::a0::l1++l2).
+    apply perm_swap; auto.
+    apply perm_skip; auto.
+    Qed.
+    Hint Resolve Permutation_cons_app.
 
     Theorem Permutation_length : forall (l l' : list A), Permutation l l' -> length l = length l'.
     Proof.
@@ -768,6 +791,108 @@ Section ListOps.
       apply Permutation_app_swap.
     Qed.
 
+    Theorem Permutation_ind_bis : 
+     forall P : list A -> list A -> Prop,
+       P (@nil A) (@nil A) ->
+       (forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
+       (forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) ->
+       (forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
+       forall l l', Permutation l l' -> P l l'.
+    Proof.
+    intros P Hnil Hskip Hswap Htrans.
+    induction 1; auto.
+    apply Htrans with (x::y::l); auto.
+    apply Hswap; auto.
+    induction l; auto.
+    apply Hskip; auto.
+    apply Hskip; auto.
+    induction l; auto.
+    eauto.
+    Qed.
+
+    Ltac break_list l x l' H := 
+     destruct l as [|x l']; simpl in *; 
+     injection H; intros; subst; clear H.
+
+    Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a,
+      Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).
+    Proof.
+    set (P:=fun l l' =>  
+             forall a l1 l2 l3 l4, l=l1++a::l2 -> l'=l3++a::l4 -> Permutation (l1++l2) (l3++l4)).
+    cut (forall l l', Permutation l l' -> P l l').
+    intros; apply (H _ _ H0 a); auto.
+    intros; apply (Permutation_ind_bis P); unfold P; clear P; try clear H l l'; simpl; auto.
+    (* nil *)
+    intros; destruct l1; simpl in *; discriminate.
+    (* skip *)
+    intros x l l' H IH; intros.
+    break_list l1 b l1' H0; break_list l3 c l3' H1.
+    auto.
+    apply perm_trans with (l3'++c::l4); auto.
+    apply perm_trans with (l1'++a::l2); auto.
+    apply perm_skip.
+    apply (IH a l1' l2 l3' l4); auto.
+    (* swap *)
+    intros x y l l' Hp IH; intros.
+    break_list l1 b l1' H; break_list l3 c l3' H0.
+    auto.
+    break_list l3' b l3'' H.
+    auto.
+    apply perm_trans with (c::l3''++b::l4); auto.
+    break_list l1' c l1'' H1. 
+    auto.
+    apply perm_trans with (b::l1''++c::l2); auto.
+    break_list l3' d l3'' H; break_list l1' e l1'' H1. 
+    auto.
+    apply perm_trans with (e::a::l1''++l2); auto.
+    apply perm_trans with (e::l1''++a::l2); auto.
+    apply perm_trans with (d::a::l3''++l4); auto.
+    apply perm_trans with (d::l3''++a::l4); auto.
+    apply perm_trans with (e::d::l1''++l2); auto.
+    apply perm_skip; apply perm_skip.
+    apply (IH a l1'' l2 l3'' l4); auto.
+    (*trans*)
+    intros.
+    destruct (In_split a l') as (l'1,(l'2,H6)).
+    apply (Permutation_in a H).
+    subst l.
+    apply in_or_app; right; red; auto.
+    apply perm_trans with (l'1++l'2).
+    apply (H0 _ _ _ _ _ H3 H6).
+    apply (H2 _ _ _ _ _ H6 H4).
+    Qed.
+
+    Theorem Permutation_cons_inv : 
+       forall l l' a, Permutation (a::l) (a::l') -> Permutation l l'.
+    Proof.
+    intros; exact (Permutation_app_inv (@nil _) l (@nil _) l' a H). 
+    Qed.
+
+    Theorem Permutation_cons_app_inv :
+       forall l l1 l2 a, Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2).
+    Proof.
+    intros; exact (Permutation_app_inv (@nil _) l l1 l2 a H). 
+    Qed.
+    
+    Theorem Permutation_app_inv_l : 
+        forall l l1 l2, Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2.
+    Proof.    
+    induction l; simpl; auto.
+    intros.
+    apply IHl.
+    apply Permutation_cons_inv with a; auto.
+    Qed.
+
+    Theorem Permutation_app_inv_r : 
+       forall l l1 l2, Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2.
+    Proof.
+    induction l.
+    intros l1 l2; do 2 rewrite <- app_nil_end; auto.
+    intros.
+    apply IHl.
+    apply Permutation_app_inv with a; auto.
+    Qed.
+
   End Permutation.
 
 
@@ -848,6 +973,13 @@ Section Map.
     rewrite IHl; auto.
   Qed.
 
+  Hint Constructors Permutation.
+
+  Lemma Permutation_map : 
+    forall l l', Permutation l l' -> Permutation (map l) (map l').
+  Proof. 
+  induction 1; simpl; auto; eauto.
+  Qed.
 
   (** [flat_map] *)
 
@@ -892,7 +1024,6 @@ Proof.
 Qed.
 
 
-
 (************************************)
 (** Left-to-right iterator on lists *)
 (************************************)
@@ -1467,8 +1598,58 @@ Section ReDun.
     | NoDup_nil : NoDup nil 
     | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l). 
 
-End ReDun.
+  Lemma NoDup_remove_1 : forall l l' a, NoDup (l++a::l') -> NoDup (l++l').
+  Proof.
+  induction l; simpl.
+  inversion_clear 1; auto.
+  inversion_clear 1.
+  constructor.
+  swap H0.
+  apply in_or_app; destruct (in_app_or _ _ _ H); simpl; tauto.
+  apply IHl with a0; auto.
+  Qed.
 
+  Lemma NoDup_remove_2 : forall l l' a, NoDup (l++a::l') -> ~In a (l++l').
+  Proof.
+  induction l; simpl.
+  inversion_clear 1; auto.
+  inversion_clear 1.
+  swap H0.
+  destruct H.
+  subst a0.
+  apply in_or_app; right; red; auto.
+  destruct (IHl _ _ H1); auto.
+  Qed.
+
+  Lemma NoDup_Permutation : forall l l', 
+    NoDup l -> NoDup l' -> (forall x, In x l <-> In x l') -> Permutation l l'.
+  Proof.
+  induction l. 
+  destruct l'; simpl; intros.
+  apply perm_nil.
+  destruct (H1 a) as (_,H2); destruct H2; auto.
+  intros.
+  destruct (In_split a l') as (l'1,(l'2,H2)).
+  destruct (H1 a) as (H2,H3); simpl in *; auto.
+  subst l'.
+  apply Permutation_cons_app.
+  inversion_clear H.
+  apply IHl; auto.
+  apply NoDup_remove_1 with a; auto.
+  intro x; split; intros.
+  assert (In x (l'1++a::l'2)).
+   destruct (H1 x); simpl in *; auto.
+  apply in_or_app; destruct (in_app_or _ _ _ H4); auto.
+  destruct H5; auto.
+  subst x; destruct H2; auto.
+  assert (In x (l'1++a::l'2)).
+    apply in_or_app; destruct (in_app_or _ _ _ H); simpl; auto.
+  destruct (H1 x) as (_,H5); destruct H5; auto. 
+  subst x.
+  destruct (NoDup_remove_2 _ _ _ H0 H).
+  Qed.
+
+End ReDun.
 
 
 (***********************************)
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
new file mode 100644
index 000000000..1e4673b64
--- /dev/null
+++ b/theories/Sorting/PermutEq.v
@@ -0,0 +1,241 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Import Omega.
+Require Import Relations.
+Require Import Setoid.
+Require Import List.
+Require Import Multiset.
+Require Import Permutation. 
+
+Set Implicit Arguments.
+
+(** This file is similar to [PermutSetoid], except that the equality used here
+      is Coq usual one instead of a setoid equality. In particular, we can then 
+      prove the equivalence between [List.Permutation] and 
+      [Permutation.permutation].
+*)
+
+Section Perm.
+
+Variable A : Set.
+Hypothesis eq_dec : forall x y:A, {x=y} + {~ x=y}.
+
+Notation permutation := (permutation _ eq_dec).
+Notation list_contents := (list_contents _ eq_dec).
+
+(** we can use [multiplicity] to define [In] and [NoDup]. *)
+
+Lemma multiplicity_In : 
+  forall l a, In a l <-> 0 < multiplicity (list_contents l) a.
+Proof.
+induction l.
+simpl.
+split; inversion 1.
+simpl.
+split; intros.
+inversion_clear H.
+subst a0.
+destruct (eq_dec a a) as [_|H]; auto with arith; destruct H; auto.
+destruct (eq_dec a a0) as [H1|H1]; auto with arith; simpl.
+rewrite <- IHl; auto.
+destruct (eq_dec a a0); auto.
+simpl in H.
+right; rewrite IHl; auto.
+Qed.
+
+Lemma multiplicity_In_O :
+  forall l a, ~ In a l -> multiplicity (list_contents l) a = 0.
+Proof.
+intros l a; rewrite multiplicity_In; 
+ destruct (multiplicity (list_contents l) a); auto.
+destruct 1; auto with arith.
+Qed.
+
+Lemma multiplicity_In_S :
+ forall l a, In a l -> multiplicity (list_contents l) a >= 1.
+Proof.
+intros l a; rewrite multiplicity_In; auto.
+Qed.
+
+Lemma multiplicity_NoDup : 
+  forall l, NoDup l <-> (forall a, multiplicity (list_contents l) a <= 1).
+Proof.
+induction l.
+simpl.
+split; auto with arith.
+intros; apply NoDup_nil.
+split; simpl.
+inversion_clear 1.
+rewrite IHl in H1.
+intros; destruct (eq_dec a a0) as [H2|H2]; simpl; auto.
+subst a0.
+rewrite multiplicity_In_O; auto.
+intros; constructor.
+rewrite multiplicity_In.
+generalize (H a).
+destruct (eq_dec a a) as [H0|H0].
+destruct (multiplicity (list_contents l) a); auto with arith.
+simpl; inversion 1. 
+inversion H3.
+destruct H0; auto.
+rewrite IHl; intros.
+generalize (H a0); auto with arith.
+destruct (eq_dec a a0); simpl; auto with arith.
+Qed.
+
+Lemma NoDup_permut : 
+  forall l l', NoDup l -> NoDup l' -> 
+     (forall x, In x l <-> In x l') -> permutation l l'.
+Proof.
+intros.
+red; unfold meq; intros.
+rewrite multiplicity_NoDup in H, H0. 
+generalize (H a) (H0 a) (H1 a); clear H H0 H1.
+do 2 rewrite multiplicity_In.
+destruct 3; omega.
+Qed.
+
+(** Permutation is compatible with In. *)
+Lemma permut_In_In :
+  forall l1 l2 e, permutation l1 l2 -> In e l1 -> In e l2.
+Proof.
+unfold Permutation.permutation, meq; intros l1 l2 e P IN.
+generalize (P e); clear P.
+destruct (In_dec eq_dec e l2) as [H|H]; auto.
+rewrite (multiplicity_In_O _ _ H).
+intros.
+generalize (multiplicity_In_S _ _ IN).
+rewrite H0.
+inversion 1.
+Qed.
+
+Lemma permut_cons_In :
+  forall l1 l2 e, permutation (e :: l1) l2 -> In e l2.
+Proof.
+intros; eapply permut_In_In; eauto.
+red; auto.
+Qed.
+
+(** Permutation of an empty list. *)
+Lemma permut_nil :
+ forall l, permutation l nil -> l = nil.
+Proof.
+intro l; destruct l as [ | e l ]; trivial.
+assert (In e (e::l)) by red; auto.
+intro Abs; generalize (permut_In_In _ Abs H).
+inversion 1.
+Qed.
+
+(** When used with [eq], this permutation notion is equivalent to 
+  the one defined in [List.v]. *)
+
+Lemma permutation_Permutation : 
+ forall l l', Permutation l l' <-> permutation l l'.
+Proof.
+split.
+induction 1.
+apply permut_refl.
+apply permut_cons; auto.
+change (permutation (y::x::l) ((x::nil)++y::l)).
+apply permut_add_cons_inside; simpl; apply permut_refl.
+apply permut_tran with l'; auto.
+revert l'.
+induction l.
+intros.
+rewrite (permut_nil (permut_sym H)).
+apply Permutation_refl.
+intros.
+destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).
+subst l'.
+apply Permutation_cons_app.
+apply IHl.
+apply permut_remove_hd with a; auto.
+Qed.
+
+(** Permutation for short lists. *)
+
+Lemma permut_length_1:
+ forall a b, permutation (a :: nil) (b :: nil)  -> a=b.
+Proof.
+intros a b; unfold Permutation.permutation, meq; intro P;
+generalize (P b); clear P; simpl.
+destruct (eq_dec b b) as [H|H]; [ | destruct H; auto].
+destruct (eq_dec a b); simpl; auto; intros; discriminate.
+Qed.
+
+Lemma permut_length_2 :
+ forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
+ (a1=a2) /\ (b1=b2) \/ (a1=b2) /\ (a2=b1).
+Proof.
+intros a1 b1 a2 b2 P.
+assert (H:=permut_cons_In P).
+inversion_clear H.
+left; split; auto.
+apply permut_length_1.
+red; red; intros.
+generalize (P a); clear P; simpl.
+destruct (eq_dec a1 a) as [H2|H2]; 
+ destruct (eq_dec a2 a) as [H3|H3]; auto.
+destruct H3; transitivity a1; auto.
+destruct H2; transitivity a2; auto.
+right.
+inversion_clear H0; [|inversion H].
+split; auto.
+apply permut_length_1.
+red; red; intros.
+generalize (P a); clear P; simpl.
+destruct (eq_dec a1 a) as [H2|H2]; 
+ destruct (eq_dec b2 a) as [H3|H3]; auto.
+simpl; rewrite <- plus_n_Sm; inversion 1; auto.
+destruct H3; transitivity a1; auto.
+destruct H2; transitivity b2; auto.
+Qed.
+
+(** Permutation is compatible with length. *)
+Lemma permut_length :
+ forall l1 l2, permutation l1 l2 -> length l1 = length l2.
+Proof.
+induction l1; intros l2 H.
+rewrite (permut_nil (permut_sym H)); auto.
+destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).
+subst l2.
+rewrite app_length.
+simpl; rewrite <- plus_n_Sm; f_equal.
+rewrite <- app_length.
+apply IHl1.
+apply permut_remove_hd with a; auto.
+Qed.
+
+Variable B : Set.
+Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }. 
+
+(** Permutation is compatible with map. *)
+
+Lemma permutation_map :
+  forall f l1 l2, permutation l1 l2 -> 
+   Permutation.permutation _ eqB_dec (map f l1) (map f l2).
+Proof.
+intros f; induction l1.
+intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl.
+intros l2 P.
+simpl.
+destruct (In_split _ _ (permut_cons_In P)) as (h2,(t2,H1)).
+subst l2.
+rewrite map_app.
+simpl.
+apply permut_add_cons_inside.
+rewrite <- map_app.
+apply IHl1; auto.
+apply permut_remove_hd with a; auto.
+Qed.
+
+End Perm.
+
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
new file mode 100644
index 000000000..e669c5fec
--- /dev/null
+++ b/theories/Sorting/PermutSetoid.v
@@ -0,0 +1,243 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Import Omega.
+Require Import Relations.
+Require Import List.
+Require Import Multiset.
+Require Import Permutation. 
+Require Import SetoidList.
+
+Set Implicit Arguments.
+
+(** This file contains additional results about permutations 
+     with respect to an setoid equality (i.e. an equivalence relation). 
+*)
+
+Section Perm.
+
+Variable A : Set.
+Variable eqA : relation A.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+
+Notation permutation := (permutation _ eqA_dec).
+Notation list_contents := (list_contents _ eqA_dec).
+
+(** The following lemmas need some knowledge on [eqA] *)
+
+Variable eqA_refl : forall x, eqA x x.
+Variable eqA_sym : forall x y, eqA x y -> eqA y x.
+Variable eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
+
+(** we can use [multiplicity] to define [InA] and [NoDupA]. *)
+
+Lemma multiplicity_InA : 
+  forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.
+Proof.
+induction l.
+simpl.
+split; inversion 1.
+simpl.
+split; intros.
+inversion_clear H.
+destruct (eqA_dec a a0) as [_|H1]; auto with arith.
+destruct H1; auto.
+destruct (eqA_dec a a0); auto with arith.
+simpl; rewrite <- IHl; auto.
+destruct (eqA_dec a a0) as [H0|H0]; auto.
+simpl in H.
+constructor 2; rewrite IHl; auto.
+Qed.
+
+Lemma multiplicity_InA_O :
+  forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.
+Proof.
+intros l a; rewrite multiplicity_InA; 
+destruct (multiplicity (list_contents l) a); auto with arith.
+destruct 1; auto with arith.
+Qed.
+
+Lemma multiplicity_InA_S :
+ forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.
+Proof.
+intros l a; rewrite multiplicity_InA; auto with arith.
+Qed.
+
+Lemma multiplicity_NoDupA : forall l, 
+  NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).
+Proof.
+induction l.
+simpl.
+split; auto with arith.
+split; simpl.
+inversion_clear 1.
+rewrite IHl in H1.
+intros; destruct (eqA_dec a a0) as [H2|H2]; simpl; auto.
+rewrite multiplicity_InA_O; auto.
+swap H0.
+apply InA_eqA with a0; auto.
+intros; constructor.
+rewrite multiplicity_InA.
+generalize (H a).
+destruct (eqA_dec a a) as [H0|H0].
+destruct (multiplicity (list_contents l) a); auto with arith.
+simpl; inversion 1. 
+inversion H3.
+destruct H0; auto.
+rewrite IHl; intros.
+generalize (H a0); auto with arith.
+destruct (eqA_dec a a0); simpl; auto with arith.
+Qed.
+
+
+(** Permutation is compatible with InA. *)
+Lemma permut_InA_InA :
+  forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.
+Proof.
+intros l1 l2 e.
+do 2 rewrite multiplicity_InA.
+unfold Permutation.permutation, meq.
+intros H;rewrite H; auto.
+Qed.
+
+Lemma permut_cons_InA :
+  forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.
+Proof.
+intros; apply (permut_InA_InA (e:=e) H); auto.
+Qed.
+
+(** Permutation of an empty list. *)
+Lemma permut_nil :
+ forall l, permutation l nil -> l = nil.
+Proof.
+intro l; destruct l as [ | e l ]; trivial.
+assert (InA eqA e (e::l)) by auto.
+intro Abs; generalize (permut_InA_InA Abs H).
+inversion 1.
+Qed.
+
+(** Permutation for short lists. *)
+
+Lemma permut_length_1:
+ forall a b, permutation (a :: nil) (b :: nil)  -> eqA a b.
+Proof.
+intros a b; unfold Permutation.permutation, meq; intro P;
+generalize (P b); clear P; simpl.
+destruct (eqA_dec b b) as [H|H]; [ | destruct H; auto].
+destruct (eqA_dec a b); simpl; auto; intros; discriminate.
+Qed.
+
+Lemma permut_length_2 :
+ forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
+ (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).
+Proof.
+intros a1 b1 a2 b2 P.
+assert (H:=permut_cons_InA P).
+inversion_clear H.
+left; split; auto.
+apply permut_length_1.
+red; red; intros.
+generalize (P a); clear P; simpl.
+destruct (eqA_dec a1 a) as [H2|H2]; 
+ destruct (eqA_dec a2 a) as [H3|H3]; auto.
+destruct H3; apply eqA_trans with a1; auto.
+destruct H2; apply eqA_trans with a2; auto.
+right.
+inversion_clear H0; [|inversion H].
+split; auto.
+apply permut_length_1.
+red; red; intros.
+generalize (P a); clear P; simpl.
+destruct (eqA_dec a1 a) as [H2|H2]; 
+ destruct (eqA_dec b2 a) as [H3|H3]; auto.
+simpl; rewrite <- plus_n_Sm; inversion 1; auto.
+destruct H3; apply eqA_trans with a1; auto.
+destruct H2; apply eqA_trans with b2; auto.
+Qed.
+
+(** Permutation is compatible with length. *)
+Lemma permut_length :
+ forall l1 l2, permutation l1 l2 -> length l1 = length l2.
+Proof.
+induction l1; intros l2 H.
+rewrite (permut_nil (permut_sym H)); auto.
+assert (H0:=permut_cons_InA H).
+destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
+subst l2.
+rewrite app_length.
+simpl; rewrite <- plus_n_Sm; f_equal.
+rewrite <- app_length.
+apply IHl1.
+apply permut_remove_hd with b.
+apply permut_tran with (a::l1); auto.
+revert H1; unfold Permutation.permutation, meq; simpl.
+intros; f_equal; auto.
+destruct (eqA_dec b a0) as [H2|H2]; 
+ destruct (eqA_dec a a0) as [H3|H3]; auto.
+destruct H3; apply eqA_trans with b; auto.
+destruct H2; apply eqA_trans with a; auto.
+Qed.
+
+Lemma NoDupA_eqlistA_permut : 
+  forall l l', NoDupA eqA l -> NoDupA eqA l' -> 
+     eqlistA eqA l l' -> permutation l l'.
+Proof.
+intros.
+red; unfold meq; intros.
+rewrite multiplicity_NoDupA in H, H0. 
+generalize (H a) (H0 a) (H1 a); clear H H0 H1.
+do 2 rewrite multiplicity_InA.
+destruct 3; omega.
+Qed.
+
+
+Variable B : Set.
+Variable eqB : B->B->Prop.
+Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }. 
+Variable eqB_trans : forall x y z, eqB x y -> eqB y z -> eqB x z.
+
+(** Permutation is compatible with map. *)
+
+Lemma permut_map :
+  forall f, 
+  (forall x y, eqA x y -> eqB (f x) (f y)) ->
+  forall l1 l2, permutation l1 l2 -> 
+   Permutation.permutation _ eqB_dec (map f l1) (map f l2).
+Proof.
+intros f; induction l1.
+intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl.
+intros l2 P.
+simpl.
+assert (H0:=permut_cons_InA P).
+destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
+subst l2.
+rewrite map_app.
+simpl.
+apply permut_tran with (f b :: map f l1).
+revert H1; unfold Permutation.permutation, meq; simpl.
+intros; f_equal; auto.
+destruct (eqB_dec (f b) a0) as [H2|H2]; 
+ destruct (eqB_dec (f a) a0) as [H3|H3]; auto.
+destruct H3; apply eqB_trans with (f b); auto.
+destruct H2; apply eqB_trans with (f a); auto.
+apply permut_add_cons_inside.
+rewrite <- map_app.
+apply IHl1; auto.
+apply permut_remove_hd with b.
+apply permut_tran with (a::l1); auto.
+revert H1; unfold Permutation.permutation, meq; simpl.
+intros; f_equal; auto.
+destruct (eqA_dec b a0) as [H2|H2]; 
+ destruct (eqA_dec a a0) as [H3|H3]; auto.
+destruct H3; apply eqA_trans with b; auto.
+destruct H2; apply eqA_trans with a; auto.
+Qed.
+
+End Perm.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index f1b53f067..182c10e6e 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -13,6 +13,24 @@ Require Import List.
 Require Import Multiset.
 Require Import Arith.
 
+(** This file define a notion of permutation for lists, based on multisets: 
+     there exists a permutation between two lists iff every elements have 
+     the same multiplicities in the two lists. 
+
+     Unlike [List.Permutation], the present notion of permutation requires
+     a decidable equality. At the same time, this definition can be used 
+     with a non-standard equality, whereas [List.Permutation] cannot.
+      
+     The present file contains basic results, obtained without any particular
+     assumption on the decidable equality used.
+	
+     File [PermutSetoid] contains additional results about permutations 
+     with respect to an setoid equality (i.e. an equivalence relation). 
+
+     Finally, file [PermutEq] concerns Coq equality : this file is similar 
+     to the previous one, but proves in addition that [List.Permutation]
+     and [permutation] are equivalent in this context.
+*)
 
 Set Implicit Arguments.
 
@@ -80,29 +98,15 @@ Lemma permut_app :
    permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
 Proof.
 unfold permutation in |- *; intros.
-apply meq_trans with (munion (list_contents l) (list_contents m));
+apply meq_trans with (munion (list_contents l) (list_contents m)); 
  auto with datatypes.
-apply meq_trans with (munion (list_contents l') (list_contents m'));
+apply meq_trans with (munion (list_contents l') (list_contents m')); 
  auto with datatypes.
 apply meq_trans with (munion (list_contents l') (list_contents m));
  auto with datatypes.
 Qed.
 Hint Resolve permut_app.
 
-Lemma permut_middle :
- forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
-Proof.
-unfold permutation in |- *.
-simple induction l; simpl in |- *; auto with datatypes.
-intros.
-apply meq_trans with
- (munion (singletonBag a)
-    (munion (singletonBag a0) (list_contents (l0 ++ m))));
- auto with datatypes.
-apply munion_perm_left; auto with datatypes.
-Qed.
-Hint Resolve permut_middle.
-
 Lemma permut_add_inside :
  forall a l1 l2 l3 l4, 
   permutation (l1 ++ l2) (l3 ++ l4) ->
@@ -126,6 +130,13 @@ replace (a :: l) with (nil ++ a :: l); trivial;
 apply permut_add_inside; trivial.
 Qed.
 
+Lemma permut_middle :
+ forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
+Proof.
+intros; apply permut_add_cons_inside; auto.
+Qed.
+Hint Resolve permut_middle.
+
 Lemma permut_sym_app :
  forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
 Proof.