diff options
Diffstat (limited to 'theories/Sorting')
-rw-r--r-- | theories/Sorting/Heap.v | 227 | ||||
-rw-r--r-- | theories/Sorting/Permutation.v | 120 | ||||
-rw-r--r-- | theories/Sorting/Sorting.v | 123 |
3 files changed, 470 insertions, 0 deletions
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v new file mode 100644 index 00000000..41594749 --- /dev/null +++ b/theories/Sorting/Heap.v @@ -0,0 +1,227 @@ +(************************************************************************) +(* 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.3.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +(** A development of Treesort on Heap trees *) + +(* G. Huet 1-9-95 uses Multiset *) + +Require Import List. +Require Import Multiset. +Require Import Permutation. +Require Import Relations. +Require Import Sorting. + + +Section defs. + +Variable A : Set. +Variable leA : relation A. +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. +Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z. +Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y. + +Hint Resolve leA_refl. +Hint Immediate eqA_dec leA_dec leA_antisym. + +Let emptyBag := EmptyBag A. +Let 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) := + match t with + | Tree_Leaf => True + | Tree_Node b T1 T2 => leA a b + end. + +Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf. +Proof. +simpl in |- *; auto with datatypes. +Qed. + +Lemma leA_Tree_Node : + forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D). +Proof. +simpl in |- *; auto with datatypes. +Qed. + +Hint 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 : + forall (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 Constructors is_heap. + +Lemma invert_heap : + forall (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 : + forall P:Tree -> Set, + P Tree_Leaf -> + (forall (a:A) (T1 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)) -> + forall T:Tree, is_heap T -> P T. +Proof. +simple 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 : + forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T. +Proof. +simple induction T; auto with datatypes. +intros; simpl in |- *; 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 := + match t with + | 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 : + forall T1:Tree, + is_heap T1 -> + meq (contents T1) (munion (contents T) (singletonBag a)) -> + (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) -> + insert_spec a T. + + +Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T. +Proof. +simple induction 1; intros. +apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf); + auto with datatypes. +simpl in |- *; unfold meq, munion in |- *; 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 in |- *; 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 in |- *; apply treesort_twist2; trivial with datatypes. +Qed. + +(** building a heap from a list *) + +Inductive build_heap (l:list A) : Set := + heap_exist : + 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. +apply (heap_exist nil Tree_Leaf); auto with datatypes. +simpl in |- *; unfold meq in |- *; auto with datatypes. +simple induction 1. +intros T i m; elim (insert T i a). +intros; apply heap_exist with T1; simpl in |- *; 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 : + forall l:list A, + sort leA l -> + (forall 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 : forall T:Tree, is_heap T -> flat_spec T. +Proof. + intros T h; elim h; intros. + apply flat_exist with (nil (A:=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 (a :: l); simpl in |- *; 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 : + forall l:list A, {m : list A | sort leA m & permutation _ eqA_dec l m}. +Proof. + intro l; unfold permutation in |- *. + 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.
\ No newline at end of file diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v new file mode 100644 index 00000000..43a0f0bc --- /dev/null +++ b/theories/Sorting/Permutation.v @@ -0,0 +1,120 @@ +(************************************************************************) +(* 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.4.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +Require Import Relations. +Require Import List. +Require Import Multiset. + +Set Implicit Arguments. + +Section defs. + +Variable A : Set. +Variable leA : relation A. +Variable eqA : relation A. + +Let gtA (x y:A) := ~ leA x y. + +Hypothesis leA_dec : forall x y:A, {leA x y} + {~ leA x y}. +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. +Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z. +Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y. + +Hint Resolve leA_refl: default. +Hint Immediate eqA_dec leA_dec leA_antisym: default. + +Let emptyBag := EmptyBag A. +Let singletonBag := SingletonBag _ eqA_dec. + +(** contents of a list *) + +Fixpoint list_contents (l:list A) : multiset A := + match l with + | nil => emptyBag + | a :: l => munion (singletonBag a) (list_contents l) + end. + +Lemma list_contents_app : + forall l m:list A, + meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)). +Proof. +simple induction l; simpl in |- *; auto with datatypes. +intros. +apply meq_trans with + (munion (singletonBag a) (munion (list_contents l0) (list_contents m))); + auto with datatypes. +Qed. +Hint Resolve list_contents_app. + +Definition permutation (l m:list A) := + meq (list_contents l) (list_contents m). + +Lemma permut_refl : forall l:list A, permutation l l. +Proof. +unfold permutation in |- *; auto with datatypes. +Qed. +Hint Resolve permut_refl. + +Lemma permut_tran : + forall l m n:list A, permutation l m -> permutation m n -> permutation l n. +Proof. +unfold permutation in |- *; intros. +apply meq_trans with (list_contents m); auto with datatypes. +Qed. + +Lemma permut_right : + forall l m:list A, + permutation l m -> forall a:A, permutation (a :: l) (a :: m). +Proof. +unfold permutation in |- *; simpl in |- *; auto with datatypes. +Qed. +Hint Resolve permut_right. + +Lemma permut_app : + forall l l' m m':list A, + permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m'). +Proof. +unfold permutation in |- *; 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. +Hint Resolve permut_app. + +Lemma permut_cons : + forall l m:list A, + permutation l m -> forall a:A, permutation (a :: l) (a :: m). +Proof. +intros l m H a. +change (permutation ((a :: nil) ++ l) ((a :: nil) ++ m)) in |- *. +apply permut_app; auto with datatypes. +Qed. +Hint Resolve permut_cons. + +Lemma permut_middle : + forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m). +Proof. +unfold permutation in |- *. +simple induction l; simpl in |- *; auto with datatypes. +intros. +apply meq_trans with + (munion (singletonBag a) + (munion (singletonBag a0) (list_contents (l0 ++ m)))); + auto with datatypes. +apply munion_perm_left; auto with datatypes. +Qed. +Hint Resolve permut_middle. + +End defs. +Unset Implicit Arguments. diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v new file mode 100644 index 00000000..aa829fea --- /dev/null +++ b/theories/Sorting/Sorting.v @@ -0,0 +1,123 @@ +(************************************************************************) +(* 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.4.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +Require Import List. +Require Import Multiset. +Require Import Permutation. +Require Import Relations. + +Set Implicit Arguments. + +Section defs. + +Variable A : Set. +Variable leA : relation A. +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. +Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z. +Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y. + +Hint Resolve leA_refl. +Hint Immediate eqA_dec leA_dec leA_antisym. + +Let emptyBag := EmptyBag A. +Let singletonBag := SingletonBag _ eqA_dec. + +(** [lelistA] *) + +Inductive lelistA (a:A) : list A -> Prop := + | nil_leA : lelistA a nil + | cons_leA : forall (b:A) (l:list A), leA a b -> lelistA a (b :: l). +Hint Constructors lelistA. + +Lemma lelistA_inv : forall (a b:A) (l:list A), lelistA a (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 + | cons_sort : + forall (a:A) (l:list A), sort l -> lelistA a l -> sort (a :: l). +Hint Constructors sort. + +Lemma sort_inv : + forall (a:A) (l:list A), sort (a :: l) -> sort l /\ lelistA a l. +Proof. +intros; inversion H; auto with datatypes. +Qed. + +Lemma sort_rec : + forall P:list A -> Set, + P nil -> + (forall (a:A) (l:list A), sort l -> P l -> lelistA a l -> P (a :: l)) -> + forall y:list A, sort y -> P y. +Proof. +simple induction y; auto with datatypes. +intros; elim (sort_inv (a:=a) (l:=l)); auto with datatypes. +Qed. + +(** merging two sorted lists *) + +Inductive merge_lem (l1 l2:list A) : Set := + merge_exist : + forall l:list A, + sort l -> + meq (list_contents _ eqA_dec l) + (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) -> + (forall a:A, lelistA a l1 -> lelistA a l2 -> lelistA a l) -> + merge_lem l1 l2. + +Lemma merge : + forall l1:list A, sort l1 -> forall l2:list A, sort l2 -> merge_lem l1 l2. +Proof. + simple induction 1; intros. + apply merge_exist with l2; auto with datatypes. + elim H3; intros. + apply merge_exist with (a :: l); simpl in |- *; auto with datatypes. + elim (leA_dec a a0); intros. + +(* 1 (leA a a0) *) + cut (merge_lem l (a0 :: l0)); auto with datatypes. + intros [l3 l3sorted l3contents Hrec]. + apply merge_exist with (a :: l3); simpl in |- *; auto 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 lelistA_inv with l; trivial with datatypes. + +(* 2 (leA a0 a) *) + elim H5; simpl in |- *; intros. + apply merge_exist with (a0 :: l3); simpl in |- *; 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 Constructors sort: datatypes v62. +Hint Constructors lelistA: datatypes v62.
\ No newline at end of file |