Addition of mergesort + cleaning of the Sorting library

- New (modular) mergesort purely using structural recursion
- Move of the (complex) notion of permutation up to setoid equality
  formerly defined in Permutation.v to file PermutSetoid.v
- Re-use of the file Permutation.v for making the canonical notion
  of permutation that was in List.v more visible
- New file Sorted.v that contains two definitions of sorted:
  "Sorted" is a renaming of "sort" that was defined in file
  Sorting.v and "StronglySorted" is the intuitive notion of sorted
  (there is also LocallySorted which is a variant of Sorted)
- File Sorting.v is replaced by a call to the main Require of the directory
- The merge function whose specification rely on counting elements is moved
  to Heap.v and both are stamped deprecated (the sort defined in
  Heap.v has complexity n^2 in worst case)
- Added some new naming conventions
- Removed uselessly-maximal implicit arguments of Forall2 predicate

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

8 files changed, 1175 insertions, 368 deletions

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 6d5564ed7..4124ef983 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -8,11 +8,15 @@
 
 (*i $Id$ i*)
 
-(** A development of Treesort on Heap trees *)
+(** This file is deprecated, for a tree on list, use [Mergesort.v]. *)
+
+(** A development of Treesort on Heap trees. It has an average
+    complexity of O(n.log n) but of O(n²) in the worst case (e.g. if
+    the list is already sorted) *)
 
 (* G. Huet 1-9-95 uses Multiset *)
 
-Require Import List Multiset Permutation Relations Sorting.
+Require Import List Multiset PermutSetoid Relations Sorting.
 
 Section defs.
 
@@ -122,6 +126,54 @@ Section defs.
     intros; simpl in |- *; apply leA_trans with b; auto with datatypes.
   Qed.
 
+  (** ** Merging two sorted lists *)
+
+  Inductive merge_lem (l1 l2:list A) : Type :=
+    merge_exist :
+    forall l:list A,
+      Sorted leA l ->
+      meq (list_contents _ eqA_dec l)
+      (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
+      (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
+      merge_lem l1 l2.
+
+  Lemma merge :
+    forall l1:list A, Sorted leA l1 ->
+    forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.
+  Proof.
+    simple induction 1; intros.
+    apply merge_exist with l2; auto with datatypes.
+    elim H2; intros.
+    apply merge_exist with (a :: l); simpl in |- *; auto using cons_sort with datatypes.
+    elim (leA_dec a a0); intros.
+
+    (* 1 (leA a a0) *)
+    cut (merge_lem l (a0 :: l0)); auto using cons_sort with datatypes.
+    intros [l3 l3sorted l3contents Hrec].
+    apply merge_exist with (a :: l3); simpl in |- *;
+      auto using cons_sort, cons_leA with datatypes.
+    apply meq_trans with
+      (munion (singletonBag a)
+	(munion (list_contents _ eqA_dec l)
+          (list_contents _ eqA_dec (a0 :: l0)))).
+    apply meq_right; trivial with datatypes.
+    apply meq_sym; apply munion_ass.
+    intros; apply cons_leA.
+    apply (@HdRel_inv _ leA) with l; trivial with datatypes.
+
+    (* 2 (leA a0 a) *)
+    elim X0; simpl in |- *; intros.
+    apply merge_exist with (a0 :: l3); simpl in |- *;
+      auto using cons_sort, cons_leA with datatypes.
+    apply meq_trans with
+      (munion (singletonBag a0)
+	(munion (munion (singletonBag a) (list_contents _ eqA_dec l))
+          (list_contents _ eqA_dec l0))).
+    apply meq_right; trivial with datatypes.
+    apply munion_perm_left.
+    intros; apply cons_leA; apply HdRel_inv with (l:=l0); trivial with datatypes.
+  Qed.
+
 
   (** ** From trees to multisets *)
 
@@ -208,8 +260,8 @@ Section defs.
   Inductive flat_spec (T:Tree) : Type :=
     flat_exist :
     forall l:list A,
-      sort leA l ->
-      (forall a:A, leA_Tree a T -> lelistA leA a l) ->
+      Sorted leA l ->
+      (forall a:A, leA_Tree a T -> HdRel leA a l) ->
       meq (contents T) (list_contents _ eqA_dec l) -> flat_spec T.
 
   Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.
@@ -217,7 +269,7 @@ Section defs.
     intros T h; elim h; intros.
     apply flat_exist with (nil (A:=A)); auto with datatypes.
     elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2.
-    elim (merge _ leA_dec eqA_dec s1 s2); intros.
+    elim (merge _ s1 _ s2); intros.
     apply flat_exist with (a :: l); simpl in |- *; auto with datatypes.
     apply meq_trans with
       (munion (list_contents _ eqA_dec l1)
@@ -234,7 +286,8 @@ Section defs.
   (** * Specification of treesort *)
 
   Theorem treesort :
-    forall l:list A, {m : list A | sort leA m &  permutation _ eqA_dec l m}.
+    forall l:list A,
+    {m : list A | Sorted leA m & permutation _ eqA_dec l m}.
   Proof.
     intro l; unfold permutation in |- *.
     elim (list_to_heap l).
@@ -245,4 +298,4 @@ Section defs.
     apply meq_trans with (contents T); trivial with datatypes.
   Qed.
 
-End defs.
\ No newline at end of file
+End defs.
diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v
new file mode 100644
index 000000000..723bb76d3
--- /dev/null
+++ b/theories/Sorting/Mergesort.v
@@ -0,0 +1,279 @@
+(************************************************************************)
+(*  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*)
+
+(** A modular implementation of mergesort (the complexity is O(n.log n) in
+   the length of the list) *)
+
+(* Initial author: Hugo Herbelin, Oct 2009 *)
+
+Require Import List Setoid Permutation Sorted.
+
+(** Notations and conventions *)
+
+Local Notation "[ ]" := nil.
+Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
+
+Open Scope bool_scope.
+
+Local Coercion eq_true : bool >-> Sortclass.
+
+(** A total relation *)
+
+Module Type TotalOrder.
+  Parameter A : Type.
+  Parameter le_bool : A -> A -> bool.
+  Infix "<=?" := le_bool (at level 35).
+  Axiom le_bool_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
+End TotalOrder.
+
+(** The main module defining [mergesort] on a given total order.
+    We require minimal hypotheses
+ *)
+
+Module Sort (Import X:TotalOrder).
+
+Fixpoint merge l1 l2 :=
+  let fix merge_aux l2 :=
+  match l1, l2 with
+  | [], _ => l2
+  | _, [] => l1
+  | a1::l1', a2::l2' =>
+      if a1 <=? a2 then a1 :: merge l1' l2 else a2 :: merge_aux l2'
+  end
+  in merge_aux l2.
+
+(** We implement mergesort using an explicit stack of pending mergings.
+    Pending merging are represented like a binary number where digits are
+    either None (denoting 0) or Some list to merge (denoting 1). The n-th
+    digit represents the pending list to be merged at level n, if any.
+    Merging a list to a stack is like adding 1 to the binary number
+    represented by the stack but the carry is propagated by merging the
+    lists. In practice, when used in mergesort, the n-th digit, if non 0,
+    carries a list of length 2^n. For instance, adding singleton list
+    [3] to the stack Some [4]::Some [2;6]::None::Some [1;3;5;5]
+    reduces to propagate the carry [3;4] (resulting of the merge of [3]
+    and [4]) to the list Some [2;6]::None::Some [1;3;5;5], which reduces
+    to propagating the carry [2;3;4;6] (resulting of the merge of [3;4] and
+    [2;6]) to the list None::Some [1;3;5;5], which locally produces
+    Some [2;3;4;6]::Some [1;3;5;5], i.e. which produces the final result
+    None::None::Some [2;3;4;6]::Some [1;3;5;5].
+
+    For instance, here is how [6;2;3;1;5] is sorted:
+
+       operation             stack                list
+       iter_merge            []                   [6;2;3;1;5]
+    =  append_list_to_stack  [ + [6]]             [2;3;1;5]
+    -> iter_merge            [[6]]                [2;3;1;5]
+    =  append_list_to_stack  [[6] + [2]]          [3;1;5]
+    =  append_list_to_stack  [ + [2;6];]          [3;1;5]
+    -> iter_merge            [[2;6];]             [3;1;5]
+    =  append_list_to_stack  [[2;6]; + [3]]       [1;5]
+    -> merge_list            [[2;6];[3]]          [1;5]
+    =  append_list_to_stack  [[2;6];[3] + [1]     [5]
+    =  append_list_to_stack  [[2;6] + [1;3];]     [5]
+    =  append_list_to_stack  [ + [1;2;3;6];;]     [5]
+    -> merge_list            [[1;2;3;6];;]        [5]
+    =  append_list_to_stack  [[1;2;3;6];; + [5]]  []
+    -> merge_stack           [[1;2;3;6];;[5]]
+    =                                             [1;2;3;5;6]
+
+    The complexity of the algorithm is n*log n, since there are
+    2^(p-1) mergings to do of length 2, 2^(p-2) of length 4, ..., 2^0
+    of length 2^p for a list of length 2^p. The algorithm does not need
+    explicitly cutting the list in 2 parts at each step since it the
+    successive accumulation of fragments on the stack which ensures
+    that lists are merged on a dichotomic basis.
+*)
+
+Fixpoint merge_list_to_stack stack l :=
+  match stack with
+  | [] => [Some l]
+  | None :: stack' => Some l :: stack'
+  | Some l' :: stack' => None :: merge_list_to_stack stack' (merge l' l)
+  end.
+
+Fixpoint merge_stack stack :=
+  match stack with
+  | [] => []
+  | None :: stack' => merge_stack stack'
+  | Some l :: stack' => merge l (merge_stack stack')
+  end.
+
+Fixpoint iter_merge stack l :=
+  match l with
+  | [] => merge_stack stack
+  | a::l' => iter_merge (merge_list_to_stack stack [a]) l'
+  end.
+
+Definition sort := iter_merge [].
+
+(** The proof of correctness *)
+
+Local Notation Sorted := (LocallySorted le_bool) (only parsing).
+
+Fixpoint SortedStack stack :=
+  match stack with
+  | [] => True
+  | None :: stack' => SortedStack stack'
+  | Some l :: stack' => Sorted l /\ SortedStack stack'
+  end.
+
+Local Ltac invert H := inversion H; subst; clear H.
+
+Fixpoint flatten_stack (stack : list (option (list A))) :=
+  match stack with
+  | [] => []
+  | None :: stack' => flatten_stack stack'
+  | Some l :: stack' => l ++ flatten_stack stack'
+  end.
+
+Theorem Sorted_merge : forall l1 l2,
+  Sorted l1 -> Sorted l2 -> Sorted (merge l1 l2).
+Proof.
+induction l1; induction l2; intros; simpl; auto.
+  destruct (a <=? a0) as ()_eqn:Heq1.
+    invert H.
+      simpl. constructor; trivial; rewrite Heq1; constructor.
+      assert (Sorted (merge (b::l) (a0::l2))) by (apply IHl1; auto).
+      clear H0 H3 IHl1; simpl in *.
+      destruct (b <=? a0); constructor; auto || rewrite Heq1; constructor.
+    assert (a0 <=? a) by
+      (destruct (le_bool_total a0 a) as [H'|H']; trivial || (rewrite Heq1 in H'; inversion H')).
+    invert H0.
+      constructor; trivial.
+      assert (Sorted (merge (a::l1) (b::l))) by auto using IHl1.
+      clear IHl2; simpl in *.
+      destruct (a <=? b) as ()_eqn:Heq2;
+        constructor; auto.
+Qed.
+
+Theorem Permuted_merge : forall l1 l2, Permutation (l1++l2) (merge l1 l2).
+Proof.
+  induction l1; simpl merge; intro.
+    assert (forall l, (fix merge_aux (l0 : list A) : list A := l0) l = l)
+    as -> by (destruct l; trivial). (* Technical lemma *)
+    apply Permutation_refl.
+  induction l2.
+    rewrite app_nil_r. apply Permutation_refl.
+    destruct (a <=? a0).
+      constructor; apply IHl1.
+      apply Permutation_sym, Permutation_cons_app, Permutation_sym, IHl2.
+Qed.
+
+Theorem Sorted_merge_list_to_stack : forall stack l,
+  SortedStack stack -> Sorted l -> SortedStack (merge_list_to_stack stack l).
+Proof.
+  induction stack as [|[|]]; intros; simpl.
+    auto.
+    apply IHstack. destruct H as (_,H1). fold SortedStack in H1. auto.
+      apply Sorted_merge; auto; destruct H; auto.
+      auto.
+Qed.
+
+Theorem Permuted_merge_list_to_stack : forall stack l,
+  Permutation (l ++ flatten_stack stack) (flatten_stack (merge_list_to_stack stack l)).
+Proof.
+  induction stack as [|[]]; simpl; intros.
+    reflexivity.
+    rewrite app_assoc.
+    etransitivity.
+      apply Permutation_app_tail.
+      etransitivity.
+        apply Permutation_app_comm.
+      apply Permuted_merge.
+    apply IHstack.
+    reflexivity.
+Qed.
+
+Theorem Sorted_merge_stack : forall stack,
+  SortedStack stack -> Sorted (merge_stack stack).
+Proof.
+induction stack as [|[|]]; simpl; intros.
+  constructor; auto.
+  apply Sorted_merge; tauto.
+  auto.
+Qed.
+
+Theorem Permuted_merge_stack : forall stack,
+  Permutation (flatten_stack stack) (merge_stack stack).
+Proof.
+induction stack as [|[]]; simpl.
+  trivial.
+  transitivity (l ++ merge_stack stack).
+    apply Permutation_app_head; trivial.
+    apply Permuted_merge.
+  assumption.
+Qed.
+
+Theorem Sorted_iter_merge : forall stack l,
+  SortedStack stack -> Sorted (iter_merge stack l).
+Proof.
+  intros stack l H; induction l in stack, H |- *; simpl.
+    auto using Sorted_merge_stack.
+    assert (Sorted [a]) by constructor.
+    auto using Sorted_merge_list_to_stack.
+Qed.
+
+Theorem Permuted_iter_merge : forall l stack,
+  Permutation (flatten_stack stack ++ l) (iter_merge stack l).
+Proof.
+  induction l; simpl; intros.
+    rewrite app_nil_r. apply Permuted_merge_stack.
+    change (a::l) with ([a]++l).
+    rewrite app_assoc.
+    etransitivity.
+      apply Permutation_app_tail.
+    etransitivity.
+    apply Permutation_app_comm.
+    apply Permuted_merge_list_to_stack.
+    apply IHl.
+Qed.
+
+Theorem Sorted_sort : forall l, Sorted (sort l).
+Proof.
+intro; apply Sorted_iter_merge. constructor.
+Qed.
+
+Corollary LocallySorted_sort : forall l, Sorted.Sorted le_bool (sort l).
+Proof. intro; eapply Sorted_LocallySorted_iff, Sorted_sort; auto. Qed.
+
+Theorem Permuted_sort : forall l, Permutation l (sort l).
+Proof.
+intro; apply (Permuted_iter_merge l []).
+Qed.
+
+Corollary StronglySorted_sort : forall l,
+  Transitive le_bool -> StronglySorted le_bool (sort l).
+Proof. auto using Sorted_StronglySorted, LocallySorted_sort. Qed.
+
+End Sort.
+
+(** An example *)
+
+Module NatOrder.
+  Definition A := nat.
+  Fixpoint le_bool x y :=
+    match x, y with
+    | 0, _ => true
+    | S x', 0 => false
+    | S x', S y' => le_bool x' y'
+    end.
+  Infix "<=?" := le_bool (at level 35).
+  Theorem le_bool_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
+  Proof.
+    induction a1; destruct a2; simpl; auto using is_eq_true.
+  Qed.
+
+End NatOrder.
+
+Module Import NatSort := Sort NatOrder.
+
+Example SimpleMergeExample := Eval compute in sort [5;3;6;1;8;6;0].
+
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index 9bfe31ed1..8e6aa6dce 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Omega Relations Setoid List Multiset Permutation.
+Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation.
 
 Set Implicit Arguments.
 
@@ -31,19 +31,9 @@ Section Perm.
   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.
+    intros; split; intro H.
+    eapply In_InA, multiplicity_InA in H; eauto with typeclass_instances.
+    eapply multiplicity_InA, InA_alt in H as (y & -> & H); eauto with typeclass_instances.
   Qed.
 
   Lemma multiplicity_In_O :
@@ -102,7 +92,7 @@ Section Perm.
   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.
+    unfold PermutSetoid.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).
@@ -141,7 +131,7 @@ Section Perm.
     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.
+    apply permut_trans with l'; auto.
     revert l'.
     induction l.
     intros.
@@ -152,7 +142,7 @@ Section Perm.
     subst l'.
     apply Permutation_cons_app.
     apply IHl.
-    apply permut_remove_hd with a; auto.
+    apply permut_remove_hd with a; auto with typeclass_instances.
   Qed.
 
   (** Permutation for short lists. *)
@@ -160,7 +150,7 @@ Section Perm.
   Lemma permut_length_1:
     forall a b, permutation (a :: nil) (b :: nil)  -> a=b.
   Proof.
-    intros a b; unfold Permutation.permutation, meq; intro P;
+    intros a b; unfold PermutSetoid.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.
@@ -206,7 +196,7 @@ Section Perm.
     simpl; rewrite <- plus_n_Sm; f_equal.
     rewrite <- app_length.
     apply IHl1.
-    apply permut_remove_hd with a; auto.
+    apply permut_remove_hd with a; auto with typeclass_instances.
   Qed.
 
   Variable B : Type.
@@ -216,7 +206,7 @@ Section Perm.
 
   Lemma permutation_map :
     forall f l1 l2, permutation l1 l2 ->
-      Permutation.permutation _ eqB_dec (map f l1) (map f l2).
+      PermutSetoid.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.
@@ -229,7 +219,7 @@ Section Perm.
     apply permut_add_cons_inside.
     rewrite <- map_app.
     apply IHl1; auto.
-    apply permut_remove_hd with a; auto.
+    apply permut_remove_hd with a; auto with typeclass_instances.
   Qed.
 
 End Perm.
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 1f1ecddcd..203e212b6 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -8,23 +8,201 @@
 
 (*i $Id$ i*)
 
-Require Import Omega Relations Multiset Permutation SetoidList.
+Require Import Omega Relations Multiset SetoidList.
 
-Set Implicit Arguments.
+(** This file is deprecated, use [Permutation.v] instead.
+
+    Indeed, this file defines a notion of permutation based on
+    multisets (there exists a permutation between two lists iff every
+    elements have the same multiplicity in the two lists) which
+    requires a more complex apparatus (the equipment of the domain
+    with a decidable equality) than [Permutation] in [Permutation.v].
 
-(** This file contains additional results about permutations
-     with respect to a setoid equality (i.e. an equivalence relation).
+    The relation between the two relations are in lemma
+    [permutation_Permutation].
+
+    File [PermutEq] concerns Leibniz equality : it shows in particular
+    that [List.Permutation] and [permutation] are equivalent in this context.
 *)
 
-Section Perm.
+Set Implicit Arguments.
+
+Local Notation "[ ]" := nil.
+Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
+
+Section Permut.
+
+(** * From lists to multisets *)
 
 Variable A : Type.
 Variable eqA : relation A.
 Hypothesis eqA_equiv : Equivalence eqA.
 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).
+Let emptyBag := EmptyBag A.
+Let singletonBag := SingletonBag _ eqA_dec.
+
+(** contents of a list *)
+
+Fixpoint list_contents (l:list A) : multiset A :=
+  match l with
+  | [] => emptyBag
+  | a :: l => munion (singletonBag a) (list_contents l)
+  end.
+
+Lemma list_contents_app :
+  forall l m:list A,
+    meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
+Proof.
+  simple induction l; simpl in |- *; auto with datatypes.
+  intros.
+  apply meq_trans with
+    (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
+    auto with datatypes.
+Qed.
+
+(** * [permutation]: definition and basic properties *)
+
+Definition permutation (l m:list A) := meq (list_contents l) (list_contents m).
+
+Lemma permut_refl : forall l:list A, permutation l l.
+Proof.
+  unfold permutation in |- *; auto with datatypes.
+Qed.
+
+Lemma permut_sym :
+  forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
+Proof.
+  unfold permutation, meq; intros; apply sym_eq; trivial.
+Qed.
+
+Lemma permut_trans :
+  forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
+Proof.
+  unfold permutation in |- *; intros.
+  apply meq_trans with (list_contents m); auto with datatypes.
+Qed.
+
+Lemma permut_cons_eq :
+  forall l m:list A,
+    permutation l m -> forall a a', eqA a a' -> permutation (a :: l) (a' :: m).
+Proof.
+  unfold permutation; simpl; intros.
+  apply meq_trans with (munion (singletonBag a') (list_contents l)).
+  apply meq_left, meq_singleton; auto.
+  auto with datatypes.
+Qed.
+
+Lemma permut_cons :
+  forall l m:list A,
+    permutation l m -> forall a:A, permutation (a :: l) (a :: m).
+Proof.
+  unfold permutation; simpl; auto with datatypes.
+Qed.
+
+Lemma permut_app :
+  forall l l' m m':list A,
+    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));
+    auto using permut_cons, list_contents_app with datatypes.
+  apply meq_trans with (munion (list_contents l') (list_contents m'));
+    auto using permut_cons, list_contents_app with datatypes.
+  apply meq_trans with (munion (list_contents l') (list_contents m));
+    auto using permut_cons, list_contents_app with datatypes.
+Qed.
+
+Lemma permut_add_inside_eq :
+  forall a a' l1 l2 l3 l4, eqA a a' ->
+    permutation (l1 ++ l2) (l3 ++ l4) ->
+    permutation (l1 ++ a :: l2) (l3 ++ a' :: l4).
+Proof.
+  unfold permutation, meq in *; intros.
+  specialize H0 with a0.
+  repeat rewrite list_contents_app in *; simpl in *.
+  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite H in Ha;
+    decide (eqA_dec a' a0) with Ha; simpl; auto with arith.
+  do 2 rewrite <- plus_n_Sm; f_equal; auto.
+Qed.
+
+Lemma permut_add_inside :
+  forall a l1 l2 l3 l4,
+    permutation (l1 ++ l2) (l3 ++ l4) ->
+    permutation (l1 ++ a :: l2) (l3 ++ a :: l4).
+Proof.
+  unfold permutation, meq in *; intros.
+  generalize (H a0); clear H.
+  do 4 rewrite list_contents_app.
+  simpl.
+  destruct (eqA_dec a a0); simpl; auto with arith.
+  do 2 rewrite <- plus_n_Sm; f_equal; auto.
+Qed.
+
+Lemma permut_add_cons_inside_eq :
+  forall a a' l l1 l2, eqA a a' ->
+    permutation l (l1 ++ l2) ->
+    permutation (a :: l) (l1 ++ a' :: l2).
+Proof.
+  intros;
+  replace (a :: l) with ([] ++ a :: l); trivial;
+    apply permut_add_inside_eq; trivial.
+Qed.
+
+Lemma permut_add_cons_inside :
+  forall a l l1 l2,
+    permutation l (l1 ++ l2) ->
+    permutation (a :: l) (l1 ++ a :: l2).
+Proof.
+  intros;
+    replace (a :: l) with ([] ++ 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 using permut_sym, permut_refl.
+Qed.
+
+Lemma permut_sym_app :
+  forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
+Proof.
+  intros l1 l2;
+    unfold permutation, meq;
+	intro a; do 2 rewrite list_contents_app; simpl;
+	  auto with arith.
+Qed.
+
+Lemma permut_rev :
+  forall l, permutation l (rev l).
+Proof.
+  induction l.
+  simpl; trivial using permut_refl.
+  simpl.
+  apply permut_add_cons_inside.
+  rewrite <- app_nil_end. trivial.
+Qed.
+
+(** * Some inversion results. *)
+Lemma permut_conv_inv :
+  forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.
+Proof.
+  intros e l1 l2; unfold permutation, meq; simpl; intros H a;
+    generalize (H a); apply plus_reg_l.
+Qed.
+
+Lemma permut_app_inv1 :
+  forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.
+Proof.
+  intros l l1 l2; unfold permutation, meq; simpl;
+    intros H a; generalize (H a); clear H.
+  do 2 rewrite list_contents_app.
+  simpl.
+  intros; apply plus_reg_l with (multiplicity (list_contents l) a).
+  rewrite plus_comm; rewrite H; rewrite plus_comm.
+  trivial.
+Qed.
 
 (** we can use [multiplicity] to define [InA] and [NoDupA]. *)
 
@@ -35,6 +213,39 @@ Proof.
   contradict NEQ; auto.
 Qed.
 
+Lemma permut_app_inv2 :
+  forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.
+Proof.
+  intros l l1 l2; unfold permutation, meq; simpl;
+    intros H a; generalize (H a); clear H.
+  do 2 rewrite list_contents_app.
+  simpl.
+  intros; apply plus_reg_l with (multiplicity (list_contents l) a).
+  trivial.
+Qed.
+
+Lemma permut_remove_hd_eq :
+  forall l l1 l2 a b, eqA a b ->
+    permutation (a :: l) (l1 ++ b :: l2) -> permutation l (l1 ++ l2).
+Proof.
+  unfold permutation, meq; simpl; intros l l1 l2 a b Heq H a0.
+  specialize H with a0.
+  rewrite list_contents_app in *; simpl in *.
+  apply plus_reg_l with (if eqA_dec a a0 then 1 else 0).
+  rewrite H; clear H.
+  symmetry; rewrite plus_comm, <- ! plus_assoc; f_equal.
+  rewrite plus_comm.
+  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite Heq in Ha;
+    decide (eqA_dec b a0) with Ha; reflexivity.
+Qed.
+
+Lemma permut_remove_hd :
+  forall l l1 l2 a,
+    permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
+Proof.
+  eauto using permut_remove_hd_eq, Equivalence_Reflexive.
+Qed.
+
 Fact if_eqA_else : forall a a' (B:Type)(b b':B),
  ~eqA a a' -> (if eqA_dec a a' then b else b') = b'.
 Proof.
@@ -137,14 +348,13 @@ Proof.
   destruct (eqA_dec a a0); simpl; auto with *.
 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.
+  unfold permutation, meq.
   intros H;rewrite H; auto.
 Qed.
 
@@ -156,7 +366,7 @@ Qed.
 
 (** Permutation of an empty list. *)
 Lemma permut_nil :
-  forall l, permutation l nil -> l = nil.
+  forall l, permutation l [] -> l = [].
 Proof.
   intro l; destruct l as [ | e l ]; trivial.
   assert (InA eqA e (e::l)) by (auto with *).
@@ -167,16 +377,16 @@ Qed.
 (** Permutation for short lists. *)
 
 Lemma permut_length_1:
-  forall a b, permutation (a :: nil) (b :: nil)  -> eqA a b.
+  forall a b, permutation [a] [b] -> eqA a b.
 Proof.
-  intros a b; unfold Permutation.permutation, meq.
+  intros a b; unfold permutation, meq.
   intro P; specialize (P b); simpl in *.
   rewrite if_eqA_refl in *.
   destruct (eqA_dec a b); simpl; auto; discriminate.
 Qed.
 
 Lemma permut_length_2 :
-  forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
+  forall a1 b1 a2 b2, permutation [a1; b1] [a2; b2] ->
     (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).
 Proof.
   intros a1 b1 a2 b2 P.
@@ -214,8 +424,8 @@ Proof.
   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.
+  apply permut_trans with (a::l1); auto.
+  revert H1; unfold permutation, meq; simpl.
   intros; f_equal; auto.
   rewrite (@if_eqA_rewrite_l a b a0); auto.
 Qed.
@@ -232,32 +442,39 @@ Proof.
   destruct 3; omega.
 Qed.
 
+End Permut.
 
-Variable B : Type.
-Variable eqB : B->B->Prop.
-Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
-Variable eqB_trans : Transitive eqB.
+Section Permut_map.
+
+Variables A B : Type.
 
+Variable eqA : relation A.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis eqA_equiv : Equivalence eqA.
+
+Variable eqB : B->B->Prop.
+Hypothesis eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
+Hypothesis eqB_trans : Transitive eqB.
 
 (** Permutation is compatible with map. *)
 
 Lemma permut_map :
   forall f,
     (Proper (eqA==>eqB) f) ->
-    forall l1 l2, permutation l1 l2 ->
-      Permutation.permutation _ eqB_dec (map f l1) (map f l2).
+    forall l1 l2, permutation _ eqA_dec l1 l2 ->
+      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; rewrite (permut_nil eqA_equiv (permut_sym P)); apply permut_refl.
   intros l2 P.
   simpl.
-  assert (H0:=permut_cons_InA P).
+  assert (H0:=permut_cons_InA eqA_equiv 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.
+  apply permut_trans with (f b :: map f l1).
+  revert H1; unfold 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.
@@ -266,11 +483,72 @@ Proof.
   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.
+  apply permut_remove_hd with b; trivial.
+  apply permut_trans with (a::l1); auto.
+  revert H1; unfold permutation, meq; simpl.
   intros; f_equal; auto.
-  rewrite (@if_eqA_rewrite_l a b a0); auto.
+  rewrite (@if_eqA_rewrite_l _ _ eqA_equiv eqA_dec a b a0); auto.
+Qed.
+
+End Permut_map.
+
+Require Import Permutation TheoryList.
+
+Section Permut_permut.
+
+Variable A : Type.
+
+Variable eqA : relation A.
+Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
+Hypothesis eqA_equiv : Equivalence eqA.
+
+Lemma Permutation_impl_permutation : forall l l',
+  Permutation l l' -> permutation _ eqA_dec l l'.
+Proof.
+  induction 1.
+    apply permut_refl.
+    apply permut_cons; auto using Equivalence_Reflexive.
+    change (x :: y :: l) with ([x] ++ y :: l);
+      apply permut_add_cons_inside; simpl;
+      apply permut_cons_eq; auto using Equivalence_Reflexive, permut_refl.
+    apply permut_trans with l'; trivial.
 Qed.
 
-End Perm.
+Lemma permut_eqA : forall l l', Forall2 eqA l l' -> permutation _ eqA_dec l l'.
+Proof.
+  induction 1.
+    apply permut_refl.
+    apply permut_cons_eq; trivial.
+Qed.
+
+Lemma permutation_Permutation : forall l l',
+  permutation _ eqA_dec l l' <->
+  exists l'', Permutation l l'' /\ Forall2 eqA l'' l'.
+Proof.
+  split; intro H.
+  (* -> *)
+  induction l in l', H |- *.
+    exists []; apply permut_sym, permut_nil in H as ->; auto using Forall2.
+    pose proof H as H'.
+    apply permut_cons_InA, InA_split in H
+      as (l1 & y & l2 & Heq & ->); trivial.
+    apply permut_remove_hd_eq, IHl in H'
+      as (l'' & IHP & IHA); clear IHl; trivial.
+    apply Forall2_app_inv_r in IHA as (l1'' & l2'' & Hl1 & Hl2 & ->).
+    exists (l1'' ++ a :: l2''); split.
+      apply Permutation_cons_app; trivial.
+      apply Forall2_app, Forall2_cons; trivial.
+  (* <- *)
+  destruct H as (l'' & H & Heq).
+  apply permut_trans with l''.
+    apply Permutation_impl_permutation; trivial.
+    apply permut_eqA; trivial.
+Qed.
+
+End Permut_permut.
+
+(* begin hide *)
+(** For compatibilty *)
+Notation permut_right := permut_cons (only parsing).
+Notation permut_tran := permut_trans (only parsing).
+(* end hide *)
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 27ba50908..da30d096c 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -8,198 +8,367 @@
 
 (*i $Id$ i*)
 
-Require Import Relations List Multiset Plus.
+(*********************************************************************)
+(** ** List permutations as a composition of adjacent transpositions *)
+(*********************************************************************)
 
-(** 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 multiplicity in the two lists.
+(* Adapted in May 2006 by Jean-Marc Notin from initial contents by
+   Laurent Théry (Huffmann contribution, October 2003) *)
 
-    Unlike [List.Permutation], the present notion of permutation
-    requires the domain to be equipped with a decidable equality. This
-    equality allows to reason modulo the effective equivalence-class
-    representative used in each list.
+Require Import List Setoid.
 
-    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).
+Set Implicit Arguments.
 
-    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.
-*)
+Local Notation "[ ]" := nil.
+Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
 
-Set Implicit Arguments.
+Section Permutation.
 
-Section defs.
-
-  (** * From lists to multisets *)
-
-  Variable A : Type.
-  Variable eqA : relation A.
-  Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
-
-  Let emptyBag := EmptyBag A.
-  Let singletonBag := SingletonBag _ eqA_dec.
-
-  (** contents of a list *)
-
-  Fixpoint list_contents (l:list A) : multiset A :=
-    match l with
-      | nil => emptyBag
-      | a :: l => munion (singletonBag a) (list_contents l)
-    end.
-
-  Lemma list_contents_app :
-    forall l m:list A,
-      meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
-  Proof.
-    simple induction l; simpl in |- *; auto with datatypes.
-    intros.
-    apply meq_trans with
-      (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
-      auto with datatypes.
-  Qed.
-
-
-  (** * [permutation]: definition and basic properties *)
-
-  Definition permutation (l m:list A) :=
-    meq (list_contents l) (list_contents m).
-
-  Lemma permut_refl : forall l:list A, permutation l l.
-  Proof.
-    unfold permutation in |- *; auto with datatypes.
-  Qed.
-
-  Lemma permut_sym :
-    forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
-  Proof.
-    unfold permutation, meq; intros; apply sym_eq; trivial.
-  Qed.
-
-  Lemma permut_tran :
-    forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
-  Proof.
-    unfold permutation in |- *; intros.
-    apply meq_trans with (list_contents m); auto with datatypes.
-  Qed.
-
-  Lemma permut_cons :
-    forall l m:list A,
-      permutation l m -> forall a:A, permutation (a :: l) (a :: m).
-  Proof.
-    unfold permutation in |- *; simpl in |- *; auto with datatypes.
-  Qed.
-
-  Lemma permut_app :
-    forall l l' m m':list A,
-      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));
-      auto using permut_cons, list_contents_app with datatypes.
-    apply meq_trans with (munion (list_contents l') (list_contents m'));
-      auto using permut_cons, list_contents_app with datatypes.
-    apply meq_trans with (munion (list_contents l') (list_contents m));
-      auto using permut_cons, list_contents_app with datatypes.
-  Qed.
-
-  Lemma permut_add_inside :
-    forall a l1 l2 l3 l4,
-      permutation (l1 ++ l2) (l3 ++ l4) ->
-      permutation (l1 ++ a :: l2) (l3 ++ a :: l4).
-  Proof.
-    unfold permutation, meq in *; intros.
-    generalize (H a0); clear H.
-    do 4 rewrite list_contents_app.
-    simpl.
-    destruct (eqA_dec a a0); simpl; auto with arith.
-    do 2 rewrite <- plus_n_Sm; f_equal; auto.
-  Qed.
-
-  Lemma permut_add_cons_inside :
-    forall a l l1 l2,
-      permutation l (l1 ++ l2) ->
-      permutation (a :: l) (l1 ++ a :: l2).
-  Proof.
-    intros;
-      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 using permut_sym, permut_refl.
-  Qed.
-
-  Lemma permut_sym_app :
-    forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
-  Proof.
-    intros l1 l2;
-      unfold permutation, meq;
-	intro a; do 2 rewrite list_contents_app; simpl;
-	  auto with arith.
-  Qed.
-
-  Lemma permut_rev :
-    forall l, permutation l (rev l).
-  Proof.
-    induction l.
-    simpl; trivial using permut_refl.
-    simpl.
-    apply permut_add_cons_inside.
-    rewrite <- app_nil_end. trivial.
-  Qed.
-
-  (** * Some inversion results. *)
-  Lemma permut_conv_inv :
-    forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.
-  Proof.
-    intros e l1 l2; unfold permutation, meq; simpl; intros H a;
-      generalize (H a); apply plus_reg_l.
-  Qed.
-
-  Lemma permut_app_inv1 :
-    forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.
-  Proof.
-    intros l l1 l2; unfold permutation, meq; simpl;
-      intros H a; generalize (H a); clear H.
-    do 2 rewrite list_contents_app.
-    simpl.
-    intros; apply plus_reg_l with (multiplicity (list_contents l) a).
-    rewrite plus_comm; rewrite H; rewrite plus_comm.
-    trivial.
-  Qed.
-
-  Lemma permut_app_inv2 :
-    forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.
-  Proof.
-    intros l l1 l2; unfold permutation, meq; simpl;
-      intros H a; generalize (H a); clear H.
-    do 2 rewrite list_contents_app.
-    simpl.
-    intros; apply plus_reg_l with (multiplicity (list_contents l) a).
-    trivial.
-  Qed.
-
-  Lemma permut_remove_hd :
-    forall l l1 l2 a,
-      permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
-  Proof.
-    intros l l1 l2 a; unfold permutation, meq; simpl; intros H a0; generalize (H a0); clear H.
-    do 2 rewrite list_contents_app; simpl; intro H.
-    apply plus_reg_l with (if eqA_dec a a0 then 1 else 0).
-    rewrite H; clear H.
-    symmetry; rewrite plus_comm.
-    repeat rewrite <- plus_assoc; f_equal.
-    apply plus_comm.
-  Qed.
-
-End defs.
-
-(** For compatibilty *)
-Notation permut_right := permut_cons.
-Unset Implicit Arguments.
+Variable A:Type.
+
+Inductive Permutation : list A -> list A -> Prop :=
+| perm_nil: Permutation [] []
+| perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
+| perm_swap x y l : Permutation (y::x::l) (x::y::l)
+| perm_trans l l' l'' : Permutation l l' -> Permutation l' l'' -> Permutation l l''.
+
+Hint Constructors Permutation.
+
+(** Some facts about [Permutation] *)
+
+Theorem Permutation_nil : forall (l : list A), Permutation [] l -> l = [].
+Proof.
+  intros l HF.
+  remember (@nil A) as m in HF.
+  induction HF; discriminate || auto.
+Qed.
+
+Theorem Permutation_nil_cons : forall (l : list A) (x : A), ~ Permutation nil (x::l).
+Proof.
+  intros l x HF.
+  apply Permutation_nil in HF; discriminate.
+Qed.
+
+(** Permutation over lists is a equivalence relation *)
+
+Theorem Permutation_refl : forall l : list A, Permutation l l.
+Proof.
+  induction l; constructor. exact IHl.
+Qed.
+
+Theorem Permutation_sym : forall l l' : list A, Permutation l l' -> Permutation l' l.
+Proof.
+  intros l l' Hperm; induction Hperm; auto.
+  apply perm_trans with (l':=l'); assumption.
+Qed.
+
+Theorem Permutation_trans : forall l l' l'' : list A, Permutation l l' -> Permutation l' l'' -> Permutation l l''.
+Proof.
+  exact perm_trans.
+Qed.
+
+End Permutation.
+
+Hint Constructors Permutation.
+Hint Resolve Permutation_refl Permutation_sym Permutation_trans.
+
+(* This provides reflexivity, symmetry and transitivity and rewriting
+   on morphims to come *)
+
+Add Parametric Relation A : (list A) (@Permutation A)
+  reflexivity proved by (@Permutation_refl A)
+  symmetry proved by (@Permutation_sym A)
+  transitivity proved by (@Permutation_trans A)
+as Permutation_Equivalence.
+
+Add Parametric Morphism A (a:A) : (cons a)
+  with signature @Permutation A ==> @Permutation A
+  as Permutation_cons.
+Proof.
+  auto using perm_skip.
+Qed.
+
+Section Permutation_properties.
+
+Variable A:Type.
+
+Implicit Types a b : A.
+Implicit Types l m : list A.
+
+(** Compatibility with others operations on lists *)
+
+Theorem Permutation_in : forall (l l' : list A) (x : A), Permutation l l' -> In x l -> In x l'.
+Proof.
+  intros l l' x Hperm; induction Hperm; simpl; tauto.
+Qed.
+
+Lemma Permutation_app_tail : forall (l l' tl : list A), Permutation l l' -> Permutation (l++tl) (l'++tl).
+Proof.
+  intros l l' tl Hperm; induction Hperm as [|x l l'|x y l|l l' l'']; simpl; auto.
+  eapply Permutation_trans with (l':=l'++tl); trivial.
+Qed.
+
+Lemma Permutation_app_head : forall (l tl tl' : list A), Permutation tl tl' -> Permutation (l++tl) (l++tl').
+Proof.
+  intros l tl tl' Hperm; induction l; [trivial | repeat rewrite <- app_comm_cons; constructor; assumption].
+Qed.
+
+Theorem Permutation_app : forall (l m l' m' : list A), Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m').
+Proof.
+  intros l m l' m' Hpermll' Hpermmm'; induction Hpermll' as [|x l l'|x y l|l l' l'']; repeat rewrite <- app_comm_cons; auto.
+  apply Permutation_trans with (l' := (x :: y :: l ++ m));
+	[idtac | repeat rewrite app_comm_cons; apply Permutation_app_head]; trivial.
+  apply Permutation_trans with (l' := (l' ++ m')); try assumption.
+  apply Permutation_app_tail; assumption.
+Qed.
+
+Add Parametric Morphism : (@app A)
+  with signature @Permutation A ==> @Permutation A ==> @Permutation A
+  as Permutation_app'.
+  auto using Permutation_app.
+Qed.
+
+Lemma Permutation_add_inside : forall a (l l' tl tl' : list A),
+  Permutation l l' -> Permutation tl tl' ->
+  Permutation (l ++ a :: tl) (l' ++ a :: tl').
+Proof.
+  intros; apply Permutation_app; auto.
+Qed.
+
+Theorem Permutation_app_comm : forall (l l' : list A),
+  Permutation (l ++ l') (l' ++ l).
+Proof.
+  induction l as [|x l]; simpl; intro l'.
+  rewrite app_nil_r; trivial.
+  induction l' as [|y l']; simpl.
+  rewrite app_nil_r; trivial.
+  transitivity (x :: y :: l' ++ l).
+  constructor; rewrite app_comm_cons; apply IHl.
+  transitivity (y :: x :: l' ++ l); constructor.
+  transitivity (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.
+  transitivity (a0::a::l1++l2).
+  apply perm_skip; auto.
+  transitivity (a::a0::l1++l2).
+  apply perm_swap; auto.
+  apply perm_skip; auto.
+Qed.
+Hint Resolve Permutation_cons_app.
+
+Theorem Permutation_middle : forall (l1 l2:list A) a,
+  Permutation (a :: l1 ++ l2) (l1 ++ a :: l2).
+Proof.
+  auto.
+Qed.
+
+Theorem Permutation_rev : forall (l : list A), Permutation l (rev l).
+Proof.
+  induction l as [| x l]; simpl; trivial.
+  apply Permutation_trans with (l' := [x] ++ rev l).
+  simpl; auto.
+  apply Permutation_app_comm.
+Qed.
+
+Theorem Permutation_length : forall (l l' : list A), Permutation l l' -> length l = length l'.
+Proof.
+  intros l l' Hperm; induction Hperm; simpl; auto.
+  apply trans_eq with (y:= (length l')); trivial.
+Qed.
+
+Theorem Permutation_ind_bis :
+ forall P : list A -> list A -> Prop,
+   P [] [] ->
+   (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 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 using Permutation_cons_app.
+  apply perm_skip.
+  apply (IH a l1' l2 l3' l4); auto.
+  (* contradict *)
+  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 [] l [] 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 [] 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_r; auto.
+  intros.
+  apply IHl.
+  apply Permutation_app_inv with a; auto.
+Qed.
+
+Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a].
+Proof.
+  intros a l H; remember [a] as m in H.
+  induction H; try (injection Heqm as -> ->; clear Heqm);
+    discriminate || auto.
+  apply Permutation_nil in H as ->; trivial.
+Qed.
+
+Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b.
+Proof.
+  intros a b H.
+  apply Permutation_length_1_inv in H; injection H as ->; trivial.
+Qed.
+
+Lemma Permutation_length_2_inv :
+  forall a1 a2 l, Permutation [a1;a2] l -> l = [a1;a2] \/ l = [a2;a1].
+Proof.
+  intros a1 a2 l H; remember [a1;a2] as m in H.
+  revert a1 a2 Heqm.
+  induction H; intros; try (injection Heqm; intros; subst; clear Heqm);
+    discriminate || (try tauto).
+  apply Permutation_length_1_inv in H as ->; left; auto.
+  apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as ();
+    auto.
+Qed.
+
+Lemma Permutation_length_2 :
+  forall a1 a2 b1 b2, Permutation [a1;a2] [b1;b2] ->
+    a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1.
+Proof.
+  intros a1 b1 a2 b2 H.
+  apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto.
+Qed.
+
+Lemma NoDup_Permutation : forall l l',
+  NoDup l -> NoDup l' -> (forall x:A, 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 Permutation_properties.
+
+Section Permutation_map.
+
+Variable A B : Type.
+Variable f : A -> B.
+
+Add Parametric Morphism : (map f)
+  with signature (@Permutation A) ==> (@Permutation B) as Permutation_map_aux.
+Proof.
+  induction 1; simpl; eauto using Permutation.
+Qed.
+
+Lemma Permutation_map :
+  forall l l', Permutation l l' -> Permutation (map f l) (map f l').
+Proof.
+  exact Permutation_map_aux_Proper.
+Qed.
+
+End Permutation_map.
+
+(* begin hide *)
+Notation Permutation_app_swap := Permutation_app_comm (only parsing).
+(* end hide *)
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
new file mode 100644
index 000000000..d87259eec
--- /dev/null
+++ b/theories/Sorting/Sorted.v
@@ -0,0 +1,154 @@
+(************************************************************************)
+(*  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*)
+
+(* Made by Hugo Herbelin *)
+
+(** This file defines two notions of sorted list:
+
+  - a list is locally sorted if any element is smaller or equal than
+    its successor in the list
+  - a list is sorted if any element coming before another one is
+    smaller or equal than this other element
+
+  The two notions are equivalent if the order is transitive.
+*)
+
+Require Import List Relations Relations_1.
+
+(** Preambule *)
+
+Set Implicit Arguments.
+Local Notation "[ ]" := nil (at level 0).
+Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0).
+Implicit Arguments Transitive [U].
+
+Section defs.
+
+  Variable A : Type.
+  Variable R : A -> A -> Prop.
+
+  (** Locally sorted: consecutive elements of the list are ordered *)
+
+  Inductive LocallySorted : list A -> Prop :=
+    | LSorted_nil : LocallySorted []
+    | LSorted_cons1 a : LocallySorted [a]
+    | LSorted_consn a b l :
+        LocallySorted (b :: l) -> R a b -> LocallySorted (a :: b :: l).
+
+  (** Alternative two-step definition of being locally sorted *)
+
+  Inductive HdRel a : list A -> Prop :=
+    | HdRel_nil : HdRel a []
+    | HdRel_cons b l : R a b -> HdRel a (b :: l).
+
+  Inductive Sorted : list A -> Prop :=
+    | Sorted_nil : Sorted []
+    | Sorted_cons a l : Sorted l -> HdRel a l -> Sorted (a :: l).
+
+  Lemma HdRel_inv : forall a b l, HdRel a (b :: l) -> R a b.
+  Proof.
+    inversion 1; auto.
+  Qed.
+
+  Lemma Sorted_inv :
+    forall a l, Sorted (a :: l) -> Sorted l /\ HdRel a l.
+  Proof.
+    intros a l H; inversion H; auto.
+  Qed.
+
+  Lemma Sorted_rect :
+    forall P:list A -> Type,
+      P [] ->
+      (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) ->
+      forall l:list A, Sorted l -> P l.
+  Proof.
+    induction l; firstorder using Sorted_inv.
+  Qed.
+
+  Lemma Sorted_LocallySorted_iff : forall l, Sorted l <-> LocallySorted l.
+  Proof.
+    split; [induction 1 as [|a l [|]]| induction 1];
+      auto using Sorted, LocallySorted, HdRel.
+    inversion H1; subst; auto using LocallySorted.
+  Qed.
+
+  (** Strongly sorted: elements of the list are pairwise ordered *)
+
+  Inductive StronglySorted : list A -> Prop :=
+    | SSorted_nil : StronglySorted []
+    | SSorted_cons a l : StronglySorted l -> Forall (R a) l -> StronglySorted (a :: l).
+
+  Lemma StronglySorted_inv : forall a l, StronglySorted (a :: l) ->
+    StronglySorted l /\ Forall (R a) l.
+  Proof.
+    intros; inversion H; auto.
+  Defined.
+
+  Lemma StronglySorted_rect :
+    forall P:list A -> Type,
+      P [] ->
+      (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) ->
+      forall l, StronglySorted l -> P l.
+  Proof.
+    induction l; firstorder using StronglySorted_inv.
+  Defined.
+
+  Lemma StronglySorted_rec :
+    forall P:list A -> Type,
+      P [] ->
+      (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) ->
+      forall l, StronglySorted l -> P l.
+  Proof.
+    firstorder using StronglySorted_rect.
+  Qed.
+
+  Lemma StronglySorted_Sorted : forall l, StronglySorted l -> Sorted l.
+  Proof.
+    induction 1 as [|? ? ? ? HForall]; constructor; trivial.
+    destruct HForall; constructor; trivial.
+  Qed.
+
+  Lemma Sorted_extends :
+    Transitive R -> forall a l, Sorted (a::l) -> Forall (R a) l.
+  Proof.
+    intros. change match a :: l with [] => True | a :: l => Forall (R a) l end.
+    induction H0 as [|? ? ? ? H1]; [trivial|].
+    destruct H1; constructor; trivial.
+    eapply Forall_impl; [|eassumption].
+    firstorder.
+  Qed.
+
+  Lemma Sorted_StronglySorted :
+    Transitive R -> forall l, Sorted l -> StronglySorted l.
+  Proof.
+    induction 2; constructor; trivial.
+    apply Sorted_extends; trivial.
+    constructor; trivial.
+  Qed.
+
+End defs.
+
+Hint Constructors HdRel: sorting.
+Hint Constructors Sorted: sorting.
+
+(* begin hide *)
+(* Compatibility with deprecated file Sorting.v *)
+Notation lelistA := HdRel (only parsing).
+Notation nil_leA := HdRel_nil (only parsing).
+Notation cons_leA := HdRel_cons (only parsing).
+
+Notation sort := Sorted (only parsing).
+Notation nil_sort := Sorted_nil (only parsing).
+Notation cons_sort := Sorted_cons (only parsing).
+
+Notation lelistA_inv := HdRel_inv (only parsing).
+Notation sort_inv := Sorted_inv (only parsing).
+Notation sort_rect := Sorted_rect (only parsing).
+(* end hide *)
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index 2d76b25a2..5f8da6a4d 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -8,123 +8,5 @@
 
 (*i $Id$ i*)
 
-Require Import List Multiset Permutation Relations.
-
-Set Implicit Arguments.
-
-Section defs.
-
-  Variable A : Type.
-  Variable leA : relation A.
-  Variable eqA : relation A.
-
-  Let gtA (x y:A) := ~ leA x y.
-
-  Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
-  Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
-  Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
-  Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
-  Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
-
-  Hint Resolve leA_refl.
-  Hint Immediate eqA_dec leA_dec leA_antisym.
-
-  Let emptyBag := EmptyBag A.
-  Let singletonBag := SingletonBag _ eqA_dec.
-
-  (** [lelistA] *)
-
-  Inductive lelistA (a:A) : list A -> Prop :=
-    | nil_leA : lelistA a nil
-    | cons_leA : forall (b:A) (l:list A), leA a b -> lelistA a (b :: l).
-
-  Lemma lelistA_inv : forall (a b:A) (l:list A), lelistA a (b :: l) -> leA a b.
-  Proof.
-    intros; inversion H; trivial with datatypes.
-  Qed.
-
-  (** * Definition for a list to be sorted *)
-
-  Inductive sort : list A -> Prop :=
-    | nil_sort : sort nil
-    | cons_sort :
-      forall (a:A) (l:list A), sort l -> lelistA a l -> sort (a :: l).
-
-  Lemma sort_inv :
-    forall (a:A) (l:list A), sort (a :: l) -> sort l /\ lelistA a l.
-  Proof.
-    intros; inversion H; auto with datatypes.
-  Qed.
-
-  Lemma sort_rect :
-    forall P:list A -> Type,
-      P nil ->
-      (forall (a:A) (l:list A), sort l -> P l -> lelistA a l -> P (a :: l)) ->
-      forall y:list A, sort y -> P y.
-  Proof.
-    simple induction y; auto with datatypes.
-    intros; elim (sort_inv (a:=a) (l:=l)); auto with datatypes.
-  Qed.
-
-  Lemma sort_rec :
-    forall P:list A -> Set,
-      P nil ->
-      (forall (a:A) (l:list A), sort l -> P l -> lelistA a l -> P (a :: l)) ->
-      forall y:list A, sort y -> P y.
-  Proof.
-    simple induction y; auto with datatypes.
-    intros; elim (sort_inv (a:=a) (l:=l)); auto with datatypes.
-  Qed.
-
-  (** * Merging two sorted lists *)
-
-  Inductive merge_lem (l1 l2:list A) : Type :=
-    merge_exist :
-    forall l:list A,
-      sort l ->
-      meq (list_contents _ eqA_dec l)
-      (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
-      (forall a:A, lelistA a l1 -> lelistA a l2 -> lelistA a l) ->
-      merge_lem l1 l2.
-
-  Lemma merge :
-    forall l1:list A, sort l1 -> forall l2:list A, sort l2 -> merge_lem l1 l2.
-  Proof.
-    simple induction 1; intros.
-    apply merge_exist with l2; auto with datatypes.
-    elim H2; intros.
-    apply merge_exist with (a :: l); simpl in |- *; auto using cons_sort with datatypes.
-    elim (leA_dec a a0); intros.
-
-    (* 1 (leA a a0) *)
-    cut (merge_lem l (a0 :: l0)); auto using cons_sort with datatypes.
-    intros [l3 l3sorted l3contents Hrec].
-    apply merge_exist with (a :: l3); simpl in |- *;
-      auto using cons_sort, cons_leA with datatypes.
-    apply meq_trans with
-      (munion (singletonBag a)
-	(munion (list_contents _ eqA_dec l)
-          (list_contents _ eqA_dec (a0 :: l0)))).
-    apply meq_right; trivial with datatypes.
-    apply meq_sym; apply munion_ass.
-    intros; apply cons_leA.
-    apply lelistA_inv with l; trivial with datatypes.
-
-    (* 2 (leA a0 a) *)
-    elim X0; simpl in |- *; intros.
-    apply merge_exist with (a0 :: l3); simpl in |- *;
-      auto using cons_sort, cons_leA with datatypes.
-    apply meq_trans with
-      (munion (singletonBag a0)
-	(munion (munion (singletonBag a) (list_contents _ eqA_dec l))
-          (list_contents _ eqA_dec l0))).
-    apply meq_right; trivial with datatypes.
-    apply munion_perm_left.
-    intros; apply cons_leA; apply lelistA_inv with l0; trivial with datatypes.
-  Qed.
-
-End defs.
-
-Unset Implicit Arguments.
-Hint Constructors sort: datatypes v62.
-Hint Constructors lelistA: datatypes v62.
+Require Export Sorted.
+Require Export Mergesort.
diff --git a/theories/Sorting/vo.itarget b/theories/Sorting/vo.itarget
index b14f8f743..079eaad18 100644
--- a/theories/Sorting/vo.itarget
+++ b/theories/Sorting/vo.itarget
@@ -1,5 +1,7 @@
 Heap.vo
 Permutation.vo
-PermutEq.vo
 PermutSetoid.vo
+PermutEq.vo
+Sorted.vo
 Sorting.vo
+Mergesort.vo