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

Last change on this file since 345 was 342, checked in by sacerdot, 10 years ago

fold_lefti

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