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

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

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