summaryrefslogtreecommitdiff
path: root/theories/Sorting/Heap.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Sorting/Heap.v
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Sorting/Heap.v')
-rw-r--r--theories/Sorting/Heap.v89
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.