diff options
Diffstat (limited to 'theories/Sorting/Sorting.v')
| -rw-r--r-- | theories/Sorting/Sorting.v | 123 |
1 files changed, 123 insertions, 0 deletions
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 |