1 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
2 | (* List.ma: Polymorphic lists, and routine operations on them. *) |
---|
3 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
4 | |
---|
5 | include "Util.ma". |
---|
6 | include "Universes.ma". |
---|
7 | include "Bool.ma". |
---|
8 | include "Nat.ma". |
---|
9 | (* include "Maybe.ma". *) |
---|
10 | include "Equality.ma". |
---|
11 | |
---|
12 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
13 | (* The datatype. *) |
---|
14 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
15 | |
---|
16 | ninductive List (A: Type[0]): Type[0] ≝ |
---|
17 | Empty: List A |
---|
18 | | Cons: A → List A → List A. |
---|
19 | |
---|
20 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
21 | (* Syntax. *) |
---|
22 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
23 | |
---|
24 | notation "hvbox(hd break :: tl)" |
---|
25 | right associative with precedence 47 |
---|
26 | for @{ 'Cons $hd $tl }. |
---|
27 | |
---|
28 | interpretation "List empty" 'Empty = (Empty ?). |
---|
29 | interpretation "List cons" 'Cons = (Cons ?). |
---|
30 | |
---|
31 | notation "[ list0 x sep ; ]" |
---|
32 | non associative with precedence 90 |
---|
33 | for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }. |
---|
34 | |
---|
35 | notation "hvbox(l break !! break n)" |
---|
36 | non associative with precedence 90 |
---|
37 | for @{ 'get_index $l $n }. |
---|
38 | |
---|
39 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
40 | (* Lookup. *) |
---|
41 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
42 | |
---|
43 | (* |
---|
44 | nlet rec get_index (A: Type[0]) (l: List A) (n: Nat) on n ≝ |
---|
45 | match n with |
---|
46 | [ Z ⇒ |
---|
47 | match l with |
---|
48 | [ Empty ⇒ Nothing A |
---|
49 | | Cons hd tl ⇒ Just A hd |
---|
50 | ] |
---|
51 | | S o ⇒ |
---|
52 | match l with |
---|
53 | [ Empty ⇒ Nothing A |
---|
54 | | Cons hd tl ⇒ get_index A tl o |
---|
55 | ] |
---|
56 | ]. |
---|
57 | |
---|
58 | interpretation "List get_index" 'get_index l n = (get_index ? l n). |
---|
59 | |
---|
60 | nlet rec set_index (A: Type[0]) (l: List A) (n: Nat) (a: A) on n ≝ |
---|
61 | match n with |
---|
62 | [ Z ⇒ |
---|
63 | match l with |
---|
64 | [ Empty ⇒ Nothing (List A) |
---|
65 | | Cons hd tl ⇒ Just (List A) (Cons A a tl) |
---|
66 | ] |
---|
67 | | S o ⇒ |
---|
68 | match l with |
---|
69 | [ Empty ⇒ Nothing (List A) |
---|
70 | | Cons hd tl ⇒ |
---|
71 | let settail ≝ set_index A tl o a in |
---|
72 | match settail with |
---|
73 | [ Nothing ⇒ Nothing (List A) |
---|
74 | | Just j ⇒ Just (List A) (Cons A hd j) |
---|
75 | ] |
---|
76 | ] |
---|
77 | ]. |
---|
78 | |
---|
79 | nlet rec drop (A: Type[0]) (l: List A) (n: Nat) on n ≝ |
---|
80 | match n with |
---|
81 | [ Z ⇒ Just (List A) l |
---|
82 | | S o ⇒ |
---|
83 | match l with |
---|
84 | [ Empty ⇒ Nothing (List A) |
---|
85 | | Cons hd tl ⇒ drop A tl o |
---|
86 | ] |
---|
87 | ]. |
---|
88 | *) |
---|
89 | |
---|
90 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
91 | (* Building lists from scratch *) |
---|
92 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
93 | |
---|
94 | nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝ |
---|
95 | match n with |
---|
96 | [ Z ⇒ Empty A |
---|
97 | | S o ⇒ a :: replicate A o a |
---|
98 | ]. |
---|
99 | |
---|
100 | nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝ |
---|
101 | match l with |
---|
102 | [ Empty ⇒ m |
---|
103 | | Cons hd tl ⇒ hd :: (append A tl m) |
---|
104 | ]. |
---|
105 | |
---|
106 | notation "hvbox(l break @ r)" |
---|
107 | right associative with precedence 47 |
---|
108 | for @{ 'append $l $r }. |
---|
109 | |
---|
110 | interpretation "List append" 'append = (append ?). |
---|
111 | |
---|
112 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
113 | (* Other manipulations. *) |
---|
114 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
115 | |
---|
116 | nlet rec length (A: Type[0]) (l: List A) on l ≝ |
---|
117 | match l with |
---|
118 | [ Empty ⇒ Z |
---|
119 | | Cons hd tl ⇒ S $ length A tl |
---|
120 | ]. |
---|
121 | |
---|
122 | nlet rec reverse (A: Type[0]) (l: List A) on l ≝ |
---|
123 | match l with |
---|
124 | [ Empty ⇒ Empty A |
---|
125 | | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A) |
---|
126 | ]. |
---|
127 | |
---|
128 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
129 | (* Deletions. *) |
---|
130 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
131 | |
---|
132 | nlet rec remove_first_with_aux (A: Type[0]) (f: A → A → Bool) (a: A) |
---|
133 | (l: List A) (b: List A) on l ≝ |
---|
134 | match l with |
---|
135 | [ Empty ⇒ reverse A b |
---|
136 | | Cons hd tl ⇒ |
---|
137 | match f hd a with |
---|
138 | [ True ⇒ (reverse A b) @ tl |
---|
139 | | False ⇒ remove_first_with_aux A f a tl (hd :: b) |
---|
140 | ] |
---|
141 | ]. |
---|
142 | |
---|
143 | ndefinition remove_first_with ≝ |
---|
144 | λA: Type[0]. |
---|
145 | λf: A → A → Bool. |
---|
146 | λa: A. |
---|
147 | λl: List A. |
---|
148 | remove_first_with_aux A f a l (Empty A). |
---|
149 | |
---|
150 | nlet rec remove_all_with_aux (A: Type[0]) (f: A → A → Bool) (a: A) |
---|
151 | (l: List A) (b: List A) on l ≝ |
---|
152 | match l with |
---|
153 | [ Empty ⇒ reverse A b |
---|
154 | | Cons hd tl ⇒ |
---|
155 | match f hd a with |
---|
156 | [ True ⇒ remove_all_with_aux A f a tl b |
---|
157 | | False ⇒ remove_all_with_aux A f a tl (hd :: b) |
---|
158 | ] |
---|
159 | ]. |
---|
160 | |
---|
161 | ndefinition remove_all_with ≝ |
---|
162 | λA: Type[0]. |
---|
163 | λf: A → A → Bool. |
---|
164 | λa: A. |
---|
165 | λl: List A. |
---|
166 | remove_all_with_aux A f a l (Empty A). |
---|
167 | |
---|
168 | nlet rec drop_while (A: Type[0]) (f: A → Bool) (l: List A) on l ≝ |
---|
169 | match l with |
---|
170 | [ Empty ⇒ Empty A |
---|
171 | | Cons hd tl ⇒ |
---|
172 | match f hd with |
---|
173 | [ True ⇒ drop_while A f tl |
---|
174 | | False ⇒ Cons A hd tl |
---|
175 | ] |
---|
176 | ]. |
---|
177 | |
---|
178 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
179 | (* Folds and builds. *) |
---|
180 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
181 | |
---|
182 | nlet rec fold_right (A: Type[0]) (B: Type[0]) |
---|
183 | (f: A → B → B) (x: B) (l: List A) on l ≝ |
---|
184 | match l with |
---|
185 | [ Empty ⇒ x |
---|
186 | | Cons hd tl ⇒ f hd (fold_right A B f x tl) |
---|
187 | ]. |
---|
188 | |
---|
189 | nlet rec fold_left (A: Type[0]) (B: Type[0]) |
---|
190 | (f: A → B → A) (x: A) (l: List B) on l ≝ |
---|
191 | match l with |
---|
192 | [ Empty ⇒ x |
---|
193 | | Cons hd tl ⇒ f (fold_left A B f x tl) hd |
---|
194 | ]. |
---|
195 | |
---|
196 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
197 | (* Filters and existence tests. *) |
---|
198 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
199 | |
---|
200 | nlet rec filter (A: Type[0]) (f: A → Bool) (l: List A) on l ≝ |
---|
201 | match l with |
---|
202 | [ Empty ⇒ Empty A |
---|
203 | | Cons hd tl ⇒ |
---|
204 | match f hd with |
---|
205 | [ True ⇒ hd :: (filter A f tl) |
---|
206 | | False ⇒ filter A f tl |
---|
207 | ] |
---|
208 | ]. |
---|
209 | |
---|
210 | nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l: Bool ≝ |
---|
211 | match l with |
---|
212 | [ Empty ⇒ cic:/matita/Cerco/Bool/Bool.con(0,2,0) |
---|
213 | | Cons hd tl ⇒ inclusive_disjunction (f hd a) (member_with A a f tl) |
---|
214 | ]. |
---|
215 | |
---|
216 | nlet rec nub_with (A: Type[0]) (f: A → A → Bool) (l: List A) on l ≝ |
---|
217 | match l with |
---|
218 | [ Empty ⇒ Empty A |
---|
219 | | Cons hd tl ⇒ |
---|
220 | match member_with A hd f tl with |
---|
221 | [ True ⇒ nub_with A f tl |
---|
222 | | False ⇒ hd :: (nub_with A f tl) |
---|
223 | ] |
---|
224 | ]. |
---|
225 | |
---|
226 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
227 | (* Maps and zips. *) |
---|
228 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
229 | |
---|
230 | nlet rec map (A: Type[0]) (B: Type[0]) |
---|
231 | (f: A → B) (l: List A) on l ≝ |
---|
232 | match l with |
---|
233 | [ Empty ⇒ Empty B |
---|
234 | | Cons hd tl ⇒ f hd :: map A B f tl |
---|
235 | ]. |
---|
236 | |
---|
237 | nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝ |
---|
238 | match l with |
---|
239 | [ Empty ⇒ Empty A |
---|
240 | | Cons hd tl ⇒ hd @ (flatten A tl) |
---|
241 | ]. |
---|
242 | |
---|
243 | ndefinition map_flatten ≝ |
---|
244 | λA: Type[0]. |
---|
245 | λf: A → List A. |
---|
246 | λl: List A. |
---|
247 | flatten A (map A (List A) f l). |
---|
248 | |
---|
249 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
250 | (* Set-like operations. *) |
---|
251 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
252 | |
---|
253 | nlet rec intersection_with (A: Type[0]) (f: A → A → Bool) |
---|
254 | (l: List A) (m: List A) on l ≝ |
---|
255 | match l with |
---|
256 | [ Empty ⇒ Empty A |
---|
257 | | Cons hd tl ⇒ |
---|
258 | match member_with A hd f m with |
---|
259 | [ True ⇒ hd :: (intersection_with A f tl m) |
---|
260 | | False ⇒ intersection_with A f tl m |
---|
261 | ] |
---|
262 | ]. |
---|
263 | |
---|
264 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
265 | (* Rotates and shifts. *) |
---|
266 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
267 | |
---|
268 | nlet rec rotate_left (A: Type[0]) (l: List A) (m: Nat) on m ≝ |
---|
269 | match m with |
---|
270 | [ Z ⇒ l |
---|
271 | | S n ⇒ |
---|
272 | match l with |
---|
273 | [ Empty ⇒ Empty A |
---|
274 | | Cons hd tl ⇒ hd :: rotate_left A tl n |
---|
275 | ] |
---|
276 | ]. |
---|
277 | |
---|
278 | ndefinition rotate_right ≝ |
---|
279 | λA: Type[0]. |
---|
280 | λl: List A. |
---|
281 | λm: Nat. |
---|
282 | reverse A (rotate_left A (reverse A l) m). |
---|
283 | |
---|
284 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
285 | (* Lemmas. *) |
---|
286 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
287 | |
---|
288 | nlemma append_empty_left_neutral: |
---|
289 | ∀A: Type[0]. |
---|
290 | ∀l: List A. |
---|
291 | l @ (Empty A) = l. |
---|
292 | #A l. |
---|
293 | nelim l. |
---|
294 | nnormalize. |
---|
295 | @. |
---|
296 | #H L H2. |
---|
297 | nnormalize. |
---|
298 | nrewrite > H2. |
---|
299 | @. |
---|
300 | nqed. |
---|
301 | |
---|
302 | nlemma append_associative: |
---|
303 | ∀A: Type[0]. |
---|
304 | ∀l,m,n: List A. |
---|
305 | l @ (m @ n) = (l @ m) @ n. |
---|
306 | #A l m n. |
---|
307 | nelim l. |
---|
308 | nnormalize. |
---|
309 | @. |
---|
310 | #H L H2. |
---|
311 | nnormalize. |
---|
312 | nrewrite > H2. |
---|
313 | @. |
---|
314 | nqed. |
---|
315 | |
---|
316 | nlemma reverse_distributes_append: |
---|
317 | ∀A: Type[0]. |
---|
318 | ∀l, m: List A. |
---|
319 | reverse A (l @ m) = reverse A m @ reverse A l. |
---|
320 | #A l m. |
---|
321 | nelim l. |
---|
322 | nnormalize. |
---|
323 | nrewrite > (append_empty_left_neutral ? ?). |
---|
324 | @. |
---|
325 | #H L A. |
---|
326 | nnormalize. |
---|
327 | nrewrite > A. |
---|
328 | nrewrite > (append_associative ? (reverse ? m) (reverse ? L) (Cons ? H (Empty ?))). |
---|
329 | @. |
---|
330 | nqed. |
---|
331 | |
---|
332 | nlemma length_distributes_append: |
---|
333 | ∀A: Type[0]. |
---|
334 | ∀l, m: List A. |
---|
335 | length A (l @ m) = length A l + length A m. |
---|
336 | #A l m. |
---|
337 | nelim l. |
---|
338 | nnormalize. |
---|
339 | @. |
---|
340 | #H L H2. |
---|
341 | nnormalize. |
---|
342 | nrewrite > H2. |
---|
343 | @. |
---|
344 | nqed. |
---|
345 | |
---|
346 | (* |
---|
347 | nlemma length_reverse: |
---|
348 | ∀A: Type[0]. |
---|
349 | ∀l: List A. |
---|
350 | length A (reverse A l) = length A l. |
---|
351 | #A l. |
---|
352 | nelim l. |
---|
353 | nnormalize. |
---|
354 | @. |
---|
355 | #H L H2. |
---|
356 | nnormalize. |
---|
357 | napply (length_distributes_append A (reverse A l) (Cons A H (Empty A))). |
---|
358 | *) |
---|
359 | |
---|
360 | (* |
---|
361 | nlemma reverse_reverse: |
---|
362 | ∀A: Type[0]. |
---|
363 | ∀l: List A. |
---|
364 | reverse A (reverse A l) = l. |
---|
365 | #A l. |
---|
366 | nelim l. |
---|
367 | nnormalize. |
---|
368 | @. |
---|
369 | #H L H2. |
---|
370 | nnormalize. |
---|
371 | *) |
---|
372 | |
---|
373 | nlemma map_fusion: |
---|
374 | ∀A, B, C: Type[0]. |
---|
375 | ∀l: List A. |
---|
376 | ∀m: List B. |
---|
377 | ∀f: A → B. |
---|
378 | ∀g: B → C. |
---|
379 | map B C g (map A B f l) = map A C (λx. g (f x)) l. |
---|
380 | #A B C l m f g. |
---|
381 | nelim l. |
---|
382 | //. |
---|
383 | #H L H2. |
---|
384 | nnormalize. |
---|
385 | nrewrite > H2. |
---|
386 | @. |
---|
387 | nqed. |
---|
388 | |
---|
389 | nlemma map_preserves_length: |
---|
390 | ∀A, B: Type[0]. |
---|
391 | ∀l: List A. |
---|
392 | ∀f: A → B. |
---|
393 | length B (map A B f l) = length A l. |
---|
394 | #A B l f. |
---|
395 | nelim l. |
---|
396 | //. |
---|
397 | #H L H2. |
---|
398 | nnormalize. |
---|
399 | nrewrite > H2. |
---|
400 | @. |
---|
401 | nqed. |
---|
402 | |
---|
403 | (* |
---|
404 | nlemma empty_get_index_nothing: |
---|
405 | ∀A: Type[0]. |
---|
406 | ∀n: Nat. |
---|
407 | ((Empty A) !! n) = Nothing A. |
---|
408 | #A n. |
---|
409 | nelim n. |
---|
410 | //. |
---|
411 | #N H. |
---|
412 | //. |
---|
413 | nqed. |
---|
414 | *) |
---|
415 | |
---|
416 | nlemma rotate_right_empty: |
---|
417 | ∀A: Type[0]. |
---|
418 | ∀n: Nat. |
---|
419 | rotate_right A (Empty A) n = Empty A. |
---|
420 | #A n. |
---|
421 | nelim n. |
---|
422 | //. |
---|
423 | #N H. |
---|
424 | //. |
---|
425 | nqed. |
---|
426 | |
---|
427 | nlemma rotate_left_empty: |
---|
428 | ∀A: Type[0]. |
---|
429 | ∀n: Nat. |
---|
430 | rotate_left A (Empty A) n = Empty A. |
---|
431 | #A n. |
---|
432 | nelim n. |
---|
433 | //. |
---|
434 | #N H. |
---|
435 | //. |
---|
436 | nqed. |
---|
437 | |
---|
438 | nlemma reverse_singleton: |
---|
439 | ∀A: Type[0]. |
---|
440 | ∀a: A. |
---|
441 | reverse A (Cons A a (Empty A)) = Cons A a (Empty A). |
---|
442 | #A a. |
---|
443 | //. |
---|
444 | nqed. |
---|