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

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

More changes to get everything to typecheck.

File size: 12.1 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_left (A: Type[0]) (B: Type[0])
219                   (f: A → B → A) (x: A) (l: List B) on l ≝
220  match l with
221    [ Empty ⇒ x
222    | Cons hd tl ⇒ f (fold_left A B f x tl) hd
223    ].
224   
225(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
226(* Filters and existence tests.                                               *)
227(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
228
229nlet rec filter (A: Type[0]) (f: A → Bool) (l: List A) on l ≝
230  match l with
231    [ Empty ⇒ Empty A
232    | Cons hd tl ⇒
233      match f hd with
234        [ true ⇒ hd :: (filter A f tl)
235        | false ⇒ filter A f tl
236        ]
237    ].
238   
239nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l: Bool ≝
240  match l with
241    [ Empty ⇒ false
242    | Cons hd tl ⇒ inclusive_disjunction (f hd a) (member_with A a f tl)
243    ].
244   
245nlet rec nub_with (A: Type[0]) (f: A → A → Bool) (l: List A) on l ≝
246  match l with
247    [ Empty ⇒ Empty A
248    | Cons hd tl ⇒
249      match member_with A hd f tl with
250        [ true ⇒ nub_with A f tl
251        | false ⇒ hd :: (nub_with A f tl)
252        ]
253    ].
254
255(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
256(* Maps and zips.                                                             *)
257(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
258
259nlet rec map (A: Type[0]) (B: Type[0])
260             (f: A → B) (l: List A) on l ≝
261  match l with
262    [ Empty ⇒ Empty B
263    | Cons hd tl ⇒ f hd :: map A B f tl
264    ].
265   
266nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝
267  match l with
268    [ Empty ⇒ Empty A
269    | Cons hd tl ⇒ hd @ (flatten A tl)
270    ].
271   
272ndefinition map_flatten ≝
273  λA: Type[0].
274  λf: A → List A.
275  λl: List A.
276    flatten A (map A (List A) f l).
277
278(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
279(* Set-like operations.                                                       *)
280(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
281
282nlet rec intersection_with (A: Type[0]) (f: A → A → Bool)
283                           (l: List A) (m: List A) on l ≝
284  match l with
285    [ Empty ⇒ Empty A
286    | Cons hd tl ⇒
287      match member_with A hd f m with
288        [ true ⇒ hd :: (intersection_with A f tl m)
289        | false ⇒ intersection_with A f tl m
290        ]
291    ].
292
293(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
294(* Rotates and shifts.                                                        *)
295(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
296
297nlet rec rotate_left (A: Type[0]) (l: List A) (m: Nat) on m ≝
298  match m with
299    [ Z ⇒ l
300    | S n ⇒
301      match l with
302        [ Empty ⇒ Empty A
303        | Cons hd tl ⇒ hd :: rotate_left A tl n
304        ]
305    ].
306
307ndefinition rotate_right ≝
308  λA: Type[0].
309  λl: List A.
310  λm: Nat.
311    reverse A (rotate_left A (reverse A l) m).
312
313(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
314(* Lemmas.                                                                    *)
315(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
316   
317nlemma append_empty_left_neutral:
318  ∀A: Type[0].
319  ∀l: List A.
320    l @ (Empty A) = l.
321  #A l.
322  nelim l.
323  nnormalize.
324  @.
325  #H L H2.
326  nnormalize.
327  nrewrite > H2.
328  @.
329nqed.
330
331nlemma append_associative:
332  ∀A: Type[0].
333  ∀l,m,n: List A.
334    l @ (m @ n) = (l @ m) @ n.
335  #A l m n.
336  nelim l.
337  nnormalize.
338  @.
339  #H L H2.
340  nnormalize.
341  nrewrite > H2.
342  @.
343nqed.
344   
345nlemma reverse_distributes_append:
346  ∀A: Type[0].
347  ∀l, m: List A.
348    reverse A (l @ m) = reverse A m @ reverse A l.
349  #A l m.
350  nelim l.
351  nnormalize.
352  nrewrite > (append_empty_left_neutral ? ?).
353  @.
354  #H L A.
355  nnormalize.
356  nrewrite > A.
357  nrewrite > (append_associative ? (reverse ? m) (reverse ? L) (Cons ? H (Empty ?))).
358  @.
359nqed.
360
361nlemma length_distributes_append:
362  ∀A: Type[0].
363  ∀l, m: List A.
364    length A (l @ m) = length A l + length A m.
365  #A l m.
366  nelim l.
367  nnormalize.
368  @.
369  #H L H2.
370  nnormalize.
371  nrewrite > H2.
372  @.
373nqed.
374
375(* 
376nlemma length_reverse:
377  ∀A: Type[0].
378  ∀l: List A.
379    length A (reverse A l) = length A l.
380  #A l.
381  nelim l.
382  nnormalize.
383  @.
384  #H L H2.
385  nnormalize.
386  napply (length_distributes_append A (reverse A l) (Cons A H (Empty A))).
387*)
388 
389(*   
390nlemma reverse_reverse:
391  ∀A: Type[0].
392  ∀l: List A.
393    reverse A (reverse A l) = l.
394  #A l.
395  nelim l.
396  nnormalize.
397  @.
398  #H L H2.
399  nnormalize.
400*)
401
402nlemma map_fusion:
403  ∀A, B, C: Type[0].
404  ∀l: List A.
405  ∀m: List B.
406  ∀f: A → B.
407  ∀g: B → C.
408    map B C g (map A B f l) = map A C (λx. g (f x)) l.
409  #A B C l m f g.
410  nelim l.
411  //.
412  #H L H2.
413  nnormalize.
414  nrewrite > H2.
415  @.
416nqed.
417
418nlemma map_preserves_length:
419  ∀A, B: Type[0].
420  ∀l: List A.
421  ∀f: A → B.
422    length B (map A B f l) = length A l.
423  #A B l f.
424  nelim l.
425  //.
426  #H L H2.
427  nnormalize.
428  nrewrite > H2.
429  @.
430nqed.
431
432(*
433nlemma empty_get_index_nothing:
434  ∀A: Type[0].
435  ∀n: Nat.
436    ((Empty A) !! n) = Nothing A.
437  #A n.
438  nelim n.
439  //.
440  #N H.
441  //.
442nqed.
443*)
444
445nlemma rotate_right_empty:
446  ∀A: Type[0].
447  ∀n: Nat.
448    rotate_right A (Empty A) n = Empty A.
449  #A n.
450  nelim n.
451  //.
452  #N H.
453  //.
454nqed.
455
456nlemma rotate_left_empty:
457  ∀A: Type[0].
458  ∀n: Nat.
459    rotate_left A (Empty A) n = Empty A.
460  #A n.
461  nelim n.
462  //.
463  #N H.
464  //.
465nqed.
466
467nlemma reverse_singleton:
468  ∀A: Type[0].
469  ∀a: A.
470    reverse A (Cons A a (Empty A)) = Cons A a (Empty A).
471  #A a.
472  //.
473nqed.
Note: See TracBrowser for help on using the repository browser.