source: src/utilities/permutations.ma @ 2896

Last change on this file since 2896 was 1976, checked in by tranquil, 7 years ago
  • monads: just changed some defs, which had to be propagated in some files
  • ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
  • added a library for permutations of lists (useful with fold AC ops on lists)
  • first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)
File size: 10.5 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "basics/lists/list.ma".
16include "basics/relations.ma".
17
18inductive permutation (A : Type[0]) : relation (list A) ≝
19| perm_nil : permutation A [ ] [ ]
20| perm_skip : ∀x, l1, l2. permutation A l1 l2 → permutation A (x :: l1) (x :: l2)
21| perm_swap : ∀x, y, l. permutation A (x :: y :: l) (y :: x :: l)
22| perm_trans : transitive ? (permutation A).
23
24interpretation "list permutation" 'napart l1 l2 = (permutation ? l1 l2).
25
26lemma perm_refl : ∀A.reflexive ? (permutation A).
27#A #l elim l /2/ qed.
28
29lemma perm_symm : ∀A.symmetric ? (permutation A).
30#A #l #m #H elim H /2 by perm_nil, perm_skip, perm_swap, perm_trans/
31qed.
32
33lemma perm_nil_eq_nil : ∀A.∀l : list A.[ ] ≈ l → l = [ ].
34#A #l lapply (refl (list A) [ ])
35generalize in match [ ] in ⊢ (??%?→%); #m #EQ #H lapply EQ -EQ elim H
36[ //
37| #x #l1 #l2 #H #IH #EQ destruct
38| #x #y #l #EQ destruct
39| #l1 #l2 #l3 #H1 #H2 #IH1 #IH2 #EQ1 lapply (IH1 EQ1) #EQ2 destruct /2/
40]
41qed.
42
43lemma perm_nil_cons : ∀A,x.∀l : list A.¬ [ ] ≈ x :: l.
44#A #x #l % #H lapply (perm_nil_eq_nil … H) #ABS destruct qed.
45
46lemma perm_append_r : ∀A.∀l,m1,m2 : list A.m1 ≈ m2 → l @ m1 ≈ l @ m2.
47#A #l elim l /3 by perm_skip/ qed.
48
49lemma perm_append : ∀A.∀l1,l2,m1,m2 : list A.l1 ≈ l2 → m1 ≈ m2 → l1 @ m1 ≈ l2 @ m2.
50#A #l1 #l2 #m1 #m2 #H lapply m2 lapply m1 -m1 -m2
51elim H
52[ //
53| /3 by perm_skip/
54| /3 by perm_swap, perm_trans, perm_append_r/
55| #l1' #l2' #l3' #H1 #H2 #IH1 #IH2 #m #n #G %4{(l2'@m)}
56  [ @IH1 @perm_refl
57  | @IH2 @G
58  ]
59]
60qed.
61
62lemma perm_append_l : ∀A.∀l1, l2, m : list A. l1 ≈ l2 → l1 @ m ≈ l2 @ m.
63/2 by perm_append/ qed.
64
65lemma perm_move_hd : ∀A,x.∀pre, post : list A. x :: pre @ post ≈ pre @ x :: post.
66#A #x #pre lapply x -x elim pre
67[ //
68| #hd #tl #IH #x #post
69  %4{(hd :: x :: tl @ post) (perm_swap …)} @perm_skip @IH
70]
71qed.
72
73lemma perm_swap_inside : ∀A.∀x,y.∀pre, mid, post : list A.
74  pre @ x :: mid @ y :: post ≈ pre @ y :: mid @ x :: post.
75#A #x #y #pre #mid #post @perm_append_r
76%4{(mid @ x :: y :: post) (perm_move_hd …)}
77%4{(mid @ y :: x :: post)} /2 by perm_swap, perm_symm, perm_append_r/
78qed.
79
80lemma perm_swap_append : ∀A.∀l1, l2 : list A. l1 @ l2 ≈ l2 @ l1.
81#A #l1 elim l1
82[ #l2 >append_nil @perm_refl
83| #hd #tl #IH #l2
84  %4{(hd :: l2 @ tl)} /2 by perm_skip/
85]
86qed.
87
88lemma perm_All : ∀A,P,l1,l2.All A P l1 → l1 ≈ l2 → All A P l2.
89#A #P #l1 #l2 #H #G lapply H -H elim G -G
90[ *%
91| #x #l1' #l2' #G #IH * #Px #Pl1' %{Px} @IH @Pl1'
92| #x #y #l * #Px * #Py #Pl %{Py} %{Px Pl}
93| #l1' #l2' #l3' #H1 #H2 #IH1 #IH2 /3/
94]
95qed.
96
97lemma perm_Exists : ∀A,P,l1,l2.Exists A P l1 → l1 ≈ l2 → Exists A P l2.
98#A #P #l1 #l2 #H #G lapply H -H elim G -G
99[ *
100| #x #l1' #l2' #G #IH * [#Px %1{Px} | #Pl %2 @IH @Pl]
101| #x #y #l * [#Px %2 %1{Px} | * [#Py %1{Py} | #Pl %2 %2{Pl}]]
102| #l1' #l2' #l3' #H1 #H2 #IH1 #IH2 /3 by /
103]
104qed.
105
106lemma perm_length : ∀A.∀l1, l2 : list A. l1 ≈ l2 → |l1| = |l2|.
107#A #l1 #l2 #H elim H -H normalize //
108qed.
109
110lemma perm_singleton_eq : ∀A,x.∀l : list A.[x] ≈ l → l = [x].
111#A #x #l lapply (refl ? ([x]))
112generalize in match ([x]) in ⊢ (??%?→%);
113#m #EQ #H lapply EQ -EQ lapply x -x elim H
114[ #x #EQ destruct
115| #x #l1 #l2 #G #IH #y #EQ destruct >(perm_nil_eq_nil … G) %
116| #x #y #l' #z #EQ destruct
117| #l1 #l2 #l3 #H1 #H2 #IH1 #IH2 #x #K lapply (IH1 ? K) >K #EQ >(IH2 ? EQ) @EQ
118]
119qed.
120
121lemma perm_map : ∀A,B,f,m,l.m ≈ l → map A B f m ≈ map A B f l.
122#A #B #f #m #l #H elim H -H /2 by perm_skip, perm_swap, perm_trans/
123qed.
124
125lemma perm_filter : ∀A,f,m,l.m ≈ l → filter A f m ≈ filter A f l.
126#A #f #m #l #H elim H -H [1,4: /2 by perm_trans/]
127[ #x #l' #m' #H #IH normalize elim (f x) normalize /2 by perm_skip/
128| #x #y #l' normalize elim (f y) elim (f x) normalize //
129]
130qed.
131
132lemma perm_reverse : ∀A.∀l : list A.l ≈ reverse A l.
133#A #l elim l [//]
134#hd #tl normalize >rev_append_def >append_nil #IH >rev_append_def
135%4{(tl @ [hd])}
136[ <(append_nil ? tl) in ⊢(??%?); @perm_move_hd
137| @perm_append_l @IH
138]
139qed.
140
141lemma permutation_ind_bis : ∀A.∀P : relation (list A).
142  (P [ ] [ ]) →
143  (∀x,l,l'.l ≈ l' → P l l' → P (x :: l) (x :: l')) →
144  (∀x,y,l,l'.l ≈ l' → P l l' → P (x :: y :: l) (y :: x :: l')) →
145  (∀l,l',l''.l ≈ l' → P l l' → l' ≈ l'' → P l' l'' → P l l'') →
146  ∀l,l'.l ≈ l' → P l l'.
147#A #P #H1 #H2 #H3 #H4 #l #l' #H elim H /2/
148[2: #l1 #l2 #l3 #G1 #G2 #G3 #G4 @(H4 … G1 G3 G2 G4)]
149#x #y #l1 @H3 //
150elim l1 [@H1] #hd #tl #Ptl @H2 //
151qed.
152
153lemma Exists_split : ∀A,P,l.Exists A P l → ∃x,pre,post.l = pre @ x :: post ∧ P x.
154#A #P #l elim l [2: #hd #tl #IH] *
155[ #Phd %{hd} %{[]} %{tl} /2 by conj/
156| #Ptl elim (IH Ptl) #x * #pre * #post
157  * #EQ #Px
158  %{x} %{(hd :: pre)} %{post} >EQ /2 by conj/
159]
160qed.
161
162lemma perm_middle_inv : ∀A.∀x.∀l1,l2,m1,m2 : list A.
163  l1 @ x :: l2 ≈ m1 @ x :: m2 → l1 @ l2 ≈ m1 @ m2.
164#A #x #l1 #l2 #m1 #m2
165lapply (refl … (l1 @ x :: l2))
166generalize in match (l1 @ x :: l2) in ⊢ (??%?→%);
167lapply (refl … (m1 @ x :: m2))
168generalize in match (m1 @ x :: m2) in ⊢ (??%?→%);
169#l #EQl #m #EQm #H
170lapply EQm -EQm lapply EQl -EQl
171lapply m2 -m2 lapply m1 -m1 lapply l2 -l2 lapply l1 -l1
172lapply x -x
173@(permutation_ind_bis … H) -H
174[ #x #l1 #l2 #m1 #m2 #H elim (nil_to_nil … (sym_eq ??? H)) #_ #ABS destruct
175| #hd #tl1 #tl2 #H #IH #x
176  * [2: #hdl1 #tll1] #l2
177  * [2,4: #hdm1 #tlm1] #m2 normalize
178  #EQ1 #EQ2 destruct
179  [ %2 @(IH … (refl …) (refl …))
180  | %4{H} @perm_symm @perm_move_hd
181  | %4{(perm_move_hd …) H}
182  | @H
183  ]
184| #hd1 #hd2 #tl1 #tl2 #H #IH #x
185  * [2: #hdl1 * [2: #hdl1' #tll1]] #l2
186  * [2,4,6: #hdm1 * [2,4,6: #hdm1' #tlm1 ]] #m2 normalize
187  #EQ1 #EQ2 destruct
188  [ %4{? (perm_swap …)} %2 %2 @(IH … (refl …)(refl …))
189  | %4{? (perm_skip … H)}
190    %4{? (perm_skip …) (perm_swap …)} @perm_symm @perm_move_hd
191  | %2 %4{? H} @perm_symm @perm_move_hd
192  | %4{?? (perm_skip … H)} change with (? :: (? :: ?) @ ? ≈ (? :: ?) @ ? :: ?)
193    @perm_move_hd
194  | %2{H}
195  | %2{H}
196  | %2 %4{?? H} @perm_move_hd
197  | %2{H}
198  | %2{H}
199  ]
200| #l1' #l2' #l3' #H1 #IH1 #H2 #IH2 #x #l1 #l2 #m1 #m2 #G2 #G1
201  cut (Exists ? (eq ? x) l2')
202  [ @(perm_Exists … H1) >G1 @Exists_mid %] #x_in_l2'
203  elim (Exists_split … x_in_l2') #y * #pre * #post * #EQ #EQ' destruct(EQ')
204  %4{? (IH1 … EQ G1) (IH2 … G2 EQ)}
205]
206qed.
207
208lemma perm_split : ∀A,x.∀pre,post,l : list A.pre@x :: post ≈ l →
209  ∃pre',post'.l = pre' @ x :: post' ∧ pre @ post ≈ pre' @ post'.
210#A #x #pre #post #l #H
211cut (Exists ? (eq ? x) l)
212[ @(perm_Exists … H) /2 by Exists_mid/ ] #G
213elim (Exists_split … G) -G #y * #pre' * #post' * #EQ #EQ' destruct(EQ')
214%{pre'} %{post'} %{EQ}
215>EQ in H; @perm_middle_inv
216qed.
217
218lemma perm_cons_inv : ∀A.∀x.∀l1,l2 : list A.x :: l1 ≈ x :: l2 → l1 ≈ l2.
219#A #x #l1 #l2 change with ([ ] @ ? ≈ [ ] @ ? → ?) #H
220@(perm_middle_inv … H)
221qed.
222
223lemma perm_cons_split : ∀A.∀x.∀l1,l2 : list A.x :: l1 ≈ l2 →
224  ∃pre,post.l2 = pre @ x :: post ∧ l1 ≈ pre @ post.
225#A #x #l1 #l2 change with ([ ] @ ? ≈ ? → ?) @perm_split qed.
226
227lemma map_append_inv : ∀A,B,f,l,m1,m2.map A B f l = m1 @ m2 →
228  ∃l1,l2.map … f l1 = m1 ∧ map … f l2 = m2 ∧ l = l1 @ l2.
229#A #B #f #l elim l
230[ #y #m normalize #H @(nil_append_elim … (sym_eq … H)) %{[]} %{[]} %%%
231| #hd #tl #IH * [ * [2: #hd' #tl' ] | #hd' #tl' #m2] normalize #EQ destruct
232  [ %{[]} % [2: %%% |]
233  | elim (IH … e0) #m1' * #m2' ** #H1 #H2 #H3 destruct
234    change with ((? :: ?) @ ?) in match (? :: ? @ ?);
235    % [2: % [2: %%% ]|]
236  ]
237]
238qed.
239
240lemma injective_map_perm : ∀A,B,f,m,l.injective ?? f → map A B f m ≈ map A B f l → m ≈ l.
241#A #B #f #m elim m
242[ #l #H normalize cases l [//] #hd #tl #G
243  lapply (perm_nil_eq_nil … G) normalize #ABS destruct
244| #hd #tl #IH #l #H normalize #G
245  elim (perm_cons_split ???? G) #pre * #post * #EQ #K
246  elim(map_append_inv … EQ) #pre' ** normalize [2: #hd' #tl']
247  ** #EQ1 #EQ2 #EQ3 destruct
248  lapply (H … e0) #EQ' destruct
249  %4{(perm_move_hd …)} %2 @(IH … H) <map_append @K
250]
251qed.
252   
253lemma perm_append_l_inv : ∀A.∀l,m1,m2 : list A.
254  l @ m1 ≈ l @ m2 → m1 ≈ m2.
255#A #l elim l
256[ //
257| #hd #tl #IH normalize #m1 #m2 #H @IH @(perm_cons_inv … H)
258]
259qed.
260
261lemma perm_append_r_inv : ∀A.∀l1,l2,m : list A.
262  l1 @ m ≈ l2 @ m → l1 ≈ l2.
263#A #l1 #l2 #m #H
264@(perm_append_l_inv ? m)
265%4{(perm_swap_append …)} %4{H} @perm_swap_append
266qed.
267
268lemma perm_cons_append_inv : ∀A,a.∀l,m1,m2 : list A.
269  a :: l ≈ m1 @ a :: m2 → l ≈ m1 @ m2.
270#A #a #l #m1 #m2 change with ([ ] @ ? ≈ ? → ?) @perm_middle_inv
271qed.
272
273lemma perm_singletons : ∀A.∀x,y : A.[x]≈[y] → x = y.
274#A #x #y #H cut (Exists ? (eq ? x) [y])
275[ @(perm_Exists … H) %1 % ] * // *
276qed.
277
278lemma perm_pair_inv : ∀A.∀x,y.∀l : list A.[x;y] ≈ l → l = [x;y] ∨ l = [y;x].
279#A #x #y #l change with ([ ] @ x :: ? ≈ l → ?) #H
280elim (perm_split ????? H) #pre * #post * #EQ #G
281>EQ in H; #H lapply (perm_middle_inv ?????? H) normalize
282<EQ #K
283lapply (perm_singleton_eq ??? K) cases pre in EQ ⊢ %; [2: #hd #tl]
284normalize #EQ1 #EQ2 destruct [2: %1 %]
285@(nil_append_elim … e0) normalize %2 %
286qed.
287
288lemma perm_pairs : ∀A.∀x,y,z,w : A.[x;y]≈[z;w] →
289  (x = z ∧ y = w) ∨ (x = w ∧ y = z).
290#A #x #y #z #w #H elim (perm_pair_inv ???? H) #EQ destruct /3 by or_introl, or_intror, conj/
291qed.
292 
293(* include for AC ops *)
294include "arithmetics/bigops.ma".
295
296lemma fold_permute : ∀A,B.∀nil.∀op : ACop B nil.∀p,f.∀l,m : list A.
297  l ≈ m → \fold[op,nil]_{i ∈ l | p i} (f i) = \fold[op, nil]_{i ∈ m | p i} (f i).
298#A #B #nil #op #p #f #l #m #H elim H -H
299[ //
300| #x #l1 #l2 #H #IH normalize >IH %
301| #x #y #l' normalize cases (p x) cases (p y) normalize [1: |*: // ]
302  >assoc >assoc >comm in ⊢ (??(????%?)?); %
303| //
304]
305qed.
Note: See TracBrowser for help on using the repository browser.