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

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

Strange problem with matita and the Maybe file? Cannot find Maybe.ng.

File size: 6.5 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* List.ma: Polymorphic lists, and routine operations on them.                *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5include "Maybe.ma".
6include "Nat.ma".
7include "Util.ma".
8
9include "Plogic/equality.ma".
10
11(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
12(* The datatype.                                                              *)
13(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
14
15ninductive List (A: Type[0]): Type[0] ≝
16  Empty: List A
17| Cons: A → List A → List A.
18
19notation "hvbox(hd break :: tl)"
20  right associative with precedence 47
21  for @{ 'Cons $hd $tl }.
22
23interpretation "List empty" 'Empty = (Empty ?).
24interpretation "List cons" 'Cons = (Cons ?).
25 
26notation "[ list0 x sep ; ]"
27  non associative with precedence 90
28  for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }.
29 
30(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
31(* Lookup.                                                                    *)
32(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
33
34nlet rec null (A: Type[0]) (l: List A) on l ≝
35  match l with
36    [ Empty ⇒ True
37    | Cons hd tl ⇒ False
38    ].
39   
40ndefinition head ≝
41  λA: Type[0].
42  λl: List A.
43    match l with
44      [ Empty ⇒ Nothing A
45      | Cons hd tl ⇒ Just A hd
46      ].
47   
48ndefinition tail ≝
49  λA: Type[0].
50  λl: List A.
51    match l with
52      [ Empty ⇒ Nothing (List A)
53      | Cons hd tl ⇒ Just (List A) tl
54      ].
55       
56   
57(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
58(* Folds and builds.                                                          *)
59(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
60
61nlet rec fold_right (A: Type[0]) (B: Type[0])
62                    (f: A → B → B) (x: B) (l: List A) on l ≝
63  match l with
64    [ Empty ⇒ x
65    | Cons hd tl ⇒ f hd (fold_right A B f x tl)
66    ].
67   
68nlet rec fold_left (A: Type[0]) (B: Type[0])
69                   (f: A → B → A) (x: A) (l: List B) on l ≝
70  match l with
71    [ Empty ⇒ x
72    | Cons hd tl ⇒ f (fold_left A B f x tl) hd
73    ].
74
75(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
76(* Maps and zips.                                                             *)
77(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
78
79nlet rec map (A: Type[0]) (B: Type[0])
80             (f: A → B) (l: List A) on l ≝
81  match l with
82    [ Empty ⇒ Empty B
83    | Cons hd tl ⇒ f hd :: map A B f tl
84    ].
85   
86nlet rec zip_safe (A: Type[0]) (B: Type[0])
87                  (l: List A) (m: List B) (p: length A l = length B m) ≝ True.
88
89(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
90(* Building lists from scratch                                                *)
91(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
92
93nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝
94  match n with
95    [ Z ⇒ Empty A
96    | S o ⇒ a :: replicate A o a
97    ].
98   
99nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝
100  match l with
101    [ Empty ⇒ m
102    | Cons hd tl ⇒ hd :: (append A tl m)
103    ].
104   
105notation "hvbox(l break @ r)"
106  right associative with precedence 47
107  for @{ 'append $l $r }.   
108 
109interpretation "List append" 'append = (append ?).
110
111(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
112(* Other manipulations.                                                       *)
113(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
114
115nlet rec length (A: Type[0]) (l: List A) on l ≝
116  match l with
117    [ Empty ⇒ Z
118    | Cons hd tl ⇒ S $ length A tl
119    ].
120   
121nlet rec reverse (A: Type[0]) (l: List A) on l ≝
122  match l with
123    [ Empty ⇒ Empty A
124    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
125    ].
126
127(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
128(* Rotates and shifts.                                                        *)
129(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
130
131nlet rec rotate_left (A: Type[0]) (l: List A) (m: Nat) on m ≝
132  match m with
133    [ Z ⇒ l
134    | S n ⇒
135      match l with
136        [ Empty ⇒ Empty A
137        | Cons hd tl ⇒ hd :: rotate_left A tl n
138        ]
139    ].
140
141ndefinition rotate_right ≝
142  λA: Type[0].
143  λl: List A.
144  λm: Nat.
145    reverse A (rotate_left A (reverse A l) m).
146
147(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
148(* Lemmas.                                                                    *)
149(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
150   
151nlemma append_empty_left_neutral:
152  ∀A: Type[0].
153  ∀l: List A.
154    l @ (Empty A) = l.
155  #A l.
156  nelim l.
157  nnormalize.
158  @.
159  #H L H2.
160  nnormalize.
161  nrewrite > H2.
162  @.
163nqed.
164
165nlemma append_associative:
166  ∀A: Type[0].
167  ∀l,m,n: List A.
168    l @ (m @ n) = (l @ m) @ n.
169  #A l m n.
170  nelim l.
171  nnormalize.
172  @.
173  #H L H2.
174  nnormalize.
175  nrewrite > H2.
176  @.
177nqed.
178   
179nlemma reverse_distributes_append:
180  ∀A: Type[0].
181  ∀l, m: List A.
182    reverse A (l @ m) = reverse A m @ reverse A l.
183  #A l m.
184  nelim l.
185  nnormalize.
186  napplyS append_empty_left_neutral.
187  #H L A.
188  nnormalize.
189  nrewrite > A.
190  napplyS append_associative.
191nqed.
192
193nlemma length_distributes_append:
194  ∀A: Type[0].
195  ∀l, m: List A.
196    length A (l @ m) = length A l + length A m.
197  #A l m.
198  nelim l.
199  nnormalize.
200  @.
201  #H L H2.
202  nnormalize.
203  nrewrite > H2.
204  @.
205nqed.
206
207(* 
208nlemma length_reverse:
209  ∀A: Type[0].
210  ∀l: List A.
211    length A (reverse A l) = length A l.
212  #A l.
213  nelim l.
214  nnormalize.
215  @.
216  #H L H2.
217  nnormalize.
218  napply (length_distributes_append A (reverse A l) (Cons A H (Empty A))).
219*)
220 
221(*   
222nlemma reverse_reverse:
223  ∀A: Type[0].
224  ∀l: List A.
225    reverse A (reverse A l) = l.
226  #A l.
227  nelim l.
228  nnormalize.
229  @.
230  #H L H2.
231  nnormalize.
232*)
233
234nlemma map_fusion:
235  ∀A, B, C: Type[0].
236  ∀l: List A.
237  ∀m: List B.
238  ∀f: A → B.
239  ∀g: B → C.
240    map B C g (map A B f l) = map A C (λx. g (f x)) l.
241  #A B C l m f g.
242  nelim l.
243  //.
244  #H L H2.
245  nnormalize.
246  //.
247nqed.
248
249nlemma map_preserves_length:
250  ∀A, B: Type[0].
251  ∀l: List A.
252  ∀f: A → B.
253    length B (map A B f l) = length A l.
254  #A B l f.
255  nelim l.
256  //.
257  #H L H2.
258  nnormalize.
259  //.
260nqed.
Note: See TracBrowser for help on using the repository browser.