(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) include "basics/lists/list.ma". include "basics/relations.ma". inductive permutation (A : Type[0]) : relation (list A) ≝ | perm_nil : permutation A [ ] [ ] | perm_skip : ∀x, l1, l2. permutation A l1 l2 → permutation A (x :: l1) (x :: l2) | perm_swap : ∀x, y, l. permutation A (x :: y :: l) (y :: x :: l) | perm_trans : transitive ? (permutation A). interpretation "list permutation" 'napart l1 l2 = (permutation ? l1 l2). lemma perm_refl : ∀A.reflexive ? (permutation A). #A #l elim l /2/ qed. lemma perm_symm : ∀A.symmetric ? (permutation A). #A #l #m #H elim H /2 by perm_nil, perm_skip, perm_swap, perm_trans/ qed. lemma perm_nil_eq_nil : ∀A.∀l : list A.[ ] ≈ l → l = [ ]. #A #l lapply (refl (list A) [ ]) generalize in match [ ] in ⊢ (??%?→%); #m #EQ #H lapply EQ -EQ elim H [ // | #x #l1 #l2 #H #IH #EQ destruct | #x #y #l #EQ destruct | #l1 #l2 #l3 #H1 #H2 #IH1 #IH2 #EQ1 lapply (IH1 EQ1) #EQ2 destruct /2/ ] qed. lemma perm_nil_cons : ∀A,x.∀l : list A.¬ [ ] ≈ x :: l. #A #x #l % #H lapply (perm_nil_eq_nil … H) #ABS destruct qed. lemma perm_append_r : ∀A.∀l,m1,m2 : list A.m1 ≈ m2 → l @ m1 ≈ l @ m2. #A #l elim l /3 by perm_skip/ qed. lemma perm_append : ∀A.∀l1,l2,m1,m2 : list A.l1 ≈ l2 → m1 ≈ m2 → l1 @ m1 ≈ l2 @ m2. #A #l1 #l2 #m1 #m2 #H lapply m2 lapply m1 -m1 -m2 elim H [ // | /3 by perm_skip/ | /3 by perm_swap, perm_trans, perm_append_r/ | #l1' #l2' #l3' #H1 #H2 #IH1 #IH2 #m #n #G %4{(l2'@m)} [ @IH1 @perm_refl | @IH2 @G ] ] qed. lemma perm_append_l : ∀A.∀l1, l2, m : list A. l1 ≈ l2 → l1 @ m ≈ l2 @ m. /2 by perm_append/ qed. lemma perm_move_hd : ∀A,x.∀pre, post : list A. x :: pre @ post ≈ pre @ x :: post. #A #x #pre lapply x -x elim pre [ // | #hd #tl #IH #x #post %4{(hd :: x :: tl @ post) (perm_swap …)} @perm_skip @IH ] qed. lemma perm_swap_inside : ∀A.∀x,y.∀pre, mid, post : list A. pre @ x :: mid @ y :: post ≈ pre @ y :: mid @ x :: post. #A #x #y #pre #mid #post @perm_append_r %4{(mid @ x :: y :: post) (perm_move_hd …)} %4{(mid @ y :: x :: post)} /2 by perm_swap, perm_symm, perm_append_r/ qed. lemma perm_swap_append : ∀A.∀l1, l2 : list A. l1 @ l2 ≈ l2 @ l1. #A #l1 elim l1 [ #l2 >append_nil @perm_refl | #hd #tl #IH #l2 %4{(hd :: l2 @ tl)} /2 by perm_skip/ ] qed. lemma perm_All : ∀A,P,l1,l2.All A P l1 → l1 ≈ l2 → All A P l2. #A #P #l1 #l2 #H #G lapply H -H elim G -G [ *% | #x #l1' #l2' #G #IH * #Px #Pl1' %{Px} @IH @Pl1' | #x #y #l * #Px * #Py #Pl %{Py} %{Px Pl} | #l1' #l2' #l3' #H1 #H2 #IH1 #IH2 /3/ ] qed. lemma perm_Exists : ∀A,P,l1,l2.Exists A P l1 → l1 ≈ l2 → Exists A P l2. #A #P #l1 #l2 #H #G lapply H -H elim G -G [ * | #x #l1' #l2' #G #IH * [#Px %1{Px} | #Pl %2 @IH @Pl] | #x #y #l * [#Px %2 %1{Px} | * [#Py %1{Py} | #Pl %2 %2{Pl}]] | #l1' #l2' #l3' #H1 #H2 #IH1 #IH2 /3 by / ] qed. lemma perm_length : ∀A.∀l1, l2 : list A. l1 ≈ l2 → |l1| = |l2|. #A #l1 #l2 #H elim H -H normalize // qed. lemma perm_singleton_eq : ∀A,x.∀l : list A.[x] ≈ l → l = [x]. #A #x #l lapply (refl ? ([x])) generalize in match ([x]) in ⊢ (??%?→%); #m #EQ #H lapply EQ -EQ lapply x -x elim H [ #x #EQ destruct | #x #l1 #l2 #G #IH #y #EQ destruct >(perm_nil_eq_nil … G) % | #x #y #l' #z #EQ destruct | #l1 #l2 #l3 #H1 #H2 #IH1 #IH2 #x #K lapply (IH1 ? K) >K #EQ >(IH2 ? EQ) @EQ ] qed. lemma perm_map : ∀A,B,f,m,l.m ≈ l → map A B f m ≈ map A B f l. #A #B #f #m #l #H elim H -H /2 by perm_skip, perm_swap, perm_trans/ qed. lemma perm_filter : ∀A,f,m,l.m ≈ l → filter A f m ≈ filter A f l. #A #f #m #l #H elim H -H [1,4: /2 by perm_trans/] [ #x #l' #m' #H #IH normalize elim (f x) normalize /2 by perm_skip/ | #x #y #l' normalize elim (f y) elim (f x) normalize // ] qed. lemma perm_reverse : ∀A.∀l : list A.l ≈ reverse A l. #A #l elim l [//] #hd #tl normalize >rev_append_def >append_nil #IH >rev_append_def %4{(tl @ [hd])} [ <(append_nil ? tl) in ⊢(??%?); @perm_move_hd | @perm_append_l @IH ] qed. lemma permutation_ind_bis : ∀A.∀P : relation (list A). (P [ ] [ ]) → (∀x,l,l'.l ≈ l' → P l l' → P (x :: l) (x :: l')) → (∀x,y,l,l'.l ≈ l' → P l l' → P (x :: y :: l) (y :: x :: l')) → (∀l,l',l''.l ≈ l' → P l l' → l' ≈ l'' → P l' l'' → P l l'') → ∀l,l'.l ≈ l' → P l l'. #A #P #H1 #H2 #H3 #H4 #l #l' #H elim H /2/ [2: #l1 #l2 #l3 #G1 #G2 #G3 #G4 @(H4 … G1 G3 G2 G4)] #x #y #l1 @H3 // elim l1 [@H1] #hd #tl #Ptl @H2 // qed. lemma Exists_split : ∀A,P,l.Exists A P l → ∃x,pre,post.l = pre @ x :: post ∧ P x. #A #P #l elim l [2: #hd #tl #IH] * [ #Phd %{hd} %{[]} %{tl} /2 by conj/ | #Ptl elim (IH Ptl) #x * #pre * #post * #EQ #Px %{x} %{(hd :: pre)} %{post} >EQ /2 by conj/ ] qed. lemma perm_middle_inv : ∀A.∀x.∀l1,l2,m1,m2 : list A. l1 @ x :: l2 ≈ m1 @ x :: m2 → l1 @ l2 ≈ m1 @ m2. #A #x #l1 #l2 #m1 #m2 lapply (refl … (l1 @ x :: l2)) generalize in match (l1 @ x :: l2) in ⊢ (??%?→%); lapply (refl … (m1 @ x :: m2)) generalize in match (m1 @ x :: m2) in ⊢ (??%?→%); #l #EQl #m #EQm #H lapply EQm -EQm lapply EQl -EQl lapply m2 -m2 lapply m1 -m1 lapply l2 -l2 lapply l1 -l1 lapply x -x @(permutation_ind_bis … H) -H [ #x #l1 #l2 #m1 #m2 #H elim (nil_to_nil … (sym_eq ??? H)) #_ #ABS destruct | #hd #tl1 #tl2 #H #IH #x * [2: #hdl1 #tll1] #l2 * [2,4: #hdm1 #tlm1] #m2 normalize #EQ1 #EQ2 destruct [ %2 @(IH … (refl …) (refl …)) | %4{H} @perm_symm @perm_move_hd | %4{(perm_move_hd …) H} | @H ] | #hd1 #hd2 #tl1 #tl2 #H #IH #x * [2: #hdl1 * [2: #hdl1' #tll1]] #l2 * [2,4,6: #hdm1 * [2,4,6: #hdm1' #tlm1 ]] #m2 normalize #EQ1 #EQ2 destruct [ %4{? (perm_swap …)} %2 %2 @(IH … (refl …)(refl …)) | %4{? (perm_skip … H)} %4{? (perm_skip …) (perm_swap …)} @perm_symm @perm_move_hd | %2 %4{? H} @perm_symm @perm_move_hd | %4{?? (perm_skip … H)} change with (? :: (? :: ?) @ ? ≈ (? :: ?) @ ? :: ?) @perm_move_hd | %2{H} | %2{H} | %2 %4{?? H} @perm_move_hd | %2{H} | %2{H} ] | #l1' #l2' #l3' #H1 #IH1 #H2 #IH2 #x #l1 #l2 #m1 #m2 #G2 #G1 cut (Exists ? (eq ? x) l2') [ @(perm_Exists … H1) >G1 @Exists_mid %] #x_in_l2' elim (Exists_split … x_in_l2') #y * #pre * #post * #EQ #EQ' destruct(EQ') %4{? (IH1 … EQ G1) (IH2 … G2 EQ)} ] qed. lemma perm_split : ∀A,x.∀pre,post,l : list A.pre@x :: post ≈ l → ∃pre',post'.l = pre' @ x :: post' ∧ pre @ post ≈ pre' @ post'. #A #x #pre #post #l #H cut (Exists ? (eq ? x) l) [ @(perm_Exists … H) /2 by Exists_mid/ ] #G elim (Exists_split … G) -G #y * #pre' * #post' * #EQ #EQ' destruct(EQ') %{pre'} %{post'} %{EQ} >EQ in H; @perm_middle_inv qed. lemma perm_cons_inv : ∀A.∀x.∀l1,l2 : list A.x :: l1 ≈ x :: l2 → l1 ≈ l2. #A #x #l1 #l2 change with ([ ] @ ? ≈ [ ] @ ? → ?) #H @(perm_middle_inv … H) qed. lemma perm_cons_split : ∀A.∀x.∀l1,l2 : list A.x :: l1 ≈ l2 → ∃pre,post.l2 = pre @ x :: post ∧ l1 ≈ pre @ post. #A #x #l1 #l2 change with ([ ] @ ? ≈ ? → ?) @perm_split qed. lemma map_append_inv : ∀A,B,f,l,m1,m2.map A B f l = m1 @ m2 → ∃l1,l2.map … f l1 = m1 ∧ map … f l2 = m2 ∧ l = l1 @ l2. #A #B #f #l elim l [ #y #m normalize #H @(nil_append_elim … (sym_eq … H)) %{[]} %{[]} %%% | #hd #tl #IH * [ * [2: #hd' #tl' ] | #hd' #tl' #m2] normalize #EQ destruct [ %{[]} % [2: %%% |] | elim (IH … e0) #m1' * #m2' ** #H1 #H2 #H3 destruct change with ((? :: ?) @ ?) in match (? :: ? @ ?); % [2: % [2: %%% ]|] ] ] qed. lemma injective_map_perm : ∀A,B,f,m,l.injective ?? f → map A B f m ≈ map A B f l → m ≈ l. #A #B #f #m elim m [ #l #H normalize cases l [//] #hd #tl #G lapply (perm_nil_eq_nil … G) normalize #ABS destruct | #hd #tl #IH #l #H normalize #G elim (perm_cons_split ???? G) #pre * #post * #EQ #K elim(map_append_inv … EQ) #pre' ** normalize [2: #hd' #tl'] ** #EQ1 #EQ2 #EQ3 destruct lapply (H … e0) #EQ' destruct %4{(perm_move_hd …)} %2 @(IH … H) EQ in H; #H lapply (perm_middle_inv ?????? H) normalize IH % | #x #y #l' normalize cases (p x) cases (p y) normalize [1: |*: // ] >assoc >assoc >comm in ⊢ (??(????%?)?); % | // ] qed.