1 | include "basics/lists/list.ma". |
---|
2 | include "ASM/Util.ma". (* coercion from bool to Prop *) |
---|
3 | |
---|
4 | lemma All_map : ∀A,B,P,Q,f,l. |
---|
5 | All A P l → |
---|
6 | (∀a.P a → Q (f a)) → |
---|
7 | All B Q (map A B f l). |
---|
8 | #A #B #P #Q #f #l elim l // |
---|
9 | #h #t #IH * #Ph #Pt #F % [@(F ? Ph) | @(IH Pt F)] qed. |
---|
10 | |
---|
11 | lemma Exists_map : ∀A,B,P,Q,f,l. |
---|
12 | Exists A P l → |
---|
13 | (∀a.P a → Q (f a)) → |
---|
14 | Exists B Q (map A B f l). |
---|
15 | #A #B #P #Q #f #l elim l // |
---|
16 | #h #t #IH * #H #F |
---|
17 | [ %1 @(F ? H) | %2 @(IH H F) ] |
---|
18 | qed. |
---|
19 | |
---|
20 | lemma All_append : ∀A,P,l,r. All A P l → All A P r → All A P (l@r). |
---|
21 | #A #P #l elim l |
---|
22 | [ // |
---|
23 | | #hd #tl #IH #r * #H1 #H2 #H3 % // @IH // |
---|
24 | ] qed. |
---|
25 | |
---|
26 | lemma All_append_l : ∀A,P,l,r. All A P (l@r) → All A P l. |
---|
27 | #A #P #l elim l |
---|
28 | [ // |
---|
29 | | #hd #tl #IH #r * #H1 #H2 % /2/ |
---|
30 | ] qed. |
---|
31 | |
---|
32 | lemma All_append_r : ∀A,P,l,r. All A P (l@r) → All A P r. |
---|
33 | #A #P #l elim l |
---|
34 | [ // |
---|
35 | | #h #t #IH #r * /2/ |
---|
36 | ] qed. |
---|
37 | |
---|
38 | (* An alternative form of All that can be easier to use sometimes. *) |
---|
39 | lemma All_alt : ∀A,P,l. |
---|
40 | (∀a,pre,post. l = pre@a::post → P a) → |
---|
41 | All A P l. |
---|
42 | #A #P #l #H lapply (refl ? l) change with ([ ] @ l) in ⊢ (???% → ?); |
---|
43 | generalize in ⊢ (???(??%?) → ?); elim l in ⊢ (? → ???(???%) → %); |
---|
44 | [ #pre #E % |
---|
45 | | #a #tl #IH #pre #E % |
---|
46 | [ @(H a pre tl E) |
---|
47 | | @(IH (pre@[a])) >associative_append @E |
---|
48 | ] |
---|
49 | ] qed. |
---|
50 | |
---|
51 | lemma All_split : ∀A,P,l. All A P l → ∀pre,x,post.l = pre @ x :: post → P x. |
---|
52 | #A #P #l elim l |
---|
53 | [ * * normalize [2: #y #pre'] #x #post #ABS destruct(ABS) |
---|
54 | | #hd #tl #IH * #Phd #Ptl * normalize [2: #y #pre'] #x #post #EQ destruct(EQ) |
---|
55 | [ @(IH Ptl … (refl …)) |
---|
56 | | @Phd |
---|
57 | ] |
---|
58 | ] |
---|
59 | qed. |
---|
60 | |
---|
61 | (* Boolean predicate version of All *) |
---|
62 | |
---|
63 | let rec all (A:Type[0]) (P:A → bool) (l:list A) on l : bool ≝ |
---|
64 | match l with |
---|
65 | [ nil ⇒ true |
---|
66 | | cons h t ⇒ P h ∧ all A P t |
---|
67 | ]. |
---|
68 | |
---|
69 | lemma all_All : ∀A,P,l. bool_to_Prop (all A P l) ↔ All A (λa.bool_to_Prop (P a)) l. |
---|
70 | #A #P #l elim l |
---|
71 | [ % // |
---|
72 | | #h #t * #IH #IH' % |
---|
73 | [ whd in ⊢ (?% → %); cases (P h) [ #p % /2/ | * ] |
---|
74 | | * #p #H whd in ⊢ (?%); >p /2/ |
---|
75 | ] |
---|
76 | ] qed. |
---|
77 | |
---|
78 | lemma all_append : ∀A,p,l1,l2. |
---|
79 | all A p (l1@l2) → |
---|
80 | all A p l1 ∧ all A p l2. |
---|
81 | #A #p #l1 elim l1 |
---|
82 | [ // |
---|
83 | | #h #t #IH #l2 |
---|
84 | whd in ⊢ (?% → ?(?%?)); |
---|
85 | cases (p h) // |
---|
86 | @IH |
---|
87 | ] qed. |
---|
88 | |
---|
89 | |
---|
90 | let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝ |
---|
91 | match la with |
---|
92 | [ nil ⇒ match lb with [ nil ⇒ True | _ ⇒ False ] |
---|
93 | | cons ha ta ⇒ |
---|
94 | match lb with [ nil ⇒ False | cons hb tb ⇒ P ha hb ∧ All2 A B P ta tb ] |
---|
95 | ]. |
---|
96 | |
---|
97 | lemma All2_length : ∀A,B,P,la,lb. All2 A B P la lb → |la| = |lb|. |
---|
98 | #A #B #P #la elim la |
---|
99 | [ * [ // | #x #y * ] |
---|
100 | | #ha #ta #IH * [ * | #hb #tb * #H1 #H2 whd in ⊢ (??%%); >(IH … H2) @refl |
---|
101 | ] qed. |
---|
102 | |
---|
103 | lemma All2_mp : ∀A,B,P,Q,la,lb. (∀a,b. P a b → Q a b) → All2 A B P la lb → All2 A B Q la lb. |
---|
104 | #A #B #P #Q #la elim la |
---|
105 | [ * [ // | #h #t #_ * ] |
---|
106 | | #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ] |
---|
107 | ] qed. |
---|
108 | |
---|
109 | lemma All2_left : ∀A,B,P,la,lb. |
---|
110 | All2 A B P la lb → All A (λa.∃b.P a b) la. |
---|
111 | #A #B #P #la elim la |
---|
112 | [ // |
---|
113 | | #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hdb} // | /2/ ] |
---|
114 | ] qed. |
---|
115 | |
---|
116 | lemma All2_right : ∀A,B,P,la,lb. |
---|
117 | All2 A B P la lb → All B (λb.∃a.P a b) lb. |
---|
118 | #A #B #P #la elim la |
---|
119 | [ * // #h #t * |
---|
120 | | #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hda} // | /2/ ] |
---|
121 | ] qed. |
---|
122 | |
---|
123 | lemma All2_tail : ∀A,B,P,a,b. |
---|
124 | All2 A B P a b → |
---|
125 | All2 A B P (tail A a) (tail B b). |
---|
126 | #A #B #P * [2: #ah #at] * [2,4: #bh #bt] |
---|
127 | * // |
---|
128 | qed. |
---|
129 | |
---|
130 | let rec map_All (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → B) (l:list A) (H:All A P l) on l : list B ≝ |
---|
131 | match l return λl. All A P l → ? with |
---|
132 | [ nil ⇒ λ_. nil B |
---|
133 | | cons hd tl ⇒ λH. cons B (f hd (proj1 … H)) (map_All A B P f tl (proj2 … H)) |
---|
134 | ] H. |
---|
135 | |
---|
136 | lemma All_rev : ∀A,P,l.All A P l → All A P (rev ? l). |
---|
137 | #A#P#l elim l // |
---|
138 | #h #t #Hi * #Ph #Pt normalize |
---|
139 | >rev_append_def |
---|
140 | @All_append |
---|
141 | [ @(Hi Pt) |
---|
142 | | %{Ph I} |
---|
143 | ] |
---|
144 | qed. |
---|
145 | |
---|
146 | lemma Exists_rev : ∀A,P,l.Exists A P l → Exists A P (rev ? l). |
---|
147 | #A#P#l elim l // |
---|
148 | #h #t #Hi normalize >rev_append_def |
---|
149 | * [ #Ph @Exists_append_r %{Ph} | #Pt @Exists_append_l @(Hi Pt)] |
---|
150 | qed. |
---|
151 | |
---|
152 | include "utilities/option.ma". |
---|
153 | |
---|
154 | lemma find_All : ∀A,B.∀P : A → Prop.∀Q : B → Prop.∀f.(∀x.P x → opt_All ? Q (f x)) → |
---|
155 | ∀l. All ? P l → opt_All ? Q (find … f l). |
---|
156 | #A#B#P#Q#f#H#l elim l [#_%] |
---|
157 | #x #l' #Hi |
---|
158 | * #Px #AllPl' |
---|
159 | whd in ⊢ (???%); |
---|
160 | lapply (H x Px) |
---|
161 | lapply (refl ? (f x)) |
---|
162 | generalize in ⊢ (???%→?); #o elim o [2: #b] #fx_eq >fx_eq [//] |
---|
163 | #_ whd in ⊢ (???%); @(Hi AllPl') |
---|
164 | qed. |
---|
165 | |
---|
166 | include "utilities/monad.ma". |
---|
167 | |
---|
168 | definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?. |
---|
169 | // qed. |
---|
170 | |
---|
171 | definition List ≝ MakeMonadProps |
---|
172 | list |
---|
173 | (λX,x.[x]) |
---|
174 | (λX,Y,l,f.foldr … (λx.append ? (f x)) [ ] l) |
---|
175 | ????. normalize |
---|
176 | [ / by / |
---|
177 | | #X#m elim m normalize // |
---|
178 | | #X#Y#Z #m #f#g |
---|
179 | elim m normalize [//] |
---|
180 | #x#l' #Hi elim (f x) |
---|
181 | [@Hi] normalize #hd #tl #IH >associative_append >IH % |
---|
182 | |#X#Y#m #f #g #H elim m normalize [//] |
---|
183 | #hd #tl #IH >H >IH % |
---|
184 | ] qed. |
---|
185 | |
---|
186 | alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". |
---|
187 | unification hint 0 ≔ X ; |
---|
188 | N ≟ max_def List |
---|
189 | (*---------------------------*)⊢ |
---|
190 | list X ≡ monad N X. |
---|
191 | |
---|
192 | definition In ≝ λA.λl : list A.λx : A.Exists A (eq ? x) l. |
---|
193 | |
---|
194 | lemma All_In : ∀A,P,l,x. All A P l → In A l x → P x. |
---|
195 | #A#P#l#x #Pl #xl elim (Exists_All … xl Pl) |
---|
196 | #x' * #EQx' >EQx' // |
---|
197 | qed. |
---|
198 | |
---|
199 | lemma In_All : ∀A,P,l.(∀x.In A l x → P x) → All A P l. |
---|
200 | #A#P#l elim l |
---|
201 | [#_ % |
---|
202 | |#x #l' #IH #H % |
---|
203 | [ @H % % |
---|
204 | | @IH #y #G @H %2 @G |
---|
205 | ] |
---|
206 | ] |
---|
207 | qed. |
---|
208 | |
---|
209 | |
---|
210 | lemma nth_opt_append_l : ∀A,l1,l2,n.|l1| > n → nth_opt A n (l1 @ l2) = nth_opt A n l1. |
---|
211 | #A#l1 elim l1 normalize |
---|
212 | [ #l2 #n #ABS elim (absurd ? ABS ?) // |
---|
213 | | #x #l' #IH #l2 #n cases n normalize |
---|
214 | [// |
---|
215 | | #n #H @IH @le_S_S_to_le assumption |
---|
216 | ] |
---|
217 | ] |
---|
218 | qed. |
---|
219 | |
---|
220 | lemma nth_opt_append_r : ∀A,l1,l2,n.|l1| ≤ n → nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2. |
---|
221 | #A#l1 elim l1 |
---|
222 | [#l2 #n #_ <minus_n_O % |
---|
223 | |#x #l' #IH #l2 #n normalize in match (|?|); whd in match (nth_opt ???); |
---|
224 | cases n -n |
---|
225 | [ #ABS elim (absurd ? ABS ?) // |
---|
226 | | #n #H whd in ⊢ (??%?); >minus_S_S @IH @le_S_S_to_le assumption |
---|
227 | ] |
---|
228 | ] |
---|
229 | qed. |
---|
230 | |
---|
231 | lemma nth_opt_append_hit_l : ∀A,l1,l2,n,x. nth_opt A n l1 = Some ? x → |
---|
232 | nth_opt A n (l1 @ l2) = Some ? x. |
---|
233 | #A #l1 elim l1 normalize |
---|
234 | [ #l2 #n #x #ABS destruct |
---|
235 | | #hd #tl #IH #l2 * [2: #n] #x normalize /2 by / |
---|
236 | ] |
---|
237 | qed. |
---|
238 | |
---|
239 | lemma nth_opt_append_miss_l : ∀A,l1,l2,n. nth_opt A n l1 = None ? → |
---|
240 | nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2. |
---|
241 | #A #l1 elim l1 normalize |
---|
242 | [ #l2 #n #_ <minus_n_O % |
---|
243 | | #hd #tl #IH #l2 * [2: #n] normalize |
---|
244 | [ @IH |
---|
245 | | #ABS destruct(ABS) |
---|
246 | ] |
---|
247 | ] |
---|
248 | qed. |
---|
249 | |
---|
250 | |
---|
251 | (* count occurrences satisfying a test *) |
---|
252 | let rec count A (f : A → bool) (l : list A) on l : ℕ ≝ |
---|
253 | match l with |
---|
254 | [ nil ⇒ 0 |
---|
255 | | cons x l' ⇒ (if f x then 1 else 0) + count A f l' |
---|
256 | ]. |
---|
257 | |
---|
258 | theorem count_append : ∀A,f,l1,l2.count A f (l1@l2) = count A f l1 + count A f l2. |
---|
259 | #A #f #l1 elim l1 |
---|
260 | [ #l2 % |
---|
261 | | #hd #tl #IH #l2 normalize elim (f hd) normalize >IH % |
---|
262 | ] |
---|
263 | qed. |
---|
264 | |
---|
265 | |
---|
266 | |
---|
267 | lemma flatten_append : ∀A,l1,l2. |
---|
268 | flatten A (l1@l2) = (flatten A l1)@(flatten A l2). |
---|
269 | #A #l1 #l2 |
---|
270 | elim l1 |
---|
271 | [ % |
---|
272 | | #h #t #IH whd in ⊢ (??%(??%?)); |
---|
273 | change with (flatten ??) in match (foldr ?????); >IH |
---|
274 | change with (flatten ??) in match (foldr ?????); |
---|
275 | >associative_append % |
---|
276 | ] qed. |
---|
277 | |
---|
278 | |
---|
279 | include "utilities/option.ma". |
---|
280 | |
---|
281 | lemma position_of_from_aux : ∀A,test,l,n. |
---|
282 | position_of_aux A test l n = !n' ← position_of A test l; return n + n'. |
---|
283 | #A #test #l elim l |
---|
284 | [ normalize #_ % |
---|
285 | | #hd #tl #IH #n |
---|
286 | normalize in ⊢ (??%?); >IH |
---|
287 | normalize elim (test hd) normalize |
---|
288 | [ <plus_n_O % |
---|
289 | | >(IH 1) whd in match (position_of ???); |
---|
290 | elim (position_of_aux ??? 0) normalize |
---|
291 | [ % | #x <plus_n_Sm % ] |
---|
292 | ] |
---|
293 | ] |
---|
294 | qed. |
---|
295 | |
---|
296 | definition position_of_safe ≝ λA,test,l.λprf : count A test l ≥ 1. |
---|
297 | opt_safe ? (position_of A test l) ?. |
---|
298 | lapply prf -prf elim l normalize |
---|
299 | [ #ABS elim (absurd ? ABS (not_le_Sn_O 0)) |
---|
300 | |#hd #tl #IH elim (test hd) normalize |
---|
301 | [2: >position_of_from_aux #H |
---|
302 | change with (position_of_aux ????) in match (position_of ???); |
---|
303 | >(opt_to_opt_safe … (IH H)) @opt_safe_elim normalize #x] |
---|
304 | #_ % #ABS destruct(ABS) |
---|
305 | qed. |
---|
306 | |
---|
307 | definition index_of ≝ |
---|
308 | λA,test,l.λprf : eqb (count A test l) 1.position_of_safe A test l ?. |
---|
309 | lapply prf -prf @eqb_elim #EQ * >EQ % |
---|
310 | qed. |
---|
311 | |
---|
312 | lemma position_of_append_hit : ∀A,test,l1,l2,x. |
---|
313 | position_of A test (l1@l2) = Some ? x → |
---|
314 | position_of A test l1 = Some ? x ∨ |
---|
315 | (position_of A test l1 = None ? ∧ |
---|
316 | ! p ← position_of A test l2 ; return (|l1| + p) = Some ? x). |
---|
317 | #A#test#l1 elim l1 |
---|
318 | [ #l2 #x change with l2 in match (? @ l2); #EQ >EQ %2 |
---|
319 | % % |
---|
320 | | #hd #tl #IH #l2 #x |
---|
321 | normalize elim (test hd) normalize |
---|
322 | [#H %{H} |
---|
323 | | >position_of_from_aux |
---|
324 | lapply (refl … (position_of A test (tl@l2))) |
---|
325 | generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq |
---|
326 | normalize #EQ destruct(EQ) |
---|
327 | elim (IH … Heq) -IH |
---|
328 | [ #G % |
---|
329 | | * #G #H |
---|
330 | lapply (refl … (position_of A test l2)) |
---|
331 | generalize in ⊢ (???%→?); * [2: #x'] #H' >H' in H; normalize |
---|
332 | #EQ destruct (EQ) %2 %] |
---|
333 | >position_of_from_aux |
---|
334 | [1,2: >G % | >H' %] |
---|
335 | ] |
---|
336 | ] |
---|
337 | qed. |
---|
338 | |
---|
339 | lemma position_of_hit : ∀A,test,l,x.position_of A test l = Some ? x → |
---|
340 | count A test l ≥ 1. |
---|
341 | #A#test#l elim l normalize |
---|
342 | [#x #ABS destruct(ABS) |
---|
343 | |#hd #tl #IH #x elim (test hd) normalize [#EQ destruct(EQ) //] |
---|
344 | >position_of_from_aux |
---|
345 | lapply (refl … (position_of ? test tl)) |
---|
346 | generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize |
---|
347 | #EQ destruct(EQ) @(IH … Heq) |
---|
348 | ] |
---|
349 | qed. |
---|
350 | |
---|
351 | lemma position_of_miss : ∀A,test,l.position_of A test l = None ? → |
---|
352 | count A test l = 0. |
---|
353 | #A#test#l elim l normalize |
---|
354 | [ #_ % |
---|
355 | |#hd #tl #IH elim (test hd) normalize [#EQ destruct(EQ)] |
---|
356 | >position_of_from_aux |
---|
357 | lapply (refl … (position_of ? test tl)) |
---|
358 | generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize |
---|
359 | #EQ destruct(EQ) @(IH … Heq) |
---|
360 | ] |
---|
361 | qed. |
---|
362 | |
---|
363 | |
---|
364 | lemma position_of_append_miss : ∀A,test,l1,l2. |
---|
365 | position_of A test (l1@l2) = None ? → |
---|
366 | position_of A test l1 = None ? ∧ position_of A test l2 = None ?. |
---|
367 | #A#test#l1 elim l1 |
---|
368 | [ #l2 change with l2 in match (? @ l2); #EQ >EQ % % |
---|
369 | | #hd #tl #IH #l2 |
---|
370 | normalize elim (test hd) normalize |
---|
371 | [#H destruct(H) |
---|
372 | | >position_of_from_aux |
---|
373 | lapply (refl … (position_of A test (tl@l2))) |
---|
374 | generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq |
---|
375 | normalize #EQ destruct(EQ) |
---|
376 | elim (IH … Heq) #H1 #H2 |
---|
377 | >position_of_from_aux |
---|
378 | >position_of_from_aux |
---|
379 | >H1 >H2 normalize % % |
---|
380 | ] |
---|
381 | ] |
---|
382 | qed. |
---|
383 | |
---|
384 | |
---|
385 | (* A not terribly efficient sort for testing purposes *) |
---|
386 | |
---|
387 | let rec ordered_insert (A:Type[0]) (lt:A → A → bool) (a:A) (l:list A) on l : list A ≝ |
---|
388 | match l with |
---|
389 | [ nil ⇒ [a] |
---|
390 | | cons h t ⇒ if lt a h then a::h::t else h::(ordered_insert A lt a t) |
---|
391 | ]. |
---|
392 | |
---|
393 | let rec insert_sort (A:Type[0]) (lt:A → A → bool) (l:list A) on l : list A ≝ |
---|
394 | match l with |
---|
395 | [ nil ⇒ [ ] |
---|
396 | | cons h t ⇒ ordered_insert A lt h (insert_sort A lt t) |
---|
397 | ]. |
---|
398 | |
---|
399 | (* range from 0 to n excluded with proof of minoration *) |
---|
400 | |
---|
401 | let rec range_strong_internal (index, how_many, end : ℕ) on how_many : |
---|
402 | index + how_many = end → |
---|
403 | list (Σn.n<end) ≝ |
---|
404 | match how_many return λhow_many.index + how_many = end → ? with |
---|
405 | [ O ⇒ λ_.[ ] |
---|
406 | | S k ⇒ λprf.«index, ?» :: range_strong_internal (S index) k end ? |
---|
407 | ]. |
---|
408 | <prf |
---|
409 | [ >(plus_n_O index) in ⊢ (?%?); @monotonic_lt_plus_r @le_S_S @le_O_n |
---|
410 | | @plus_n_Sm |
---|
411 | ] |
---|
412 | qed. |
---|
413 | |
---|
414 | definition range_strong : ∀end.list (Σn.n < end) ≝ |
---|
415 | λend.range_strong_internal 0 ? end (refl …). |
---|