diff options
Diffstat (limited to 'theories7/Sorting')
| -rw-r--r-- | theories7/Sorting/Heap.v | 223 | ||||
| -rw-r--r-- | theories7/Sorting/Permutation.v | 111 | ||||
| -rw-r--r-- | theories7/Sorting/Sorting.v | 117 |
3 files changed, 451 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. diff --git a/theories7/Sorting/Permutation.v b/theories7/Sorting/Permutation.v new file mode 100644 index 00000000..46b8da00 --- /dev/null +++ b/theories7/Sorting/Permutation.v @@ -0,0 +1,111 @@ +(************************************************************************) +(* 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: Permutation.v,v 1.1.2.1 2004/07/16 19:31:41 herbelin Exp $ i*) + +Require Relations. +Require PolyList. +Require Multiset. + +Set Implicit Arguments. + +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 x y)}. +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 : default. +Hints Immediate eqA_dec leA_dec leA_antisym : default. + +Local emptyBag := (EmptyBag A). +Local singletonBag := (SingletonBag eqA_dec). + +(** contents of a list *) + +Fixpoint list_contents [l:(list A)] : (multiset A) := + Cases l of + nil => emptyBag + | (cons a l) => (munion (singletonBag a) (list_contents l)) + end. + +Lemma list_contents_app : (l,m:(list A)) + (meq (list_contents (app l m)) (munion (list_contents l) (list_contents m))). +Proof. +Induction l; Simpl; Auto with datatypes. +Intros. +Apply meq_trans with + (munion (singletonBag a) (munion (list_contents l0) (list_contents m))); Auto with datatypes. +Qed. +Hints Resolve list_contents_app. + +Definition permutation := [l,m:(list A)](meq (list_contents l) (list_contents m)). + +Lemma permut_refl : (l:(list A))(permutation l l). +Proof. +Unfold permutation; Auto with datatypes. +Qed. +Hints Resolve permut_refl. + +Lemma permut_tran : (l,m,n:(list A)) + (permutation l m) -> (permutation m n) -> (permutation l n). +Proof. +Unfold permutation; Intros. +Apply meq_trans with (list_contents m); Auto with datatypes. +Qed. + +Lemma permut_right : (l,m:(list A)) + (permutation l m) -> (a:A)(permutation (cons a l) (cons a m)). +Proof. +Unfold permutation; Simpl; Auto with datatypes. +Qed. +Hints Resolve permut_right. + +Lemma permut_app : (l,l',m,m':(list A)) + (permutation l l') -> (permutation m m') -> + (permutation (app l m) (app l' m')). +Proof. +Unfold permutation; 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. +Hints Resolve permut_app. + +Lemma permut_cons : (l,m:(list A))(permutation l m) -> + (a:A)(permutation (cons a l) (cons a m)). +Proof. +Intros l m H a. +Change (permutation (app (cons a (nil A)) l) (app (cons a (nil A)) m)). +Apply permut_app; Auto with datatypes. +Qed. +Hints Resolve permut_cons. + +Lemma permut_middle : (l,m:(list A)) + (a:A)(permutation (cons a (app l m)) (app l (cons a m))). +Proof. +Unfold permutation. +Induction l; Simpl; Auto with datatypes. +Intros. +Apply meq_trans with (munion (singletonBag a) + (munion (singletonBag a0) (list_contents (app l0 m)))); Auto with datatypes. +Apply munion_perm_left; Auto with datatypes. +Qed. +Hints Resolve permut_middle. + +End defs. +Unset Implicit Arguments. + diff --git a/theories7/Sorting/Sorting.v b/theories7/Sorting/Sorting.v new file mode 100644 index 00000000..a6e38976 --- /dev/null +++ b/theories7/Sorting/Sorting.v @@ -0,0 +1,117 @@ +(************************************************************************) +(* 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: Sorting.v,v 1.1.2.1 2004/07/16 19:31:41 herbelin Exp $ i*) + +Require PolyList. +Require Multiset. +Require Permutation. +Require Relations. + +Set Implicit Arguments. + +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). + +(** [lelistA] *) + +Inductive lelistA [a:A] : (list A) -> Prop := + nil_leA : (lelistA a (nil A)) + | cons_leA : (b:A)(l:(list A))(leA a b)->(lelistA a (cons b l)). +Hint constr_lelistA := Constructors lelistA. + +Lemma lelistA_inv : (a,b:A)(l:(list A)) + (lelistA a (cons 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 A)) + | cons_sort : (a:A)(l:(list A))(sort l) -> (lelistA a l) -> (sort (cons a l)). +Hint constr_sort := Constructors sort. + +Lemma sort_inv : (a:A)(l:(list A))(sort (cons a l))->(sort l) /\ (lelistA a l). +Proof. +Intros; Inversion H; Auto with datatypes. +Qed. + +Lemma sort_rec : (P:(list A)->Set) + (P (nil A)) -> + ((a:A)(l:(list A))(sort l)->(P l)->(lelistA a l)->(P (cons a l))) -> + (y:(list A))(sort y) -> (P y). +Proof. +Induction y; Auto with datatypes. +Intros; Elim (!sort_inv a l); Auto with datatypes. +Qed. + +(** merging two sorted lists *) + +Inductive merge_lem [l1:(list A);l2:(list A)] : Set := + merge_exist : (l:(list A))(sort l) -> + (meq (list_contents eqA_dec l) + (munion (list_contents eqA_dec l1) (list_contents eqA_dec l2))) -> + ((a:A)(lelistA a l1)->(lelistA a l2)->(lelistA a l)) -> + (merge_lem l1 l2). + +Lemma merge : (l1:(list A))(sort l1)->(l2:(list A))(sort l2)->(merge_lem l1 l2). +Proof. + Induction 1; Intros. + Apply merge_exist with l2; Auto with datatypes. + Elim H3; Intros. + Apply merge_exist with (cons a l); Simpl; Auto with datatypes. + Elim (leA_dec a a0); Intros. + +(* 1 (leA a a0) *) + Cut (merge_lem l (cons a0 l0)); Auto with datatypes. + Intros (l3, l3sorted, l3contents, Hrec). + Apply merge_exist with (cons a l3); Simpl; Auto with datatypes. + Apply meq_trans with (munion (singletonBag a) + (munion (list_contents eqA_dec l) + (list_contents eqA_dec (cons 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; Intros. + Apply merge_exist with (cons a0 l3); Simpl; 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. + +End defs. + +Unset Implicit Arguments. +Hint constr_sort : datatypes v62 := Constructors sort. +Hint constr_lelistA : datatypes v62 := Constructors lelistA. |