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

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

Got List to compile.

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