source: Deliverables/D4.1/Matita/List.ma @ 241

Last change on this file since 241 was 241, checked in by mulligan, 9 years ago

Also needed an updated List.ma.

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