Imported Upstream version 8.1~gammaupstream/8.1.gamma

5 files changed, 811 insertions, 801 deletions

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 346ae95a..e1e026f5 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Heap.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: Heap.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 (** A development of Treesort on Heap trees *)
 
@@ -21,207 +21,216 @@ Require Import Sorting.
 
 Section defs.
 
-Variable A : Set.
-Variable leA : relation A.
-Variable eqA : relation A.
+  (** * Trees and heap trees *)
 
-Let gtA (x y:A) := ~ leA x y.
+  (** ** Definition of trees over an ordered set *)
 
-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.
+  Variable A : Set.
+  Variable leA : relation A.
+  Variable eqA : relation A.
 
-Hint Resolve leA_refl.
-Hint Immediate eqA_dec leA_dec leA_antisym.
+  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.
 
-Let emptyBag := EmptyBag A.
-Let singletonBag := SingletonBag _ eqA_dec.
+  Hint Resolve leA_refl.
+  Hint Immediate eqA_dec leA_dec leA_antisym.
 
-Inductive Tree : Set :=
-  | Tree_Leaf : Tree
-  | Tree_Node : A -> Tree -> Tree -> Tree.
+  Let emptyBag := EmptyBag A.
+  Let singletonBag := SingletonBag _ eqA_dec.
+  
+  Inductive Tree : Set :=
+    | Tree_Leaf : Tree
+    | Tree_Node : A -> Tree -> Tree -> Tree.
 
-(** [a] is lower than a Tree [T] if [T] is a Leaf
-    or [T] is a Node holding [b>a] *)
+  (** [a] is lower than a Tree [T] if [T] is a Leaf
+      or [T] is a Node holding [b>a] *)
 
-Definition leA_Tree (a:A) (t:Tree) :=
-  match t with
-  | Tree_Leaf => True
-  | Tree_Node b T1 T2 => leA a b
-  end.
+  Definition leA_Tree (a:A) (t:Tree) :=
+    match t with
+      | Tree_Leaf => True
+      | Tree_Node b T1 T2 => leA a b
+    end.
 
-Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
-Proof.
-simpl in |- *; auto with datatypes.
-Qed.
+  Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
+  Proof.
+    simpl in |- *; auto with datatypes.
+  Qed.
 
-Lemma leA_Tree_Node :
- forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
-Proof.
-simpl in |- *; auto with datatypes.
-Qed.
+  Lemma leA_Tree_Node :
+    forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
+  Proof.
+    simpl in |- *; auto with datatypes.
+  Qed.
 
-Hint Resolve leA_Tree_Leaf leA_Tree_Node.
 
+  (** ** The heap property *)
 
-(** The heap property *)
-
-Inductive is_heap : Tree -> Prop :=
-  | nil_is_heap : is_heap Tree_Leaf
-  | node_is_heap :
+  Inductive is_heap : Tree -> Prop :=
+    | nil_is_heap : is_heap Tree_Leaf
+    | node_is_heap :
       forall (a:A) (T1 T2:Tree),
         leA_Tree a T1 ->
         leA_Tree a T2 ->
         is_heap T1 -> is_heap T2 -> is_heap (Tree_Node a T1 T2).
 
-Hint Constructors is_heap.
-
-Lemma invert_heap :
- forall (a:A) (T1 T2:Tree),
-   is_heap (Tree_Node a T1 T2) ->
-   leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.
-Proof.
-intros; inversion H; auto with datatypes.
-Qed.
-
-(* This lemma ought to be generated automatically by the Inversion tools *)
-Lemma is_heap_rec :
- forall P:Tree -> Set,
-   P Tree_Leaf ->
-   (forall (a:A) (T1 T2:Tree),
-      leA_Tree a T1 ->
-      leA_Tree a T2 ->
-      is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
-   forall T:Tree, is_heap T -> P T.
-Proof.
-simple induction T; auto with datatypes.
-intros a G PG D PD PN. 
-elim (invert_heap a G D); auto with datatypes.
-intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
-apply H0; auto with datatypes.
-Qed.
-
-Lemma low_trans :
- forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.
-Proof.
-simple induction T; auto with datatypes.
-intros; simpl in |- *; apply leA_trans with b; auto with datatypes.
-Qed.
-
-(** contents of a tree as a multiset *)
-
-(** Nota Bene : In what follows the definition of SingletonBag
-    in not used. Actually, we could just take as postulate:
-    [Parameter SingletonBag : A->multiset].  *)
-
-Fixpoint contents (t:Tree) : multiset A :=
-  match t with
-  | Tree_Leaf => emptyBag
-  | Tree_Node a t1 t2 =>
-      munion (contents t1) (munion (contents t2) (singletonBag a))
-  end.
-
-
-(** equivalence of two trees is equality of corresponding multisets *)
-
-Definition equiv_Tree (t1 t2:Tree) := meq (contents t1) (contents t2).
-
-
-(** specification of heap insertion *)
-
-Inductive insert_spec (a:A) (T:Tree) : Set :=
+  Lemma invert_heap :
+    forall (a:A) (T1 T2:Tree),
+      is_heap (Tree_Node a T1 T2) ->
+      leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.
+  Proof.
+    intros; inversion H; auto with datatypes.
+  Qed.
+
+  (* This lemma ought to be generated automatically by the Inversion tools *)
+  Lemma is_heap_rec :
+    forall P:Tree -> Set,
+      P Tree_Leaf ->
+      (forall (a:A) (T1 T2:Tree),
+	leA_Tree a T1 ->
+	leA_Tree a T2 ->
+	is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
+      forall T:Tree, is_heap T -> P T.
+  Proof.
+    simple induction T; auto with datatypes.
+    intros a G PG D PD PN. 
+    elim (invert_heap a G D); auto with datatypes.
+    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
+    apply H0; auto with datatypes.
+  Qed.
+
+  Lemma low_trans :
+    forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.
+  Proof.
+    simple induction T; auto with datatypes.
+    intros; simpl in |- *; apply leA_trans with b; auto with datatypes.
+  Qed.
+
+
+  (** ** From trees to multisets *)
+
+  (** contents of a tree as a multiset *)
+
+  (** Nota Bene : In what follows the definition of SingletonBag
+      in not used. Actually, we could just take as postulate:
+      [Parameter SingletonBag : A->multiset].  *)
+
+  Fixpoint contents (t:Tree) : multiset A :=
+    match t with
+      | Tree_Leaf => emptyBag
+      | Tree_Node a t1 t2 =>
+	munion (contents t1) (munion (contents t2) (singletonBag a))
+    end.
+
+
+  (** equivalence of two trees is equality of corresponding multisets *)
+  Definition equiv_Tree (t1 t2:Tree) := meq (contents t1) (contents t2).
+
+
+
+  (** * From lists to sorted lists *)
+
+  (** ** Specification of heap insertion *)
+
+  Inductive insert_spec (a:A) (T:Tree) : Set :=
     insert_exist :
-      forall T1:Tree,
-        is_heap T1 ->
-        meq (contents T1) (munion (contents T) (singletonBag a)) ->
-        (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
-        insert_spec a T.
-
-
-Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.
-Proof.
-simple induction 1; intros.
-apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
- auto with datatypes.
-simpl in |- *; unfold meq, munion in |- *; auto with datatypes.
-elim (leA_dec a a0); intros.
-elim (H3 a0); intros.
-apply insert_exist with (Tree_Node a T2 T0); auto with datatypes.
-simpl in |- *; apply treesort_twist1; trivial with datatypes. 
-elim (H3 a); intros T3 HeapT3 ConT3 LeA.
-apply insert_exist with (Tree_Node a0 T2 T3); auto with datatypes.
-apply node_is_heap; auto with datatypes.
-apply low_trans with a; auto with datatypes.
-apply LeA; auto with datatypes.
-apply low_trans with a; auto with datatypes.
-simpl in |- *; apply treesort_twist2; trivial with datatypes. 
-Qed.
-
-(** building a heap from a list *)
-
-Inductive build_heap (l:list A) : Set :=
+    forall T1:Tree,
+      is_heap T1 ->
+      meq (contents T1) (munion (contents T) (singletonBag a)) ->
+      (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
+      insert_spec a T.
+
+
+  Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.
+  Proof.
+    simple induction 1; intros.
+    apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
+      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    simpl in |- *; unfold meq, munion in |- *; auto using node_is_heap with datatypes.
+    elim (leA_dec a a0); intros.
+    elim (H3 a0); intros.
+    apply insert_exist with (Tree_Node a T2 T0);
+      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    simpl in |- *; apply treesort_twist1; trivial with datatypes. 
+    elim (H3 a); intros T3 HeapT3 ConT3 LeA.
+    apply insert_exist with (Tree_Node a0 T2 T3); 
+      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
+    apply low_trans with a; auto with datatypes. 
+    apply LeA; auto with datatypes.
+    apply low_trans with a; auto with datatypes.
+    simpl in |- *; apply treesort_twist2; trivial with datatypes. 
+  Qed.
+
+
+  (** ** Building a heap from a list *)
+
+  Inductive build_heap (l:list A) : Set :=
     heap_exist :
-      forall T:Tree,
-        is_heap T ->
-        meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.
-
-Lemma list_to_heap : forall l:list A, build_heap l.
-Proof.
-simple induction l.
-apply (heap_exist nil Tree_Leaf); auto with datatypes.
-simpl in |- *; unfold meq in |- *; auto with datatypes.
-simple induction 1.
-intros T i m; elim (insert T i a).
-intros; apply heap_exist with T1; simpl in |- *; auto with datatypes.
-apply meq_trans with (munion (contents T) (singletonBag a)).
-apply meq_trans with (munion (singletonBag a) (contents T)).
-apply meq_right; trivial with datatypes.
-apply munion_comm.
-apply meq_sym; trivial with datatypes.
-Qed.
-
-
-(** building the sorted list *)
-
-Inductive flat_spec (T:Tree) : Set :=
+    forall T:Tree,
+      is_heap T ->
+      meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.
+  
+  Lemma list_to_heap : forall l:list A, build_heap l.
+  Proof.
+    simple induction l.
+    apply (heap_exist nil Tree_Leaf); auto with datatypes.
+    simpl in |- *; unfold meq in |- *; exact nil_is_heap.
+    simple induction 1.
+    intros T i m; elim (insert T i a).
+    intros; apply heap_exist with T1; simpl in |- *; auto with datatypes.
+    apply meq_trans with (munion (contents T) (singletonBag a)).
+    apply meq_trans with (munion (singletonBag a) (contents T)).
+    apply meq_right; trivial with datatypes.
+    apply munion_comm.
+    apply meq_sym; trivial with datatypes.
+  Qed.
+
+
+  (** ** Building the sorted list *)
+  
+  Inductive flat_spec (T:Tree) : Set :=
     flat_exist :
-      forall l:list A,
-        sort leA l ->
-        (forall a:A, leA_Tree a T -> lelistA 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.
-Proof.
-  intros T h; elim h; intros.
-  apply flat_exist with (nil (A:=A)); auto with datatypes.
-  elim H2; intros l1 s1 i1 m1; elim H4; intros l2 s2 i2 m2.
-  elim (merge _ leA_dec eqA_dec s1 s2); intros.
-  apply flat_exist with (a :: l); simpl in |- *; auto with datatypes.
-  apply meq_trans with
-   (munion (list_contents _ eqA_dec l1)
-      (munion (list_contents _ eqA_dec l2) (singletonBag a))).
-  apply meq_congr; auto with datatypes.
-  apply meq_trans with
-   (munion (singletonBag a)
-      (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
-  apply munion_rotate.
-  apply meq_right; apply meq_sym; trivial with datatypes.
-Qed.
-
-(** specification of treesort *)
-
-Theorem treesort :
- forall l:list A, {m : list A | sort leA m &  permutation _ eqA_dec l m}.
-Proof.
-  intro l; unfold permutation in |- *.
-  elim (list_to_heap l).
-  intros.
-  elim (heap_to_list T); auto with datatypes.
-  intros.
-  exists l0; auto with datatypes.
-  apply meq_trans with (contents T); trivial with datatypes.
-Qed.
+    forall l:list A,
+      sort leA l ->
+      (forall a:A, leA_Tree a T -> lelistA 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.
+  Proof.
+    intros T h; elim h; intros.
+    apply flat_exist with (nil (A:=A)); auto with datatypes.
+    elim H2; intros l1 s1 i1 m1; elim H4; intros l2 s2 i2 m2.
+    elim (merge _ leA_dec eqA_dec s1 s2); intros.
+    apply flat_exist with (a :: l); simpl in |- *; auto with datatypes.
+    apply meq_trans with
+      (munion (list_contents _ eqA_dec l1)
+	(munion (list_contents _ eqA_dec l2) (singletonBag a))).
+    apply meq_congr; auto with datatypes.
+    apply meq_trans with
+      (munion (singletonBag a)
+	(munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
+    apply munion_rotate.
+    apply meq_right; apply meq_sym; trivial with datatypes.
+  Qed.
+
+
+  (** * Specification of treesort *)
+
+  Theorem treesort :
+    forall l:list A, {m : list A | sort leA m &  permutation _ eqA_dec l m}.
+  Proof.
+    intro l; unfold permutation in |- *.
+    elim (list_to_heap l).
+    intros.
+    elim (heap_to_list T); auto with datatypes.
+    intros.
+    exists l0; auto with datatypes.
+    apply meq_trans with (contents T); trivial with datatypes.
+  Qed.
 
 End defs.
\ No newline at end of file
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index e56ff27d..f4986198 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: PermutEq.v 8853 2006-05-23 18:17:38Z herbelin $ i*)
+(*i $Id: PermutEq.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Omega.
 Require Import Relations.
@@ -18,224 +18,224 @@ Require Import Permutation.
 Set Implicit Arguments.
 
 (** This file is similar to [PermutSetoid], except that the equality used here
-      is Coq usual one instead of a setoid equality. In particular, we can then 
-      prove the equivalence between [List.Permutation] and 
-      [Permutation.permutation].
+    is Coq usual one instead of a setoid equality. In particular, we can then 
+    prove the equivalence between [List.Permutation] and 
+    [Permutation.permutation].
 *)
 
 Section Perm.
-
-Variable A : Set.
-Hypothesis eq_dec : forall x y:A, {x=y} + {~ x=y}.
-
-Notation permutation := (permutation _ eq_dec).
-Notation list_contents := (list_contents _ eq_dec).
-
-(** we can use [multiplicity] to define [In] and [NoDup]. *)
-
-Lemma multiplicity_In : 
-  forall l a, In a l <-> 0 < multiplicity (list_contents l) a.
-Proof.
-induction l.
-simpl.
-split; inversion 1.
-simpl.
-split; intros.
-inversion_clear H.
-subst a0.
-destruct (eq_dec a a) as [_|H]; auto with arith; destruct H; auto.
-destruct (eq_dec a a0) as [H1|H1]; auto with arith; simpl.
-rewrite <- IHl; auto.
-destruct (eq_dec a a0); auto.
-simpl in H.
-right; rewrite IHl; auto.
-Qed.
-
-Lemma multiplicity_In_O :
-  forall l a, ~ In a l -> multiplicity (list_contents l) a = 0.
-Proof.
-intros l a; rewrite multiplicity_In; 
- destruct (multiplicity (list_contents l) a); auto.
-destruct 1; auto with arith.
-Qed.
-
-Lemma multiplicity_In_S :
- forall l a, In a l -> multiplicity (list_contents l) a >= 1.
-Proof.
-intros l a; rewrite multiplicity_In; auto.
-Qed.
-
-Lemma multiplicity_NoDup : 
-  forall l, NoDup l <-> (forall a, multiplicity (list_contents l) a <= 1).
-Proof.
-induction l.
-simpl.
-split; auto with arith.
-intros; apply NoDup_nil.
-split; simpl.
-inversion_clear 1.
-rewrite IHl in H1.
-intros; destruct (eq_dec a a0) as [H2|H2]; simpl; auto.
-subst a0.
-rewrite multiplicity_In_O; auto.
-intros; constructor.
-rewrite multiplicity_In.
-generalize (H a).
-destruct (eq_dec a a) as [H0|H0].
-destruct (multiplicity (list_contents l) a); auto with arith.
-simpl; inversion 1. 
-inversion H3.
-destruct H0; auto.
-rewrite IHl; intros.
-generalize (H a0); auto with arith.
-destruct (eq_dec a a0); simpl; auto with arith.
-Qed.
-
-Lemma NoDup_permut : 
-  forall l l', NoDup l -> NoDup l' -> 
-     (forall x, In x l <-> In x l') -> permutation l l'.
-Proof.
-intros.
-red; unfold meq; intros.
-rewrite multiplicity_NoDup in H, H0. 
-generalize (H a) (H0 a) (H1 a); clear H H0 H1.
-do 2 rewrite multiplicity_In.
-destruct 3; omega.
-Qed.
-
-(** Permutation is compatible with In. *)
-Lemma permut_In_In :
-  forall l1 l2 e, permutation l1 l2 -> In e l1 -> In e l2.
-Proof.
-unfold Permutation.permutation, meq; intros l1 l2 e P IN.
-generalize (P e); clear P.
-destruct (In_dec eq_dec e l2) as [H|H]; auto.
-rewrite (multiplicity_In_O _ _ H).
-intros.
-generalize (multiplicity_In_S _ _ IN).
-rewrite H0.
-inversion 1.
-Qed.
-
-Lemma permut_cons_In :
-  forall l1 l2 e, permutation (e :: l1) l2 -> In e l2.
-Proof.
-intros; eapply permut_In_In; eauto.
-red; auto.
-Qed.
-
-(** Permutation of an empty list. *)
-Lemma permut_nil :
- forall l, permutation l nil -> l = nil.
-Proof.
-intro l; destruct l as [ | e l ]; trivial.
-assert (In e (e::l)) by (red; auto).
-intro Abs; generalize (permut_In_In _ Abs H).
-inversion 1.
-Qed.
-
-(** When used with [eq], this permutation notion is equivalent to 
-  the one defined in [List.v]. *)
-
-Lemma permutation_Permutation : 
- forall l l', Permutation l l' <-> permutation l l'.
-Proof.
-split.
-induction 1.
-apply permut_refl.
-apply permut_cons; auto.
-change (permutation (y::x::l) ((x::nil)++y::l)).
-apply permut_add_cons_inside; simpl; apply permut_refl.
-apply permut_tran with l'; auto.
-revert l'.
-induction l.
-intros.
-rewrite (permut_nil (permut_sym H)).
-apply Permutation_refl.
-intros.
-destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).
-subst l'.
-apply Permutation_cons_app.
-apply IHl.
-apply permut_remove_hd with a; auto.
-Qed.
-
-(** Permutation for short lists. *)
-
-Lemma permut_length_1:
- forall a b, permutation (a :: nil) (b :: nil)  -> a=b.
-Proof.
-intros a b; unfold Permutation.permutation, meq; intro P;
-generalize (P b); clear P; simpl.
-destruct (eq_dec b b) as [H|H]; [ | destruct H; auto].
-destruct (eq_dec a b); simpl; auto; intros; discriminate.
-Qed.
-
-Lemma permut_length_2 :
- forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
- (a1=a2) /\ (b1=b2) \/ (a1=b2) /\ (a2=b1).
-Proof.
-intros a1 b1 a2 b2 P.
-assert (H:=permut_cons_In P).
-inversion_clear H.
-left; split; auto.
-apply permut_length_1.
-red; red; intros.
-generalize (P a); clear P; simpl.
-destruct (eq_dec a1 a) as [H2|H2]; 
- destruct (eq_dec a2 a) as [H3|H3]; auto.
-destruct H3; transitivity a1; auto.
-destruct H2; transitivity a2; auto.
-right.
-inversion_clear H0; [|inversion H].
-split; auto.
-apply permut_length_1.
-red; red; intros.
-generalize (P a); clear P; simpl.
-destruct (eq_dec a1 a) as [H2|H2]; 
- destruct (eq_dec b2 a) as [H3|H3]; auto.
-simpl; rewrite <- plus_n_Sm; inversion 1; auto.
-destruct H3; transitivity a1; auto.
-destruct H2; transitivity b2; auto.
-Qed.
-
-(** Permutation is compatible with length. *)
-Lemma permut_length :
- forall l1 l2, permutation l1 l2 -> length l1 = length l2.
-Proof.
-induction l1; intros l2 H.
-rewrite (permut_nil (permut_sym H)); auto.
-destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).
-subst l2.
-rewrite app_length.
-simpl; rewrite <- plus_n_Sm; f_equal.
-rewrite <- app_length.
-apply IHl1.
-apply permut_remove_hd with a; auto.
-Qed.
-
-Variable B : Set.
-Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }. 
-
-(** Permutation is compatible with map. *)
-
-Lemma permutation_map :
-  forall f l1 l2, permutation l1 l2 -> 
-   Permutation.permutation _ eqB_dec (map f l1) (map f l2).
-Proof.
-intros f; induction l1.
-intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl.
-intros l2 P.
-simpl.
-destruct (In_split _ _ (permut_cons_In P)) as (h2,(t2,H1)).
-subst l2.
-rewrite map_app.
-simpl.
-apply permut_add_cons_inside.
-rewrite <- map_app.
-apply IHl1; auto.
-apply permut_remove_hd with a; auto.
-Qed.
+  
+  Variable A : Set.
+  Hypothesis eq_dec : forall x y:A, {x=y} + {~ x=y}.
+  
+  Notation permutation := (permutation _ eq_dec).
+  Notation list_contents := (list_contents _ eq_dec).
+
+  (** we can use [multiplicity] to define [In] and [NoDup]. *)
+
+  Lemma multiplicity_In : 
+    forall l a, In a l <-> 0 < multiplicity (list_contents l) a.
+  Proof.
+    induction l.
+    simpl.
+    split; inversion 1.
+    simpl.
+    split; intros.
+    inversion_clear H.
+    subst a0.
+    destruct (eq_dec a a) as [_|H]; auto with arith; destruct H; auto.
+    destruct (eq_dec a a0) as [H1|H1]; auto with arith; simpl.
+    rewrite <- IHl; auto.
+    destruct (eq_dec a a0); auto.
+    simpl in H.
+    right; rewrite IHl; auto.
+  Qed.
+
+  Lemma multiplicity_In_O :
+    forall l a, ~ In a l -> multiplicity (list_contents l) a = 0.
+  Proof.
+    intros l a; rewrite multiplicity_In; 
+      destruct (multiplicity (list_contents l) a); auto.
+    destruct 1; auto with arith.
+  Qed.
+  
+  Lemma multiplicity_In_S :
+    forall l a, In a l -> multiplicity (list_contents l) a >= 1.
+  Proof.
+    intros l a; rewrite multiplicity_In; auto.
+  Qed.
+
+  Lemma multiplicity_NoDup : 
+    forall l, NoDup l <-> (forall a, multiplicity (list_contents l) a <= 1).
+  Proof.
+    induction l.
+    simpl.
+    split; auto with arith.
+    intros; apply NoDup_nil.
+    split; simpl.
+    inversion_clear 1.
+    rewrite IHl in H1.
+    intros; destruct (eq_dec a a0) as [H2|H2]; simpl; auto.
+    subst a0.
+    rewrite multiplicity_In_O; auto.
+    intros; constructor.
+    rewrite multiplicity_In.
+    generalize (H a).
+    destruct (eq_dec a a) as [H0|H0].
+    destruct (multiplicity (list_contents l) a); auto with arith.
+    simpl; inversion 1. 
+    inversion H3.
+    destruct H0; auto.
+    rewrite IHl; intros.
+    generalize (H a0); auto with arith.
+    destruct (eq_dec a a0); simpl; auto with arith.
+  Qed.
+
+  Lemma NoDup_permut : 
+    forall l l', NoDup l -> NoDup l' -> 
+      (forall x, In x l <-> In x l') -> permutation l l'.
+  Proof.
+    intros.
+    red; unfold meq; intros.
+    rewrite multiplicity_NoDup in H, H0. 
+    generalize (H a) (H0 a) (H1 a); clear H H0 H1.
+    do 2 rewrite multiplicity_In.
+    destruct 3; omega.
+  Qed.
+
+  (** Permutation is compatible with In. *)
+  Lemma permut_In_In :
+    forall l1 l2 e, permutation l1 l2 -> In e l1 -> In e l2.
+  Proof.
+    unfold Permutation.permutation, meq; intros l1 l2 e P IN.
+    generalize (P e); clear P.
+    destruct (In_dec eq_dec e l2) as [H|H]; auto.
+    rewrite (multiplicity_In_O _ _ H).
+    intros.
+    generalize (multiplicity_In_S _ _ IN).
+    rewrite H0.
+    inversion 1.
+  Qed.
+
+  Lemma permut_cons_In :
+    forall l1 l2 e, permutation (e :: l1) l2 -> In e l2.
+  Proof.
+    intros; eapply permut_In_In; eauto.
+    red; auto.
+  Qed.
+
+  (** Permutation of an empty list. *)
+  Lemma permut_nil :
+    forall l, permutation l nil -> l = nil.
+  Proof.
+    intro l; destruct l as [ | e l ]; trivial.
+    assert (In e (e::l)) by (red; auto).
+    intro Abs; generalize (permut_In_In _ Abs H).
+    inversion 1.
+  Qed.
+  
+  (** When used with [eq], this permutation notion is equivalent to 
+      the one defined in [List.v]. *)
+
+  Lemma permutation_Permutation : 
+    forall l l', Permutation l l' <-> permutation l l'.
+  Proof.
+    split.
+    induction 1.
+    apply permut_refl.
+    apply permut_cons; auto.
+    change (permutation (y::x::l) ((x::nil)++y::l)).
+    apply permut_add_cons_inside; simpl; apply permut_refl.
+    apply permut_tran with l'; auto.
+    revert l'.
+    induction l.
+    intros.
+    rewrite (permut_nil (permut_sym H)).
+    apply Permutation_refl.
+    intros.
+    destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).
+    subst l'.
+    apply Permutation_cons_app.
+    apply IHl.
+    apply permut_remove_hd with a; auto.
+  Qed.
+
+  (** Permutation for short lists. *)
+
+  Lemma permut_length_1:
+    forall a b, permutation (a :: nil) (b :: nil)  -> a=b.
+  Proof.
+    intros a b; unfold Permutation.permutation, meq; intro P;
+      generalize (P b); clear P; simpl.
+    destruct (eq_dec b b) as [H|H]; [ | destruct H; auto].
+    destruct (eq_dec a b); simpl; auto; intros; discriminate.
+  Qed.
+  
+  Lemma permut_length_2 :
+    forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
+      (a1=a2) /\ (b1=b2) \/ (a1=b2) /\ (a2=b1).
+  Proof.
+    intros a1 b1 a2 b2 P.
+    assert (H:=permut_cons_In P).
+    inversion_clear H.
+    left; split; auto.
+    apply permut_length_1.
+    red; red; intros.
+    generalize (P a); clear P; simpl.
+    destruct (eq_dec a1 a) as [H2|H2]; 
+      destruct (eq_dec a2 a) as [H3|H3]; auto.
+    destruct H3; transitivity a1; auto.
+    destruct H2; transitivity a2; auto.
+    right.
+    inversion_clear H0; [|inversion H].
+    split; auto.
+    apply permut_length_1.
+    red; red; intros.
+    generalize (P a); clear P; simpl.
+    destruct (eq_dec a1 a) as [H2|H2]; 
+      destruct (eq_dec b2 a) as [H3|H3]; auto.
+    simpl; rewrite <- plus_n_Sm; inversion 1; auto.
+    destruct H3; transitivity a1; auto.
+    destruct H2; transitivity b2; auto.
+  Qed.
+
+  (** Permutation is compatible with length. *)
+  Lemma permut_length :
+    forall l1 l2, permutation l1 l2 -> length l1 = length l2.
+  Proof.
+    induction l1; intros l2 H.
+    rewrite (permut_nil (permut_sym H)); auto.
+    destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).
+    subst l2.
+    rewrite app_length.
+    simpl; rewrite <- plus_n_Sm; f_equal.
+    rewrite <- app_length.
+    apply IHl1.
+    apply permut_remove_hd with a; auto.
+  Qed.
+
+  Variable B : Set.
+  Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }. 
+
+  (** Permutation is compatible with map. *)
+
+  Lemma permutation_map :
+    forall f l1 l2, permutation l1 l2 -> 
+      Permutation.permutation _ eqB_dec (map f l1) (map f l2).
+  Proof.
+    intros f; induction l1.
+    intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl.
+    intros l2 P.
+    simpl.
+    destruct (In_split _ _ (permut_cons_In P)) as (h2,(t2,H1)).
+    subst l2.
+    rewrite map_app.
+    simpl.
+    apply permut_add_cons_inside.
+    rewrite <- map_app.
+    apply IHl1; auto.
+    apply permut_remove_hd with a; auto.
+  Qed.
 
 End Perm.
 
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 46ea088f..65369a01 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: PermutSetoid.v 8823 2006-05-16 16:17:43Z letouzey $ i*)
+(*i $Id: PermutSetoid.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Omega.
 Require Import Relations.
@@ -41,59 +41,59 @@ Variable eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
 Lemma multiplicity_InA : 
   forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.
 Proof.
-induction l.
-simpl.
-split; inversion 1.
-simpl.
-split; intros.
-inversion_clear H.
-destruct (eqA_dec a a0) as [_|H1]; auto with arith.
-destruct H1; auto.
-destruct (eqA_dec a a0); auto with arith.
-simpl; rewrite <- IHl; auto.
-destruct (eqA_dec a a0) as [H0|H0]; auto.
-simpl in H.
-constructor 2; rewrite IHl; auto.
+  induction l.
+  simpl.
+  split; inversion 1.
+  simpl.
+  split; intros.
+  inversion_clear H.
+  destruct (eqA_dec a a0) as [_|H1]; auto with arith.
+  destruct H1; auto.
+  destruct (eqA_dec a a0); auto with arith.
+  simpl; rewrite <- IHl; auto.
+  destruct (eqA_dec a a0) as [H0|H0]; auto.
+  simpl in H.
+  constructor 2; rewrite IHl; auto.
 Qed.
 
 Lemma multiplicity_InA_O :
   forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.
 Proof.
-intros l a; rewrite multiplicity_InA; 
-destruct (multiplicity (list_contents l) a); auto with arith.
-destruct 1; auto with arith.
+  intros l a; rewrite multiplicity_InA; 
+    destruct (multiplicity (list_contents l) a); auto with arith.
+  destruct 1; auto with arith.
 Qed.
 
 Lemma multiplicity_InA_S :
- forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.
+  forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.
 Proof.
-intros l a; rewrite multiplicity_InA; auto with arith.
+  intros l a; rewrite multiplicity_InA; auto with arith.
 Qed.
 
 Lemma multiplicity_NoDupA : forall l, 
   NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).
 Proof.
-induction l.
-simpl.
-split; auto with arith.
-split; simpl.
-inversion_clear 1.
-rewrite IHl in H1.
-intros; destruct (eqA_dec a a0) as [H2|H2]; simpl; auto.
-rewrite multiplicity_InA_O; auto.
-swap H0.
-apply InA_eqA with a0; auto.
-intros; constructor.
-rewrite multiplicity_InA.
-generalize (H a).
-destruct (eqA_dec a a) as [H0|H0].
-destruct (multiplicity (list_contents l) a); auto with arith.
-simpl; inversion 1. 
-inversion H3.
-destruct H0; auto.
-rewrite IHl; intros.
-generalize (H a0); auto with arith.
-destruct (eqA_dec a a0); simpl; auto with arith.
+  induction l.
+  simpl.
+  split; auto with arith.
+  split; simpl.
+  inversion_clear 1.
+  rewrite IHl in H1.
+  intros; destruct (eqA_dec a a0) as [H2|H2]; simpl; auto.
+  rewrite multiplicity_InA_O; auto.
+  swap H0.
+  apply InA_eqA with a0; auto.
+  intros; constructor.
+  rewrite multiplicity_InA.
+  generalize (H a).
+  destruct (eqA_dec a a) as [H0|H0].
+  destruct (multiplicity (list_contents l) a); auto with arith.
+  simpl; inversion 1. 
+  inversion H3.
+  destruct H0; auto.
+  rewrite IHl; intros.
+  generalize (H a0); auto with arith.
+  destruct (eqA_dec a a0); simpl; auto with arith.
 Qed.
 
 
@@ -101,100 +101,100 @@ Qed.
 Lemma permut_InA_InA :
   forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.
 Proof.
-intros l1 l2 e.
-do 2 rewrite multiplicity_InA.
-unfold Permutation.permutation, meq.
-intros H;rewrite H; auto.
+  intros l1 l2 e.
+  do 2 rewrite multiplicity_InA.
+  unfold Permutation.permutation, meq.
+  intros H;rewrite H; auto.
 Qed.
 
 Lemma permut_cons_InA :
   forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.
 Proof.
-intros; apply (permut_InA_InA (e:=e) H); auto.
+  intros; apply (permut_InA_InA (e:=e) H); auto.
 Qed.
 
 (** Permutation of an empty list. *)
 Lemma permut_nil :
- forall l, permutation l nil -> l = nil.
+  forall l, permutation l nil -> l = nil.
 Proof.
-intro l; destruct l as [ | e l ]; trivial.
-assert (InA eqA e (e::l)) by auto.
-intro Abs; generalize (permut_InA_InA Abs H).
-inversion 1.
+  intro l; destruct l as [ | e l ]; trivial.
+  assert (InA eqA e (e::l)) by auto.
+  intro Abs; generalize (permut_InA_InA Abs H).
+  inversion 1.
 Qed.
 
 (** Permutation for short lists. *)
 
 Lemma permut_length_1:
- forall a b, permutation (a :: nil) (b :: nil)  -> eqA a b.
+  forall a b, permutation (a :: nil) (b :: nil)  -> eqA a b.
 Proof.
-intros a b; unfold Permutation.permutation, meq; intro P;
-generalize (P b); clear P; simpl.
-destruct (eqA_dec b b) as [H|H]; [ | destruct H; auto].
-destruct (eqA_dec a b); simpl; auto; intros; discriminate.
+  intros a b; unfold Permutation.permutation, meq; intro P;
+  generalize (P b); clear P; simpl.
+  destruct (eqA_dec b b) as [H|H]; [ | destruct H; auto].
+  destruct (eqA_dec a b); simpl; auto; intros; discriminate.
 Qed.
 
 Lemma permut_length_2 :
- forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
- (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).
+  forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
+    (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).
 Proof.
-intros a1 b1 a2 b2 P.
-assert (H:=permut_cons_InA P).
-inversion_clear H.
-left; split; auto.
-apply permut_length_1.
-red; red; intros.
-generalize (P a); clear P; simpl.
-destruct (eqA_dec a1 a) as [H2|H2]; 
- destruct (eqA_dec a2 a) as [H3|H3]; auto.
-destruct H3; apply eqA_trans with a1; auto.
-destruct H2; apply eqA_trans with a2; auto.
-right.
-inversion_clear H0; [|inversion H].
-split; auto.
-apply permut_length_1.
-red; red; intros.
-generalize (P a); clear P; simpl.
-destruct (eqA_dec a1 a) as [H2|H2]; 
- destruct (eqA_dec b2 a) as [H3|H3]; auto.
-simpl; rewrite <- plus_n_Sm; inversion 1; auto.
-destruct H3; apply eqA_trans with a1; auto.
-destruct H2; apply eqA_trans with b2; auto.
+  intros a1 b1 a2 b2 P.
+  assert (H:=permut_cons_InA P).
+  inversion_clear H.
+  left; split; auto.
+  apply permut_length_1.
+  red; red; intros.
+  generalize (P a); clear P; simpl.
+  destruct (eqA_dec a1 a) as [H2|H2]; 
+    destruct (eqA_dec a2 a) as [H3|H3]; auto.
+  destruct H3; apply eqA_trans with a1; auto.
+  destruct H2; apply eqA_trans with a2; auto.
+  right.
+  inversion_clear H0; [|inversion H].
+  split; auto.
+  apply permut_length_1.
+  red; red; intros.
+  generalize (P a); clear P; simpl.
+  destruct (eqA_dec a1 a) as [H2|H2]; 
+    destruct (eqA_dec b2 a) as [H3|H3]; auto.
+  simpl; rewrite <- plus_n_Sm; inversion 1; auto.
+  destruct H3; apply eqA_trans with a1; auto.
+  destruct H2; apply eqA_trans with b2; auto.
 Qed.
 
 (** Permutation is compatible with length. *)
 Lemma permut_length :
- forall l1 l2, permutation l1 l2 -> length l1 = length l2.
+  forall l1 l2, permutation l1 l2 -> length l1 = length l2.
 Proof.
-induction l1; intros l2 H.
-rewrite (permut_nil (permut_sym H)); auto.
-assert (H0:=permut_cons_InA H).
-destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
-subst l2.
-rewrite app_length.
-simpl; rewrite <- plus_n_Sm; f_equal.
-rewrite <- app_length.
-apply IHl1.
-apply permut_remove_hd with b.
-apply permut_tran with (a::l1); auto.
-revert H1; unfold Permutation.permutation, meq; simpl.
-intros; f_equal; auto.
-destruct (eqA_dec b a0) as [H2|H2]; 
- destruct (eqA_dec a a0) as [H3|H3]; auto.
-destruct H3; apply eqA_trans with b; auto.
-destruct H2; apply eqA_trans with a; auto.
+  induction l1; intros l2 H.
+  rewrite (permut_nil (permut_sym H)); auto.
+  assert (H0:=permut_cons_InA H).
+  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
+  subst l2.
+  rewrite app_length.
+  simpl; rewrite <- plus_n_Sm; f_equal.
+  rewrite <- app_length.
+  apply IHl1.
+  apply permut_remove_hd with b.
+  apply permut_tran with (a::l1); auto.
+  revert H1; unfold Permutation.permutation, meq; simpl.
+  intros; f_equal; auto.
+  destruct (eqA_dec b a0) as [H2|H2]; 
+    destruct (eqA_dec a a0) as [H3|H3]; auto.
+  destruct H3; apply eqA_trans with b; auto.
+  destruct H2; apply eqA_trans with a; auto.
 Qed.
 
 Lemma NoDupA_eqlistA_permut : 
   forall l l', NoDupA eqA l -> NoDupA eqA l' -> 
-     eqlistA eqA l l' -> permutation l l'.
+    eqlistA eqA l l' -> permutation l l'.
 Proof.
-intros.
-red; unfold meq; intros.
-rewrite multiplicity_NoDupA in H, H0. 
-generalize (H a) (H0 a) (H1 a); clear H H0 H1.
-do 2 rewrite multiplicity_InA.
-destruct 3; omega.
+  intros.
+  red; unfold meq; intros.
+  rewrite multiplicity_NoDupA in H, H0. 
+  generalize (H a) (H0 a) (H1 a); clear H H0 H1.
+  do 2 rewrite multiplicity_InA.
+  destruct 3; omega.
 Qed.
 
 
@@ -207,37 +207,37 @@ Variable eqB_trans : forall x y z, eqB x y -> eqB y z -> eqB x z.
 
 Lemma permut_map :
   forall f, 
-  (forall x y, eqA x y -> eqB (f x) (f y)) ->
-  forall l1 l2, permutation l1 l2 -> 
-   Permutation.permutation _ eqB_dec (map f l1) (map f l2).
+    (forall x y, eqA x y -> eqB (f x) (f y)) ->
+    forall l1 l2, permutation l1 l2 -> 
+      Permutation.permutation _ eqB_dec (map f l1) (map f l2).
 Proof.
-intros f; induction l1.
-intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl.
-intros l2 P.
-simpl.
-assert (H0:=permut_cons_InA P).
-destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
-subst l2.
-rewrite map_app.
-simpl.
-apply permut_tran with (f b :: map f l1).
-revert H1; unfold Permutation.permutation, meq; simpl.
-intros; f_equal; auto.
-destruct (eqB_dec (f b) a0) as [H2|H2]; 
- destruct (eqB_dec (f a) a0) as [H3|H3]; auto.
-destruct H3; apply eqB_trans with (f b); auto.
-destruct H2; apply eqB_trans with (f a); auto.
-apply permut_add_cons_inside.
-rewrite <- map_app.
-apply IHl1; auto.
-apply permut_remove_hd with b.
-apply permut_tran with (a::l1); auto.
-revert H1; unfold Permutation.permutation, meq; simpl.
-intros; f_equal; auto.
-destruct (eqA_dec b a0) as [H2|H2]; 
- destruct (eqA_dec a a0) as [H3|H3]; auto.
-destruct H3; apply eqA_trans with b; auto.
-destruct H2; apply eqA_trans with a; auto.
+  intros f; induction l1.
+  intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl.
+  intros l2 P.
+  simpl.
+  assert (H0:=permut_cons_InA P).
+  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
+  subst l2.
+  rewrite map_app.
+  simpl.
+  apply permut_tran with (f b :: map f l1).
+  revert H1; unfold Permutation.permutation, meq; simpl.
+  intros; f_equal; auto.
+  destruct (eqB_dec (f b) a0) as [H2|H2]; 
+    destruct (eqB_dec (f a) a0) as [H3|H3]; auto.
+  destruct H3; apply eqB_trans with (f b); auto.
+  destruct H2; apply eqB_trans with (f a); auto.
+  apply permut_add_cons_inside.
+  rewrite <- map_app.
+  apply IHl1; auto.
+  apply permut_remove_hd with b.
+  apply permut_tran with (a::l1); auto.
+  revert H1; unfold Permutation.permutation, meq; simpl.
+  intros; f_equal; auto.
+  destruct (eqA_dec b a0) as [H2|H2]; 
+    destruct (eqA_dec a a0) as [H3|H3]; auto.
+  destruct H3; apply eqA_trans with b; auto.
+  destruct H2; apply eqA_trans with a; auto.
 Qed.
 
 End Perm.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 0f2e02b5..3ff026c2 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Permutation.v 8823 2006-05-16 16:17:43Z letouzey $ i*)
+(*i $Id: Permutation.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Relations.
 Require Import List.
@@ -14,193 +14,194 @@ Require Import Multiset.
 Require Import Arith.
 
 (** This file define a notion of permutation for lists, based on multisets: 
-     there exists a permutation between two lists iff every elements have 
-     the same multiplicities in the two lists. 
+    there exists a permutation between two lists iff every elements have 
+    the same multiplicities in the two lists. 
 
-     Unlike [List.Permutation], the present notion of permutation requires
-     a decidable equality. At the same time, this definition can be used 
-     with a non-standard equality, whereas [List.Permutation] cannot.
+    Unlike [List.Permutation], the present notion of permutation requires
+    a decidable equality. At the same time, this definition can be used 
+    with a non-standard equality, whereas [List.Permutation] cannot.
       
-     The present file contains basic results, obtained without any particular
-     assumption on the decidable equality used.
+    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). 
+    File [PermutSetoid] contains additional results about permutations 
+    with respect to an setoid equality (i.e. an equivalence relation). 
 
-     Finally, file [PermutEq] concerns Coq equality : this file is similar 
-     to the previous one, but proves in addition that [List.Permutation]
-     and [permutation] are equivalent in this context.
-*)
+    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.
+x*)
 
 Set Implicit Arguments.
 
 Section defs.
 
-Variable A : Set.
-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.
-Hint Resolve list_contents_app.
-
-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.
-Hint Resolve permut_refl.
-
-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.
-Hint Resolve permut_cons.
-
-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 with datatypes.
-apply meq_trans with (munion (list_contents l') (list_contents m')); 
- auto with datatypes.
-apply meq_trans with (munion (list_contents l') (list_contents m));
- auto with datatypes.
-Qed.
-Hint Resolve permut_app.
-
-Lemma permut_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.
-Qed.
-Hint Resolve permut_middle.
-
-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; auto.
-simpl.
-apply permut_add_cons_inside.
-rewrite <- app_nil_end; auto.
-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.
+  (** * From lists to multisets *)
+
+  Variable A : Set.
+  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 *) 
+
+(** For compatibilty *) 
 Notation permut_right := permut_cons.
 Unset Implicit Arguments.
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index 0e0bfe8f..f895d79e 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Sorting.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: Sorting.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import List.
 Require Import Multiset.
@@ -17,107 +17,107 @@ Set Implicit Arguments.
 
 Section defs.
 
-Variable A : Set.
-Variable leA : relation A.
-Variable eqA : relation A.
+  Variable A : Set.
+  Variable leA : relation A.
+  Variable eqA : relation A.
 
-Let gtA (x y:A) := ~ leA x y.
+  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.
 
-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.
 
-Hint Resolve leA_refl.
-Hint Immediate eqA_dec leA_dec leA_antisym.
+  Let emptyBag := EmptyBag A.
+  Let singletonBag := SingletonBag _ eqA_dec.
 
-Let emptyBag := EmptyBag A.
-Let singletonBag := SingletonBag _ eqA_dec.
+  (** [lelistA] *)
 
-(** [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).
 
-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).
-Hint Constructors lelistA.
+  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.
 
-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 *)
 
-(** definition for a list to be sorted *)
-
-Inductive sort : list A -> Prop :=
-  | nil_sort : sort nil
-  | cons_sort :
+  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).
-Hint Constructors sort.
-
-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_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) : Set :=
+
+  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_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) : Set :=
     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 H3; intros.
-  apply merge_exist with (a :: l); simpl in |- *; auto with datatypes.
-  elim (leA_dec a a0); intros.
-
-(* 1 (leA a a0) *)
-  cut (merge_lem l (a0 :: l0)); auto with datatypes.
-  intros [l3 l3sorted l3contents Hrec].
-  apply merge_exist with (a :: l3); simpl in |- *; auto 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 H5; simpl in |- *; intros.
-  apply merge_exist with (a0 :: l3); simpl in |- *; auto 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.
+    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 H3; 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 H5; 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.
\ No newline at end of file
+Hint Constructors lelistA: datatypes v62.