(************************************************************************) (* Houda ANOUN *) (* 2004 -2005 *) (* About List Permutation *) (* LaBRI *) (************************************************************************) Require Export Permutation. Require Export List. Require Export Arith. Require Export Omega. Require Import Relations. Require Import Multiset. Set Implicit Arguments. Section perm. Variables A B:Set. Variable decA : forall a b : A, {a = b} + {a <> b}. (* some additional lemmas and definitions about lists *) Inductive insert(A:Set)(a:A):list A ->list A->Prop:= |insert_fst:forall (l1 :list A), insert a l1 (a::l1) |insert_rest :forall l1 l2 b, insert a l1 l2 -> insert a (b::l1) (b::l2). Lemma insert_in:forall (l1:list A)a, In a l1-> (exists l2, insert a l2 l1). Proof. intros l1; elim l1. simpl in |- *; tauto. simpl in |- *. intros. case H0. intro; subst; exists l; constructor. intro. elim (H _ H1); intros. econstructor. constructor 2; eauto. Qed. (*********************************************************) (* Inductive definition of list permutation *) (*********************************************************) (* taken from Coq reference manual (Chapter 10) *) Inductive permI :list A ->list A ->Prop:= |permI_refl:forall l, permI l l |permI_cons:forall a l0 l1, permI l0 l1-> permI (a::l0)(a::l1) |permI_app:forall a l, permI (a::l) (l++(a::nil)) |permI_trans:forall l1 l2 l3, permI l1 l2 -> permI l2 l3 -> permI l1 l3. Lemma permI_app_com:forall (l1 l2:list A), permI (l1++l2)(l2++l1). Proof. intro l1; elim l1. simpl in |- *. intro; rewrite <- app_nil_end. constructor. intros. econstructor 4. simpl in |- *. constructor 3. rewrite app_ass. replace (l2 ++ a :: l) with ((l2 ++ a :: nil) ++ l). auto. rewrite app_ass. cut ((a :: nil) ++ l = a :: l). intro; subst; auto. simpl in |- *. auto. Qed. Lemma permI_sym: symmetric _ permI. Proof. unfold symmetric; induction 1. constructor. constructor; auto. replace (a :: l) with ((a :: nil) ++ l). apply permI_app_com; constructor. simpl in |- *; auto. econstructor 4; eauto. Qed. Lemma permI_insert:forall (l1 l2:list A)a, insert a l1 l2-> permI (a::l1) l2. Proof. induction 1. constructor. econstructor 4. econstructor 3. simpl in |- *. constructor. constructor 4 with (a :: l1). apply permI_sym; constructor. auto. Qed. (***************************************************) (* properties about permutation (with multisets) *) (***************************************************) Lemma multiplicity_of_append:forall (l1 l2:list A)a, multiplicity (list_contents (eq (A:=A)) decA (l1 ++l2)) a= multiplicity (list_contents (eq (A:=A))decA l1) a + multiplicity (list_contents (eq (A:=A))decA l2) a. Proof. intros l1; elim l1; simpl in |- *. auto. intros. rewrite (H l2 a0). omega. Qed. Lemma permutation_of_nil:forall (l:list A), permutation (eq(A:=A)) decA nil l-> l=nil. Proof. unfold permutation, meq in |- *. simpl in |- *. intro l; case l. auto. simpl in |- *. intros. absurd (0 = 1 + multiplicity (list_contents (eq (A:=A)) decA l0) a). omega. replace 1 with (if decA a a then 1 else 0). auto. case (decA a a). auto. induction 1. auto. Qed. Lemma multiplicity_positive:forall (l:list A) a, multiplicity (list_contents (eq (A:=A)) decA l) a >=1 -> In a l. Proof. intro l; elim l. simpl in |- *. inversion 2. intros. simpl in H0. generalize H0; case (decA a a0). intros; subst; simpl in |- *; tauto. simpl in |- *. intros; right. auto. Qed. Lemma multiplicity_insert_eq:forall (l1 l2:list A) a, insert a l1 l2-> multiplicity (list_contents (eq (A:=A)) decA l2) a= S(multiplicity (list_contents (eq (A:=A)) decA l1) a). Proof. induction 1. simpl in |- *. case (decA a a). intro; omega. induction 1. auto. simpl in |- *. rewrite IHinsert; omega. Qed. Lemma multiplicity_insert_diff:forall (l1 l2:list A) a a0, insert a l1 l2-> a<>a0-> multiplicity (list_contents (eq (A:=A)) decA l2) a0= multiplicity (list_contents (eq (A:=A)) decA l1) a0. Proof. induction 1. simpl in |- *. case (decA a a0). intros. elim H; auto. intros; auto. simpl in |- *. intro; rewrite IHinsert. omega. auto. Qed. Lemma permutation_of_insert:forall (l1 l2 :list A) a, insert a l1 l2 -> forall l3 , permutation (eq(A:=A)) decA (a::l3) l2-> permutation (eq(A:=A)) decA l3 l1. Proof. unfold permutation, meq in |- *. simpl in |- *. intros. pose (H0 a0). generalize e. clear e. case (decA a a0). intros H1 H2. subst. rewrite (multiplicity_insert_eq H) in H2. omega. intros H1 H2; rewrite (multiplicity_insert_diff H H1) in H2. omega. Qed. (************************************************) (* equivalence between the two definitions *) (************************************************) Theorem perm_inductive_mset : forall (l1 l2:list A), permI l1 l2 -> permutation (eq(A:=A)) decA l1 l2. Proof. induction 1. apply permut_refl. apply permut_cons; auto. unfold permutation, meq in |- *. simpl in |- *. intros. rewrite multiplicity_of_append. simpl in |- *. omega. eapply permut_tran; eauto. Qed. (* from multiset definition to inductive definition *) Theorem perm_mset_inductive : forall (l1 l2:list A), permutation (eq(A:=A)) decA l1 l2-> permI l1 l2. Proof. intro l1; elim l1. intros. rewrite (permutation_of_nil H). constructor. intros. assert (In a l2). apply multiplicity_positive. unfold permutation, meq in H0. simpl in H0. rewrite <- (H0 a). case (decA a a). intro; omega. induction 1; auto. elim (insert_in _ _ H1). intros. constructor 4 with (a :: x). constructor. apply H. eapply permutation_of_insert. eauto. auto. apply permI_insert; auto. Qed. End perm. Lemma counterexample : ~ permI (2::3::5::5::8::7::4::nil) (3::2::8::7::4::3::5::nil). red;intro. generalize (perm_inductive_mset eq_nat_dec H). intro H0. generalize (H0 3). discriminate 1. Qed.