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

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

Changes from this morning: Bool / Prop division = nightmare.

File size: 6.3 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
86(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
87(* Building lists from scratch                                                *)
88(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
89
90nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝
91  match n with
92    [ Z ⇒ Empty A
93    | S o ⇒ a :: replicate A o a
94    ].
95   
96nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝
97  match l with
98    [ Empty ⇒ m
99    | Cons hd tl ⇒ hd :: (append A tl m)
100    ].
101   
102notation "hvbox(l break @ r)"
103  right associative with precedence 47
104  for @{ 'append $l $r }.   
105 
106interpretation "List append" 'append = (append ?).
107
108(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
109(* Other manipulations.                                                       *)
110(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
111
112nlet rec length (A: Type[0]) (l: List A) on l ≝
113  match l with
114    [ Empty ⇒ Z
115    | Cons hd tl ⇒ S $ length A tl
116    ].
117   
118nlet rec reverse (A: Type[0]) (l: List A) on l ≝
119  match l with
120    [ Empty ⇒ Empty A
121    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
122    ].
123
124(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
125(* Rotates and shifts.                                                        *)
126(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
127
128nlet rec rotate_left (A: Type[0]) (l: List A) (m: Nat) on m ≝
129  match m with
130    [ Z ⇒ l
131    | S n ⇒
132      match l with
133        [ Empty ⇒ Empty A
134        | Cons hd tl ⇒ hd :: rotate_left A tl n
135        ]
136    ].
137
138ndefinition rotate_right ≝
139  λA: Type[0].
140  λl: List A.
141  λm: Nat.
142    reverse A (rotate_left A (reverse A l) m).
143
144(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
145(* Lemmas.                                                                    *)
146(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
147   
148nlemma append_empty_left_neutral:
149  ∀A: Type[0].
150  ∀l: List A.
151    l @ (Empty A) = l.
152  #A l.
153  nelim l.
154  nnormalize.
155  @.
156  #H L H2.
157  nnormalize.
158  nrewrite > H2.
159  @.
160nqed.
161
162nlemma append_associative:
163  ∀A: Type[0].
164  ∀l,m,n: List A.
165    l @ (m @ n) = (l @ m) @ n.
166  #A l m n.
167  nelim l.
168  nnormalize.
169  @.
170  #H L H2.
171  nnormalize.
172  nrewrite > H2.
173  @.
174nqed.
175   
176nlemma reverse_distributes_append:
177  ∀A: Type[0].
178  ∀l, m: List A.
179    reverse A (l @ m) = reverse A m @ reverse A l.
180  #A l m.
181  nelim l.
182  nnormalize.
183  napplyS append_empty_left_neutral.
184  #H L A.
185  nnormalize.
186  nrewrite > A.
187  napplyS append_associative.
188nqed.
189
190nlemma length_distributes_append:
191  ∀A: Type[0].
192  ∀l, m: List A.
193    length A (l @ m) = length A l + length A m.
194  #A l m.
195  nelim l.
196  nnormalize.
197  @.
198  #H L H2.
199  nnormalize.
200  nrewrite > H2.
201  @.
202nqed.
203
204(* 
205nlemma length_reverse:
206  ∀A: Type[0].
207  ∀l: List A.
208    length A (reverse A l) = length A l.
209  #A l.
210  nelim l.
211  nnormalize.
212  @.
213  #H L H2.
214  nnormalize.
215  napply (length_distributes_append A (reverse A l) (Cons A H (Empty A))).
216*)
217 
218(*   
219nlemma reverse_reverse:
220  ∀A: Type[0].
221  ∀l: List A.
222    reverse A (reverse A l) = l.
223  #A l.
224  nelim l.
225  nnormalize.
226  @.
227  #H L H2.
228  nnormalize.
229*)
230
231nlemma map_fusion:
232  ∀A, B, C: Type[0].
233  ∀l: List A.
234  ∀m: List B.
235  ∀f: A → B.
236  ∀g: B → C.
237    map B C g (map A B f l) = map A C (λx. g (f x)) l.
238  #A B C l m f g.
239  nelim l.
240  //.
241  #H L H2.
242  nnormalize.
243  //.
244nqed.
245
246nlemma map_preserves_length:
247  ∀A, B: Type[0].
248  ∀l: List A.
249  ∀f: A → B.
250    length B (map A B f l) = length A l.
251  #A B l f.
252  nelim l.
253  //.
254  #H L H2.
255  nnormalize.
256  //.
257nqed.
Note: See TracBrowser for help on using the repository browser.