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

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