diff options
Diffstat (limited to 'theories/Sorting/Permutation.v')
| -rw-r--r-- | theories/Sorting/Permutation.v | 357 |
1 files changed, 179 insertions, 178 deletions
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 0f2e02b5..3ff026c2 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Permutation.v 8823 2006-05-16 16:17:43Z letouzey $ i*) +(*i $Id: Permutation.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Relations. Require Import List. @@ -14,193 +14,194 @@ Require Import Multiset. Require Import Arith. (** 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 multiplicities in the two lists. + there exists a permutation between two lists iff every elements have + the same multiplicities in the two lists. - Unlike [List.Permutation], the present notion of permutation requires - a decidable equality. At the same time, this definition can be used - with a non-standard equality, whereas [List.Permutation] cannot. + Unlike [List.Permutation], the present notion of permutation requires + a decidable equality. At the same time, this definition can be used + with a non-standard equality, whereas [List.Permutation] cannot. - The present file contains basic results, obtained without any particular - assumption on the decidable equality used. + 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). + File [PermutSetoid] contains additional results about permutations + with respect to an setoid equality (i.e. an equivalence relation). - 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. -*) + 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. +x*) Set Implicit Arguments. Section defs. -Variable A : Set. -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. -Hint Resolve list_contents_app. - -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. -Hint Resolve permut_refl. - -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. -Hint Resolve permut_cons. - -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 with datatypes. -apply meq_trans with (munion (list_contents l') (list_contents m')); - auto with datatypes. -apply meq_trans with (munion (list_contents l') (list_contents m)); - auto with datatypes. -Qed. -Hint Resolve permut_app. - -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. -Qed. -Hint Resolve permut_middle. - -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; auto. -simpl. -apply permut_add_cons_inside. -rewrite <- app_nil_end; auto. -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. + (** * From lists to multisets *) + + Variable A : Set. + 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 *) + +(** For compatibilty *) Notation permut_right := permut_cons. Unset Implicit Arguments. |