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

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

Added fold_right_i (with dependent type) to List file.

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