Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 71 insertions, 18 deletions

diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index fe7902aa..4124ef98 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -6,13 +6,17 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Heap.v 10698 2008-03-19 18:46:59Z letouzey $ i*)
+(*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.
 
@@ -25,7 +29,7 @@ Section defs.
   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.
@@ -37,7 +41,7 @@ Section defs.
 
   Let emptyBag := EmptyBag A.
   Let singletonBag := SingletonBag _ eqA_dec.
-  
+
   Inductive Tree :=
     | Tree_Leaf : Tree
     | Tree_Node : A -> Tree -> Tree -> Tree.
@@ -92,7 +96,7 @@ Section defs.
       forall T:Tree, is_heap T -> P T.
   Proof.
     simple induction T; auto with datatypes.
-    intros a G PG D PD PN. 
+    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 X0; auto with datatypes.
@@ -109,7 +113,7 @@ Section defs.
       forall T:Tree, is_heap T -> P T.
   Proof.
     simple induction T; auto with datatypes.
-    intros a G PG D PD PN. 
+    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 X; auto with datatypes.
@@ -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 *)
 
@@ -167,15 +219,15 @@ Section defs.
     elim (X 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. 
+    simpl in |- *; apply treesort_twist1; trivial with datatypes.
     elim (X a); intros T3 HeapT3 ConT3 LeA.
-    apply insert_exist with (Tree_Node a0 T2 T3); 
+    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 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. 
+    simpl in |- *; apply treesort_twist2; trivial with datatypes.
   Qed.
 
 
@@ -186,7 +238,7 @@ Section defs.
     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.
@@ -204,12 +256,12 @@ Section defs.
 
 
   (** ** Building the sorted list *)
-  
+
   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.