summaryrefslogtreecommitdiff
path: root/theories7/Sorting/Heap.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories7/Sorting/Heap.v')
-rw-r--r--theories7/Sorting/Heap.v223
1 files changed, 0 insertions, 223 deletions
diff --git a/theories7/Sorting/Heap.v b/theories7/Sorting/Heap.v
deleted file mode 100644
index 63e7f324..00000000
--- a/theories7/Sorting/Heap.v
+++ /dev/null
@@ -1,223 +0,0 @@
-(************************************************************************)
-(* 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 08:25:51 +0000