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

Last change on this file since 289 was 260, checked in by sacerdot, 9 years ago
  • Minimal changes to make it compile with the standard distribution of Matita once this directory is substituted to nlibrary
  • ambiguity reduced by lower-casing booleans
File size: 11.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".
9(* include "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(* Lookup.                                                                    *)
41(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
42   
43(*   
44nlet rec get_index (A: Type[0]) (l: List A) (n: Nat) on n ≝
45  match n with
46    [ Z ⇒
47      match l with
48        [ Empty ⇒ Nothing A
49        | Cons hd tl ⇒ Just A hd
50        ]
51    | S o ⇒
52      match l with
53        [ Empty ⇒ Nothing A
54        | Cons hd tl ⇒ get_index A tl o
55        ]
56    ].
57   
58interpretation "List get_index" 'get_index l n = (get_index ? l n).
59
60nlet rec set_index (A: Type[0]) (l: List A) (n: Nat) (a: A) on n ≝
61  match n with
62    [ Z ⇒
63      match l with
64        [ Empty ⇒ Nothing (List A)
65        | Cons hd tl ⇒ Just (List A) (Cons A a tl)
66        ]
67    | S o ⇒
68      match l with
69        [ Empty ⇒ Nothing (List A)
70        | Cons hd tl ⇒
71            let settail ≝ set_index A tl o a in
72              match settail with
73                [ Nothing ⇒ Nothing (List A)
74                | Just j ⇒ Just (List A) (Cons A hd j)
75                ]
76        ]
77    ].
78
79nlet rec drop (A: Type[0]) (l: List A) (n: Nat) on n ≝
80  match n with
81    [ Z ⇒ Just (List A) l
82    | S o ⇒
83        match l with
84          [ Empty ⇒ Nothing (List A)
85          | Cons hd tl ⇒ drop A tl o
86          ]
87    ].
88*)
89   
90(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
91(* Building lists from scratch                                                *)
92(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
93
94nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝
95  match n with
96    [ Z ⇒ Empty A
97    | S o ⇒ a :: replicate A o a
98    ].
99   
100nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝
101  match l with
102    [ Empty ⇒ m
103    | Cons hd tl ⇒ hd :: (append A tl m)
104    ].
105   
106notation "hvbox(l break @ r)"
107  right associative with precedence 47
108  for @{ 'append $l $r }.   
109 
110interpretation "List append" 'append = (append ?).   
111
112(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
113(* Other manipulations.                                                       *)
114(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
115
116nlet rec length (A: Type[0]) (l: List A) on l ≝
117  match l with
118    [ Empty ⇒ Z
119    | Cons hd tl ⇒ S $ length A tl
120    ].
121   
122nlet rec reverse (A: Type[0]) (l: List A) on l ≝
123  match l with
124    [ Empty ⇒ Empty A
125    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
126    ].
127
128(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
129(* Deletions.                                                                 *)
130(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
131
132nlet rec remove_first_with_aux (A: Type[0]) (f: A → A → Bool) (a: A)
133                               (l: List A) (b: List A) on l ≝
134  match l with
135    [ Empty ⇒ reverse A b
136    | Cons hd tl ⇒
137      match f hd a with
138        [ true ⇒ (reverse A b) @ tl
139        | false ⇒ remove_first_with_aux A f a tl (hd :: b)
140        ]
141    ].
142
143ndefinition remove_first_with ≝
144  λA: Type[0].
145  λf: A → A → Bool.
146  λa: A.
147  λl: List A.
148    remove_first_with_aux A f a l (Empty A).
149   
150nlet rec remove_all_with_aux (A: Type[0]) (f: A → A → Bool) (a: A)
151                             (l: List A) (b: List A) on l ≝
152  match l with
153    [ Empty ⇒ reverse A b
154    | Cons hd tl ⇒
155      match f hd a with
156        [ true ⇒ remove_all_with_aux A f a tl b
157        | false ⇒ remove_all_with_aux A f a tl (hd :: b)
158        ]
159    ].
160   
161ndefinition remove_all_with ≝
162  λA: Type[0].
163  λf: A → A → Bool.
164  λa: A.
165  λl: List A.
166    remove_all_with_aux A f a l (Empty A).
167
168nlet rec drop_while (A: Type[0]) (f: A → Bool) (l: List A) on l ≝
169  match l with
170    [ Empty ⇒ Empty A
171    | Cons hd tl ⇒
172      match f hd with
173        [ true ⇒ drop_while A f tl
174        | false ⇒ Cons A hd tl
175        ]
176    ].
177   
178(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
179(* Folds and builds.                                                          *)
180(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
181
182nlet rec fold_right (A: Type[0]) (B: Type[0])
183                    (f: A → B → B) (x: B) (l: List A) on l ≝
184  match l with
185    [ Empty ⇒ x
186    | Cons hd tl ⇒ f hd (fold_right A B f x tl)
187    ].
188   
189nlet rec fold_left (A: Type[0]) (B: Type[0])
190                   (f: A → B → A) (x: A) (l: List B) on l ≝
191  match l with
192    [ Empty ⇒ x
193    | Cons hd tl ⇒ f (fold_left A B f x tl) hd
194    ].
195   
196(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
197(* Filters and existence tests.                                               *)
198(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
199
200nlet rec filter (A: Type[0]) (f: A → Bool) (l: List A) on l ≝
201  match l with
202    [ Empty ⇒ Empty A
203    | Cons hd tl ⇒
204      match f hd with
205        [ true ⇒ hd :: (filter A f tl)
206        | false ⇒ filter A f tl
207        ]
208    ].
209   
210nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l: Bool ≝
211  match l with
212    [ Empty ⇒ false
213    | Cons hd tl ⇒ inclusive_disjunction (f hd a) (member_with A a f tl)
214    ].
215   
216nlet rec nub_with (A: Type[0]) (f: A → A → Bool) (l: List A) on l ≝
217  match l with
218    [ Empty ⇒ Empty A
219    | Cons hd tl ⇒
220      match member_with A hd f tl with
221        [ true ⇒ nub_with A f tl
222        | false ⇒ hd :: (nub_with A f tl)
223        ]
224    ].
225
226(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
227(* Maps and zips.                                                             *)
228(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
229
230nlet rec map (A: Type[0]) (B: Type[0])
231             (f: A → B) (l: List A) on l ≝
232  match l with
233    [ Empty ⇒ Empty B
234    | Cons hd tl ⇒ f hd :: map A B f tl
235    ].
236   
237nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝
238  match l with
239    [ Empty ⇒ Empty A
240    | Cons hd tl ⇒ hd @ (flatten A tl)
241    ].
242   
243ndefinition map_flatten ≝
244  λA: Type[0].
245  λf: A → List A.
246  λl: List A.
247    flatten A (map A (List A) f l).
248
249(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
250(* Set-like operations.                                                       *)
251(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
252
253nlet rec intersection_with (A: Type[0]) (f: A → A → Bool)
254                           (l: List A) (m: List A) on l ≝
255  match l with
256    [ Empty ⇒ Empty A
257    | Cons hd tl ⇒
258      match member_with A hd f m with
259        [ true ⇒ hd :: (intersection_with A f tl m)
260        | false ⇒ intersection_with A f tl m
261        ]
262    ].
263
264(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
265(* Rotates and shifts.                                                        *)
266(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
267
268nlet rec rotate_left (A: Type[0]) (l: List A) (m: Nat) on m ≝
269  match m with
270    [ Z ⇒ l
271    | S n ⇒
272      match l with
273        [ Empty ⇒ Empty A
274        | Cons hd tl ⇒ hd :: rotate_left A tl n
275        ]
276    ].
277
278ndefinition rotate_right ≝
279  λA: Type[0].
280  λl: List A.
281  λm: Nat.
282    reverse A (rotate_left A (reverse A l) m).
283
284(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
285(* Lemmas.                                                                    *)
286(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
287   
288nlemma append_empty_left_neutral:
289  ∀A: Type[0].
290  ∀l: List A.
291    l @ (Empty A) = l.
292  #A l.
293  nelim l.
294  nnormalize.
295  @.
296  #H L H2.
297  nnormalize.
298  nrewrite > H2.
299  @.
300nqed.
301
302nlemma append_associative:
303  ∀A: Type[0].
304  ∀l,m,n: List A.
305    l @ (m @ n) = (l @ m) @ n.
306  #A l m n.
307  nelim l.
308  nnormalize.
309  @.
310  #H L H2.
311  nnormalize.
312  nrewrite > H2.
313  @.
314nqed.
315   
316nlemma reverse_distributes_append:
317  ∀A: Type[0].
318  ∀l, m: List A.
319    reverse A (l @ m) = reverse A m @ reverse A l.
320  #A l m.
321  nelim l.
322  nnormalize.
323  nrewrite > (append_empty_left_neutral ? ?).
324  @.
325  #H L A.
326  nnormalize.
327  nrewrite > A.
328  nrewrite > (append_associative ? (reverse ? m) (reverse ? L) (Cons ? H (Empty ?))).
329  @.
330nqed.
331
332nlemma length_distributes_append:
333  ∀A: Type[0].
334  ∀l, m: List A.
335    length A (l @ m) = length A l + length A m.
336  #A l m.
337  nelim l.
338  nnormalize.
339  @.
340  #H L H2.
341  nnormalize.
342  nrewrite > H2.
343  @.
344nqed.
345
346(* 
347nlemma length_reverse:
348  ∀A: Type[0].
349  ∀l: List A.
350    length A (reverse A l) = length A l.
351  #A l.
352  nelim l.
353  nnormalize.
354  @.
355  #H L H2.
356  nnormalize.
357  napply (length_distributes_append A (reverse A l) (Cons A H (Empty A))).
358*)
359 
360(*   
361nlemma reverse_reverse:
362  ∀A: Type[0].
363  ∀l: List A.
364    reverse A (reverse A l) = l.
365  #A l.
366  nelim l.
367  nnormalize.
368  @.
369  #H L H2.
370  nnormalize.
371*)
372
373nlemma map_fusion:
374  ∀A, B, C: Type[0].
375  ∀l: List A.
376  ∀m: List B.
377  ∀f: A → B.
378  ∀g: B → C.
379    map B C g (map A B f l) = map A C (λx. g (f x)) l.
380  #A B C l m f g.
381  nelim l.
382  //.
383  #H L H2.
384  nnormalize.
385  nrewrite > H2.
386  @.
387nqed.
388
389nlemma map_preserves_length:
390  ∀A, B: Type[0].
391  ∀l: List A.
392  ∀f: A → B.
393    length B (map A B f l) = length A l.
394  #A B l f.
395  nelim l.
396  //.
397  #H L H2.
398  nnormalize.
399  nrewrite > H2.
400  @.
401nqed.
402
403(*
404nlemma empty_get_index_nothing:
405  ∀A: Type[0].
406  ∀n: Nat.
407    ((Empty A) !! n) = Nothing A.
408  #A n.
409  nelim n.
410  //.
411  #N H.
412  //.
413nqed.
414*)
415
416nlemma rotate_right_empty:
417  ∀A: Type[0].
418  ∀n: Nat.
419    rotate_right A (Empty A) n = Empty A.
420  #A n.
421  nelim n.
422  //.
423  #N H.
424  //.
425nqed.
426
427nlemma rotate_left_empty:
428  ∀A: Type[0].
429  ∀n: Nat.
430    rotate_left A (Empty A) n = Empty A.
431  #A n.
432  nelim n.
433  //.
434  #N H.
435  //.
436nqed.
437
438nlemma reverse_singleton:
439  ∀A: Type[0].
440  ∀a: A.
441    reverse A (Cons A a (Empty A)) = Cons A a (Empty A).
442  #A a.
443  //.
444nqed.
Note: See TracBrowser for help on using the repository browser.