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/PermutSetoid.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/PermutSetoid.v')
-rw-r--r-- | theories/Sorting/PermutSetoid.v | 338 |
1 files changed, 308 insertions, 30 deletions
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index 1f1ecddcd..203e212b6 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -8,23 +8,201 @@ (*i $Id$ i*) -Require Import Omega Relations Multiset Permutation SetoidList. +Require Import Omega Relations Multiset SetoidList. -Set Implicit Arguments. +(** This file is deprecated, use [Permutation.v] instead. + + Indeed, this file defines a notion of permutation based on + multisets (there exists a permutation between two lists iff every + elements have the same multiplicity in the two lists) which + requires a more complex apparatus (the equipment of the domain + with a decidable equality) than [Permutation] in [Permutation.v]. -(** This file contains additional results about permutations - with respect to a setoid equality (i.e. an equivalence relation). + The relation between the two relations are in lemma + [permutation_Permutation]. + + File [PermutEq] concerns Leibniz equality : it shows in particular + that [List.Permutation] and [permutation] are equivalent in this context. *) -Section Perm. +Set Implicit Arguments. + +Local Notation "[ ]" := nil. +Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..). + +Section Permut. + +(** * From lists to multisets *) Variable A : Type. Variable eqA : relation A. Hypothesis eqA_equiv : Equivalence eqA. Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}. -Notation permutation := (permutation _ eqA_dec). -Notation list_contents := (list_contents _ eqA_dec). +Let emptyBag := EmptyBag A. +Let singletonBag := SingletonBag _ eqA_dec. + +(** contents of a list *) + +Fixpoint list_contents (l:list A) : multiset A := + match l with + | [] => 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. + +(** * [permutation]: definition and basic properties *) + +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. + +Lemma permut_sym : + forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1. +Proof. + unfold permutation, meq; intros; apply sym_eq; trivial. +Qed. + +Lemma permut_trans : + 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_cons_eq : + forall l m:list A, + permutation l m -> forall a a', eqA a a' -> permutation (a :: l) (a' :: m). +Proof. + unfold permutation; simpl; intros. + apply meq_trans with (munion (singletonBag a') (list_contents l)). + apply meq_left, meq_singleton; auto. + auto with datatypes. +Qed. + +Lemma permut_cons : + forall l m:list A, + permutation l m -> forall a:A, permutation (a :: l) (a :: m). +Proof. + unfold permutation; simpl; auto with datatypes. +Qed. + +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 using permut_cons, list_contents_app with datatypes. + apply meq_trans with (munion (list_contents l') (list_contents m')); + auto using permut_cons, list_contents_app with datatypes. + apply meq_trans with (munion (list_contents l') (list_contents m)); + auto using permut_cons, list_contents_app with datatypes. +Qed. + +Lemma permut_add_inside_eq : + forall a a' l1 l2 l3 l4, eqA a a' -> + permutation (l1 ++ l2) (l3 ++ l4) -> + permutation (l1 ++ a :: l2) (l3 ++ a' :: l4). +Proof. + unfold permutation, meq in *; intros. + specialize H0 with a0. + repeat rewrite list_contents_app in *; simpl in *. + destruct (eqA_dec a a0) as [Ha|Ha]; rewrite H in Ha; + decide (eqA_dec a' a0) with Ha; simpl; auto with arith. + do 2 rewrite <- plus_n_Sm; f_equal; auto. +Qed. + +Lemma permut_add_inside : + forall a l1 l2 l3 l4, + permutation (l1 ++ l2) (l3 ++ l4) -> + permutation (l1 ++ a :: l2) (l3 ++ a :: l4). +Proof. + unfold permutation, meq in *; intros. + generalize (H a0); clear H. + do 4 rewrite list_contents_app. + simpl. + destruct (eqA_dec a a0); simpl; auto with arith. + do 2 rewrite <- plus_n_Sm; f_equal; auto. +Qed. + +Lemma permut_add_cons_inside_eq : + forall a a' l l1 l2, eqA a a' -> + permutation l (l1 ++ l2) -> + permutation (a :: l) (l1 ++ a' :: l2). +Proof. + intros; + replace (a :: l) with ([] ++ a :: l); trivial; + apply permut_add_inside_eq; trivial. +Qed. + +Lemma permut_add_cons_inside : + forall a l l1 l2, + permutation l (l1 ++ l2) -> + permutation (a :: l) (l1 ++ a :: l2). +Proof. + intros; + replace (a :: l) with ([] ++ a :: l); trivial; + apply permut_add_inside; trivial. +Qed. + +Lemma permut_middle : + forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m). +Proof. + intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl. +Qed. + +Lemma permut_sym_app : + forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1). +Proof. + intros l1 l2; + unfold permutation, meq; + intro a; do 2 rewrite list_contents_app; simpl; + auto with arith. +Qed. + +Lemma permut_rev : + forall l, permutation l (rev l). +Proof. + induction l. + simpl; trivial using permut_refl. + simpl. + apply permut_add_cons_inside. + rewrite <- app_nil_end. trivial. +Qed. + +(** * Some inversion results. *) +Lemma permut_conv_inv : + forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2. +Proof. + intros e l1 l2; unfold permutation, meq; simpl; intros H a; + generalize (H a); apply plus_reg_l. +Qed. + +Lemma permut_app_inv1 : + forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2. +Proof. + intros l l1 l2; unfold permutation, meq; simpl; + intros H a; generalize (H a); clear H. + do 2 rewrite list_contents_app. + simpl. + intros; apply plus_reg_l with (multiplicity (list_contents l) a). + rewrite plus_comm; rewrite H; rewrite plus_comm. + trivial. +Qed. (** we can use [multiplicity] to define [InA] and [NoDupA]. *) @@ -35,6 +213,39 @@ Proof. contradict NEQ; auto. Qed. +Lemma permut_app_inv2 : + forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2. +Proof. + intros l l1 l2; unfold permutation, meq; simpl; + intros H a; generalize (H a); clear H. + do 2 rewrite list_contents_app. + simpl. + intros; apply plus_reg_l with (multiplicity (list_contents l) a). + trivial. +Qed. + +Lemma permut_remove_hd_eq : + forall l l1 l2 a b, eqA a b -> + permutation (a :: l) (l1 ++ b :: l2) -> permutation l (l1 ++ l2). +Proof. + unfold permutation, meq; simpl; intros l l1 l2 a b Heq H a0. + specialize H with a0. + rewrite list_contents_app in *; simpl in *. + apply plus_reg_l with (if eqA_dec a a0 then 1 else 0). + rewrite H; clear H. + symmetry; rewrite plus_comm, <- ! plus_assoc; f_equal. + rewrite plus_comm. + destruct (eqA_dec a a0) as [Ha|Ha]; rewrite Heq in Ha; + decide (eqA_dec b a0) with Ha; reflexivity. +Qed. + +Lemma permut_remove_hd : + forall l l1 l2 a, + permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2). +Proof. + eauto using permut_remove_hd_eq, Equivalence_Reflexive. +Qed. + Fact if_eqA_else : forall a a' (B:Type)(b b':B), ~eqA a a' -> (if eqA_dec a a' then b else b') = b'. Proof. @@ -137,14 +348,13 @@ Proof. destruct (eqA_dec a a0); simpl; auto with *. Qed. - (** Permutation is compatible with InA. *) Lemma permut_InA_InA : forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2. Proof. intros l1 l2 e. do 2 rewrite multiplicity_InA. - unfold Permutation.permutation, meq. + unfold permutation, meq. intros H;rewrite H; auto. Qed. @@ -156,7 +366,7 @@ Qed. (** Permutation of an empty list. *) Lemma permut_nil : - forall l, permutation l nil -> l = nil. + forall l, permutation l [] -> l = []. Proof. intro l; destruct l as [ | e l ]; trivial. assert (InA eqA e (e::l)) by (auto with *). @@ -167,16 +377,16 @@ Qed. (** Permutation for short lists. *) Lemma permut_length_1: - forall a b, permutation (a :: nil) (b :: nil) -> eqA a b. + forall a b, permutation [a] [b] -> eqA a b. Proof. - intros a b; unfold Permutation.permutation, meq. + intros a b; unfold permutation, meq. intro P; specialize (P b); simpl in *. rewrite if_eqA_refl in *. destruct (eqA_dec a b); simpl; auto; discriminate. Qed. Lemma permut_length_2 : - forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) -> + forall a1 b1 a2 b2, permutation [a1; b1] [a2; b2] -> (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1). Proof. intros a1 b1 a2 b2 P. @@ -214,8 +424,8 @@ Proof. rewrite <- app_length. apply IHl1. apply permut_remove_hd with b. - apply permut_tran with (a::l1); auto. - revert H1; unfold Permutation.permutation, meq; simpl. + apply permut_trans with (a::l1); auto. + revert H1; unfold permutation, meq; simpl. intros; f_equal; auto. rewrite (@if_eqA_rewrite_l a b a0); auto. Qed. @@ -232,32 +442,39 @@ Proof. destruct 3; omega. Qed. +End Permut. -Variable B : Type. -Variable eqB : B->B->Prop. -Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }. -Variable eqB_trans : Transitive eqB. +Section Permut_map. + +Variables A B : Type. +Variable eqA : relation A. +Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}. +Hypothesis eqA_equiv : Equivalence eqA. + +Variable eqB : B->B->Prop. +Hypothesis eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }. +Hypothesis eqB_trans : Transitive eqB. (** Permutation is compatible with map. *) Lemma permut_map : forall f, (Proper (eqA==>eqB) f) -> - forall l1 l2, permutation l1 l2 -> - Permutation.permutation _ eqB_dec (map f l1) (map f l2). + forall l1 l2, permutation _ eqA_dec l1 l2 -> + permutation _ eqB_dec (map f l1) (map f l2). Proof. intros f; induction l1. - intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl. + intros l2 P; rewrite (permut_nil eqA_equiv (permut_sym P)); apply permut_refl. intros l2 P. simpl. - assert (H0:=permut_cons_InA P). + assert (H0:=permut_cons_InA eqA_equiv P). destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))). subst l2. rewrite map_app. simpl. - apply permut_tran with (f b :: map f l1). - revert H1; unfold Permutation.permutation, meq; simpl. + apply permut_trans with (f b :: map f l1). + revert H1; unfold permutation, meq; simpl. intros; f_equal; auto. destruct (eqB_dec (f b) a0) as [H2|H2]; destruct (eqB_dec (f a) a0) as [H3|H3]; auto. @@ -266,11 +483,72 @@ Proof. apply permut_add_cons_inside. rewrite <- map_app. apply IHl1; auto. - apply permut_remove_hd with b. - apply permut_tran with (a::l1); auto. - revert H1; unfold Permutation.permutation, meq; simpl. + apply permut_remove_hd with b; trivial. + apply permut_trans with (a::l1); auto. + revert H1; unfold permutation, meq; simpl. intros; f_equal; auto. - rewrite (@if_eqA_rewrite_l a b a0); auto. + rewrite (@if_eqA_rewrite_l _ _ eqA_equiv eqA_dec a b a0); auto. +Qed. + +End Permut_map. + +Require Import Permutation TheoryList. + +Section Permut_permut. + +Variable A : Type. + +Variable eqA : relation A. +Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}. +Hypothesis eqA_equiv : Equivalence eqA. + +Lemma Permutation_impl_permutation : forall l l', + Permutation l l' -> permutation _ eqA_dec l l'. +Proof. + induction 1. + apply permut_refl. + apply permut_cons; auto using Equivalence_Reflexive. + change (x :: y :: l) with ([x] ++ y :: l); + apply permut_add_cons_inside; simpl; + apply permut_cons_eq; auto using Equivalence_Reflexive, permut_refl. + apply permut_trans with l'; trivial. Qed. -End Perm. +Lemma permut_eqA : forall l l', Forall2 eqA l l' -> permutation _ eqA_dec l l'. +Proof. + induction 1. + apply permut_refl. + apply permut_cons_eq; trivial. +Qed. + +Lemma permutation_Permutation : forall l l', + permutation _ eqA_dec l l' <-> + exists l'', Permutation l l'' /\ Forall2 eqA l'' l'. +Proof. + split; intro H. + (* -> *) + induction l in l', H |- *. + exists []; apply permut_sym, permut_nil in H as ->; auto using Forall2. + pose proof H as H'. + apply permut_cons_InA, InA_split in H + as (l1 & y & l2 & Heq & ->); trivial. + apply permut_remove_hd_eq, IHl in H' + as (l'' & IHP & IHA); clear IHl; trivial. + apply Forall2_app_inv_r in IHA as (l1'' & l2'' & Hl1 & Hl2 & ->). + exists (l1'' ++ a :: l2''); split. + apply Permutation_cons_app; trivial. + apply Forall2_app, Forall2_cons; trivial. + (* <- *) + destruct H as (l'' & H & Heq). + apply permut_trans with l''. + apply Permutation_impl_permutation; trivial. + apply permut_eqA; trivial. +Qed. + +End Permut_permut. + +(* begin hide *) +(** For compatibilty *) +Notation permut_right := permut_cons (only parsing). +Notation permut_tran := permut_trans (only parsing). +(* end hide *) |