From f698148f6aee01a207ce5ddd4bebf19da2108bff Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 13 Dec 2009 21:23:17 +0000 Subject: 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 --- theories/Sorting/Heap.v | 67 ++++- theories/Sorting/Mergesort.v | 279 ++++++++++++++++++++ theories/Sorting/PermutEq.v | 32 +-- theories/Sorting/PermutSetoid.v | 338 ++++++++++++++++++++++--- theories/Sorting/Permutation.v | 547 ++++++++++++++++++++++++++-------------- theories/Sorting/Sorted.v | 154 +++++++++++ theories/Sorting/Sorting.v | 122 +-------- theories/Sorting/vo.itarget | 4 +- 8 files changed, 1175 insertions(+), 368 deletions(-) create mode 100644 theories/Sorting/Mergesort.v create mode 100644 theories/Sorting/Sorted.v (limited to 'theories/Sorting') diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 6d5564ed7..4124ef983 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -8,11 +8,15 @@ (*i $Id$ i*) -(** A development of Treesort on Heap trees *) +(** This file is deprecated, for a tree on list, use [Mergesort.v]. *) + +(** A development of Treesort on Heap trees. It has an average + complexity of O(n.log n) but of O(n²) in the worst case (e.g. if + the list is already sorted) *) (* G. Huet 1-9-95 uses Multiset *) -Require Import List Multiset Permutation Relations Sorting. +Require Import List Multiset PermutSetoid Relations Sorting. Section defs. @@ -122,6 +126,54 @@ Section defs. intros; simpl in |- *; apply leA_trans with b; auto with datatypes. Qed. + (** ** Merging two sorted lists *) + + Inductive merge_lem (l1 l2:list A) : Type := + merge_exist : + forall l:list A, + Sorted leA l -> + meq (list_contents _ eqA_dec l) + (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) -> + (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) -> + merge_lem l1 l2. + + Lemma merge : + forall l1:list A, Sorted leA l1 -> + forall l2:list A, Sorted leA 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 (@HdRel_inv _ leA) 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 HdRel_inv with (l:=l0); trivial with datatypes. + Qed. + (** ** From trees to multisets *) @@ -208,8 +260,8 @@ Section defs. Inductive flat_spec (T:Tree) : Type := flat_exist : forall l:list A, - sort leA l -> - (forall a:A, leA_Tree a T -> lelistA leA a l) -> + Sorted leA l -> + (forall a:A, leA_Tree a T -> HdRel 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. @@ -217,7 +269,7 @@ Section defs. intros T h; elim h; intros. apply flat_exist with (nil (A:=A)); auto with datatypes. elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2. - elim (merge _ leA_dec eqA_dec s1 s2); intros. + elim (merge _ s1 _ s2); intros. apply flat_exist with (a :: l); simpl in |- *; auto with datatypes. apply meq_trans with (munion (list_contents _ eqA_dec l1) @@ -234,7 +286,8 @@ Section defs. (** * Specification of treesort *) Theorem treesort : - forall l:list A, {m : list A | sort leA m & permutation _ eqA_dec l m}. + forall l:list A, + {m : list A | Sorted leA m & permutation _ eqA_dec l m}. Proof. intro l; unfold permutation in |- *. elim (list_to_heap l). @@ -245,4 +298,4 @@ Section defs. apply meq_trans with (contents T); trivial with datatypes. Qed. -End defs. \ No newline at end of file +End defs. diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v new file mode 100644 index 000000000..723bb76d3 --- /dev/null +++ b/theories/Sorting/Mergesort.v @@ -0,0 +1,279 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* -> Sortclass. + +(** A total relation *) + +Module Type TotalOrder. + Parameter A : Type. + Parameter le_bool : A -> A -> bool. + Infix "<=?" := le_bool (at level 35). + Axiom le_bool_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1. +End TotalOrder. + +(** The main module defining [mergesort] on a given total order. + We require minimal hypotheses + *) + +Module Sort (Import X:TotalOrder). + +Fixpoint merge l1 l2 := + let fix merge_aux l2 := + match l1, l2 with + | [], _ => l2 + | _, [] => l1 + | a1::l1', a2::l2' => + if a1 <=? a2 then a1 :: merge l1' l2 else a2 :: merge_aux l2' + end + in merge_aux l2. + +(** We implement mergesort using an explicit stack of pending mergings. + Pending merging are represented like a binary number where digits are + either None (denoting 0) or Some list to merge (denoting 1). The n-th + digit represents the pending list to be merged at level n, if any. + Merging a list to a stack is like adding 1 to the binary number + represented by the stack but the carry is propagated by merging the + lists. In practice, when used in mergesort, the n-th digit, if non 0, + carries a list of length 2^n. For instance, adding singleton list + [3] to the stack Some [4]::Some [2;6]::None::Some [1;3;5;5] + reduces to propagate the carry [3;4] (resulting of the merge of [3] + and [4]) to the list Some [2;6]::None::Some [1;3;5;5], which reduces + to propagating the carry [2;3;4;6] (resulting of the merge of [3;4] and + [2;6]) to the list None::Some [1;3;5;5], which locally produces + Some [2;3;4;6]::Some [1;3;5;5], i.e. which produces the final result + None::None::Some [2;3;4;6]::Some [1;3;5;5]. + + For instance, here is how [6;2;3;1;5] is sorted: + + operation stack list + iter_merge [] [6;2;3;1;5] + = append_list_to_stack [ + [6]] [2;3;1;5] + -> iter_merge [[6]] [2;3;1;5] + = append_list_to_stack [[6] + [2]] [3;1;5] + = append_list_to_stack [ + [2;6];] [3;1;5] + -> iter_merge [[2;6];] [3;1;5] + = append_list_to_stack [[2;6]; + [3]] [1;5] + -> merge_list [[2;6];[3]] [1;5] + = append_list_to_stack [[2;6];[3] + [1] [5] + = append_list_to_stack [[2;6] + [1;3];] [5] + = append_list_to_stack [ + [1;2;3;6];;] [5] + -> merge_list [[1;2;3;6];;] [5] + = append_list_to_stack [[1;2;3;6];; + [5]] [] + -> merge_stack [[1;2;3;6];;[5]] + = [1;2;3;5;6] + + The complexity of the algorithm is n*log n, since there are + 2^(p-1) mergings to do of length 2, 2^(p-2) of length 4, ..., 2^0 + of length 2^p for a list of length 2^p. The algorithm does not need + explicitly cutting the list in 2 parts at each step since it the + successive accumulation of fragments on the stack which ensures + that lists are merged on a dichotomic basis. +*) + +Fixpoint merge_list_to_stack stack l := + match stack with + | [] => [Some l] + | None :: stack' => Some l :: stack' + | Some l' :: stack' => None :: merge_list_to_stack stack' (merge l' l) + end. + +Fixpoint merge_stack stack := + match stack with + | [] => [] + | None :: stack' => merge_stack stack' + | Some l :: stack' => merge l (merge_stack stack') + end. + +Fixpoint iter_merge stack l := + match l with + | [] => merge_stack stack + | a::l' => iter_merge (merge_list_to_stack stack [a]) l' + end. + +Definition sort := iter_merge []. + +(** The proof of correctness *) + +Local Notation Sorted := (LocallySorted le_bool) (only parsing). + +Fixpoint SortedStack stack := + match stack with + | [] => True + | None :: stack' => SortedStack stack' + | Some l :: stack' => Sorted l /\ SortedStack stack' + end. + +Local Ltac invert H := inversion H; subst; clear H. + +Fixpoint flatten_stack (stack : list (option (list A))) := + match stack with + | [] => [] + | None :: stack' => flatten_stack stack' + | Some l :: stack' => l ++ flatten_stack stack' + end. + +Theorem Sorted_merge : forall l1 l2, + Sorted l1 -> Sorted l2 -> Sorted (merge l1 l2). +Proof. +induction l1; induction l2; intros; simpl; auto. + destruct (a <=? a0) as ()_eqn:Heq1. + invert H. + simpl. constructor; trivial; rewrite Heq1; constructor. + assert (Sorted (merge (b::l) (a0::l2))) by (apply IHl1; auto). + clear H0 H3 IHl1; simpl in *. + destruct (b <=? a0); constructor; auto || rewrite Heq1; constructor. + assert (a0 <=? a) by + (destruct (le_bool_total a0 a) as [H'|H']; trivial || (rewrite Heq1 in H'; inversion H')). + invert H0. + constructor; trivial. + assert (Sorted (merge (a::l1) (b::l))) by auto using IHl1. + clear IHl2; simpl in *. + destruct (a <=? b) as ()_eqn:Heq2; + constructor; auto. +Qed. + +Theorem Permuted_merge : forall l1 l2, Permutation (l1++l2) (merge l1 l2). +Proof. + induction l1; simpl merge; intro. + assert (forall l, (fix merge_aux (l0 : list A) : list A := l0) l = l) + as -> by (destruct l; trivial). (* Technical lemma *) + apply Permutation_refl. + induction l2. + rewrite app_nil_r. apply Permutation_refl. + destruct (a <=? a0). + constructor; apply IHl1. + apply Permutation_sym, Permutation_cons_app, Permutation_sym, IHl2. +Qed. + +Theorem Sorted_merge_list_to_stack : forall stack l, + SortedStack stack -> Sorted l -> SortedStack (merge_list_to_stack stack l). +Proof. + induction stack as [|[|]]; intros; simpl. + auto. + apply IHstack. destruct H as (_,H1). fold SortedStack in H1. auto. + apply Sorted_merge; auto; destruct H; auto. + auto. +Qed. + +Theorem Permuted_merge_list_to_stack : forall stack l, + Permutation (l ++ flatten_stack stack) (flatten_stack (merge_list_to_stack stack l)). +Proof. + induction stack as [|[]]; simpl; intros. + reflexivity. + rewrite app_assoc. + etransitivity. + apply Permutation_app_tail. + etransitivity. + apply Permutation_app_comm. + apply Permuted_merge. + apply IHstack. + reflexivity. +Qed. + +Theorem Sorted_merge_stack : forall stack, + SortedStack stack -> Sorted (merge_stack stack). +Proof. +induction stack as [|[|]]; simpl; intros. + constructor; auto. + apply Sorted_merge; tauto. + auto. +Qed. + +Theorem Permuted_merge_stack : forall stack, + Permutation (flatten_stack stack) (merge_stack stack). +Proof. +induction stack as [|[]]; simpl. + trivial. + transitivity (l ++ merge_stack stack). + apply Permutation_app_head; trivial. + apply Permuted_merge. + assumption. +Qed. + +Theorem Sorted_iter_merge : forall stack l, + SortedStack stack -> Sorted (iter_merge stack l). +Proof. + intros stack l H; induction l in stack, H |- *; simpl. + auto using Sorted_merge_stack. + assert (Sorted [a]) by constructor. + auto using Sorted_merge_list_to_stack. +Qed. + +Theorem Permuted_iter_merge : forall l stack, + Permutation (flatten_stack stack ++ l) (iter_merge stack l). +Proof. + induction l; simpl; intros. + rewrite app_nil_r. apply Permuted_merge_stack. + change (a::l) with ([a]++l). + rewrite app_assoc. + etransitivity. + apply Permutation_app_tail. + etransitivity. + apply Permutation_app_comm. + apply Permuted_merge_list_to_stack. + apply IHl. +Qed. + +Theorem Sorted_sort : forall l, Sorted (sort l). +Proof. +intro; apply Sorted_iter_merge. constructor. +Qed. + +Corollary LocallySorted_sort : forall l, Sorted.Sorted le_bool (sort l). +Proof. intro; eapply Sorted_LocallySorted_iff, Sorted_sort; auto. Qed. + +Theorem Permuted_sort : forall l, Permutation l (sort l). +Proof. +intro; apply (Permuted_iter_merge l []). +Qed. + +Corollary StronglySorted_sort : forall l, + Transitive le_bool -> StronglySorted le_bool (sort l). +Proof. auto using Sorted_StronglySorted, LocallySorted_sort. Qed. + +End Sort. + +(** An example *) + +Module NatOrder. + Definition A := nat. + Fixpoint le_bool x y := + match x, y with + | 0, _ => true + | S x', 0 => false + | S x', S y' => le_bool x' y' + end. + Infix "<=?" := le_bool (at level 35). + Theorem le_bool_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1. + Proof. + induction a1; destruct a2; simpl; auto using is_eq_true. + Qed. + +End NatOrder. + +Module Import NatSort := Sort NatOrder. + +Example SimpleMergeExample := Eval compute in sort [5;3;6;1;8;6;0]. + diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v index 9bfe31ed1..8e6aa6dce 100644 --- a/theories/Sorting/PermutEq.v +++ b/theories/Sorting/PermutEq.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require Import Omega Relations Setoid List Multiset Permutation. +Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation. Set Implicit Arguments. @@ -31,19 +31,9 @@ Section Perm. Lemma multiplicity_In : forall l a, In a l <-> 0 < multiplicity (list_contents l) a. Proof. - induction l. - simpl. - split; inversion 1. - simpl. - split; intros. - inversion_clear H. - subst a0. - destruct (eq_dec a a) as [_|H]; auto with arith; destruct H; auto. - destruct (eq_dec a a0) as [H1|H1]; auto with arith; simpl. - rewrite <- IHl; auto. - destruct (eq_dec a a0); auto. - simpl in H. - right; rewrite IHl; auto. + intros; split; intro H. + eapply In_InA, multiplicity_InA in H; eauto with typeclass_instances. + eapply multiplicity_InA, InA_alt in H as (y & -> & H); eauto with typeclass_instances. Qed. Lemma multiplicity_In_O : @@ -102,7 +92,7 @@ Section Perm. Lemma permut_In_In : forall l1 l2 e, permutation l1 l2 -> In e l1 -> In e l2. Proof. - unfold Permutation.permutation, meq; intros l1 l2 e P IN. + unfold PermutSetoid.permutation, meq; intros l1 l2 e P IN. generalize (P e); clear P. destruct (In_dec eq_dec e l2) as [H|H]; auto. rewrite (multiplicity_In_O _ _ H). @@ -141,7 +131,7 @@ Section Perm. apply permut_cons; auto. change (permutation (y::x::l) ((x::nil)++y::l)). apply permut_add_cons_inside; simpl; apply permut_refl. - apply permut_tran with l'; auto. + apply permut_trans with l'; auto. revert l'. induction l. intros. @@ -152,7 +142,7 @@ Section Perm. subst l'. apply Permutation_cons_app. apply IHl. - apply permut_remove_hd with a; auto. + apply permut_remove_hd with a; auto with typeclass_instances. Qed. (** Permutation for short lists. *) @@ -160,7 +150,7 @@ Section Perm. Lemma permut_length_1: forall a b, permutation (a :: nil) (b :: nil) -> a=b. Proof. - intros a b; unfold Permutation.permutation, meq; intro P; + intros a b; unfold PermutSetoid.permutation, meq; intro P; generalize (P b); clear P; simpl. destruct (eq_dec b b) as [H|H]; [ | destruct H; auto]. destruct (eq_dec a b); simpl; auto; intros; discriminate. @@ -206,7 +196,7 @@ Section Perm. simpl; rewrite <- plus_n_Sm; f_equal. rewrite <- app_length. apply IHl1. - apply permut_remove_hd with a; auto. + apply permut_remove_hd with a; auto with typeclass_instances. Qed. Variable B : Type. @@ -216,7 +206,7 @@ Section Perm. Lemma permutation_map : forall f l1 l2, permutation l1 l2 -> - Permutation.permutation _ eqB_dec (map f l1) (map f l2). + PermutSetoid.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. @@ -229,7 +219,7 @@ Section Perm. apply permut_add_cons_inside. rewrite <- map_app. apply IHl1; auto. - apply permut_remove_hd with a; auto. + apply permut_remove_hd with a; auto with typeclass_instances. Qed. End Perm. 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 *) diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 27ba50908..da30d096c 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -8,198 +8,367 @@ (*i $Id$ i*) -Require Import Relations List Multiset Plus. +(*********************************************************************) +(** ** List permutations as a composition of adjacent transpositions *) +(*********************************************************************) -(** This file define a notion of permutation for lists, based on multisets: - there exists a permutation between two lists iff every elements have - the same multiplicity in the two lists. +(* Adapted in May 2006 by Jean-Marc Notin from initial contents by + Laurent Théry (Huffmann contribution, October 2003) *) - Unlike [List.Permutation], the present notion of permutation - requires the domain to be equipped with a decidable equality. This - equality allows to reason modulo the effective equivalence-class - representative used in each list. +Require Import List Setoid. - The present file contains basic results, obtained without any particular - assumption on the decidable equality used. - - File [PermutSetoid] contains additional results about permutations - with respect to an setoid equality (i.e. an equivalence relation). +Set Implicit Arguments. - Finally, file [PermutEq] concerns Coq equality : this file is similar - to the previous one, but proves in addition that [List.Permutation] - and [permutation] are equivalent in this context. -*) +Local Notation "[ ]" := nil. +Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..). -Set Implicit Arguments. +Section Permutation. -Section defs. - - (** * From lists to multisets *) - - Variable A : Type. - Variable eqA : relation A. - Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}. - - 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. - - - (** * [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_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_cons : - 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. - - 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 : - 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 : - forall a l l1 l2, - permutation l (l1 ++ l2) -> - permutation (a :: l) (l1 ++ a :: l2). - Proof. - intros; - replace (a :: l) with (nil ++ 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. - - 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 : - forall l l1 l2 a, - permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2). - Proof. - intros l l1 l2 a; unfold permutation, meq; simpl; intros H a0; generalize (H a0); clear H. - do 2 rewrite list_contents_app; simpl; intro H. - apply plus_reg_l with (if eqA_dec a a0 then 1 else 0). - rewrite H; clear H. - symmetry; rewrite plus_comm. - repeat rewrite <- plus_assoc; f_equal. - apply plus_comm. - Qed. - -End defs. - -(** For compatibilty *) -Notation permut_right := permut_cons. -Unset Implicit Arguments. +Variable A:Type. + +Inductive Permutation : list A -> list A -> Prop := +| perm_nil: Permutation [] [] +| perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l') +| perm_swap x y l : Permutation (y::x::l) (x::y::l) +| perm_trans l l' l'' : Permutation l l' -> Permutation l' l'' -> Permutation l l''. + +Hint Constructors Permutation. + +(** Some facts about [Permutation] *) + +Theorem Permutation_nil : forall (l : list A), Permutation [] l -> l = []. +Proof. + intros l HF. + remember (@nil A) as m in HF. + induction HF; discriminate || auto. +Qed. + +Theorem Permutation_nil_cons : forall (l : list A) (x : A), ~ Permutation nil (x::l). +Proof. + intros l x HF. + apply Permutation_nil in HF; discriminate. +Qed. + +(** Permutation over lists is a equivalence relation *) + +Theorem Permutation_refl : forall l : list A, Permutation l l. +Proof. + induction l; constructor. exact IHl. +Qed. + +Theorem Permutation_sym : forall l l' : list A, Permutation l l' -> Permutation l' l. +Proof. + intros l l' Hperm; induction Hperm; auto. + apply perm_trans with (l':=l'); assumption. +Qed. + +Theorem Permutation_trans : forall l l' l'' : list A, Permutation l l' -> Permutation l' l'' -> Permutation l l''. +Proof. + exact perm_trans. +Qed. + +End Permutation. + +Hint Constructors Permutation. +Hint Resolve Permutation_refl Permutation_sym Permutation_trans. + +(* This provides reflexivity, symmetry and transitivity and rewriting + on morphims to come *) + +Add Parametric Relation A : (list A) (@Permutation A) + reflexivity proved by (@Permutation_refl A) + symmetry proved by (@Permutation_sym A) + transitivity proved by (@Permutation_trans A) +as Permutation_Equivalence. + +Add Parametric Morphism A (a:A) : (cons a) + with signature @Permutation A ==> @Permutation A + as Permutation_cons. +Proof. + auto using perm_skip. +Qed. + +Section Permutation_properties. + +Variable A:Type. + +Implicit Types a b : A. +Implicit Types l m : list A. + +(** Compatibility with others operations on lists *) + +Theorem Permutation_in : forall (l l' : list A) (x : A), Permutation l l' -> In x l -> In x l'. +Proof. + intros l l' x Hperm; induction Hperm; simpl; tauto. +Qed. + +Lemma Permutation_app_tail : forall (l l' tl : list A), Permutation l l' -> Permutation (l++tl) (l'++tl). +Proof. + intros l l' tl Hperm; induction Hperm as [|x l l'|x y l|l l' l'']; simpl; auto. + eapply Permutation_trans with (l':=l'++tl); trivial. +Qed. + +Lemma Permutation_app_head : forall (l tl tl' : list A), Permutation tl tl' -> Permutation (l++tl) (l++tl'). +Proof. + intros l tl tl' Hperm; induction l; [trivial | repeat rewrite <- app_comm_cons; constructor; assumption]. +Qed. + +Theorem Permutation_app : forall (l m l' m' : list A), Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m'). +Proof. + intros l m l' m' Hpermll' Hpermmm'; induction Hpermll' as [|x l l'|x y l|l l' l'']; repeat rewrite <- app_comm_cons; auto. + apply Permutation_trans with (l' := (x :: y :: l ++ m)); + [idtac | repeat rewrite app_comm_cons; apply Permutation_app_head]; trivial. + apply Permutation_trans with (l' := (l' ++ m')); try assumption. + apply Permutation_app_tail; assumption. +Qed. + +Add Parametric Morphism : (@app A) + with signature @Permutation A ==> @Permutation A ==> @Permutation A + as Permutation_app'. + auto using Permutation_app. +Qed. + +Lemma Permutation_add_inside : forall a (l l' tl tl' : list A), + Permutation l l' -> Permutation tl tl' -> + Permutation (l ++ a :: tl) (l' ++ a :: tl'). +Proof. + intros; apply Permutation_app; auto. +Qed. + +Theorem Permutation_app_comm : forall (l l' : list A), + Permutation (l ++ l') (l' ++ l). +Proof. + induction l as [|x l]; simpl; intro l'. + rewrite app_nil_r; trivial. + induction l' as [|y l']; simpl. + rewrite app_nil_r; trivial. + transitivity (x :: y :: l' ++ l). + constructor; rewrite app_comm_cons; apply IHl. + transitivity (y :: x :: l' ++ l); constructor. + transitivity (x :: l ++ l'); auto. +Qed. + +Theorem Permutation_cons_app : forall (l l1 l2:list A) a, + Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2). +Proof. + intros l l1; revert l. + induction l1. + simpl. + intros; apply perm_skip; auto. + simpl; intros. + transitivity (a0::a::l1++l2). + apply perm_skip; auto. + transitivity (a::a0::l1++l2). + apply perm_swap; auto. + apply perm_skip; auto. +Qed. +Hint Resolve Permutation_cons_app. + +Theorem Permutation_middle : forall (l1 l2:list A) a, + Permutation (a :: l1 ++ l2) (l1 ++ a :: l2). +Proof. + auto. +Qed. + +Theorem Permutation_rev : forall (l : list A), Permutation l (rev l). +Proof. + induction l as [| x l]; simpl; trivial. + apply Permutation_trans with (l' := [x] ++ rev l). + simpl; auto. + apply Permutation_app_comm. +Qed. + +Theorem Permutation_length : forall (l l' : list A), Permutation l l' -> length l = length l'. +Proof. + intros l l' Hperm; induction Hperm; simpl; auto. + apply trans_eq with (y:= (length l')); trivial. +Qed. + +Theorem Permutation_ind_bis : + forall P : list A -> list A -> Prop, + P [] [] -> + (forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) -> + (forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) -> + (forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') -> + forall l l', Permutation l l' -> P l l'. +Proof. + intros P Hnil Hskip Hswap Htrans. + induction 1; auto. + apply Htrans with (x::y::l); auto. + apply Hswap; auto. + induction l; auto. + apply Hskip; auto. + apply Hskip; auto. + induction l; auto. + eauto. +Qed. + +Ltac break_list l x l' H := + destruct l as [|x l']; simpl in *; + injection H; intros; subst; clear H. + +Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a, + Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4). +Proof. + set (P l l' := + forall a l1 l2 l3 l4, l=l1++a::l2 -> l'=l3++a::l4 -> Permutation (l1++l2) (l3++l4)). + cut (forall l l', Permutation l l' -> P l l'). + intros; apply (H _ _ H0 a); auto. + intros; apply (Permutation_ind_bis P); unfold P; clear P; try clear H l l'; simpl; auto. +(* nil *) + intros; destruct l1; simpl in *; discriminate. + (* skip *) + intros x l l' H IH; intros. + break_list l1 b l1' H0; break_list l3 c l3' H1. + auto. + apply perm_trans with (l3'++c::l4); auto. + apply perm_trans with (l1'++a::l2); auto using Permutation_cons_app. + apply perm_skip. + apply (IH a l1' l2 l3' l4); auto. + (* contradict *) + intros x y l l' Hp IH; intros. + break_list l1 b l1' H; break_list l3 c l3' H0. + auto. + break_list l3' b l3'' H. + auto. + apply perm_trans with (c::l3''++b::l4); auto. + break_list l1' c l1'' H1. + auto. + apply perm_trans with (b::l1''++c::l2); auto. + break_list l3' d l3'' H; break_list l1' e l1'' H1. + auto. + apply perm_trans with (e::a::l1''++l2); auto. + apply perm_trans with (e::l1''++a::l2); auto. + apply perm_trans with (d::a::l3''++l4); auto. + apply perm_trans with (d::l3''++a::l4); auto. + apply perm_trans with (e::d::l1''++l2); auto. + apply perm_skip; apply perm_skip. + apply (IH a l1'' l2 l3'' l4); auto. + (*trans*) + intros. + destruct (In_split a l') as (l'1,(l'2,H6)). + apply (Permutation_in a H). + subst l. + apply in_or_app; right; red; auto. + apply perm_trans with (l'1++l'2). + apply (H0 _ _ _ _ _ H3 H6). + apply (H2 _ _ _ _ _ H6 H4). +Qed. + +Theorem Permutation_cons_inv : + forall l l' a, Permutation (a::l) (a::l') -> Permutation l l'. +Proof. + intros; exact (Permutation_app_inv [] l [] l' a H). +Qed. + +Theorem Permutation_cons_app_inv : + forall l l1 l2 a, Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2). +Proof. + intros; exact (Permutation_app_inv [] l l1 l2 a H). +Qed. + +Theorem Permutation_app_inv_l : + forall l l1 l2, Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2. +Proof. + induction l; simpl; auto. + intros. + apply IHl. + apply Permutation_cons_inv with a; auto. +Qed. + +Theorem Permutation_app_inv_r : + forall l l1 l2, Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2. +Proof. + induction l. + intros l1 l2; do 2 rewrite app_nil_r; auto. + intros. + apply IHl. + apply Permutation_app_inv with a; auto. +Qed. + +Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a]. +Proof. + intros a l H; remember [a] as m in H. + induction H; try (injection Heqm as -> ->; clear Heqm); + discriminate || auto. + apply Permutation_nil in H as ->; trivial. +Qed. + +Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b. +Proof. + intros a b H. + apply Permutation_length_1_inv in H; injection H as ->; trivial. +Qed. + +Lemma Permutation_length_2_inv : + forall a1 a2 l, Permutation [a1;a2] l -> l = [a1;a2] \/ l = [a2;a1]. +Proof. + intros a1 a2 l H; remember [a1;a2] as m in H. + revert a1 a2 Heqm. + induction H; intros; try (injection Heqm; intros; subst; clear Heqm); + discriminate || (try tauto). + apply Permutation_length_1_inv in H as ->; left; auto. + apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as (); + auto. +Qed. + +Lemma Permutation_length_2 : + forall a1 a2 b1 b2, Permutation [a1;a2] [b1;b2] -> + a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1. +Proof. + intros a1 b1 a2 b2 H. + apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto. +Qed. + +Lemma NoDup_Permutation : forall l l', + NoDup l -> NoDup l' -> (forall x:A, In x l <-> In x l') -> Permutation l l'. +Proof. + induction l. + destruct l'; simpl; intros. + apply perm_nil. + destruct (H1 a) as (_,H2); destruct H2; auto. + intros. + destruct (In_split a l') as (l'1,(l'2,H2)). + destruct (H1 a) as (H2,H3); simpl in *; auto. + subst l'. + apply Permutation_cons_app. + inversion_clear H. + apply IHl; auto. + apply NoDup_remove_1 with a; auto. + intro x; split; intros. + assert (In x (l'1++a::l'2)). + destruct (H1 x); simpl in *; auto. + apply in_or_app; destruct (in_app_or _ _ _ H4); auto. + destruct H5; auto. + subst x; destruct H2; auto. + assert (In x (l'1++a::l'2)). + apply in_or_app; destruct (in_app_or _ _ _ H); simpl; auto. + destruct (H1 x) as (_,H5); destruct H5; auto. + subst x. + destruct (NoDup_remove_2 _ _ _ H0 H). +Qed. + +End Permutation_properties. + +Section Permutation_map. + +Variable A B : Type. +Variable f : A -> B. + +Add Parametric Morphism : (map f) + with signature (@Permutation A) ==> (@Permutation B) as Permutation_map_aux. +Proof. + induction 1; simpl; eauto using Permutation. +Qed. + +Lemma Permutation_map : + forall l l', Permutation l l' -> Permutation (map f l) (map f l'). +Proof. + exact Permutation_map_aux_Proper. +Qed. + +End Permutation_map. + +(* begin hide *) +Notation Permutation_app_swap := Permutation_app_comm (only parsing). +(* end hide *) diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v new file mode 100644 index 000000000..d87259eec --- /dev/null +++ b/theories/Sorting/Sorted.v @@ -0,0 +1,154 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* A -> Prop. + + (** Locally sorted: consecutive elements of the list are ordered *) + + Inductive LocallySorted : list A -> Prop := + | LSorted_nil : LocallySorted [] + | LSorted_cons1 a : LocallySorted [a] + | LSorted_consn a b l : + LocallySorted (b :: l) -> R a b -> LocallySorted (a :: b :: l). + + (** Alternative two-step definition of being locally sorted *) + + Inductive HdRel a : list A -> Prop := + | HdRel_nil : HdRel a [] + | HdRel_cons b l : R a b -> HdRel a (b :: l). + + Inductive Sorted : list A -> Prop := + | Sorted_nil : Sorted [] + | Sorted_cons a l : Sorted l -> HdRel a l -> Sorted (a :: l). + + Lemma HdRel_inv : forall a b l, HdRel a (b :: l) -> R a b. + Proof. + inversion 1; auto. + Qed. + + Lemma Sorted_inv : + forall a l, Sorted (a :: l) -> Sorted l /\ HdRel a l. + Proof. + intros a l H; inversion H; auto. + Qed. + + Lemma Sorted_rect : + forall P:list A -> Type, + P [] -> + (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) -> + forall l:list A, Sorted l -> P l. + Proof. + induction l; firstorder using Sorted_inv. + Qed. + + Lemma Sorted_LocallySorted_iff : forall l, Sorted l <-> LocallySorted l. + Proof. + split; [induction 1 as [|a l [|]]| induction 1]; + auto using Sorted, LocallySorted, HdRel. + inversion H1; subst; auto using LocallySorted. + Qed. + + (** Strongly sorted: elements of the list are pairwise ordered *) + + Inductive StronglySorted : list A -> Prop := + | SSorted_nil : StronglySorted [] + | SSorted_cons a l : StronglySorted l -> Forall (R a) l -> StronglySorted (a :: l). + + Lemma StronglySorted_inv : forall a l, StronglySorted (a :: l) -> + StronglySorted l /\ Forall (R a) l. + Proof. + intros; inversion H; auto. + Defined. + + Lemma StronglySorted_rect : + forall P:list A -> Type, + P [] -> + (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) -> + forall l, StronglySorted l -> P l. + Proof. + induction l; firstorder using StronglySorted_inv. + Defined. + + Lemma StronglySorted_rec : + forall P:list A -> Type, + P [] -> + (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) -> + forall l, StronglySorted l -> P l. + Proof. + firstorder using StronglySorted_rect. + Qed. + + Lemma StronglySorted_Sorted : forall l, StronglySorted l -> Sorted l. + Proof. + induction 1 as [|? ? ? ? HForall]; constructor; trivial. + destruct HForall; constructor; trivial. + Qed. + + Lemma Sorted_extends : + Transitive R -> forall a l, Sorted (a::l) -> Forall (R a) l. + Proof. + intros. change match a :: l with [] => True | a :: l => Forall (R a) l end. + induction H0 as [|? ? ? ? H1]; [trivial|]. + destruct H1; constructor; trivial. + eapply Forall_impl; [|eassumption]. + firstorder. + Qed. + + Lemma Sorted_StronglySorted : + Transitive R -> forall l, Sorted l -> StronglySorted l. + Proof. + induction 2; constructor; trivial. + apply Sorted_extends; trivial. + constructor; trivial. + Qed. + +End defs. + +Hint Constructors HdRel: sorting. +Hint Constructors Sorted: sorting. + +(* begin hide *) +(* Compatibility with deprecated file Sorting.v *) +Notation lelistA := HdRel (only parsing). +Notation nil_leA := HdRel_nil (only parsing). +Notation cons_leA := HdRel_cons (only parsing). + +Notation sort := Sorted (only parsing). +Notation nil_sort := Sorted_nil (only parsing). +Notation cons_sort := Sorted_cons (only parsing). + +Notation lelistA_inv := HdRel_inv (only parsing). +Notation sort_inv := Sorted_inv (only parsing). +Notation sort_rect := Sorted_rect (only parsing). +(* end hide *) 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. diff --git a/theories/Sorting/vo.itarget b/theories/Sorting/vo.itarget index b14f8f743..079eaad18 100644 --- a/theories/Sorting/vo.itarget +++ b/theories/Sorting/vo.itarget @@ -1,5 +1,7 @@ Heap.vo Permutation.vo -PermutEq.vo PermutSetoid.vo +PermutEq.vo +Sorted.vo Sorting.vo +Mergesort.vo -- cgit v1.2.3