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
RevLine 
[233]1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* List.ma: Polymorphic lists, and routine operations on them.                *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
[229]5include "Util.ma".
[228]6
[242]7include "logic/pts.ma".
[241]8
[242]9include "Nat.ma".
[241]10
[242]11include "Maybe.ma".
[241]12
[230]13include "Plogic/equality.ma".
14
[233]15(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
16(* The datatype.                                                              *)
17(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
18
[228]19ninductive List (A: Type[0]): Type[0] ≝
20  Empty: List A
21| Cons: A → List A → List A.
22
[241]23(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
24(* Syntax.                                                                    *)
25(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
26
[228]27notation "hvbox(hd break :: tl)"
28  right associative with precedence 47
29  for @{ 'Cons $hd $tl }.
30
[230]31interpretation "List empty" 'Empty = (Empty ?).
32interpretation "List cons" 'Cons = (Cons ?).
[228]33 
34notation "[ list0 x sep ; ]"
35  non associative with precedence 90
36  for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }.
37 
[241]38notation "hvbox(l break !! break n)"
39  non associative with precedence 90
40  for @{ 'get_index $l $n }.
41 
[233]42(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
43(* Lookup.                                                                    *)
44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[241]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).
[233]61
[241]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 ≝
[228]102  match l with
[241]103    [ Empty ⇒ m
104    | Cons hd tl ⇒ hd :: (append A tl m)
[228]105    ].
106   
[241]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 ≝
[233]145  λA: Type[0].
[241]146  λf: A → A → Bool.
147  λa: A.
[233]148  λl: List A.
[241]149    remove_first_with_aux A f a l (Empty A).
[228]150   
[241]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 ≝
[233]163  λA: Type[0].
[241]164  λf: A → A → Bool.
165  λa: A.
[233]166  λl: List A.
[241]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   
[233]179(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
180(* Folds and builds.                                                          *)
181(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
182
[228]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    ].
[241]196   
197(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
198(* Filters and existence tests.                                               *)
199(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[233]200
[241]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
[233]227(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
228(* Maps and zips.                                                             *)
229(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
230
[228]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   
[241]238nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝
[228]239  match l with
[241]240    [ Empty ⇒ Empty A
241    | Cons hd tl ⇒ hd @ (flatten A tl)
[228]242    ].
243   
[241]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).
[233]249
250(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[241]251(* Set-like operations.                                                       *)
[233]252(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
253
[241]254nlet rec intersection_with (A: Type[0]) (f: A → A → Bool)
255                           (l: List A) (m: List A) on l ≝
[233]256  match l with
[228]257    [ Empty ⇒ Empty A
[241]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    ].
[233]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 ≝
[228]280  λA: Type[0].
281  λl: List A.
[233]282  λm: Nat.
283    reverse A (rotate_left A (reverse A l) m).
284
285(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
286(* Lemmas.                                                                    *)
287(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[228]288   
[233]289nlemma append_empty_left_neutral:
[230]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   
[233]317nlemma reverse_distributes_append:
[230]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.
[233]324  napplyS append_empty_left_neutral.
[230]325  #H L A.
326  nnormalize.
327  nrewrite > A.
328  napplyS append_associative.
329nqed.
330
[233]331nlemma length_distributes_append:
[230]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.
[233]356  napply (length_distributes_append A (reverse A l) (Cons A H (Empty A))).
357*)
358 
359(*   
[230]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.
[233]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  //.
[241]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  //.
[233]439nqed.
Note: See TracBrowser for help on using the repository browser.