diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Sorting/Sorting.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Sorting/Sorting.v')
-rw-r--r-- | theories/Sorting/Sorting.v | 124 |
1 files changed, 3 insertions, 121 deletions
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v index aed8cd15..5f8da6a4 100644 --- a/theories/Sorting/Sorting.v +++ b/theories/Sorting/Sorting.v @@ -6,125 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Sorting.v 10698 2008-03-19 18:46:59Z letouzey $ i*) +(*i $Id$ i*) -Require Import List Multiset Permutation Relations. - -Set Implicit Arguments. - -Section defs. - - Variable A : Type. - 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). - - 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). - - 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_rect : - forall P:list A -> Type, - 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. - - 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) : Type := - 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 H2; intros. - apply merge_exist with (a :: l); simpl in |- *; auto using cons_sort with datatypes. - elim (leA_dec a a0); intros. - - (* 1 (leA a a0) *) - cut (merge_lem l (a0 :: l0)); auto using cons_sort with datatypes. - intros [l3 l3sorted l3contents Hrec]. - apply merge_exist with (a :: l3); simpl in |- *; - auto using cons_sort, cons_leA 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 X0; simpl in |- *; intros. - apply merge_exist with (a0 :: l3); simpl in |- *; - auto using cons_sort, cons_leA 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. +Require Export Sorted. +Require Export Mergesort. |