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 | |
---|
79 | let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝ |
---|
80 | match la with |
---|
81 | [ nil ⇒ match lb with [ nil ⇒ True | _ ⇒ False ] |
---|
82 | | cons ha ta ⇒ |
---|
83 | match lb with [ nil ⇒ False | cons hb tb ⇒ P ha hb ∧ All2 A B P ta tb ] |
---|
84 | ]. |
---|
85 | |
---|
86 | lemma All2_length : ∀A,B,P,la,lb. All2 A B P la lb → |la| = |lb|. |
---|
87 | #A #B #P #la elim la |
---|
88 | [ * [ // | #x #y * ] |
---|
89 | | #ha #ta #IH * [ * | #hb #tb * #H1 #H2 whd in ⊢ (??%%); >(IH … H2) @refl |
---|
90 | ] qed. |
---|
91 | |
---|
92 | 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. |
---|
93 | #A #B #P #Q #la elim la |
---|
94 | [ * [ // | #h #t #_ * ] |
---|
95 | | #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ] |
---|
96 | ] qed. |
---|
97 | |
---|
98 | lemma All2_left : ∀A,B,P,la,lb. |
---|
99 | All2 A B P la lb → All A (λa.∃b.P a b) la. |
---|
100 | #A #B #P #la elim la |
---|
101 | [ // |
---|
102 | | #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hdb} // | /2/ ] |
---|
103 | ] qed. |
---|
104 | |
---|
105 | lemma All2_right : ∀A,B,P,la,lb. |
---|
106 | All2 A B P la lb → All B (λb.∃a.P a b) lb. |
---|
107 | #A #B #P #la elim la |
---|
108 | [ * // #h #t * |
---|
109 | | #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hda} // | /2/ ] |
---|
110 | ] qed. |
---|
111 | |
---|
112 | 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 ≝ |
---|
113 | match l return λl. All A P l → ? with |
---|
114 | [ nil ⇒ λ_. nil B |
---|
115 | | cons hd tl ⇒ λH. cons B (f hd (proj1 … H)) (map_All A B P f tl (proj2 … H)) |
---|
116 | ] H. |
---|
117 | |
---|
118 | lemma All_rev : ∀A,P,l.All A P l → All A P (rev ? l). |
---|
119 | #A#P#l elim l // |
---|
120 | #h #t #Hi * #Ph #Pt normalize |
---|
121 | >rev_append_def |
---|
122 | @All_append |
---|
123 | [ @(Hi Pt) |
---|
124 | | %{Ph I} |
---|
125 | ] |
---|
126 | qed. |
---|
127 | |
---|
128 | lemma Exists_rev : ∀A,P,l.Exists A P l → Exists A P (rev ? l). |
---|
129 | #A#P#l elim l // |
---|
130 | #h #t #Hi normalize >rev_append_def |
---|
131 | * [ #Ph @Exists_append_r %{Ph} | #Pt @Exists_append_l @(Hi Pt)] |
---|
132 | qed. |
---|
133 | |
---|
134 | include "utilities/option.ma". |
---|
135 | |
---|
136 | lemma find_All : ∀A,B.∀P : A → Prop.∀Q : B → Prop.∀f.(∀x.P x → opt_All ? Q (f x)) → |
---|
137 | ∀l. All ? P l → opt_All ? Q (find … f l). |
---|
138 | #A#B#P#Q#f#H#l elim l [#_%] |
---|
139 | #x #l' #Hi |
---|
140 | * #Px #AllPl' |
---|
141 | whd in ⊢ (???%); |
---|
142 | lapply (H x Px) |
---|
143 | lapply (refl ? (f x)) |
---|
144 | generalize in ⊢ (???%→?); #o elim o [2: #b] #fx_eq >fx_eq [//] |
---|
145 | #_ whd in ⊢ (???%); @(Hi AllPl') |
---|
146 | qed. |
---|
147 | |
---|
148 | include "utilities/monad.ma". |
---|
149 | |
---|
150 | definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?. |
---|
151 | // qed. |
---|
152 | |
---|
153 | definition List ≝ MakeMonadProps |
---|
154 | list |
---|
155 | (λX,x.[x]) |
---|
156 | (λX,Y,l,f.foldr … (λx.append ? (f x)) [ ] l) |
---|
157 | ????. normalize |
---|
158 | [ / by / |
---|
159 | | #X#m elim m normalize // |
---|
160 | | #X#Y#Z #m #f#g |
---|
161 | elim m normalize [//] |
---|
162 | #x#l' #Hi elim (f x) |
---|
163 | [@Hi] normalize #hd #tl #IH >associative_append >IH % |
---|
164 | |#X#Y#m #f #g #H elim m normalize [//] |
---|
165 | #hd #tl #IH >H >IH % |
---|
166 | ] qed. |
---|
167 | |
---|
168 | alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". |
---|
169 | unification hint 0 ≔ X ; |
---|
170 | N ≟ max_def List |
---|
171 | (*---------------------------*)⊢ |
---|
172 | list X ≡ monad N X. |
---|
173 | |
---|
174 | definition In ≝ λA.λl : list A.λx : A.Exists A (eq ? x) l. |
---|
175 | |
---|
176 | lemma All_In : ∀A,P,l,x. All A P l → In A l x → P x. |
---|
177 | #A#P#l#x #Pl #xl elim (Exists_All … xl Pl) |
---|
178 | #x' * #EQx' >EQx' // |
---|
179 | qed. |
---|
180 | |
---|
181 | lemma In_All : ∀A,P,l.(∀x.In A l x → P x) → All A P l. |
---|
182 | #A#P#l elim l |
---|
183 | [#_ % |
---|
184 | |#x #l' #IH #H % |
---|
185 | [ @H % % |
---|
186 | | @IH #y #G @H %2 @G |
---|
187 | ] |
---|
188 | ] |
---|
189 | qed. |
---|
190 | |
---|
191 | |
---|
192 | lemma nth_opt_append_l : ∀A,l1,l2,n.|l1| > n → nth_opt A n (l1 @ l2) = nth_opt A n l1. |
---|
193 | #A#l1 elim l1 normalize |
---|
194 | [ #l2 #n #ABS elim (absurd ? ABS ?) // |
---|
195 | | #x #l' #IH #l2 #n cases n normalize |
---|
196 | [// |
---|
197 | | #n #H @IH @le_S_S_to_le assumption |
---|
198 | ] |
---|
199 | ] |
---|
200 | qed. |
---|
201 | |
---|
202 | lemma nth_opt_append_r : ∀A,l1,l2,n.|l1| ≤ n → nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2. |
---|
203 | #A#l1 elim l1 |
---|
204 | [#l2 #n #_ <minus_n_O % |
---|
205 | |#x #l' #IH #l2 #n normalize in match (|?|); whd in match (nth_opt ???); |
---|
206 | cases n -n |
---|
207 | [ #ABS elim (absurd ? ABS ?) // |
---|
208 | | #n #H whd in ⊢ (??%?); >minus_S_S @IH @le_S_S_to_le assumption |
---|
209 | ] |
---|
210 | ] |
---|
211 | qed. |
---|
212 | |
---|
213 | lemma nth_opt_append_hit_l : ∀A,l1,l2,n,x. nth_opt A n l1 = Some ? x → |
---|
214 | nth_opt A n (l1 @ l2) = Some ? x. |
---|
215 | #A #l1 elim l1 normalize |
---|
216 | [ #l2 #n #x #ABS destruct |
---|
217 | | #hd #tl #IH #l2 * [2: #n] #x normalize /2 by / |
---|
218 | ] |
---|
219 | qed. |
---|
220 | |
---|
221 | lemma nth_opt_append_miss_l : ∀A,l1,l2,n. nth_opt A n l1 = None ? → |
---|
222 | nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2. |
---|
223 | #A #l1 elim l1 normalize |
---|
224 | [ #l2 #n #_ <minus_n_O % |
---|
225 | | #hd #tl #IH #l2 * [2: #n] normalize |
---|
226 | [ @IH |
---|
227 | | #ABS destruct(ABS) |
---|
228 | ] |
---|
229 | ] |
---|
230 | qed. |
---|
231 | |
---|
232 | |
---|
233 | (* count occurrences satisfying a test *) |
---|
234 | let rec count A (f : A → bool) (l : list A) on l : ℕ ≝ |
---|
235 | match l with |
---|
236 | [ nil ⇒ 0 |
---|
237 | | cons x l' ⇒ (if f x then 1 else 0) + count A f l' |
---|
238 | ]. |
---|
239 | |
---|
240 | theorem count_append : ∀A,f,l1,l2.count A f (l1@l2) = count A f l1 + count A f l2. |
---|
241 | #A #f #l1 elim l1 |
---|
242 | [ #l2 % |
---|
243 | | #hd #tl #IH #l2 normalize elim (f hd) normalize >IH % |
---|
244 | ] |
---|
245 | qed. |
---|
246 | |
---|
247 | |
---|
248 | include "utilities/option.ma". |
---|
249 | |
---|
250 | lemma position_of_from_aux : ∀A,test,l,n. |
---|
251 | position_of_aux A test l n = !n' ← position_of A test l; return n + n'. |
---|
252 | #A #test #l elim l |
---|
253 | [ normalize #_ % |
---|
254 | | #hd #tl #IH #n |
---|
255 | normalize in ⊢ (??%?); >IH |
---|
256 | normalize elim (test hd) normalize |
---|
257 | [ <plus_n_O % |
---|
258 | | >(IH 1) whd in match (position_of ???); |
---|
259 | elim (position_of_aux ??? 0) normalize |
---|
260 | [ % | #x <plus_n_Sm % ] |
---|
261 | ] |
---|
262 | ] |
---|
263 | qed. |
---|
264 | |
---|
265 | definition position_of_safe ≝ λA,test,l.λprf : count A test l ≥ 1. |
---|
266 | opt_safe ? (position_of A test l) ?. |
---|
267 | lapply prf -prf elim l normalize |
---|
268 | [ #ABS elim (absurd ? ABS (not_le_Sn_O 0)) |
---|
269 | |#hd #tl #IH elim (test hd) normalize |
---|
270 | [2: >position_of_from_aux #H |
---|
271 | change with (position_of_aux ????) in match (position_of ???); |
---|
272 | >(opt_to_opt_safe … (IH H)) @opt_safe_elim normalize #x] |
---|
273 | #_ % #ABS destruct(ABS) |
---|
274 | qed. |
---|
275 | |
---|
276 | definition index_of ≝ |
---|
277 | λA,test,l.λprf : eqb (count A test l) 1.position_of_safe A test l ?. |
---|
278 | lapply prf -prf @eqb_elim #EQ * >EQ % |
---|
279 | qed. |
---|
280 | |
---|
281 | lemma position_of_append_hit : ∀A,test,l1,l2,x. |
---|
282 | position_of A test (l1@l2) = Some ? x → |
---|
283 | position_of A test l1 = Some ? x ∨ |
---|
284 | (position_of A test l1 = None ? ∧ |
---|
285 | ! p ← position_of A test l2 ; return (|l1| + p) = Some ? x). |
---|
286 | #A#test#l1 elim l1 |
---|
287 | [ #l2 #x change with l2 in match (? @ l2); #EQ >EQ %2 |
---|
288 | % % |
---|
289 | | #hd #tl #IH #l2 #x |
---|
290 | normalize elim (test hd) normalize |
---|
291 | [#H %{H} |
---|
292 | | >position_of_from_aux |
---|
293 | lapply (refl … (position_of A test (tl@l2))) |
---|
294 | generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq |
---|
295 | normalize #EQ destruct(EQ) |
---|
296 | elim (IH … Heq) -IH |
---|
297 | [ #G % |
---|
298 | | * #G #H |
---|
299 | lapply (refl … (position_of A test l2)) |
---|
300 | generalize in ⊢ (???%→?); * [2: #x'] #H' >H' in H; normalize |
---|
301 | #EQ destruct (EQ) %2 %] |
---|
302 | >position_of_from_aux |
---|
303 | [1,2: >G % | >H' %] |
---|
304 | ] |
---|
305 | ] |
---|
306 | qed. |
---|
307 | |
---|
308 | lemma position_of_hit : ∀A,test,l,x.position_of A test l = Some ? x → |
---|
309 | count A test l ≥ 1. |
---|
310 | #A#test#l elim l normalize |
---|
311 | [#x #ABS destruct(ABS) |
---|
312 | |#hd #tl #IH #x elim (test hd) normalize [#EQ destruct(EQ) //] |
---|
313 | >position_of_from_aux |
---|
314 | lapply (refl … (position_of ? test tl)) |
---|
315 | generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize |
---|
316 | #EQ destruct(EQ) @(IH … Heq) |
---|
317 | ] |
---|
318 | qed. |
---|
319 | |
---|
320 | lemma position_of_miss : ∀A,test,l.position_of A test l = None ? → |
---|
321 | count A test l = 0. |
---|
322 | #A#test#l elim l normalize |
---|
323 | [ #_ % |
---|
324 | |#hd #tl #IH elim (test hd) normalize [#EQ destruct(EQ)] |
---|
325 | >position_of_from_aux |
---|
326 | lapply (refl … (position_of ? test tl)) |
---|
327 | generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize |
---|
328 | #EQ destruct(EQ) @(IH … Heq) |
---|
329 | ] |
---|
330 | qed. |
---|
331 | |
---|
332 | |
---|
333 | lemma position_of_append_miss : ∀A,test,l1,l2. |
---|
334 | position_of A test (l1@l2) = None ? → |
---|
335 | position_of A test l1 = None ? ∧ position_of A test l2 = None ?. |
---|
336 | #A#test#l1 elim l1 |
---|
337 | [ #l2 change with l2 in match (? @ l2); #EQ >EQ % % |
---|
338 | | #hd #tl #IH #l2 |
---|
339 | normalize elim (test hd) normalize |
---|
340 | [#H destruct(H) |
---|
341 | | >position_of_from_aux |
---|
342 | lapply (refl … (position_of A test (tl@l2))) |
---|
343 | generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq |
---|
344 | normalize #EQ destruct(EQ) |
---|
345 | elim (IH … Heq) #H1 #H2 |
---|
346 | >position_of_from_aux |
---|
347 | >position_of_from_aux |
---|
348 | >H1 >H2 normalize % % |
---|
349 | ] |
---|
350 | ] |
---|
351 | qed. |
---|
352 | |
---|
353 | |
---|
354 | (* Not terribly efficient sort for testing purposes *) |
---|
355 | |
---|
356 | let rec ordered_insert (A:Type[0]) (lt:A → A → bool) (a:A) (l:list A) on l : list A ≝ |
---|
357 | match l with |
---|
358 | [ nil ⇒ [a] |
---|
359 | | cons h t ⇒ if lt a h then a::h::t else h::(ordered_insert A lt a t) |
---|
360 | ]. |
---|
361 | |
---|
362 | let rec insert_sort (A:Type[0]) (lt:A → A → bool) (l:list A) on l : list A ≝ |
---|
363 | match l with |
---|
364 | [ nil ⇒ [ ] |
---|
365 | | cons h t ⇒ ordered_insert A lt h (insert_sort A lt t) |
---|
366 | ]. |
---|
367 | |
---|
368 | (* range from 0 to n excluded with proof of minoration *) |
---|
369 | |
---|
370 | let rec range_strong_internal (index, how_many, end : ℕ) on how_many : |
---|
371 | index + how_many = end → |
---|
372 | list (Σn.n<end) ≝ |
---|
373 | match how_many return λhow_many.index + how_many = end → ? with |
---|
374 | [ O ⇒ λ_.[ ] |
---|
375 | | S k ⇒ λprf.«index, ?» :: range_strong_internal (S index) k end ? |
---|
376 | ]. |
---|
377 | <prf |
---|
378 | [ >(plus_n_O index) in ⊢ (?%?); @monotonic_lt_plus_r @le_S_S @le_O_n |
---|
379 | | @plus_n_Sm |
---|
380 | ] |
---|
381 | qed. |
---|
382 | |
---|
383 | definition range_strong : ∀end.list (Σn.n < end) ≝ |
---|
384 | λend.range_strong_internal 0 ? end (refl …). |
---|