diff options
Diffstat (limited to 'theories/Sorting/PermutEq.v')
| -rw-r--r-- | theories/Sorting/PermutEq.v | 241 |
1 files changed, 241 insertions, 0 deletions
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v new file mode 100644 index 00000000..e56ff27d --- /dev/null +++ b/theories/Sorting/PermutEq.v @@ -0,0 +1,241 @@ +(************************************************************************) +(* 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: PermutEq.v 8853 2006-05-23 18:17:38Z herbelin $ i*) + +Require Import Omega. +Require Import Relations. +Require Import Setoid. +Require Import List. +Require Import Multiset. +Require Import Permutation. + +Set Implicit Arguments. + +(** This file is similar to [PermutSetoid], except that the equality used here + is Coq usual one instead of a setoid equality. In particular, we can then + prove the equivalence between [List.Permutation] and + [Permutation.permutation]. +*) + +Section Perm. + +Variable A : Set. +Hypothesis eq_dec : forall x y:A, {x=y} + {~ x=y}. + +Notation permutation := (permutation _ eq_dec). +Notation list_contents := (list_contents _ eq_dec). + +(** we can use [multiplicity] to define [In] and [NoDup]. *) + +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. +Qed. + +Lemma multiplicity_In_O : + forall l a, ~ In a l -> multiplicity (list_contents l) a = 0. +Proof. +intros l a; rewrite multiplicity_In; + destruct (multiplicity (list_contents l) a); auto. +destruct 1; auto with arith. +Qed. + +Lemma multiplicity_In_S : + forall l a, In a l -> multiplicity (list_contents l) a >= 1. +Proof. +intros l a; rewrite multiplicity_In; auto. +Qed. + +Lemma multiplicity_NoDup : + forall l, NoDup l <-> (forall a, multiplicity (list_contents l) a <= 1). +Proof. +induction l. +simpl. +split; auto with arith. +intros; apply NoDup_nil. +split; simpl. +inversion_clear 1. +rewrite IHl in H1. +intros; destruct (eq_dec a a0) as [H2|H2]; simpl; auto. +subst a0. +rewrite multiplicity_In_O; auto. +intros; constructor. +rewrite multiplicity_In. +generalize (H a). +destruct (eq_dec a a) as [H0|H0]. +destruct (multiplicity (list_contents l) a); auto with arith. +simpl; inversion 1. +inversion H3. +destruct H0; auto. +rewrite IHl; intros. +generalize (H a0); auto with arith. +destruct (eq_dec a a0); simpl; auto with arith. +Qed. + +Lemma NoDup_permut : + forall l l', NoDup l -> NoDup l' -> + (forall x, In x l <-> In x l') -> permutation l l'. +Proof. +intros. +red; unfold meq; intros. +rewrite multiplicity_NoDup in H, H0. +generalize (H a) (H0 a) (H1 a); clear H H0 H1. +do 2 rewrite multiplicity_In. +destruct 3; omega. +Qed. + +(** Permutation is compatible with In. *) +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. +generalize (P e); clear P. +destruct (In_dec eq_dec e l2) as [H|H]; auto. +rewrite (multiplicity_In_O _ _ H). +intros. +generalize (multiplicity_In_S _ _ IN). +rewrite H0. +inversion 1. +Qed. + +Lemma permut_cons_In : + forall l1 l2 e, permutation (e :: l1) l2 -> In e l2. +Proof. +intros; eapply permut_In_In; eauto. +red; auto. +Qed. + +(** Permutation of an empty list. *) +Lemma permut_nil : + forall l, permutation l nil -> l = nil. +Proof. +intro l; destruct l as [ | e l ]; trivial. +assert (In e (e::l)) by (red; auto). +intro Abs; generalize (permut_In_In _ Abs H). +inversion 1. +Qed. + +(** When used with [eq], this permutation notion is equivalent to + the one defined in [List.v]. *) + +Lemma permutation_Permutation : + forall l l', Permutation l l' <-> permutation l l'. +Proof. +split. +induction 1. +apply permut_refl. +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. +revert l'. +induction l. +intros. +rewrite (permut_nil (permut_sym H)). +apply Permutation_refl. +intros. +destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)). +subst l'. +apply Permutation_cons_app. +apply IHl. +apply permut_remove_hd with a; auto. +Qed. + +(** Permutation for short lists. *) + +Lemma permut_length_1: + forall a b, permutation (a :: nil) (b :: nil) -> a=b. +Proof. +intros a b; unfold Permutation.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. +Qed. + +Lemma permut_length_2 : + forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) -> + (a1=a2) /\ (b1=b2) \/ (a1=b2) /\ (a2=b1). +Proof. +intros a1 b1 a2 b2 P. +assert (H:=permut_cons_In P). +inversion_clear H. +left; split; auto. +apply permut_length_1. +red; red; intros. +generalize (P a); clear P; simpl. +destruct (eq_dec a1 a) as [H2|H2]; + destruct (eq_dec a2 a) as [H3|H3]; auto. +destruct H3; transitivity a1; auto. +destruct H2; transitivity a2; auto. +right. +inversion_clear H0; [|inversion H]. +split; auto. +apply permut_length_1. +red; red; intros. +generalize (P a); clear P; simpl. +destruct (eq_dec a1 a) as [H2|H2]; + destruct (eq_dec b2 a) as [H3|H3]; auto. +simpl; rewrite <- plus_n_Sm; inversion 1; auto. +destruct H3; transitivity a1; auto. +destruct H2; transitivity b2; auto. +Qed. + +(** Permutation is compatible with length. *) +Lemma permut_length : + forall l1 l2, permutation l1 l2 -> length l1 = length l2. +Proof. +induction l1; intros l2 H. +rewrite (permut_nil (permut_sym H)); auto. +destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)). +subst l2. +rewrite app_length. +simpl; rewrite <- plus_n_Sm; f_equal. +rewrite <- app_length. +apply IHl1. +apply permut_remove_hd with a; auto. +Qed. + +Variable B : Set. +Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }. + +(** Permutation is compatible with map. *) + +Lemma permutation_map : + forall f l1 l2, permutation l1 l2 -> + Permutation.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. +simpl. +destruct (In_split _ _ (permut_cons_In P)) as (h2,(t2,H1)). +subst l2. +rewrite map_app. +simpl. +apply permut_add_cons_inside. +rewrite <- map_app. +apply IHl1; auto. +apply permut_remove_hd with a; auto. +Qed. + +End Perm. + |