1 files changed, 3 insertions, 121 deletions
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v
index aed8cd15..5f8da6a4 100644
--- a/theories/Sorting/Sorting.v
+++ b/theories/Sorting/Sorting.v
@@ -6,125 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Sorting.v 10698 2008-03-19 18:46:59Z letouzey $ i*)
+(*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.