diff options
-rw-r--r-- | .gitignore | 1 | ||||
-rw-r--r-- | CHANGES | 11 | ||||
-rw-r--r-- | LocallySorted.v | 44 | ||||
-rw-r--r-- | dev/doc/naming-conventions.tex | 70 | ||||
-rw-r--r-- | merge-essai-type-classes.v | 310 | ||||
-rw-r--r-- | theories/Lists/List.v | 592 | ||||
-rw-r--r-- | theories/Lists/TheoryList.v | 36 | ||||
-rw-r--r-- | theories/Sets/Multiset.v | 12 | ||||
-rw-r--r-- | theories/Sorting/Heap.v | 67 | ||||
-rw-r--r-- | theories/Sorting/Mergesort.v | 279 | ||||
-rw-r--r-- | theories/Sorting/PermutEq.v | 32 | ||||
-rw-r--r-- | theories/Sorting/PermutSetoid.v | 338 | ||||
-rw-r--r-- | theories/Sorting/Permutation.v | 547 | ||||
-rw-r--r-- | theories/Sorting/Sorted.v | 154 | ||||
-rw-r--r-- | theories/Sorting/Sorting.v | 122 | ||||
-rw-r--r-- | theories/Sorting/vo.itarget | 4 |
16 files changed, 1837 insertions, 782 deletions
diff --git a/.gitignore b/.gitignore index ba4811b8f..aee7ed659 100644 --- a/.gitignore +++ b/.gitignore @@ -93,6 +93,7 @@ doc/stdlib/index-list.html doc/RecTutorial/RecTutorial.html doc/RecTutorial/RecTutorial.pdf doc/RecTutorial/RecTutorial.ps +dev/doc/naming-conventions.pdf _build plugins/*/*_mod.ml myocamlbuild_config.ml @@ -121,7 +121,16 @@ Library available under the name nat_compare_alt. - Lemmas in library Relations and Reals have been homogenized a bit. - The implicit argument of Logic.eq is now maximally inserted, allowing - to simply write "eq" instead of "@eq _" in morphism signatures. + to simply write "eq" instead of "@eq _" in morphism signatures. +- Revision of the Sorting library: + - new mergesort of worst-case complexity O(n*ln(n)) made available in + Mergesort.v; + - notion of permutation up to setoid from Permutation.v is deprecated and + was moved to PermutSetoid.v; + - Permutation.v now contains the notion of permutation that was formerly in + List.v; + - heapsort from Heap.v of worst-case complexity O(n*n) is deprecated; + - new file Sorted.v for some definitions of being sorted. Changes from V8.1 to V8.2 ========================= diff --git a/LocallySorted.v b/LocallySorted.v new file mode 100644 index 000000000..8f6264134 --- /dev/null +++ b/LocallySorted.v @@ -0,0 +1,44 @@ +Require Import List Program.Syntax. + +Variable A:Type. +Variable le:A->A->Prop. +Infix "<=" := le. + +(* +if of_sumbool H then _ else _ +if H then _ else _ +*) + +Inductive locally_sorted : list A -> Prop := +| nil_locally_sorted : locally_sorted [] +| cons1_locally_sorted a : locally_sorted [a] +| consn_locally_sorted a b l : locally_sorted (b::l) -> a <= b -> locally_sorted (a::b::l). + +Inductive lelist (a:A) : list A -> Prop := + | nil_le : lelist a nil + | cons_le : forall (b:A) (l:list A), le a b -> lelist a (b :: l). + +Inductive sort : list A -> Prop := + | nil_sort : sort nil + | cons_sort : + forall (a:A) (l:list A), sort l -> lelist a l -> sort (a :: l). + +Goal forall l, sort l -> locally_sorted l. +induction l. + constructor. + inversion 1; subst. + destruct l; constructor. + apply IHl; trivial. + inversion H3; auto. +Qed. + +Goal forall l, lelist + +Goal forall l, locally_sorted l -> sort l. +induction 1; constructor. + constructor. + constructor. + assumption. + inversion IHlocally_sorted; subst. + + diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex index c9151d829..e7c8975bd 100644 --- a/dev/doc/naming-conventions.tex +++ b/dev/doc/naming-conventions.tex @@ -143,6 +143,47 @@ will have a named ended in \texttt{\_dec}. Idem for cotransitivity lemmas which are inherently computational that are ended in \texttt{\_cotrans}. +\subsection{Inductive types constructor names} + +As a general rule, constructor names start with the name of the +inductive type being defined as in \texttt{Inductive Z := Z0 : Z | + Zpos : Z -> Z | Zneg : Z -> Z} to the exception of very standard +types like \texttt{bool}, \texttt{nat}, \texttt{list}... + +For inductive predicates, constructor names also start with the name +of the notion being defined with one or more suffixes separated with +\texttt{\_} for discriminating the different cases as e.g. in + +\begin{verbatim} +Inductive even : nat -> Prop := + | even_O : even 0 + | even_S n : odd n -> even (S n) +with odd : nat -> Prop := + | odd_S n : even n -> odd (S n). +\end{verbatim} + +As a general rule, inductive predicate names should be lowercase (to +the exception of notions referring to a proper name, e.g. \texttt{Bezout}) +and multiple words must be separated by ``{\_}''. + +As an exception, when extending libraries whose general rule is that +predicates names start with a capital letter, the convention of this +library should be kept and the separation between multiple words is +done by making the initial of each work a capital letter (if one of +these words is a proper name, then a ``{\_}'' is added to emphasize +that the capital letter is proper and not an application of the rule +for marking the change of word). + +Inductive predicates that characterize the specification of a function +should be named after the function it specifies followed by +\texttt{\_spec} as in: + +\begin{verbatim} +Inductive nth_spec : list A -> nat -> A -> Prop := + | nth_spec_O a l : nth_spec (a :: l) 0 a + | nth_spec_S n a b l : nth_spec l n a -> nth_spec (b :: l) (S n) a. +\end{verbatim} + \section{Equational properties of operations} \subsection{General conventions} @@ -205,12 +246,24 @@ If the conclusion is in the other way than listed below, add suffix \itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr} {forall x y:D, op (op' x y) = op' (op x) (op y)} -\itemrule{Left distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_l} +\itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr} +{forall x y:D, op (op' x y) = op' (op x) (op y)} + + Remark: For a non commutative operation with inversion of arguments, as in + \formula{forall x y z:D, op (op' x y) = op' (op y) (op y z)}, + we may probably still call the property distributivity since there + is no ambiguity. + + Example: \formula{forall n m : Z, -(n+m) = (-n)+(-m)}. + + Example: \formula{forall l l' : list A, rev (l++l') = (rev l)++(rev l')}. + +\itemrule{Left extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_l} {forall x y:D, op (op' x y) = op' (op x) y} - Question: Call it left commutativity ?? + Question: Call it left commutativity ?? left swap ? -\itemrule{Right distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_r} +\itemrule{Right extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_r} {forall x y:D, op (op' x y) = op' x (op y)} \itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent} @@ -309,7 +362,7 @@ argument respectively and their return type identical. Remark: When the type are heterogeneous, only one extrusion law is possible and it can simply be named {Dop\_op'\_extrusion}. -Example: \formula{app\_cons\_extrusion : forall a l l', (a :: l) ++ l' = a :: (l ++ l')}, in arithmetic +Example: \formula{app\_cons\_extrusion : forall a l l', (a :: l) ++ l' = a :: (l ++ l')}. %====================================================================== %\section{Properties of elements} @@ -384,6 +437,12 @@ Example: \formula{app\_cons\_extrusion : forall a l l', (a :: l) ++ l' = a :: (l \name{Dop\_op'\_rel\_distr\_mon\_l} and \name{Dop\_op'\_rel\_distr\_anti\_l})? +\itemrule{Commutativity of binary operator {\op} along (equivalence) relation {\rel} on domain {\D}}{Dop\_op'\_rel\_comm} +{forall x y z:D, rel (op x y) (op y x)} + + Example: +\formula{forall l l':list A, Permutation (l++l') (l'++l)} + \itemrule{Irreducibility of binary operator {\op} on domain {\D}}{Dop\_irreducible} {forall x y z:D, z = op x y -> z = x $\backslash/$ z = y} @@ -472,7 +531,8 @@ Example: \formula{eq\_true\_neg: \~{} eq\_true b <-> eq\_true (negb b)}. \itemrule{Linearity of relation {\rel} on domain {\D}}{Drel\_trichotomy} {forall x y:D, \{rel x y\} + \{x = y\} + \{rel y x\}} - Questions: Or call it \name{Drel\_total}, or \name{Drel\_linear} use + Questions: Or call it \name{Drel\_total}, or \name{Drel\_linear}, or + \name{Drel\_connected}? Use $\backslash/$ ? or use a ternary sumbool, or a ternary disjunction, for nicer elimination. diff --git a/merge-essai-type-classes.v b/merge-essai-type-classes.v new file mode 100644 index 000000000..bc48ecbfe --- /dev/null +++ b/merge-essai-type-classes.v @@ -0,0 +1,310 @@ +(************************************************************************) +(* 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$ i*) + +(* An implementation of mergesort *) + +(* Author: Hugo Herbelin *) + +Require Import List Program.Syntax. +Open Scope bool_scope. + +Coercion eq_true : bool >-> Sortclass. + +Class BinaryCharacteristicFunction (A:Type) := { + rel_bool : A -> A -> bool +}. + +(* Technical remark: one could have declared DecidableRelation as an instance of the following class +and, with the associated notation, one would have obtained for free a notation +"<=" for rel_bool that we could have used wherever it is possible instead of "<=?". +However, the problem would then have been that "a <= b" and "a <=? b" in Prop would +only have been equivalent module commutative cuts (due to the hidden projections) +what Coq does not support. + +Class Relation (A:Type) := { + rel : A -> A -> Prop +}. + +Instance dec_rel `(f: BinaryCharacteristicFunction A) : Relation A := + let (f) := f in f. + +Infix "<=" := rel. +*) + +Infix "<=?" := rel_bool (at level 35). + +Class DecidableTotalPreOrder `(le : BinaryCharacteristicFunction A) := { + le_bool_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1; + le_trans : forall a1 a2 a3, a1 <=? a2 -> a2 <=? a3 -> a1 <=? a3 +}. + +Section Sort. + +Context `(le : DecidableTotalPreOrder A). + +(** Provides support for tactics reflexivity, symmetry, transitive *) + +Require Import Equivalence. + +Program Instance equiv_reflexive A : Reflexive (@Permutation A) + := @Permutation_refl A. + +Program Instance equiv_symmetric : Symmetric (@Permutation A) + := @Permutation_sym A. + +Program Instance equiv_transitive : Transitive (@Permutation A) + := @Permutation_trans A. +(* +Module T (Import X:TotalOrder). +*) +Theorem le_refl : forall a, a <=? a. +intro; destruct (le_bool_total a a); assumption. +Qed. + +(* +End T. + +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 []. + +Inductive sorted : list A -> Prop := +| nil_sort : sorted [] +| cons1_sort a : sorted [a] +| consn_sort a b l : sorted (b::l) -> a <=? b -> sorted (a::b::l). + +Fixpoint sorted_stack stack := + match stack with + | [] => True + | None :: stack' => sorted_stack stack' + | Some l :: stack' => sorted l /\ sorted_stack stack' + end. + +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 merge_sorted : 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. + inversion H; subst; clear 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')). + inversion H0; subst; clear 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. + +Hint Constructors Permutation. + +Theorem merge_permuted : 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 merge_list_to_stack_sorted : forall stack l, + sorted_stack stack -> sorted l -> sorted_stack (merge_list_to_stack stack l). +Proof. + induction stack as [|[|]]; intros; simpl. + auto. + apply IHstack. destruct H as (_,H1). fold sorted_stack in H1. auto. (* Pq déplie-t-il sorted_stack ici ? *) + apply merge_sorted; auto; destruct H; auto. + auto. +Qed. + +Theorem merge_list_to_stack_permuted : 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_swap. + apply merge_permuted. + apply IHstack. + reflexivity. +Qed. + +Theorem merge_stack_sorted : forall stack, + sorted_stack stack -> sorted (merge_stack stack). +Proof. +induction stack as [|[|]]; simpl; intros. + constructor; auto. + apply merge_sorted; tauto. + auto. +Qed. + +Theorem merge_stack_permuted : 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 merge_permuted. + assumption. +Qed. + +Theorem iter_merge_sorted : forall stack l, + sorted_stack stack -> sorted (iter_merge stack l). +Proof. + intros stack l H; induction l in stack, H |- *; simpl. + auto using merge_stack_sorted. + assert (sorted [a]) by constructor. + auto using merge_list_to_stack_sorted. +Qed. + +Theorem iter_merge_permuted : forall l stack, + Permutation (flatten_stack stack ++ l) (iter_merge stack l). +Proof. + induction l; simpl; intros. + rewrite app_nil_r. apply merge_stack_permuted. + change (a::l) with ([a]++l). + rewrite app_assoc. + etransitivity. + apply Permutation_app_tail. + etransitivity. + apply Permutation_app_swap. + apply merge_list_to_stack_permuted. + apply IHl. +Qed. + +Theorem sort_sorted : forall l, sorted (sort l). +Proof. +intro; apply iter_merge_sorted. constructor. +Qed. + +Theorem sort_permuted : forall l, Permutation l (sort l). +Proof. +intro; apply (iter_merge_permuted l []). +Qed. + +(* It remains to prove that "sort" returns a permutation *) +(* of the original elements *) + + + Fixpoint le_bool x y := + match x, y with + | 0, _ => true + | S x', 0 => false + | S x', S y' => le_bool x' y' + end. + +Instance le_bool_char : BinaryCharacteristicFunction nat := le_bool. + +Theorem nat_le_bool_total : forall a1 a2, le_bool a1 a2 \/ le_bool a2 a1. +Proof. + induction a1; destruct a2; simpl; auto using is_eq_true. +Qed. + +Instance nat_order : DecidableTotalPreOrder le_bool_char := { + le_bool_total := nat_le_bool_total +}. + +Admitted. + +End Sort. +Eval compute in sort [5;3;6;1;8;6;0]. + diff --git a/theories/Lists/List.v b/theories/Lists/List.v index d6b4c1354..2c89af4f1 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -26,20 +26,21 @@ Section Lists. Variable A : Type. - (** Head and tail *) - Definition head (l:list A) := + (** Head and tail *) + + Definition hd (default:A) (l:list A) := + match l with + | nil => default + | x :: _ => x + end. + + Definition hd_error (l:list A) := match l with | nil => error | x :: _ => value x end. - Definition hd (default:A) (l:list A) := - match l with - | nil => default - | x :: _ => x - end. - - Definition tail (l:list A) : list A := + Definition tl (l:list A) := match l with | nil => nil | a :: m => m @@ -54,6 +55,10 @@ Section Lists. End Lists. +(* Keep these notations local to prevent conflicting notations *) +Local Notation "[ ]" := nil : list_scope. +Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope. + (** ** Facts about lists *) Section Facts. @@ -64,7 +69,7 @@ Section Facts. (** *** Genereric facts *) (** Discrimination *) - Theorem nil_cons : forall (x:A) (l:list A), nil <> x :: l. + Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l. Proof. intros; discriminate. Qed. @@ -72,21 +77,21 @@ Section Facts. (** Destruction *) - Theorem destruct_list : forall l : list A, {x:A & {tl:list A | l = x::tl}}+{l = nil}. + Theorem destruct_list : forall l : list A, {x:A & {tl:list A | l = x::tl}}+{l = []}. Proof. - induction l as [|a tl]. + induction l as [|a tail]. right; reflexivity. - left; exists a; exists tl; reflexivity. + left; exists a, tail; reflexivity. Qed. (** *** Head and tail *) - Theorem head_nil : head (@nil A) = None. + Theorem hd_error_nil : hd_error (@nil A) = None. Proof. simpl; reflexivity. Qed. - Theorem head_cons : forall (l : list A) (x : A), head (x::l) = Some x. + Theorem hd_error_cons : forall (l : list A) (x : A), hd_error (x::l) = Some x. Proof. intros; simpl; reflexivity. Qed. @@ -101,44 +106,44 @@ Section Facts. Theorem in_eq : forall (a:A) (l:list A), In a (a :: l). Proof. - simpl in |- *; auto. + simpl; auto. Qed. Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l). Proof. - simpl in |- *; auto. + simpl; auto. Qed. - Theorem in_nil : forall a:A, ~ In a nil. + Theorem in_nil : forall a:A, ~ In a []. Proof. - unfold not in |- *; intros a H; inversion_clear H. + unfold not; intros a H; inversion_clear H. Qed. - Lemma In_split : forall x (l:list A), In x l -> exists l1, exists l2, l = l1++x::l2. + Theorem in_split : forall x (l:list A), In x l -> exists l1, exists l2, l = l1++x::l2. Proof. induction l; simpl; destruct 1. subst a; auto. - exists (@nil A); exists l; auto. + exists [], l; auto. destruct (IHl H) as (l1,(l2,H0)). - exists (a::l1); exists l2; simpl; f_equal; auto. + exists (a::l1), l2; simpl; f_equal; auto. Qed. (** Inversion *) - Theorem in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l. + Lemma in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l. Proof. intros a b l H; inversion_clear H; auto. Qed. (** Decidability of [In] *) - Theorem In_dec : + Theorem in_dec : (forall x y:A, {x = y} + {x <> y}) -> forall (a:A) (l:list A), {In a l} + {~ In a l}. Proof. intro H; induction l as [| a0 l IHl]. right; apply in_nil. - destruct (H a0 a); simpl in |- *; auto. - destruct IHl; simpl in |- *; auto. - right; unfold not in |- *; intros [Hc1| Hc2]; auto. + destruct (H a0 a); simpl; auto. + destruct IHl; simpl; auto. + right; unfold not; intros [Hc1| Hc2]; auto. Defined. @@ -147,29 +152,29 @@ Section Facts. (**************************) (** Discrimination *) - Theorem app_cons_not_nil : forall (x y:list A) (a:A), nil <> x ++ a :: y. + Theorem app_cons_not_nil : forall (x y:list A) (a:A), [] <> x ++ a :: y. Proof. - unfold not in |- *. - destruct x as [| a l]; simpl in |- *; intros. + unfold not. + destruct x as [| a l]; simpl; intros. discriminate H. discriminate H. Qed. (** Concat with [nil] *) - Theorem app_nil_l : forall l:list A, nil ++ l = l. + Theorem app_nil_l : forall l:list A, [] ++ l = l. Proof. reflexivity. Qed. - Theorem app_nil_r : forall l:list A, l ++ nil = l. + Theorem app_nil_r : forall l:list A, l ++ [] = l. Proof. induction l; simpl; f_equal; auto. Qed. (* begin hide *) - (* Compatibility *) - Theorem app_nil_end : forall (l:list A), l = l ++ nil. + (* Deprecated *) + Theorem app_nil_end : forall (l:list A), l = l ++ []. Proof. symmetry; apply app_nil_r. Qed. (* end hide *) @@ -179,11 +184,14 @@ Section Facts. intros l m n; induction l; simpl; f_equal; auto. Qed. + (* begin hide *) + (* Deprecated *) Theorem app_assoc_reverse : forall l m n:list A, (l ++ m) ++ n = l ++ m ++ n. Proof. auto using app_assoc. Qed. Hint Resolve app_assoc_reverse. + (* end hide *) (** [app] commutes with [cons] *) Theorem app_comm_cons : forall (x y:list A) (a:A), a :: (x ++ y) = (a :: x) ++ y. @@ -193,19 +201,19 @@ Section Facts. (** Facts deduced from the result of a concatenation *) - Theorem app_eq_nil : forall l l':list A, l ++ l' = nil -> l = nil /\ l' = nil. + Theorem app_eq_nil : forall l l':list A, l ++ l' = [] -> l = [] /\ l' = []. Proof. - destruct l as [| x l]; destruct l' as [| y l']; simpl in |- *; auto. + destruct l as [| x l]; destruct l' as [| y l']; simpl; auto. intro; discriminate. intros H; discriminate H. Qed. Theorem app_eq_unit : forall (x y:list A) (a:A), - x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil. + x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = []. Proof. destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ]; - simpl in |- *. + simpl. intros a H; discriminate H. left; split; auto. right; split; auto. @@ -215,18 +223,18 @@ Section Facts. intros. injection H. intro. - cut (nil = l ++ a0 :: l0); auto. + cut ([] = l ++ a0 :: l0); auto. intro. generalize (app_cons_not_nil _ _ _ H1); intro. elim H2. Qed. Lemma app_inj_tail : - forall (x y:list A) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b. + forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b. Proof. induction x as [| x l IHl]; [ destruct y as [| a l] | destruct y as [| a l0] ]; - simpl in |- *; auto. + simpl; auto. intros a b H. injection H. auto. @@ -235,7 +243,7 @@ Section Facts. generalize (app_cons_not_nil _ _ _ H0); destruct 1. intros a b H. injection H; intros. - cut (nil = l ++ a :: nil); auto. + cut ([] = l ++ [a]); auto. intro. generalize (app_cons_not_nil _ _ _ H2); destruct 1. intros a0 b H. @@ -256,7 +264,7 @@ Section Facts. Lemma in_app_or : forall (l m:list A) (a:A), In a (l ++ m) -> In a l \/ In a m. Proof. intros l m a. - elim l; simpl in |- *; auto. + elim l; simpl; auto. intros a0 y H H0. now_show ((a0 = a \/ In a y) \/ In a m). elim H0; auto. @@ -268,7 +276,7 @@ Section Facts. Lemma in_or_app : forall (l m:list A) (a:A), In a l \/ In a m -> In a (l ++ m). Proof. intros l m a. - elim l; simpl in |- *; intro H. + elim l; simpl; intro H. now_show (In a m). elim H; auto; intro H0. now_show (In a m). @@ -287,13 +295,13 @@ Section Facts. Qed. Lemma app_inv_head: - forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. + forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. Proof. induction l; simpl; auto; injection 1; auto. Qed. Lemma app_inv_tail: - forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. + forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. Proof. intros l l1 l2; revert l1 l2 l. induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; @@ -333,7 +341,7 @@ Section Elts. match n, l with | O, x :: l' => x | O, other => default - | S m, nil => default + | S m, [] => default | S m, x :: t => nth m t default end. @@ -341,7 +349,7 @@ Section Elts. match n, l with | O, x :: l' => true | O, other => false - | S m, nil => false + | S m, [] => false | S m, x :: t => nth_ok m t default end. @@ -351,7 +359,7 @@ Section Elts. Proof. intros n l d; generalize n; induction l; intro n0. right; case n0; trivial. - case n0; simpl in |- *. + case n0; simpl. auto. intro n1; elim (IHl n1); auto. Qed. @@ -360,7 +368,7 @@ Section Elts. forall (n:nat) (l:list A) (d a:A), In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l). Proof. - simpl in |- *; auto. + simpl; auto. Qed. Fixpoint nth_error (l:list A) (n:nat) {struct n} : Exc A := @@ -386,9 +394,9 @@ Section Elts. forall (n:nat) (l:list A) (d:A), n < length l -> In (nth n l d) l. Proof. - unfold lt in |- *; induction n as [| n hn]; simpl in |- *. - destruct l; simpl in |- *; [ inversion 2 | auto ]. - destruct l as [| a l hl]; simpl in |- *. + unfold lt; induction n as [| n hn]; simpl. + destruct l; simpl; [ inversion 2 | auto ]. + destruct l as [| a l hl]; simpl. inversion 2. intros d ie; right; apply hn; auto with arith. Qed. @@ -441,26 +449,22 @@ Section Elts. (** ** Remove *) (*****************) - Section Remove. - - Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. + Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. - Fixpoint remove (x : A) (l : list A) : list A := - match l with - | nil => nil - | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) - end. - - Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l). - Proof. - induction l as [|x l]; auto. - intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. - apply IHl. - unfold not; intro HF; simpl in HF; destruct HF; auto. - apply (IHl y); assumption. - Qed. + Fixpoint remove (x : A) (l : list A) : list A := + match l with + | [] => [] + | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) + end. - End Remove. + Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l). + Proof. + induction l as [|x l]; auto. + intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. + apply IHl. + unfold not; intro HF; simpl in HF; destruct HF; auto. + apply (IHl y); assumption. + Qed. (******************************) @@ -472,8 +476,8 @@ Section Elts. Fixpoint last (l:list A) (d:A) : A := match l with - | nil => d - | a :: nil => a + | [] => d + | [a] => a | a :: l => last l d end. @@ -481,13 +485,13 @@ Section Elts. Fixpoint removelast (l:list A) : list A := match l with - | nil => nil - | a :: nil => nil + | [] => [] + | [a] => [] | a :: l => a :: removelast l end. Lemma app_removelast_last : - forall l d, l<>nil -> l = removelast l ++ (last l d :: nil). + forall l d, l <> [] -> l = removelast l ++ [last l d]. Proof. induction l. destruct 1; auto. @@ -497,25 +501,25 @@ Section Elts. Qed. Lemma exists_last : - forall l, l<>nil -> { l' : (list A) & { a : A | l = l'++a::nil}}. + forall l, l <> [] -> { l' : (list A) & { a : A | l = l' ++ [a]}}. Proof. induction l. destruct 1; auto. intros _. destruct l. - exists (@nil A); exists a; auto. + exists [], a; auto. destruct IHl as [l' (a',H)]; try discriminate. rewrite H. - exists (a::l'); exists a'; auto. + exists (a::l'), a'; auto. Qed. Lemma removelast_app : - forall l l', l' <> nil -> removelast (l++l') = l ++ removelast l'. + forall l l', l' <> [] -> removelast (l++l') = l ++ removelast l'. Proof. induction l. simpl; auto. simpl; intros. - assert (l++l' <> nil). + assert (l++l' <> []). destruct l. simpl; auto. simpl; discriminate. @@ -528,14 +532,12 @@ Section Elts. (** ** Counting occurences of a element *) (****************************************) - Hypotheses eqA_dec : forall x y : A, {x = y}+{x <> y}. - Fixpoint count_occ (l : list A) (x : A) : nat := match l with - | nil => 0 + | [] => 0 | y :: tl => let n := count_occ tl x in - if eqA_dec y x then S n else n + if eq_dec y x then S n else n end. (** Compatibility of count_occ with operations on list *) @@ -543,12 +545,12 @@ Section Elts. Proof. induction l as [|y l]. simpl; intros; split; [destruct 1 | apply gt_irrefl]. - simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq]. + simpl. intro x; destruct (eq_dec y x) as [Heq|Hneq]. rewrite Heq; intuition. pose (IHl x). intuition. Qed. - Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = nil. + Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = []. Proof. split. (* Case -> *) @@ -558,14 +560,14 @@ Section Elts. elim (O_S (count_occ l x)). apply sym_eq. generalize (H x). - simpl. destruct (eqA_dec x x) as [|HF]. + simpl. destruct (eq_dec x x) as [|HF]. trivial. elim HF; reflexivity. (* Case <- *) intro H; rewrite H; simpl; reflexivity. Qed. - Lemma count_occ_nil : forall (x : A), count_occ nil x = 0. + Lemma count_occ_nil : forall (x : A), count_occ [] x = 0. Proof. intro x; simpl; reflexivity. Qed. @@ -573,13 +575,13 @@ Section Elts. Lemma count_occ_cons_eq : forall (l : list A) (x y : A), x = y -> count_occ (x::l) y = S (count_occ l y). Proof. intros l x y H; simpl. - destruct (eqA_dec x y); [reflexivity | contradiction]. + destruct (eq_dec x y); [reflexivity | contradiction]. Qed. Lemma count_occ_cons_neq : forall (l : list A) (x y : A), x <> y -> count_occ (x::l) y = count_occ l y. Proof. intros l x y H; simpl. - destruct (eqA_dec x y); [contradiction | reflexivity]. + destruct (eq_dec x y); [contradiction | reflexivity]. Qed. End Elts. @@ -600,38 +602,38 @@ Section ListOps. Fixpoint rev (l:list A) : list A := match l with - | nil => nil - | x :: l' => rev l' ++ x :: nil + | [] => [] + | x :: l' => rev l' ++ [x] end. - Lemma distr_rev : forall x y:list A, rev (x ++ y) = rev y ++ rev x. + Lemma rev_app_distr : forall x y:list A, rev (x ++ y) = rev y ++ rev x. Proof. induction x as [| a l IHl]. destruct y as [| a l]. - simpl in |- *. + simpl. auto. - simpl in |- *. + simpl. rewrite app_nil_r; auto. intro y. - simpl in |- *. + simpl. rewrite (IHl y). rewrite app_assoc; trivial. Qed. - Remark rev_unit : forall (l:list A) (a:A), rev (l ++ a :: nil) = a :: rev l. + Remark rev_unit : forall (l:list A) (a:A), rev (l ++ [a]) = a :: rev l. Proof. intros. - apply (distr_rev l (a :: nil)); simpl in |- *; auto. + apply (rev_app_distr l [a]); simpl; auto. Qed. Lemma rev_involutive : forall l:list A, rev (rev l) = l. Proof. induction l as [| a l IHl]. - simpl in |- *; auto. + simpl; auto. - simpl in |- *. + simpl. rewrite (rev_unit (rev l) a). rewrite IHl; auto. Qed. @@ -639,7 +641,7 @@ Section ListOps. (** Compatibility with other operations *) - Lemma In_rev : forall l x, In x l <-> In x (rev l). + Lemma in_rev : forall l x, In x l <-> In x (rev l). Proof. induction l. simpl; intuition. @@ -688,23 +690,19 @@ Section ListOps. Fixpoint rev_append (l l': list A) : list A := match l with - | nil => l' + | [] => l' | a::l => rev_append l (a::l') end. - Definition rev' l : list A := rev_append l nil. - - Notation rev_acc := rev_append (only parsing). + Definition rev' l : list A := rev_append l []. - Lemma rev_append_rev : forall l l', rev_acc l l' = rev l ++ l'. + Lemma rev_append_rev : forall l l', rev_append l l' = rev l ++ l'. Proof. induction l; simpl; auto; intros. rewrite <- app_assoc; firstorder. Qed. - Notation rev_acc_rev := rev_append_rev (only parsing). - - Lemma rev_alt : forall l, rev l = rev_append l nil. + Lemma rev_alt : forall l, rev l = rev_append l []. Proof. intros; rewrite rev_append_rev. rewrite app_nil_r; trivial. @@ -717,22 +715,19 @@ Section ListOps. Section Reverse_Induction. - Unset Implicit Arguments. - Lemma rev_list_ind : forall P:list A-> Prop, - P nil -> + P [] -> (forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) -> forall l:list A, P (rev l). Proof. induction l; auto. Qed. - Set Implicit Arguments. Theorem rev_ind : forall P:list A -> Prop, - P nil -> - (forall (x:A) (l:list A), P l -> P (l ++ x :: nil)) -> forall l:list A, P l. + P [] -> + (forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l. Proof. intros. generalize (rev_involutive l). @@ -740,7 +735,7 @@ Section ListOps. apply (rev_list_ind P). auto. - simpl in |- *. + simpl. intros. apply (H0 a (rev l0)). auto. @@ -748,235 +743,11 @@ Section ListOps. End Reverse_Induction. - - (*********************************************************************) - (** ** List permutations as a composition of adjacent transpositions *) - (*********************************************************************) - - Section Permutation. - - Inductive Permutation : list A -> list A -> Prop := - | perm_nil: Permutation nil nil - | perm_skip: forall (x:A) (l l':list A), Permutation l l' -> Permutation (cons x l) (cons x l') - | perm_swap: forall (x y:A) (l:list A), Permutation (cons y (cons x l)) (cons x (cons y l)) - | perm_trans: forall (l l' l'':list A), Permutation l l' -> Permutation l' l'' -> Permutation l l''. - - Hint Constructors Permutation. - - (** Some facts about [Permutation] *) - - Theorem Permutation_nil : forall (l : list A), Permutation nil l -> l = nil. - Proof. - intros l HF. - set (m:=@nil A) in HF; assert (m = nil); [reflexivity|idtac]; clearbody m. - induction HF; try elim (nil_cons (sym_eq H)); auto. - Qed. - - Theorem Permutation_nil_cons : forall (l : list A) (x : A), ~ Permutation nil (x::l). - Proof. - unfold not; intros l x HF. - elim (@nil_cons A x l). apply sym_eq. exact (Permutation_nil HF). - 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. - - Hint Resolve Permutation_refl Permutation_sym Permutation_trans. - - (** 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. - - Theorem Permutation_app_swap : 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. - simpl; apply Permutation_trans with (l' := x :: y :: l' ++ l). - constructor; rewrite app_comm_cons; apply IHl. - apply Permutation_trans with (l' := y :: x :: l' ++ l); constructor. - apply Permutation_trans with (l' := 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. - apply perm_trans with (a0::a::l1++l2). - apply perm_skip; auto. - apply perm_trans with (a::a0::l1++l2). - apply perm_swap; auto. - apply perm_skip; auto. - Qed. - Hint Resolve Permutation_cons_app. - - 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_rev : forall (l : list A), Permutation l (rev l). - Proof. - induction l as [| x l]; simpl; trivial. - apply Permutation_trans with (l' := (x::nil)++rev l). - simpl; auto. - apply Permutation_app_swap. - Qed. - - Theorem Permutation_ind_bis : - forall P : list A -> list A -> Prop, - P (@nil A) (@nil A) -> - (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:=fun 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 (@nil _) l (@nil _) 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 (@nil _) 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. - - End Permutation. - - (***********************************) (** ** Decidable equality on lists *) (***********************************) - Hypotheses eqA_dec : forall (x y : A), {x = y}+{x <> y}. + Hypothesis eq_dec : forall (x y : A), {x = y}+{x <> y}. Lemma list_eq_dec : forall l l':list A, {l = l'} + {l <> l'}. @@ -985,7 +756,7 @@ Section ListOps. left; trivial. right; apply nil_cons. right; unfold not; intro HF; apply (nil_cons (sym_eq HF)). - destruct (eqA_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql']; + destruct (eq_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql']; try (right; unfold not; intro HF; injection HF; intros; contradiction). rewrite xeqy; rewrite leql'; left; trivial. Qed. @@ -1054,14 +825,6 @@ Section Map. rewrite IHl; auto. Qed. - Hint Constructors Permutation. - - Lemma Permutation_map : - forall l l', Permutation l l' -> Permutation (map l) (map l'). - Proof. - induction 1; simpl; auto; eauto. - Qed. - (** [flat_map] *) Definition flat_map (f:A -> list B) := @@ -1193,10 +956,10 @@ End Fold_Right_Recursor. Proof. destruct l as [| a l]. reflexivity. - simpl in |- *. + simpl. rewrite <- H0. generalize a0 a. - induction l as [| a3 l IHl]; simpl in |- *. + induction l as [| a3 l IHl]; simpl. trivial. intros. rewrite H. @@ -1480,8 +1243,8 @@ End Fold_Right_Recursor. In y l -> In (x, y) (map (fun y0:B => (x, y0)) l). Proof. induction l; - [ simpl in |- *; auto - | simpl in |- *; destruct 1 as [H1| ]; + [ simpl; auto + | simpl; destruct 1 as [H1| ]; [ left; rewrite H1; trivial | right; auto ] ]. Qed. @@ -1490,8 +1253,8 @@ End Fold_Right_Recursor. In x l -> In y l' -> In (x, y) (list_prod l l'). Proof. induction l; - [ simpl in |- *; tauto - | simpl in |- *; intros; apply in_or_app; destruct H; + [ simpl; tauto + | simpl; intros; apply in_or_app; destruct H; [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. Qed. @@ -1524,9 +1287,9 @@ End Fold_Right_Recursor. -(***************************************) -(** * Miscelenous operations on lists *) -(***************************************) +(*****************************************) +(** * Miscellaneous operations on lists *) +(*****************************************) @@ -1544,29 +1307,29 @@ Section length_order. Lemma lel_refl : lel l l. Proof. - unfold lel in |- *; auto with arith. + unfold lel; auto with arith. Qed. Lemma lel_trans : lel l m -> lel m n -> lel l n. Proof. - unfold lel in |- *; intros. + unfold lel; intros. now_show (length l <= length n). apply le_trans with (length m); auto with arith. Qed. Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m). Proof. - unfold lel in |- *; simpl in |- *; auto with arith. + unfold lel; simpl; auto with arith. Qed. Lemma lel_cons : lel l m -> lel l (b :: m). Proof. - unfold lel in |- *; simpl in |- *; auto with arith. + unfold lel; simpl; auto with arith. Qed. Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m. Proof. - unfold lel in |- *; simpl in |- *; auto with arith. + unfold lel; simpl; auto with arith. Qed. Lemma lel_nil : forall l':list A, lel l' nil -> nil = l'. @@ -1625,7 +1388,7 @@ Section SetIncl. Lemma incl_cons : forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m. Proof. - unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1. + unfold incl; simpl; intros a l m H H0 a0 H1. now_show (In a0 m). elim H1. now_show (a = a0 -> In a0 m). @@ -1639,7 +1402,7 @@ Section SetIncl. Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n. Proof. - unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1. + unfold incl; simpl; intros l m n H H0 a H1. now_show (In a n). elim (in_app_or _ _ _ H1); auto. Qed. @@ -1762,34 +1525,6 @@ Section ReDun. destruct (IHl _ _ H1); auto. Qed. - Lemma NoDup_Permutation : forall l l', - NoDup l -> NoDup l' -> (forall x, 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 ReDun. @@ -1872,14 +1607,63 @@ induction 1; firstorder; subst; auto. induction l; firstorder. Qed. +Lemma Forall_inv : forall A P (a:A) l, Forall P (a :: l) -> P a. +Proof. +intros; inversion H; trivial. +Defined. + +Lemma Forall_rect : forall A (P:A->Prop) (Q : list A -> Type), + Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall P l -> Q l. +Proof. +intros A P Q H H'; induction l; intro; [|eapply H', Forall_inv]; eassumption. +Defined. + +Lemma Forall_impl : forall A (P Q : A -> Prop), (forall a, P a -> Q a) -> + forall l, Forall P l -> Forall Q l. +Proof. + intros A P Q Himp l H. + induction H; firstorder. +Qed. + (** [Forall2]: stating that elements of two lists are pairwise related. *) -Inductive Forall2 {A B} (R:A->B->Prop) : list A -> list B -> Prop := - | Forall2_nil : Forall2 R nil nil +Inductive Forall2 A B (R:A->B->Prop) : list A -> list B -> Prop := + | Forall2_nil : Forall2 R [] [] | Forall2_cons : forall x y l l', R x y -> Forall2 R l l' -> Forall2 R (x::l) (y::l'). Hint Constructors Forall2. +Theorem Forall2_refl : forall A B (R:A->B->Prop), Forall2 R [] []. +Proof. exact Forall2_nil. Qed. + +Theorem Forall2_app_inv_l : forall A B (R:A->B->Prop) l1 l2 l', + Forall2 R (l1 ++ l2) l' -> + exists l1', exists l2', Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l' = l1' ++ l2'. +Proof. + induction l1; intros. + exists [], l'; auto. + simpl in H; inversion H; subst; clear H. + apply IHl1 in H4 as (l1' & l2' & Hl1 & Hl2 & ->). + exists (y::l1'), l2'; simpl; auto. +Qed. + +Theorem Forall2_app_inv_r : forall A B (R:A->B->Prop) l1' l2' l, + Forall2 R l (l1' ++ l2') -> + exists l1, exists l2, Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l = l1 ++ l2. +Proof. + induction l1'; intros. + exists [], l; auto. + simpl in H; inversion H; subst; clear H. + apply IHl1' in H4 as (l1 & l2 & Hl1 & Hl2 & ->). + exists (x::l1), l2; simpl; auto. +Qed. + +Theorem Forall2_app : forall A B (R:A->B->Prop) l1 l2 l1' l2', + Forall2 R l1 l1' -> Forall2 R l2 l2' -> Forall2 R (l1 ++ l2) (l1' ++ l2'). +Proof. + intros. induction l1 in l1', H, H0 |- *; inversion H; subst; simpl; auto. +Qed. + (** [ForallPairs] : specifies that a certain relation should always hold when inspecting all possible pairs of elements of a list. *) @@ -1928,7 +1712,6 @@ Proof. destruct (ForallOrdPairs_In Hl _ _ Hx Hy); subst; intuition. Qed. - (** * Inversion of predicates over lists based on head symbol *) Ltac is_list_constr c := @@ -1978,8 +1761,19 @@ Notation cons := cons (only parsing). Notation length := length (only parsing). Notation app := app (only parsing). (* Compatibility Names *) +Notation tail := tl (only parsing). +Notation head := hd_error (only parsing). +Notation head_nil := hd_error_nil (only parsing). +Notation head_cons := hd_error_cons (only parsing). Notation ass_app := app_assoc (only parsing). Notation app_ass := app_assoc_reverse (only parsing). +Notation In_split := in_split (only parsing). +Notation In_rev := in_rev (only parsing). +Notation In_dec := in_dec (only parsing). +Notation distr_rev := rev_app_distr (only parsing). +Notation rev_acc := rev_append (only parsing). +Notation rev_acc_rev := rev_append_rev (only parsing). +Notation AllS := Forall (only parsing). (* was formerly in TheoryList *) + Hint Resolve app_nil_end : datatypes v62. (* end hide *) - diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index da3018a48..7ed9c519b 100644 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -12,6 +12,10 @@ Require Export List. Set Implicit Arguments. + +Local Notation "[ ]" := nil (at level 0). +Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0). + Section Lists. Variable A : Type. @@ -23,11 +27,13 @@ Variable A : Type. Definition Isnil (l:list A) : Prop := nil = l. Lemma Isnil_nil : Isnil nil. +Proof. red in |- *; auto. Qed. Hint Resolve Isnil_nil. Lemma not_Isnil_cons : forall (a:A) (l:list A), ~ Isnil (a :: l). +Proof. unfold Isnil in |- *. intros; discriminate. Qed. @@ -35,6 +41,7 @@ Qed. Hint Resolve Isnil_nil not_Isnil_cons. Lemma Isnil_dec : forall l:list A, {Isnil l} + {~ Isnil l}. +Proof. intro l; case l; auto. (* Realizer (fun l => match l with @@ -50,6 +57,7 @@ Qed. Lemma Uncons : forall l:list A, {a : A & {m : list A | a :: m = l}} + {Isnil l}. +Proof. intro l; case l. auto. intros a m; intros; left; exists a; exists m; reflexivity. @@ -67,6 +75,7 @@ Qed. Lemma Hd : forall l:list A, {a : A | exists m : list A, a :: m = l} + {Isnil l}. +Proof. intro l; case l. auto. intros a m; intros; left; exists a; exists m; reflexivity. @@ -81,6 +90,7 @@ Qed. Lemma Tl : forall l:list A, {m : list A | (exists a : A, a :: m = l) \/ Isnil l /\ Isnil m}. +Proof. intro l; case l. exists (nil (A:=A)); auto. intros a m; intros; exists m; left; exists a; reflexivity. @@ -105,6 +115,7 @@ Fixpoint Length_l (l:list A) (n:nat) : nat := (* A tail recursive version *) Lemma Length_l_pf : forall (l:list A) (n:nat), {m : nat | n + length l = m}. +Proof. induction l as [| a m lrec]. intro n; exists n; simpl in |- *; auto. intro n; elim (lrec (S n)); simpl in |- *; intros. @@ -115,6 +126,7 @@ Realizer Length_l. Qed. Lemma Length : forall l:list A, {m : nat | length l = m}. +Proof. intro l. apply (Length_l_pf l 0). (* Realizer (fun l -> Length_l_pf l O). @@ -139,11 +151,6 @@ elim l; intros; elim H; auto. Qed. -Inductive AllS (P:A -> Prop) : list A -> Prop := - | allS_nil : AllS P nil - | allS_cons : forall (a:A) (l:list A), P a -> AllS P l -> AllS P (a :: l). -Hint Resolve allS_nil allS_cons. - Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}. Fixpoint mem (a:A) (l:list A) : bool := @@ -154,7 +161,7 @@ Fixpoint mem (a:A) (l:list A) : bool := Hint Unfold In. Lemma Mem : forall (a:A) (l:list A), {In a l} + {AllS (fun b:A => b <> a) l}. -intros a l. +Proof. induction l. auto. elim (eqA_dec a a0). @@ -188,16 +195,19 @@ Hint Resolve fst_nth_O fst_nth_S. Lemma fst_nth_nth : forall (l:list A) (n:nat) (a:A), fst_nth_spec l n a -> nth_spec l n a. +Proof. induction 1; auto. Qed. Hint Immediate fst_nth_nth. Lemma nth_lt_O : forall (l:list A) (n:nat) (a:A), nth_spec l n a -> 0 < n. +Proof. induction 1; auto. Qed. Lemma nth_le_length : forall (l:list A) (n:nat) (a:A), nth_spec l n a -> n <= length l. +Proof. induction 1; simpl in |- *; auto with arith. Qed. @@ -211,6 +221,7 @@ Fixpoint Nth_func (l:list A) (n:nat) : Exc A := Lemma Nth : forall (l:list A) (n:nat), {a : A | nth_spec l n a} + {n = 0 \/ length l < n}. +Proof. induction l as [| a l IHl]. intro n; case n; simpl in |- *; auto with arith. intro n; destruct n as [| [| n1]]; simpl in |- *; auto. @@ -227,6 +238,7 @@ Qed. Lemma Item : forall (l:list A) (n:nat), {a : A | nth_spec l (S n) a} + {length l <= n}. +Proof. intros l n; case (Nth l (S n)); intro. case s; intro a; left; exists a; auto. right; case o; intro. @@ -246,6 +258,7 @@ Fixpoint index_p (a:A) (l:list A) : nat -> Exc nat := Lemma Index_p : forall (a:A) (l:list A) (p:nat), {n : nat | fst_nth_spec l (S n - p) a} + {AllS (fun b:A => a <> b) l}. +Proof. induction l as [| b m irec]. auto. intro p. @@ -264,6 +277,7 @@ Lemma Index : forall (a:A) (l:list A), {n : nat | fst_nth_spec l n a} + {AllS (fun b:A => a <> b) l}. +Proof. intros a l; case (Index_p a l 1); auto. intros [n P]; left; exists n; auto. rewrite (minus_n_O n); trivial. @@ -287,20 +301,24 @@ Definition InR_inv (l:list A) := end. Lemma InR_INV : forall l:list A, InR l -> InR_inv l. +Proof. induction 1; simpl in |- *; auto. Qed. Lemma InR_cons_inv : forall (a:A) (l:list A), InR (a :: l) -> R a \/ InR l. +Proof. intros a l H; exact (InR_INV H). Qed. Lemma InR_or_app : forall l m:list A, InR l \/ InR m -> InR (l ++ m). +Proof. intros l m [| ]. induction 1; simpl in |- *; auto. intro. induction l; simpl in |- *; auto. Qed. Lemma InR_app_or : forall l m:list A, InR (l ++ m) -> InR l \/ InR m. +Proof. intros l m; elim l; simpl in |- *; auto. intros b l' Hrec IAc; elim (InR_cons_inv IAc); auto. intros; elim Hrec; auto. @@ -315,6 +333,7 @@ Fixpoint find (l:list A) : Exc A := end. Lemma Find : forall l:list A, {a : A | In a l & R a} + {AllS P l}. +Proof. induction l as [| a m [[b H1 H2]| H]]; auto. left; exists b; auto. destruct (RS_dec a). @@ -342,6 +361,7 @@ Fixpoint try_find (l:list A) : Exc B := Lemma Try_find : forall l:list A, {c : B | exists2 a : A, In a l & T a c} + {AllS P l}. +Proof. induction l as [| a m [[b H1]| H]]. auto. left; exists b; destruct H1 as [a' H2 H3]; exists a'; auto. @@ -383,6 +403,7 @@ Hint Resolve allS_assoc_nil allS_assoc_cons. Lemma Assoc : forall (a:A) (l:list (A * B)), B + {AllS_assoc (fun a':A => a <> a') l}. +Proof. induction l as [| [a' b] m assrec]. auto. destruct (eqA_dec a a'). left; exact b. @@ -398,6 +419,5 @@ End Assoc_sec. End Lists. -Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons: - datatypes. +Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons : datatypes. Hint Immediate fst_nth_nth: datatypes. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 75b9f2efa..7216ae335 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -10,7 +10,7 @@ (* G. Huet 1-9-95 *) -Require Import Permut. +Require Import Permut Setoid. Set Implicit Arguments. @@ -18,6 +18,7 @@ Section multiset_defs. Variable A : Type. Variable eqA : A -> A -> Prop. + Hypothesis eqA_equiv : Equivalence eqA. Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}. Inductive multiset : Type := @@ -167,6 +168,15 @@ Section multiset_defs. apply multiset_twist2. Qed. + (** SingletonBag *) + + Lemma meq_singleton : forall a a', + eqA a a' -> meq (SingletonBag a) (SingletonBag a'). + Proof. + intros; red; simpl; intro a0. + destruct (Aeq_dec a a0) as [Ha|Ha]; rewrite H in Ha; + decide (Aeq_dec a' a0) with Ha; reflexivity. + Qed. (*i theory of minter to do similarly Require Min. 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 *) +(* <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$ i*) + +(** A modular implementation of mergesort (the complexity is O(n.log n) in + the length of the list) *) + +(* Initial author: Hugo Herbelin, Oct 2009 *) + +Require Import List Setoid Permutation Sorted. + +(** Notations and conventions *) + +Local Notation "[ ]" := nil. +Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..). + +Open Scope bool_scope. + +Local Coercion eq_true : bool >-> 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 *) +(* <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$ i*) + +(* Made by Hugo Herbelin *) + +(** This file defines two notions of sorted list: + + - a list is locally sorted if any element is smaller or equal than + its successor in the list + - a list is sorted if any element coming before another one is + smaller or equal than this other element + + The two notions are equivalent if the order is transitive. +*) + +Require Import List Relations Relations_1. + +(** Preambule *) + +Set Implicit Arguments. +Local Notation "[ ]" := nil (at level 0). +Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0). +Implicit Arguments Transitive [U]. + +Section defs. + + Variable A : Type. + Variable R : A -> 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 |