diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-13 21:23:17 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-13 21:23:17 +0000 |
commit | f698148f6aee01a207ce5ddd4bebf19da2108bff (patch) | |
tree | 54a1ddbec7c5cd5fe326e2e90d6a45317270aad8 /theories/Sorting/Sorting.v | |
parent | ebc3fe11bc68ac517ff6203504c3d1d4640f8259 (diff) |
Addition of mergesort + cleaning of the Sorting library
- New (modular) mergesort purely using structural recursion
- Move of the (complex) notion of permutation up to setoid equality
formerly defined in Permutation.v to file PermutSetoid.v
- Re-use of the file Permutation.v for making the canonical notion
of permutation that was in List.v more visible
- New file Sorted.v that contains two definitions of sorted:
"Sorted" is a renaming of "sort" that was defined in file
Sorting.v and "StronglySorted" is the intuitive notion of sorted
(there is also LocallySorted which is a variant of Sorted)
- File Sorting.v is replaced by a call to the main Require of the directory
- The merge function whose specification rely on counting elements is moved
to Heap.v and both are stamped deprecated (the sort defined in
Heap.v has complexity n^2 in worst case)
- Added some new naming conventions
- Removed uselessly-maximal implicit arguments of Forall2 predicate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12585 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Sorting/Sorting.v')
-rw-r--r-- | theories/Sorting/Sorting.v | 122 |
1 files changed, 2 insertions, 120 deletions
diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v index 2d76b25a2..5f8da6a4d 100644 --- a/theories/Sorting/Sorting.v +++ b/theories/Sorting/Sorting.v @@ -8,123 +8,5 @@ (*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. |