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

16 files changed, 1837 insertions, 782 deletions

diff --git a/.gitignore b/.gitignore
index ba4811b8f..aee7ed659 100644
--- a/.gitignore
+++ b/.gitignore
@@ -93,6 +93,7 @@ doc/stdlib/index-list.html
 doc/RecTutorial/RecTutorial.html
 doc/RecTutorial/RecTutorial.pdf
 doc/RecTutorial/RecTutorial.ps
+dev/doc/naming-conventions.pdf
 _build
 plugins/*/*_mod.ml
 myocamlbuild_config.ml
diff --git a/CHANGES b/CHANGES
index 686b226ed..9998364d9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -121,7 +121,16 @@ Library
   available under the name nat_compare_alt.
 - Lemmas in library Relations and Reals have been homogenized a bit.
 - The implicit argument of Logic.eq is now maximally inserted, allowing
-  to simply write "eq" instead of "@eq _" in morphism signatures. 
+  to simply write "eq" instead of "@eq _" in morphism signatures.
+- Revision of the Sorting library:
+  - new mergesort of worst-case complexity O(n*ln(n)) made available in 
+    Mergesort.v;
+  - notion of permutation up to setoid from Permutation.v is deprecated and 
+    was moved to PermutSetoid.v;
+  - Permutation.v now contains the notion of permutation that was formerly in 
+    List.v;
+  - heapsort from Heap.v of worst-case complexity O(n*n) is deprecated;
+  - new file Sorted.v for some definitions of being sorted.
 
 Changes from V8.1 to V8.2
 =========================
diff --git a/LocallySorted.v b/LocallySorted.v
new file mode 100644
index 000000000..8f6264134
--- /dev/null
+++ b/LocallySorted.v
@@ -0,0 +1,44 @@
+Require Import List Program.Syntax.
+
+Variable A:Type.
+Variable le:A->A->Prop.
+Infix "<=" := le.
+
+(*
+if of_sumbool H then _ else _
+if H then _ else _
+*)
+
+Inductive locally_sorted : list A -> Prop :=
+| nil_locally_sorted : locally_sorted []
+| cons1_locally_sorted a : locally_sorted [a]
+| consn_locally_sorted a b l : locally_sorted (b::l) -> a <= b -> locally_sorted (a::b::l).
+
+Inductive lelist (a:A) : list A -> Prop :=
+    | nil_le : lelist a nil
+    | cons_le : forall (b:A) (l:list A), le a b -> lelist a (b :: l).
+
+Inductive sort : list A -> Prop :=
+    | nil_sort : sort nil
+    | cons_sort :
+      forall (a:A) (l:list A), sort l -> lelist a l -> sort (a :: l).
+
+Goal forall l, sort l -> locally_sorted l.
+induction l.
+  constructor.
+  inversion 1; subst.
+  destruct l; constructor.
+  apply IHl; trivial.
+  inversion H3; auto.
+Qed.
+
+Goal forall l, lelist
+
+Goal forall l, locally_sorted l -> sort l.
+induction 1; constructor.
+  constructor.
+  constructor.
+  assumption.
+  inversion IHlocally_sorted; subst.
+
+
diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex
index c9151d829..e7c8975bd 100644
--- a/dev/doc/naming-conventions.tex
+++ b/dev/doc/naming-conventions.tex
@@ -143,6 +143,47 @@ will have a named ended in \texttt{\_dec}. Idem for cotransitivity
 lemmas which are inherently computational that are ended in
 \texttt{\_cotrans}.
 
+\subsection{Inductive types constructor names}
+
+As a general rule, constructor names start with the name of the
+inductive type being defined as in \texttt{Inductive Z := Z0 : Z |
+  Zpos : Z -> Z | Zneg : Z -> Z} to the exception of very standard
+types like \texttt{bool}, \texttt{nat}, \texttt{list}...
+
+For inductive predicates, constructor names also start with the name
+of the notion being defined with one or more suffixes separated with
+\texttt{\_} for discriminating the different cases as e.g. in
+
+\begin{verbatim}
+Inductive even : nat -> Prop :=
+  | even_O : even 0
+  | even_S n : odd n -> even (S n)
+with odd : nat -> Prop :=
+  | odd_S n : even n -> odd (S n).
+\end{verbatim}
+
+As a general rule, inductive predicate names should be lowercase (to
+the exception of notions referring to a proper name, e.g. \texttt{Bezout})
+and multiple words must be separated by ``{\_}''.
+
+As an exception, when extending libraries whose general rule is that
+predicates names start with a capital letter, the convention of this
+library should be kept and the separation between multiple words is
+done by making the initial of each work a capital letter (if one of
+these words is a proper name, then a ``{\_}'' is added to emphasize
+that the capital letter is proper and not an application of the rule
+for marking the change of word).
+
+Inductive predicates that characterize the specification of a function
+should be named after the function it specifies followed by
+\texttt{\_spec} as in:
+
+\begin{verbatim}
+Inductive nth_spec : list A -> nat -> A -> Prop :=
+  | nth_spec_O a l : nth_spec (a :: l) 0 a
+  | nth_spec_S n a b l : nth_spec l n a -> nth_spec (b :: l) (S n) a.
+\end{verbatim}
+
 \section{Equational properties of operations}
 
 \subsection{General conventions}
@@ -205,12 +246,24 @@ If the conclusion is in the other way than listed below, add suffix
 \itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr}
 {forall x y:D, op (op' x y) = op' (op x) (op y)}
 
-\itemrule{Left distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_l}
+\itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr}
+{forall x y:D, op (op' x y) = op' (op x) (op y)}
+
+  Remark: For a non commutative operation with inversion of arguments, as in
+  \formula{forall x y z:D, op (op' x y) = op' (op y) (op y z)},
+  we may probably still call the property distributivity since there
+  is no ambiguity.
+
+  Example: \formula{forall n m : Z, -(n+m) = (-n)+(-m)}.
+
+  Example: \formula{forall l l' : list A, rev (l++l') = (rev l)++(rev l')}.
+
+\itemrule{Left extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_l}
 {forall x y:D, op (op' x y) = op' (op x) y}
 
-  Question: Call it left commutativity ??
+  Question: Call it left commutativity ?? left swap ?
 
-\itemrule{Right distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_r}
+\itemrule{Right extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_r}
 {forall x y:D, op (op' x y) = op' x (op y)}
 
 \itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent}
@@ -309,7 +362,7 @@ argument respectively and their return type identical.
 
 Remark: When the type are heterogeneous, only one extrusion law is possible and it can simply be named {Dop\_op'\_extrusion}.
 
-Example: \formula{app\_cons\_extrusion : forall a l l', (a :: l) ++ l' = a :: (l ++ l')}, in arithmetic
+Example: \formula{app\_cons\_extrusion : forall a l l', (a :: l) ++ l' = a :: (l ++ l')}.
 
 %======================================================================
 %\section{Properties of elements}
@@ -384,6 +437,12 @@ Example: \formula{app\_cons\_extrusion : forall a l l', (a :: l) ++ l' = a :: (l
  \name{Dop\_op'\_rel\_distr\_mon\_l} and
  \name{Dop\_op'\_rel\_distr\_anti\_l})?
 
+\itemrule{Commutativity of binary operator {\op} along (equivalence) relation {\rel} on domain {\D}}{Dop\_op'\_rel\_comm}
+{forall x y z:D, rel (op x y) (op y x)}
+
+  Example:
+\formula{forall l l':list A, Permutation (l++l') (l'++l)}
+
 \itemrule{Irreducibility of binary operator {\op} on domain {\D}}{Dop\_irreducible}
 {forall x y z:D, z = op x y -> z = x $\backslash/$ z = y}
 
@@ -472,7 +531,8 @@ Example: \formula{eq\_true\_neg: \~{} eq\_true b <-> eq\_true (negb b)}.
 \itemrule{Linearity of relation {\rel} on domain {\D}}{Drel\_trichotomy}
 {forall x y:D, \{rel x y\} + \{x = y\} + \{rel y x\}}
 
-  Questions: Or call it \name{Drel\_total}, or \name{Drel\_linear} use
+  Questions: Or call it \name{Drel\_total}, or \name{Drel\_linear}, or
+  \name{Drel\_connected}? Use
   $\backslash/$ ? or use a ternary sumbool, or a ternary disjunction,
   for nicer elimination.
 
diff --git a/merge-essai-type-classes.v b/merge-essai-type-classes.v
new file mode 100644
index 000000000..bc48ecbfe
--- /dev/null
+++ b/merge-essai-type-classes.v
@@ -0,0 +1,310 @@
+(************************************************************************)
+(*  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*)
+
+(* An implementation of mergesort *)
+
+(* Author: Hugo Herbelin *)
+
+Require Import List Program.Syntax.
+Open Scope bool_scope.
+
+Coercion eq_true : bool >-> Sortclass.
+
+Class BinaryCharacteristicFunction (A:Type) := {
+  rel_bool : A -> A -> bool
+}.
+
+(* Technical remark: one could have declared DecidableRelation as an instance of the following class
+and, with the associated notation, one would have obtained for free a notation
+"<=" for rel_bool that we could have used wherever it is possible instead of "<=?".
+However, the problem would then have been that "a <= b" and "a <=? b" in Prop would
+only have been equivalent module commutative cuts (due to the hidden projections)
+what Coq does not support.
+
+Class Relation (A:Type) := {
+  rel : A -> A -> Prop
+}.
+
+Instance dec_rel `(f: BinaryCharacteristicFunction A) : Relation A :=
+  let (f) := f in f.
+
+Infix "<=" := rel.
+*)
+
+Infix "<=?" := rel_bool (at level 35).
+
+Class DecidableTotalPreOrder `(le : BinaryCharacteristicFunction A) := {
+  le_bool_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1;
+  le_trans : forall a1 a2 a3, a1 <=? a2 -> a2 <=? a3 -> a1 <=? a3
+}.
+
+Section Sort.
+
+Context `(le : DecidableTotalPreOrder A).
+
+(** Provides support for tactics reflexivity, symmetry, transitive *)
+
+Require Import Equivalence.
+
+Program Instance equiv_reflexive A : Reflexive (@Permutation A)
+  := @Permutation_refl A.
+
+Program Instance equiv_symmetric : Symmetric (@Permutation A)
+  := @Permutation_sym A.
+
+Program Instance equiv_transitive : Transitive (@Permutation A)
+  := @Permutation_trans A.
+(*
+Module T (Import X:TotalOrder).
+*)
+Theorem le_refl : forall a, a <=? a.
+intro; destruct (le_bool_total a a); assumption.
+Qed.
+
+(*
+End T.
+
+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 [].
+
+Inductive sorted : list A -> Prop :=
+| nil_sort : sorted []
+| cons1_sort a : sorted [a]
+| consn_sort a b l : sorted (b::l) -> a <=? b -> sorted (a::b::l).
+
+Fixpoint sorted_stack stack :=
+  match stack with
+  | [] => True
+  | None :: stack' => sorted_stack stack'
+  | Some l :: stack' => sorted l /\ sorted_stack stack'
+  end.
+
+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 merge_sorted : 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.
+    inversion H; subst; clear 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')).
+    inversion H0; subst; clear 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.
+
+Hint Constructors Permutation.
+
+Theorem merge_permuted : 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 merge_list_to_stack_sorted : forall stack l,
+  sorted_stack stack -> sorted l -> sorted_stack (merge_list_to_stack stack l).
+Proof.
+  induction stack as [|[|]]; intros; simpl.
+    auto.
+    apply IHstack. destruct H as (_,H1). fold sorted_stack in H1. auto.  (* Pq déplie-t-il sorted_stack ici ? *)
+      apply merge_sorted; auto; destruct H; auto.
+      auto.
+Qed.
+
+Theorem merge_list_to_stack_permuted : 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_swap.
+      apply merge_permuted.
+    apply IHstack.
+    reflexivity.
+Qed.
+
+Theorem merge_stack_sorted : forall stack,
+  sorted_stack stack -> sorted (merge_stack stack).
+Proof.
+induction stack as [|[|]]; simpl; intros.
+  constructor; auto.
+  apply merge_sorted; tauto.
+  auto.
+Qed.
+
+Theorem merge_stack_permuted : 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 merge_permuted.
+  assumption.
+Qed.
+
+Theorem iter_merge_sorted : forall stack l,
+  sorted_stack stack -> sorted (iter_merge stack l).
+Proof.
+  intros stack l H; induction l in stack, H |- *; simpl.
+    auto using merge_stack_sorted.
+    assert (sorted [a]) by constructor.
+    auto using merge_list_to_stack_sorted.
+Qed.
+
+Theorem iter_merge_permuted : forall l stack,
+  Permutation (flatten_stack stack ++ l) (iter_merge stack l).
+Proof.
+  induction l; simpl; intros.
+    rewrite app_nil_r. apply merge_stack_permuted.
+    change (a::l) with ([a]++l).
+    rewrite app_assoc.
+    etransitivity.
+      apply Permutation_app_tail.
+    etransitivity.
+    apply Permutation_app_swap.
+    apply merge_list_to_stack_permuted.
+    apply IHl.
+Qed.
+
+Theorem sort_sorted : forall l, sorted (sort l).
+Proof.
+intro; apply iter_merge_sorted. constructor.
+Qed.
+
+Theorem sort_permuted : forall l, Permutation l (sort l).
+Proof.
+intro; apply (iter_merge_permuted l []).
+Qed.
+
+(* It remains to prove that "sort" returns a permutation *)
+(* of the original elements *)
+
+
+  Fixpoint le_bool x y :=
+    match x, y with
+    | 0, _ => true
+    | S x', 0 => false
+    | S x', S y' => le_bool x' y'
+    end.
+
+Instance le_bool_char : BinaryCharacteristicFunction nat := le_bool.
+
+Theorem nat_le_bool_total : forall a1 a2, le_bool a1 a2 \/ le_bool a2 a1.
+Proof.
+  induction a1; destruct a2; simpl; auto using is_eq_true.
+Qed.
+
+Instance nat_order : DecidableTotalPreOrder le_bool_char := {
+  le_bool_total := nat_le_bool_total
+}.
+
+Admitted.
+
+End Sort.
+Eval compute in sort [5;3;6;1;8;6;0].
+
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index d6b4c1354..2c89af4f1 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -26,20 +26,21 @@ Section Lists.
 
   Variable A : Type.
 
-  (** Head and tail        *)
-  Definition head (l:list A) :=
+  (** Head and tail *)
+
+  Definition hd (default:A) (l:list A) :=
+    match l with
+      | nil => default
+      | x :: _ => x
+    end.
+
+  Definition hd_error (l:list A) :=
     match l with
       | nil => error
       | x :: _ => value x
     end.
 
- Definition hd (default:A) (l:list A) :=
-   match l with
-     | nil => default
-     | x :: _ => x
-   end.
-
-  Definition tail (l:list A) : list A :=
+  Definition tl (l:list A) :=
     match l with
       | nil => nil
       | a :: m => m
@@ -54,6 +55,10 @@ Section Lists.
 
 End Lists.
 
+(* Keep these notations local to prevent conflicting notations *)
+Local Notation "[ ]" := nil : list_scope.
+Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
+
 (** ** Facts about lists *)
 
 Section Facts.
@@ -64,7 +69,7 @@ Section Facts.
   (** *** Genereric facts *)
 
   (** Discrimination *)
-  Theorem nil_cons : forall (x:A) (l:list A), nil <> x :: l.
+  Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l.
   Proof.
     intros; discriminate.
   Qed.
@@ -72,21 +77,21 @@ Section Facts.
 
   (** Destruction *)
 
-  Theorem destruct_list : forall l : list A, {x:A & {tl:list A | l = x::tl}}+{l = nil}.
+  Theorem destruct_list : forall l : list A, {x:A & {tl:list A | l = x::tl}}+{l = []}.
   Proof.
-    induction l as [|a tl].
+    induction l as [|a tail].
     right; reflexivity.
-    left; exists a; exists tl; reflexivity.
+    left; exists a, tail; reflexivity.
   Qed.
 
   (** *** Head and tail *)
 
-  Theorem head_nil : head (@nil A) = None.
+  Theorem hd_error_nil : hd_error (@nil A) = None.
   Proof.
     simpl; reflexivity.
   Qed.
 
-  Theorem head_cons : forall (l : list A) (x : A), head (x::l) = Some x.
+  Theorem hd_error_cons : forall (l : list A) (x : A), hd_error (x::l) = Some x.
   Proof.
     intros; simpl; reflexivity.
   Qed.
@@ -101,44 +106,44 @@ Section Facts.
 
   Theorem in_eq : forall (a:A) (l:list A), In a (a :: l).
   Proof.
-    simpl in |- *; auto.
+    simpl; auto.
   Qed.
 
   Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l).
   Proof.
-    simpl in |- *; auto.
+    simpl; auto.
   Qed.
 
-  Theorem in_nil : forall a:A, ~ In a nil.
+  Theorem in_nil : forall a:A, ~ In a [].
   Proof.
-    unfold not in |- *; intros a H; inversion_clear H.
+    unfold not; 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.
+  Theorem 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.
+  exists [], l; auto.
   destruct (IHl H) as (l1,(l2,H0)).
-  exists (a::l1); exists l2; simpl; f_equal; auto.
+  exists (a::l1), 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.
+  Lemma in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l.
   Proof.
     intros a b l H; inversion_clear H; auto.
   Qed.
 
   (** Decidability of [In] *)
-  Theorem In_dec :
+  Theorem in_dec :
     (forall x y:A, {x = y} + {x <> y}) ->
     forall (a:A) (l:list A), {In a l} + {~ In a l}.
   Proof.
     intro H; induction l as [| a0 l IHl].
     right; apply in_nil.
-    destruct (H a0 a); simpl in |- *; auto.
-    destruct IHl; simpl in |- *; auto.
-    right; unfold not in |- *; intros [Hc1| Hc2]; auto.
+    destruct (H a0 a); simpl; auto.
+    destruct IHl; simpl; auto.
+    right; unfold not; intros [Hc1| Hc2]; auto.
   Defined.
 
 
@@ -147,29 +152,29 @@ Section Facts.
   (**************************)
 
   (** Discrimination *)
-  Theorem app_cons_not_nil : forall (x y:list A) (a:A), nil <> x ++ a :: y.
+  Theorem app_cons_not_nil : forall (x y:list A) (a:A), [] <> x ++ a :: y.
   Proof.
-    unfold not in |- *.
-    destruct x as [| a l]; simpl in |- *; intros.
+    unfold not.
+    destruct x as [| a l]; simpl; intros.
     discriminate H.
     discriminate H.
   Qed.
 
 
   (** Concat with [nil] *)
-  Theorem app_nil_l : forall l:list A, nil ++ l = l.
+  Theorem app_nil_l : forall l:list A, [] ++ l = l.
   Proof.
     reflexivity.
   Qed.
 
-  Theorem app_nil_r : forall l:list A, l ++ nil = l.
+  Theorem app_nil_r : forall l:list A, l ++ [] = l.
   Proof.
     induction l; simpl; f_equal; auto.
   Qed.
 
   (* begin hide *)
-  (* Compatibility *)
-  Theorem app_nil_end : forall (l:list A), l = l ++ nil.
+  (* Deprecated *)
+  Theorem app_nil_end : forall (l:list A), l = l ++ [].
   Proof. symmetry; apply app_nil_r. Qed.
   (* end hide *)
 
@@ -179,11 +184,14 @@ Section Facts.
     intros l m n; induction l; simpl; f_equal; auto.
   Qed.
 
+  (* begin hide *)
+  (* Deprecated *)
   Theorem app_assoc_reverse : forall l m n:list A, (l ++ m) ++ n = l ++ m ++ n.
   Proof.
      auto using app_assoc.
   Qed.
   Hint Resolve app_assoc_reverse.
+  (* end hide *)
 
   (** [app] commutes with [cons] *)
   Theorem app_comm_cons : forall (x y:list A) (a:A), a :: (x ++ y) = (a :: x) ++ y.
@@ -193,19 +201,19 @@ Section Facts.
 
   (** Facts deduced from the result of a concatenation *)
 
-  Theorem app_eq_nil : forall l l':list A, l ++ l' = nil -> l = nil /\ l' = nil.
+  Theorem app_eq_nil : forall l l':list A, l ++ l' = [] -> l = [] /\ l' = [].
   Proof.
-    destruct l as [| x l]; destruct l' as [| y l']; simpl in |- *; auto.
+    destruct l as [| x l]; destruct l' as [| y l']; simpl; auto.
     intro; discriminate.
     intros H; discriminate H.
   Qed.
 
   Theorem app_eq_unit :
     forall (x y:list A) (a:A),
-      x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil.
+      x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = [].
   Proof.
     destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ];
-      simpl in |- *.
+      simpl.
     intros a H; discriminate H.
     left; split; auto.
     right; split; auto.
@@ -215,18 +223,18 @@ Section Facts.
     intros.
     injection H.
     intro.
-    cut (nil = l ++ a0 :: l0); auto.
+    cut ([] = l ++ a0 :: l0); auto.
     intro.
     generalize (app_cons_not_nil _ _ _ H1); intro.
     elim H2.
   Qed.
 
   Lemma app_inj_tail :
-    forall (x y:list A) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b.
+    forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b.
   Proof.
     induction x as [| x l IHl];
       [ destruct y as [| a l] | destruct y as [| a l0] ];
-      simpl in |- *; auto.
+      simpl; auto.
     intros a b H.
     injection H.
     auto.
@@ -235,7 +243,7 @@ Section Facts.
     generalize (app_cons_not_nil _ _ _ H0); destruct 1.
     intros a b H.
     injection H; intros.
-    cut (nil = l ++ a :: nil); auto.
+    cut ([] = l ++ [a]); auto.
     intro.
     generalize (app_cons_not_nil _ _ _ H2); destruct 1.
     intros a0 b H.
@@ -256,7 +264,7 @@ Section Facts.
   Lemma in_app_or : forall (l m:list A) (a:A), In a (l ++ m) -> In a l \/ In a m.
   Proof.
     intros l m a.
-    elim l; simpl in |- *; auto.
+    elim l; simpl; auto.
     intros a0 y H H0.
     now_show ((a0 = a \/ In a y) \/ In a m).
     elim H0; auto.
@@ -268,7 +276,7 @@ Section Facts.
   Lemma in_or_app : forall (l m:list A) (a:A), In a l \/ In a m -> In a (l ++ m).
   Proof.
     intros l m a.
-    elim l; simpl in |- *; intro H.
+    elim l; simpl; intro H.
     now_show (In a m).
     elim H; auto; intro H0.
     now_show (In a m).
@@ -287,13 +295,13 @@ Section Facts.
   Qed.
 
   Lemma app_inv_head:
-   forall l l1 l2 : list A, l ++ l1 = l ++ l2 ->  l1 = l2.
+   forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2.
   Proof.
     induction l; simpl; auto; injection 1; auto.
   Qed.
 
   Lemma app_inv_tail:
-    forall l l1 l2 : list A, l1 ++ l = l2 ++ l ->  l1 = l2.
+    forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2.
   Proof.
     intros l l1 l2; revert l1 l2 l.
     induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2];
@@ -333,7 +341,7 @@ Section Elts.
     match n, l with
       | O, x :: l' => x
       | O, other => default
-      | S m, nil => default
+      | S m, [] => default
       | S m, x :: t => nth m t default
     end.
 
@@ -341,7 +349,7 @@ Section Elts.
     match n, l with
       | O, x :: l' => true
       | O, other => false
-      | S m, nil => false
+      | S m, [] => false
       | S m, x :: t => nth_ok m t default
     end.
 
@@ -351,7 +359,7 @@ Section Elts.
   Proof.
     intros n l d; generalize n; induction l; intro n0.
     right; case n0; trivial.
-    case n0; simpl in |- *.
+    case n0; simpl.
     auto.
     intro n1; elim (IHl n1); auto.
   Qed.
@@ -360,7 +368,7 @@ Section Elts.
     forall (n:nat) (l:list A) (d a:A),
       In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l).
   Proof.
-    simpl in |- *; auto.
+    simpl; auto.
   Qed.
 
   Fixpoint nth_error (l:list A) (n:nat) {struct n} : Exc A :=
@@ -386,9 +394,9 @@ Section Elts.
     forall (n:nat) (l:list A) (d:A), n < length l -> In (nth n l d) l.
 
   Proof.
-    unfold lt in |- *; induction n as [| n hn]; simpl in |- *.
-    destruct l; simpl in |- *; [ inversion 2 | auto ].
-    destruct l as [| a l hl]; simpl in |- *.
+    unfold lt; induction n as [| n hn]; simpl.
+    destruct l; simpl; [ inversion 2 | auto ].
+    destruct l as [| a l hl]; simpl.
     inversion 2.
     intros d ie; right; apply hn; auto with arith.
   Qed.
@@ -441,26 +449,22 @@ Section Elts.
   (** ** Remove    *)
   (*****************)
 
-  Section Remove.
-
-    Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
+  Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
 
-    Fixpoint remove (x : A) (l : list A) : list A :=
-      match l with
-	| nil => nil
-	| y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl)
-      end.
-
-    Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l).
-    Proof.
-      induction l as [|x l]; auto.
-      intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx].
-      apply IHl.
-      unfold not; intro HF; simpl in HF; destruct HF; auto.
-      apply (IHl y); assumption.
-    Qed.
+  Fixpoint remove (x : A) (l : list A) : list A :=
+    match l with
+      | [] => []
+      | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl)
+    end.
 
-  End Remove.
+  Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l).
+  Proof.
+    induction l as [|x l]; auto.
+    intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx].
+    apply IHl.
+    unfold not; intro HF; simpl in HF; destruct HF; auto.
+    apply (IHl y); assumption.
+  Qed.
 
 
 (******************************)
@@ -472,8 +476,8 @@ Section Elts.
 
   Fixpoint last (l:list A) (d:A) : A :=
   match l with
-    | nil => d
-    | a :: nil => a
+    | [] => d
+    | [a] => a
     | a :: l => last l d
   end.
 
@@ -481,13 +485,13 @@ Section Elts.
 
   Fixpoint removelast (l:list A) : list A :=
     match l with
-      | nil =>  nil
-      | a :: nil => nil
+      | [] =>  []
+      | [a] => []
       | a :: l => a :: removelast l
     end.
 
   Lemma app_removelast_last :
-    forall l d, l<>nil -> l = removelast l ++ (last l d :: nil).
+    forall l d, l <> [] -> l = removelast l ++ [last l d].
   Proof.
     induction l.
     destruct 1; auto.
@@ -497,25 +501,25 @@ Section Elts.
   Qed.
 
   Lemma exists_last :
-    forall l, l<>nil -> { l' : (list A) & { a : A | l = l'++a::nil}}.
+    forall l, l <> [] -> { l' : (list A) & { a : A | l = l' ++ [a]}}.
   Proof.
     induction l.
     destruct 1; auto.
     intros _.
     destruct l.
-    exists (@nil A); exists a; auto.
+    exists [], a; auto.
     destruct IHl as [l' (a',H)]; try discriminate.
     rewrite H.
-    exists (a::l'); exists a'; auto.
+    exists (a::l'), a'; auto.
   Qed.
 
   Lemma removelast_app :
-    forall l l', l' <> nil -> removelast (l++l') = l ++ removelast l'.
+    forall l l', l' <> [] -> removelast (l++l') = l ++ removelast l'.
   Proof.
     induction l.
     simpl; auto.
     simpl; intros.
-    assert (l++l' <> nil).
+    assert (l++l' <> []).
     destruct l.
     simpl; auto.
     simpl; discriminate.
@@ -528,14 +532,12 @@ Section Elts.
   (** ** Counting occurences of a element *)
   (****************************************)
 
-  Hypotheses eqA_dec : forall x y : A, {x = y}+{x <> y}.
-
   Fixpoint count_occ (l : list A) (x : A) : nat :=
     match l with
-      | nil => 0
+      | [] => 0
       | y :: tl =>
 	let n := count_occ tl x in
-	  if eqA_dec y x then S n else n
+	  if eq_dec y x then S n else n
     end.
 
   (** Compatibility of count_occ with operations on list *)
@@ -543,12 +545,12 @@ Section Elts.
   Proof.
     induction l as [|y l].
     simpl; intros; split; [destruct 1 | apply gt_irrefl].
-    simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq].
+    simpl. intro x; destruct (eq_dec y x) as [Heq|Hneq].
     rewrite Heq; intuition.
     pose (IHl x). intuition.
   Qed.
 
-  Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = nil.
+  Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = [].
   Proof.
     split.
     (* Case -> *)
@@ -558,14 +560,14 @@ Section Elts.
     elim (O_S (count_occ l x)).
     apply sym_eq.
     generalize (H x).
-    simpl. destruct (eqA_dec x x) as [|HF].
+    simpl. destruct (eq_dec x x) as [|HF].
     trivial.
     elim HF; reflexivity.
     (* Case <- *)
     intro H; rewrite H; simpl; reflexivity.
   Qed.
 
-  Lemma count_occ_nil : forall (x : A), count_occ nil x = 0.
+  Lemma count_occ_nil : forall (x : A), count_occ [] x = 0.
   Proof.
     intro x; simpl; reflexivity.
   Qed.
@@ -573,13 +575,13 @@ Section Elts.
   Lemma count_occ_cons_eq : forall (l : list A) (x y : A), x = y -> count_occ (x::l) y = S (count_occ l y).
   Proof.
     intros l x y H; simpl.
-    destruct (eqA_dec x y); [reflexivity | contradiction].
+    destruct (eq_dec x y); [reflexivity | contradiction].
   Qed.
 
   Lemma count_occ_cons_neq : forall (l : list A) (x y : A), x <> y -> count_occ (x::l) y = count_occ l y.
   Proof.
     intros l x y H; simpl.
-    destruct (eqA_dec x y); [contradiction | reflexivity].
+    destruct (eq_dec x y); [contradiction | reflexivity].
   Qed.
 
 End Elts.
@@ -600,38 +602,38 @@ Section ListOps.
 
   Fixpoint rev (l:list A) : list A :=
     match l with
-      | nil => nil
-      | x :: l' => rev l' ++ x :: nil
+      | [] => []
+      | x :: l' => rev l' ++ [x]
     end.
 
-  Lemma distr_rev : forall x y:list A, rev (x ++ y) = rev y ++ rev x.
+  Lemma rev_app_distr : forall x y:list A, rev (x ++ y) = rev y ++ rev x.
   Proof.
     induction x as [| a l IHl].
     destruct y as [| a l].
-    simpl in |- *.
+    simpl.
     auto.
 
-    simpl in |- *.
+    simpl.
     rewrite app_nil_r; auto.
 
     intro y.
-    simpl in |- *.
+    simpl.
     rewrite (IHl y).
     rewrite app_assoc; trivial.
   Qed.
 
-  Remark rev_unit : forall (l:list A) (a:A), rev (l ++ a :: nil) = a :: rev l.
+  Remark rev_unit : forall (l:list A) (a:A), rev (l ++ [a]) = a :: rev l.
   Proof.
     intros.
-    apply (distr_rev l (a :: nil)); simpl in |- *; auto.
+    apply (rev_app_distr l [a]); simpl; auto.
   Qed.
 
   Lemma rev_involutive : forall l:list A, rev (rev l) = l.
   Proof.
     induction l as [| a l IHl].
-    simpl in |- *; auto.
+    simpl; auto.
 
-    simpl in |- *.
+    simpl.
     rewrite (rev_unit (rev l) a).
     rewrite IHl; auto.
   Qed.
@@ -639,7 +641,7 @@ Section ListOps.
 
   (** Compatibility with other operations *)
 
-  Lemma In_rev : forall l x, In x l <-> In x (rev l).
+  Lemma in_rev : forall l x, In x l <-> In x (rev l).
   Proof.
     induction l.
     simpl; intuition.
@@ -688,23 +690,19 @@ Section ListOps.
 
   Fixpoint rev_append (l l': list A) : list A :=
     match l with
-      | nil => l'
+      | [] => l'
       | a::l => rev_append l (a::l')
     end.
 
-  Definition rev' l : list A := rev_append l nil.
-
-  Notation rev_acc := rev_append (only parsing).
+  Definition rev' l : list A := rev_append l [].
 
-  Lemma rev_append_rev : forall l l', rev_acc l l' = rev l ++ l'.
+  Lemma rev_append_rev : forall l l', rev_append l l' = rev l ++ l'.
   Proof.
     induction l; simpl; auto; intros.
     rewrite <- app_assoc; firstorder.
   Qed.
 
-  Notation rev_acc_rev := rev_append_rev (only parsing).
-
-  Lemma rev_alt : forall l, rev l = rev_append l nil.
+  Lemma rev_alt : forall l, rev l = rev_append l [].
   Proof.
     intros; rewrite rev_append_rev.
     rewrite app_nil_r; trivial.
@@ -717,22 +715,19 @@ Section ListOps.
 
   Section Reverse_Induction.
 
-    Unset Implicit Arguments.
-
     Lemma rev_list_ind :
       forall P:list A-> Prop,
-	P nil ->
+	P [] ->
 	(forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) ->
 	forall l:list A, P (rev l).
     Proof.
       induction l; auto.
     Qed.
-    Set Implicit Arguments.
 
     Theorem rev_ind :
       forall P:list A -> Prop,
-	P nil ->
-	(forall (x:A) (l:list A), P l -> P (l ++ x :: nil)) -> forall l:list A, P l.
+	P [] ->
+	(forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l.
     Proof.
       intros.
       generalize (rev_involutive l).
@@ -740,7 +735,7 @@ Section ListOps.
       apply (rev_list_ind P).
       auto.
 
-      simpl in |- *.
+      simpl.
       intros.
       apply (H0 a (rev l0)).
       auto.
@@ -748,235 +743,11 @@ Section ListOps.
 
   End Reverse_Induction.
 
-
-  (*********************************************************************)
-  (** ** List permutations as a composition of adjacent transpositions *)
-  (*********************************************************************)
-
-  Section Permutation.
-
-    Inductive Permutation : list A -> list A -> Prop :=
-      | perm_nil: Permutation nil nil
-      | perm_skip: forall (x:A) (l l':list A), Permutation l l' -> Permutation (cons x l) (cons x l')
-      | perm_swap: forall (x y:A) (l:list A), Permutation (cons y (cons x l)) (cons x (cons y l))
-      | perm_trans: forall (l l' l'':list A), Permutation l l' -> Permutation l' l'' -> Permutation l l''.
-
-    Hint Constructors Permutation.
-
-  (** Some facts about [Permutation] *)
-
-    Theorem Permutation_nil : forall (l : list A), Permutation nil l -> l = nil.
-    Proof.
-      intros l HF.
-      set (m:=@nil A) in HF; assert (m = nil); [reflexivity|idtac]; clearbody m.
-      induction HF; try elim (nil_cons (sym_eq H)); auto.
-    Qed.
-
-    Theorem Permutation_nil_cons : forall (l : list A) (x : A), ~ Permutation nil (x::l).
-    Proof.
-      unfold not; intros l x HF.
-      elim (@nil_cons A x l). apply sym_eq. exact (Permutation_nil HF).
-    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.
-
-    Hint Resolve Permutation_refl Permutation_sym Permutation_trans.
-
-  (** 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.
-
-    Theorem Permutation_app_swap : 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.
-      simpl; apply Permutation_trans with (l' := x :: y :: l' ++ l).
-      constructor; rewrite app_comm_cons; apply IHl.
-      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.
-      intros l l' Hperm; induction Hperm; simpl; auto.
-      apply trans_eq with (y:= (length l')); trivial.
-    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::nil)++rev l).
-      simpl; auto.
-      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 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 (@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_r; auto.
-    intros.
-    apply IHl.
-    apply Permutation_app_inv with a; auto.
-    Qed.
-
-  End Permutation.
-
-
   (***********************************)
   (** ** Decidable equality on lists *)
   (***********************************)
 
-  Hypotheses eqA_dec : forall (x y : A), {x = y}+{x <> y}.
+  Hypothesis eq_dec : forall (x y : A), {x = y}+{x <> y}.
 
   Lemma list_eq_dec :
     forall l l':list A, {l = l'} + {l <> l'}.
@@ -985,7 +756,7 @@ Section ListOps.
     left; trivial.
     right; apply nil_cons.
     right; unfold not; intro HF; apply (nil_cons (sym_eq HF)).
-    destruct (eqA_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql'];
+    destruct (eq_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql'];
       try (right; unfold not; intro HF; injection HF; intros; contradiction).
     rewrite xeqy; rewrite leql'; left; trivial.
   Qed.
@@ -1054,14 +825,6 @@ 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] *)
 
   Definition flat_map (f:A -> list B) :=
@@ -1193,10 +956,10 @@ End Fold_Right_Recursor.
   Proof.
     destruct l as [| a l].
     reflexivity.
-    simpl in |- *.
+    simpl.
     rewrite <- H0.
     generalize a0 a.
-    induction l as [| a3 l IHl]; simpl in |- *.
+    induction l as [| a3 l IHl]; simpl.
     trivial.
     intros.
     rewrite H.
@@ -1480,8 +1243,8 @@ End Fold_Right_Recursor.
 	In y l -> In (x, y) (map (fun y0:B => (x, y0)) l).
     Proof.
       induction l;
-	[ simpl in |- *; auto
-	  | simpl in |- *; destruct 1 as [H1| ];
+	[ simpl; auto
+	  | simpl; destruct 1 as [H1| ];
 	    [ left; rewrite H1; trivial | right; auto ] ].
     Qed.
 
@@ -1490,8 +1253,8 @@ End Fold_Right_Recursor.
 	In x l -> In y l' -> In (x, y) (list_prod l l').
     Proof.
       induction l;
-	[ simpl in |- *; tauto
-	  | simpl in |- *; intros; apply in_or_app; destruct H;
+	[ simpl; tauto
+	  | simpl; intros; apply in_or_app; destruct H;
 	    [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ].
     Qed.
 
@@ -1524,9 +1287,9 @@ End Fold_Right_Recursor.
 
 
 
-(***************************************)
-(** * Miscelenous operations on lists  *)
-(***************************************)
+(*****************************************)
+(** * Miscellaneous operations on lists  *)
+(*****************************************)
 
 
 
@@ -1544,29 +1307,29 @@ Section length_order.
 
   Lemma lel_refl : lel l l.
   Proof.
-    unfold lel in |- *; auto with arith.
+    unfold lel; auto with arith.
   Qed.
 
   Lemma lel_trans : lel l m -> lel m n -> lel l n.
   Proof.
-    unfold lel in |- *; intros.
+    unfold lel; intros.
     now_show (length l <= length n).
     apply le_trans with (length m); auto with arith.
   Qed.
 
   Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m).
   Proof.
-    unfold lel in |- *; simpl in |- *; auto with arith.
+    unfold lel; simpl; auto with arith.
   Qed.
 
   Lemma lel_cons : lel l m -> lel l (b :: m).
   Proof.
-    unfold lel in |- *; simpl in |- *; auto with arith.
+    unfold lel; simpl; auto with arith.
   Qed.
 
   Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m.
   Proof.
-    unfold lel in |- *; simpl in |- *; auto with arith.
+    unfold lel; simpl; auto with arith.
   Qed.
 
   Lemma lel_nil : forall l':list A, lel l' nil -> nil = l'.
@@ -1625,7 +1388,7 @@ Section SetIncl.
   Lemma incl_cons :
     forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m.
   Proof.
-    unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1.
+    unfold incl; simpl; intros a l m H H0 a0 H1.
     now_show (In a0 m).
     elim H1.
     now_show (a = a0 -> In a0 m).
@@ -1639,7 +1402,7 @@ Section SetIncl.
 
   Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n.
   Proof.
-    unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
+    unfold incl; simpl; intros l m n H H0 a H1.
     now_show (In a n).
     elim (in_app_or _ _ _ H1); auto.
   Qed.
@@ -1762,34 +1525,6 @@ Section ReDun.
   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.
 
 
@@ -1872,14 +1607,63 @@ induction 1; firstorder; subst; auto.
 induction l; firstorder.
 Qed.
 
+Lemma Forall_inv : forall A P (a:A) l, Forall P (a :: l) -> P a.
+Proof.
+intros; inversion H; trivial.
+Defined.
+
+Lemma Forall_rect : forall A (P:A->Prop) (Q : list A -> Type),
+     Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall P l -> Q l.
+Proof.
+intros A P Q H H'; induction l; intro; [|eapply H', Forall_inv]; eassumption.
+Defined.
+
+Lemma Forall_impl : forall A (P Q : A -> Prop), (forall a, P a -> Q a) ->
+  forall l, Forall P l -> Forall Q l.
+Proof.
+  intros A P Q Himp l H.
+  induction H; firstorder.
+Qed.
+
 (** [Forall2]: stating that elements of two lists are pairwise related. *)
 
-Inductive Forall2 {A B} (R:A->B->Prop) : list A -> list B -> Prop :=
- | Forall2_nil : Forall2 R nil nil
+Inductive Forall2 A B (R:A->B->Prop) : list A -> list B -> Prop :=
+ | Forall2_nil : Forall2 R [] []
  | Forall2_cons : forall x y l l',
     R x y -> Forall2 R l l' -> Forall2 R (x::l) (y::l').
 Hint Constructors Forall2.
 
+Theorem Forall2_refl : forall A B (R:A->B->Prop), Forall2 R [] [].
+Proof. exact Forall2_nil. Qed.
+
+Theorem Forall2_app_inv_l : forall A B (R:A->B->Prop) l1 l2 l',
+  Forall2 R (l1 ++ l2) l' ->
+  exists l1', exists l2', Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l' = l1' ++ l2'.
+Proof.
+  induction l1; intros.
+    exists [], l'; auto.
+    simpl in H; inversion H; subst; clear H.
+    apply IHl1 in H4 as (l1' & l2' & Hl1 & Hl2 & ->).
+    exists (y::l1'), l2'; simpl; auto.
+Qed.
+
+Theorem Forall2_app_inv_r : forall A B (R:A->B->Prop) l1' l2' l,
+  Forall2 R l (l1' ++ l2') ->
+  exists l1, exists l2, Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l = l1 ++ l2.
+Proof.
+  induction l1'; intros.
+    exists [], l; auto.
+    simpl in H; inversion H; subst; clear H.
+    apply IHl1' in H4 as (l1 & l2 & Hl1 & Hl2 & ->).
+    exists (x::l1), l2; simpl; auto.
+Qed.
+
+Theorem Forall2_app : forall A B (R:A->B->Prop) l1 l2 l1' l2',
+  Forall2 R l1 l1' -> Forall2 R l2 l2' -> Forall2 R (l1 ++ l2) (l1' ++ l2').
+Proof.
+  intros. induction l1 in l1', H, H0 |- *; inversion H; subst; simpl; auto.
+Qed.
+
 (** [ForallPairs] : specifies that a certain relation should
     always hold when inspecting all possible pairs of elements of a list. *)
 
@@ -1928,7 +1712,6 @@ Proof.
  destruct (ForallOrdPairs_In Hl _ _ Hx Hy); subst; intuition.
 Qed.
 
-
 (** * Inversion of predicates over lists based on head symbol *)
 
 Ltac is_list_constr c :=
@@ -1978,8 +1761,19 @@ Notation cons := cons (only parsing).
 Notation length := length (only parsing).
 Notation app := app (only parsing).
 (* Compatibility Names *)
+Notation tail := tl (only parsing).
+Notation head := hd_error (only parsing).
+Notation head_nil := hd_error_nil (only parsing).
+Notation head_cons := hd_error_cons (only parsing).
 Notation ass_app := app_assoc (only parsing).
 Notation app_ass := app_assoc_reverse (only parsing).
+Notation In_split := in_split (only parsing).
+Notation In_rev := in_rev (only parsing).
+Notation In_dec := in_dec (only parsing).
+Notation distr_rev := rev_app_distr (only parsing).
+Notation rev_acc := rev_append (only parsing).
+Notation rev_acc_rev := rev_append_rev (only parsing).
+Notation AllS := Forall (only parsing). (* was formerly in TheoryList *)
+
 Hint Resolve app_nil_end : datatypes v62.
 (* end hide *)
-
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index da3018a48..7ed9c519b 100644
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -12,6 +12,10 @@
 
 Require Export List.
 Set Implicit Arguments.
+
+Local Notation "[ ]" := nil (at level 0).
+Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0).
+
 Section Lists.
 
 Variable A : Type.
@@ -23,11 +27,13 @@ Variable A : Type.
 Definition Isnil (l:list A) : Prop := nil = l.
 
 Lemma Isnil_nil : Isnil nil.
+Proof.
 red in |- *; auto.
 Qed.
 Hint Resolve Isnil_nil.
 
 Lemma not_Isnil_cons : forall (a:A) (l:list A), ~ Isnil (a :: l).
+Proof.
 unfold Isnil in |- *.
 intros; discriminate.
 Qed.
@@ -35,6 +41,7 @@ Qed.
 Hint Resolve Isnil_nil not_Isnil_cons.
 
 Lemma Isnil_dec : forall l:list A, {Isnil l} + {~ Isnil l}.
+Proof.
 intro l; case l; auto.
 (*
 Realizer (fun l => match l with
@@ -50,6 +57,7 @@ Qed.
 
 Lemma Uncons :
  forall l:list A, {a : A &  {m : list A | a :: m = l}} + {Isnil l}.
+Proof.
 intro l; case l.
 auto.
 intros a m; intros; left; exists a; exists m; reflexivity.
@@ -67,6 +75,7 @@ Qed.
 
 Lemma Hd :
  forall l:list A, {a : A |  exists m : list A, a :: m = l} + {Isnil l}.
+Proof.
 intro l; case l.
 auto.
 intros a m; intros; left; exists a; exists m; reflexivity.
@@ -81,6 +90,7 @@ Qed.
 Lemma Tl :
  forall l:list A,
    {m : list A | (exists a : A, a :: m = l) \/ Isnil l /\ Isnil m}.
+Proof.
 intro l; case l.
 exists (nil (A:=A)); auto.
 intros a m; intros; exists m; left; exists a; reflexivity.
@@ -105,6 +115,7 @@ Fixpoint Length_l (l:list A) (n:nat) : nat :=
 
 (* A tail recursive version *)
 Lemma Length_l_pf : forall (l:list A) (n:nat), {m : nat | n + length l = m}.
+Proof.
 induction l as [| a m lrec].
 intro n; exists n; simpl in |- *; auto.
 intro n; elim (lrec (S n)); simpl in |- *; intros.
@@ -115,6 +126,7 @@ Realizer Length_l.
 Qed.
 
 Lemma Length : forall l:list A, {m : nat | length l = m}.
+Proof.
 intro l. apply (Length_l_pf l 0).
 (*
 Realizer (fun l -> Length_l_pf l O).
@@ -139,11 +151,6 @@ elim l;
 intros; elim H; auto.
 Qed.
 
-Inductive AllS (P:A -> Prop) : list A -> Prop :=
-  | allS_nil : AllS P nil
-  | allS_cons : forall (a:A) (l:list A), P a -> AllS P l -> AllS P (a :: l).
-Hint Resolve allS_nil allS_cons.
-
 Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}.
 
 Fixpoint mem (a:A) (l:list A) : bool :=
@@ -154,7 +161,7 @@ Fixpoint mem (a:A) (l:list A) : bool :=
 
 Hint Unfold In.
 Lemma Mem : forall (a:A) (l:list A), {In a l} + {AllS (fun b:A => b <> a) l}.
-intros a l.
+Proof.
 induction l.
 auto.
 elim (eqA_dec a a0).
@@ -188,16 +195,19 @@ Hint Resolve fst_nth_O fst_nth_S.
 
 Lemma fst_nth_nth :
  forall (l:list A) (n:nat) (a:A), fst_nth_spec l n a -> nth_spec l n a.
+Proof.
 induction 1; auto.
 Qed.
 Hint Immediate fst_nth_nth.
 
 Lemma nth_lt_O : forall (l:list A) (n:nat) (a:A), nth_spec l n a -> 0 < n.
+Proof.
 induction 1; auto.
 Qed.
 
 Lemma nth_le_length :
  forall (l:list A) (n:nat) (a:A), nth_spec l n a -> n <= length l.
+Proof.
 induction 1; simpl in |- *; auto with arith.
 Qed.
 
@@ -211,6 +221,7 @@ Fixpoint Nth_func (l:list A) (n:nat) : Exc A :=
 Lemma Nth :
  forall (l:list A) (n:nat),
    {a : A | nth_spec l n a} + {n = 0 \/ length l < n}.
+Proof.
 induction l as [| a l IHl].
 intro n; case n; simpl in |- *; auto with arith.
 intro n; destruct n as [| [| n1]]; simpl in |- *; auto.
@@ -227,6 +238,7 @@ Qed.
 
 Lemma Item :
  forall (l:list A) (n:nat), {a : A | nth_spec l (S n) a} + {length l <= n}.
+Proof.
 intros l n; case (Nth l (S n)); intro.
 case s; intro a; left; exists a; auto.
 right; case o; intro.
@@ -246,6 +258,7 @@ Fixpoint index_p (a:A) (l:list A) : nat -> Exc nat :=
 Lemma Index_p :
  forall (a:A) (l:list A) (p:nat),
    {n : nat | fst_nth_spec l (S n - p) a} + {AllS (fun b:A => a <> b) l}.
+Proof.
 induction l as [| b m irec].
 auto.
 intro p.
@@ -264,6 +277,7 @@ Lemma Index :
  forall (a:A) (l:list A),
    {n : nat | fst_nth_spec l n a} + {AllS (fun b:A => a <> b) l}.
 
+Proof.
 intros a l; case (Index_p a l 1); auto.
 intros [n P]; left; exists n; auto.
 rewrite (minus_n_O n); trivial.
@@ -287,20 +301,24 @@ Definition InR_inv (l:list A) :=
   end.
 
 Lemma InR_INV : forall l:list A, InR l -> InR_inv l.
+Proof.
 induction 1; simpl in |- *; auto.
 Qed.
 
 Lemma InR_cons_inv : forall (a:A) (l:list A), InR (a :: l) -> R a \/ InR l.
+Proof.
 intros a l H; exact (InR_INV H).
 Qed.
 
 Lemma InR_or_app : forall l m:list A, InR l \/ InR m -> InR (l ++ m).
+Proof.
 intros l m [| ].
 induction 1; simpl in |- *; auto.
 intro. induction l; simpl in |- *; auto.
 Qed.
 
 Lemma InR_app_or : forall l m:list A, InR (l ++ m) -> InR l \/ InR m.
+Proof.
 intros l m; elim l; simpl in |- *; auto.
 intros b l' Hrec IAc; elim (InR_cons_inv IAc); auto.
 intros; elim Hrec; auto.
@@ -315,6 +333,7 @@ Fixpoint find (l:list A) : Exc A :=
   end.
 
 Lemma Find : forall l:list A, {a : A | In a l &  R a} + {AllS P l}.
+Proof.
 induction l as [| a m [[b H1 H2]| H]]; auto.
 left; exists b; auto.
 destruct (RS_dec a).
@@ -342,6 +361,7 @@ Fixpoint try_find (l:list A) : Exc B :=
 
 Lemma Try_find :
  forall l:list A, {c : B |  exists2 a : A, In a l & T a c} + {AllS P l}.
+Proof.
 induction l as [| a m [[b H1]| H]].
 auto.
 left; exists b; destruct H1 as [a' H2 H3]; exists a'; auto.
@@ -383,6 +403,7 @@ Hint Resolve allS_assoc_nil allS_assoc_cons.
 
 Lemma Assoc :
  forall (a:A) (l:list (A * B)), B + {AllS_assoc (fun a':A => a <> a') l}.
+Proof.
 induction l as [| [a' b] m assrec]. auto.
 destruct (eqA_dec a a').
 left; exact b.
@@ -398,6 +419,5 @@ End Assoc_sec.
 
 End Lists.
 
-Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons:
-  datatypes.
+Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons : datatypes.
 Hint Immediate fst_nth_nth: datatypes.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 75b9f2efa..7216ae335 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -10,7 +10,7 @@
 
 (* G. Huet 1-9-95 *)
 
-Require Import Permut.
+Require Import Permut Setoid.
 
 Set Implicit Arguments.
 
@@ -18,6 +18,7 @@ Section multiset_defs.
 
   Variable A : Type.
   Variable eqA : A -> A -> Prop.
+  Hypothesis eqA_equiv : Equivalence eqA.
   Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
   Inductive multiset : Type :=
@@ -167,6 +168,15 @@ Section multiset_defs.
     apply multiset_twist2.
   Qed.
 
+  (** SingletonBag *)
+
+  Lemma meq_singleton : forall a a',
+    eqA a a' -> meq (SingletonBag a) (SingletonBag a').
+  Proof.
+    intros; red; simpl; intro a0.
+    destruct (Aeq_dec a a0) as [Ha|Ha]; rewrite H in Ha;
+      decide (Aeq_dec a' a0) with Ha; reflexivity.
+  Qed.
 
 (*i theory of minter to do similarly
 Require Min.
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