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

Last change on this file since 329 was 329, checked in by mulligan, 10 years ago

Commit to restore deleted file.

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