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

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

Changes to get directory to compile.

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