Changeset 241 for Deliverables/D4.1/Matita/List.ma
 Timestamp:
 Nov 15, 2010, 10:26:20 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/List.ma
r237 r241 3 3 (* ===================================== *) 4 4 5 include "Maybe.ma".6 include "Nat.ma".7 5 include "Util.ma". 6 7 include "Universes/Universes.ma". 8 9 include "Datatypes/Nat/Nat.ma". 10 include "Datatypes/Nat/Addition.ma". 11 12 include "Datatypes/Maybe.ma". 8 13 9 14 include "Plogic/equality.ma". … … 16 21 Empty: List A 17 22  Cons: A → List A → List A. 23 24 (* ===================================== *) 25 (* Syntax. *) 26 (* ===================================== *) 18 27 19 28 notation "hvbox(hd break :: tl)" … … 28 37 for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }. 29 38 39 notation "hvbox(l break !! break n)" 40 non associative with precedence 90 41 for @{ 'get_index $l $n }. 42 30 43 (* ===================================== *) 31 44 (* Lookup. *) 32 45 (* ===================================== *) 33 34 nlet rec null (A: Type[0]) (l: List A) on l ≝ 35 match l with 36 [ Empty ⇒ True 37  Cons hd tl ⇒ False 38 ]. 39 40 ndefinition 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 48 ndefinition 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 61 nlet 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 68 nlet 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 79 nlet 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 46 47 nlet rec get_index (A: Type[0]) (l: List A) (n: Nat) on n ≝ 48 match n with 49 [ Z ⇒ 50 match l with 51 [ Empty ⇒ Nothing A 52  Cons hd tl ⇒ Just A hd 53 ] 54  S o ⇒ 55 match l with 56 [ Empty ⇒ Nothing A 57  Cons hd tl ⇒ get_index A tl o 58 ] 59 ]. 60 61 interpretation "List get_index" 'get_index l n = (get_index ? l n). 62 63 nlet rec set_index (A: Type[0]) (l: List A) (n: Nat) (a: A) on n ≝ 64 match n with 65 [ Z ⇒ 66 match l with 67 [ Empty ⇒ Nothing (List A) 68  Cons hd tl ⇒ Just (List A) (Cons A a tl) 69 ] 70  S o ⇒ 71 match l with 72 [ Empty ⇒ Nothing (List A) 73  Cons hd tl ⇒ 74 let settail ≝ set_index A tl o a in 75 match settail with 76 [ Nothing ⇒ Nothing (List A) 77  Just j ⇒ Just (List A) (Cons A hd j) 78 ] 79 ] 80 ]. 81 82 nlet rec drop (A: Type[0]) (l: List A) (n: Nat) on n ≝ 83 match n with 84 [ Z ⇒ Just (List A) l 85  S o ⇒ 86 match l with 87 [ Empty ⇒ Nothing (List A) 88  Cons hd tl ⇒ drop A tl o 89 ] 90 ]. 91 86 92 (* ===================================== *) 87 93 (* Building lists from scratch *) … … 104 110 for @{ 'append $l $r }. 105 111 106 interpretation "List append" 'append = (append ?). 112 interpretation "List append" 'append = (append ?). 107 113 108 114 (* ===================================== *) … … 121 127  Cons hd tl ⇒ reverse A tl @ (hd :: Empty A) 122 128 ]. 129 130 (* ===================================== *) 131 (* Deletions. *) 132 (* ===================================== *) 133 134 nlet rec remove_first_with_aux (A: Type[0]) (f: A → A → Bool) (a: A) 135 (l: List A) (b: List A) on l ≝ 136 match l with 137 [ Empty ⇒ reverse A b 138  Cons hd tl ⇒ 139 match f hd a with 140 [ True ⇒ (reverse A b) @ tl 141  False ⇒ remove_first_with_aux A f a tl (hd :: b) 142 ] 143 ]. 144 145 ndefinition remove_first_with ≝ 146 λA: Type[0]. 147 λf: A → A → Bool. 148 λa: A. 149 λl: List A. 150 remove_first_with_aux A f a l (Empty A). 151 152 nlet rec remove_all_with_aux (A: Type[0]) (f: A → A → Bool) (a: A) 153 (l: List A) (b: List A) on l ≝ 154 match l with 155 [ Empty ⇒ reverse A b 156  Cons hd tl ⇒ 157 match f hd a with 158 [ True ⇒ remove_all_with_aux A f a tl b 159  False ⇒ remove_all_with_aux A f a tl (hd :: b) 160 ] 161 ]. 162 163 ndefinition remove_all_with ≝ 164 λA: Type[0]. 165 λf: A → A → Bool. 166 λa: A. 167 λl: List A. 168 remove_all_with_aux A f a l (Empty A). 169 170 ncheck remove_all_with. 171 172 nlet rec drop_while (A: Type[0]) (f: A → Bool) (l: List A) on l ≝ 173 match l with 174 [ Empty ⇒ Empty A 175  Cons hd tl ⇒ 176 match f hd with 177 [ True ⇒ drop_while A f tl 178  False ⇒ Cons A hd tl 179 ] 180 ]. 181 182 (* ===================================== *) 183 (* Folds and builds. *) 184 (* ===================================== *) 185 186 nlet rec fold_right (A: Type[0]) (B: Type[0]) 187 (f: A → B → B) (x: B) (l: List A) on l ≝ 188 match l with 189 [ Empty ⇒ x 190  Cons hd tl ⇒ f hd (fold_right A B f x tl) 191 ]. 192 193 nlet rec fold_left (A: Type[0]) (B: Type[0]) 194 (f: A → B → A) (x: A) (l: List B) on l ≝ 195 match l with 196 [ Empty ⇒ x 197  Cons hd tl ⇒ f (fold_left A B f x tl) hd 198 ]. 199 200 (* ===================================== *) 201 (* Filters and existence tests. *) 202 (* ===================================== *) 203 204 nlet rec filter (A: Type[0]) (f: A → Bool) (l: List A) on l ≝ 205 match l with 206 [ Empty ⇒ Empty A 207  Cons hd tl ⇒ 208 match f hd with 209 [ True ⇒ hd :: (filter A f tl) 210  False ⇒ filter A f tl 211 ] 212 ]. 213 214 nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l ≝ 215 match l with 216 [ Empty ⇒ False 217  Cons hd tl ⇒ inclusive_disjunction (f hd a) (member_with A a f tl) 218 ]. 219 220 nlet rec nub_with (A: Type[0]) (f: A → A → Bool) (l: List A) on l ≝ 221 match l with 222 [ Empty ⇒ Empty A 223  Cons hd tl ⇒ 224 match member_with A hd f tl with 225 [ True ⇒ nub_with A f tl 226  False ⇒ hd :: (nub_with A f tl) 227 ] 228 ]. 229 230 (* ===================================== *) 231 (* Maps and zips. *) 232 (* ===================================== *) 233 234 nlet rec map (A: Type[0]) (B: Type[0]) 235 (f: A → B) (l: List A) on l ≝ 236 match l with 237 [ Empty ⇒ Empty B 238  Cons hd tl ⇒ f hd :: map A B f tl 239 ]. 240 241 nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝ 242 match l with 243 [ Empty ⇒ Empty A 244  Cons hd tl ⇒ hd @ (flatten A tl) 245 ]. 246 247 ndefinition map_flatten ≝ 248 λA: Type[0]. 249 λf: A → List A. 250 λl: List A. 251 flatten A (map A (List A) f l). 252 253 (* ===================================== *) 254 (* Setlike operations. *) 255 (* ===================================== *) 256 257 nlet rec intersection_with (A: Type[0]) (f: A → A → Bool) 258 (l: List A) (m: List A) on l ≝ 259 match l with 260 [ Empty ⇒ Empty A 261  Cons hd tl ⇒ 262 match member_with A hd f m with 263 [ True ⇒ hd :: (intersection_with A f tl m) 264  False ⇒ intersection_with A f tl m 265 ] 266 ]. 123 267 124 268 (* ===================================== *) … … 256 400 //. 257 401 nqed. 402 403 nlemma empty_get_index_nothing: 404 ∀A: Type[0]. 405 ∀n: Nat. 406 ((Empty A) !! n) = Nothing A. 407 #A n. 408 nelim n. 409 //. 410 #N H. 411 //. 412 nqed. 413 414 nlemma rotate_right_empty: 415 ∀A: Type[0]. 416 ∀n: Nat. 417 rotate_right A (Empty A) n = Empty A. 418 #A n. 419 nelim n. 420 //. 421 #N H. 422 //. 423 nqed. 424 425 nlemma rotate_left_empty: 426 ∀A: Type[0]. 427 ∀n: Nat. 428 rotate_left A (Empty A) n = Empty A. 429 #A n. 430 nelim n. 431 //. 432 #N H. 433 //. 434 nqed. 435 436 nlemma reverse_singleton: 437 ∀A: Type[0]. 438 ∀a: A. 439 reverse A (Cons A a (Empty A)) = Cons A a (Empty A). 440 #A a. 441 //. 442 nqed.
Note: See TracChangeset
for help on using the changeset viewer.