diff options
Diffstat (limited to 'theories7/Sorting/Heap.v')
| -rw-r--r-- | theories7/Sorting/Heap.v | 223 |
1 files changed, 223 insertions, 0 deletions
diff --git a/theories7/Sorting/Heap.v b/theories7/Sorting/Heap.v new file mode 100644 index 00000000..63e7f324 --- /dev/null +++ b/theories7/Sorting/Heap.v @@ -0,0 +1,223 @@ +(************************************************************************) +(* 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: Heap.v,v 1.1.2.1 2004/07/16 19:31:41 herbelin Exp $ i*) + +(** A development of Treesort on Heap trees *) + +(* G. Huet 1-9-95 uses Multiset *) + +Require PolyList. +Require Multiset. +Require Permutation. +Require Relations. +Require Sorting. + + +Section defs. + +Variable A : Set. +Variable leA : (relation A). +Variable eqA : (relation A). + +Local gtA := [x,y:A]~(leA x y). + +Hypothesis leA_dec : (x,y:A){(leA x y)}+{(leA y x)}. +Hypothesis eqA_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}. +Hypothesis leA_refl : (x,y:A) (eqA x y) -> (leA x y). +Hypothesis leA_trans : (x,y,z:A) (leA x y) -> (leA y z) -> (leA x z). +Hypothesis leA_antisym : (x,y:A)(leA x y) -> (leA y x) -> (eqA x y). + +Hints Resolve leA_refl. +Hints Immediate eqA_dec leA_dec leA_antisym. + +Local emptyBag := (EmptyBag A). +Local 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] *) + +Definition leA_Tree := [a:A; t:Tree] + Cases t of + Tree_Leaf => True + | (Tree_Node b T1 T2) => (leA a b) + end. + +Lemma leA_Tree_Leaf : (a:A)(leA_Tree a Tree_Leaf). +Proof. +Simpl; Auto with datatypes. +Qed. + +Lemma leA_Tree_Node : (a,b:A)(G,D:Tree)(leA a b) -> + (leA_Tree a (Tree_Node b G D)). +Proof. +Simpl; Auto with datatypes. +Qed. + +Hints Resolve leA_Tree_Leaf leA_Tree_Node. + + +(** The heap property *) + +Inductive is_heap : Tree -> Prop := + nil_is_heap : (is_heap Tree_Leaf) + | node_is_heap : (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 constr_is_heap := Constructors is_heap. + +Lemma invert_heap : (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 : (P:Tree->Set) + (P Tree_Leaf)-> + ((a:A) + (T1:Tree) + (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))) + -> (T:Tree)(is_heap T) -> (P T). +Proof. +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 : + (T:Tree)(a,b:A)(leA a b) -> (leA_Tree b T) -> (leA_Tree a T). +Proof. +Induction T; Auto with datatypes. +Intros; Simpl; 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) := + Cases t of + 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 := + insert_exist : (T1:Tree)(is_heap T1) -> + (meq (contents T1) (munion (contents T) (singletonBag a))) -> + ((b:A)(leA b a)->(leA_Tree b T)->(leA_Tree b T1)) -> + (insert_spec a T). + + +Lemma insert : (T:Tree)(is_heap T) -> (a:A)(insert_spec a T). +Proof. +Induction 1; Intros. +Apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf); Auto with datatypes. +Simpl; Unfold meq munion; 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; 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; Apply treesort_twist2; Trivial with datatypes. +Qed. + +(** building a heap from a list *) + +Inductive build_heap [l:(list A)] : Set := + heap_exist : (T:Tree)(is_heap T) -> + (meq (list_contents eqA_dec l)(contents T)) -> + (build_heap l). + +Lemma list_to_heap : (l:(list A))(build_heap l). +Proof. +Induction l. +Apply (heap_exist (nil A) Tree_Leaf); Auto with datatypes. +Simpl; Unfold meq; Auto with datatypes. +Induction 1. +Intros T i m; Elim (insert T i a). +Intros; Apply heap_exist with T1; Simpl; 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 : (l:(list A))(sort leA l) -> + ((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 : (T:Tree)(is_heap T) -> (flat_spec T). +Proof. + Intros T h; Elim h; Intros. + Apply flat_exist with (nil 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 (cons a l); Simpl; 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 : (l:(list A)) + {m:(list A) | (sort leA m) & (permutation eqA_dec l m)}. +Proof. + Intro l; Unfold permutation. + 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. |