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

Last change on this file since 350 was 350, checked in by mulligan, 9 years ago

less axioms

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