Changeset 233 for Deliverables/D4.1/Matita/List.ma
- Timestamp:
- Nov 12, 2010, 11:51:18 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/List.ma
r230 r233 1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 2 (* List.ma: Polymorphic lists, and routine operations on them. *) 3 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 4 1 5 include "Maybe.ma". 2 6 include "Nat.ma". … … 5 9 include "Plogic/equality.ma". 6 10 11 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 12 (* The datatype. *) 13 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 14 7 15 ninductive List (A: Type[0]): Type[0] ≝ 8 16 Empty: List A … … 20 28 for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }. 21 29 22 nlet rec length (A: Type[0]) (l: List A) on l ≝ 23 match l with 24 [ Empty ⇒ Z 25 | Cons hd tl ⇒ S $ length A tl 26 ]. 27 28 nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝ 29 match l with 30 [ Empty ⇒ m 31 | Cons hd tl ⇒ hd :: (append A tl m) 32 ]. 33 34 notation "hvbox(l break @ r)" 35 right associative with precedence 47 36 for @{ 'append $l $r }. 37 38 interpretation "List append" 'append = (append ?). 39 40 nlet rec fold_right (A: Type[0]) (B: Type[0]) 41 (f: A → B → B) (x: B) (l: List A) on l ≝ 42 match l with 43 [ Empty ⇒ x 44 | Cons hd tl ⇒ f hd (fold_right A B f x tl) 45 ]. 46 47 nlet rec fold_left (A: Type[0]) (B: Type[0]) 48 (f: A → B → A) (x: A) (l: List B) on l ≝ 49 match l with 50 [ Empty ⇒ x 51 | Cons hd tl ⇒ f (fold_left A B f x tl) hd 52 ]. 53 54 nlet rec map (A: Type[0]) (B: Type[0]) 55 (f: A → B) (l: List A) on l ≝ 56 match l with 57 [ Empty ⇒ Empty B 58 | Cons hd tl ⇒ f hd :: map A B f tl 59 ]. 60 30 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 31 (* Lookup. *) 32 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 33 61 34 nlet rec null (A: Type[0]) (l: List A) on l ≝ 62 35 match l with 63 36 [ Empty ⇒ True 64 37 | Cons hd tl ⇒ False 65 ].66 67 nlet rec reverse (A: Type[0]) (l: List A) on l ≝68 match l with69 [ Empty ⇒ Empty A70 | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)71 38 ]. 72 39 … … 86 53 | Cons hd tl ⇒ Just (List A) tl 87 54 ]. 88 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 86 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 87 (* Building lists from scratch *) 88 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 89 89 90 nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝ 90 91 match n with … … 93 94 ]. 94 95 95 nlemma append_empty: 96 nlet 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 102 notation "hvbox(l break @ r)" 103 right associative with precedence 47 104 for @{ 'append $l $r }. 105 106 interpretation "List append" 'append = (append ?). 107 108 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 109 (* Other manipulations. *) 110 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 111 112 nlet 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 118 nlet 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 128 nlet 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 138 ndefinition 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 148 nlemma append_empty_left_neutral: 96 149 ∀A: Type[0]. 97 150 ∀l: List A. … … 121 174 nqed. 122 175 123 nlemma reverse_ append:176 nlemma reverse_distributes_append: 124 177 ∀A: Type[0]. 125 178 ∀l, m: List A. … … 128 181 nelim l. 129 182 nnormalize. 130 napplyS append_empty .183 napplyS append_empty_left_neutral. 131 184 #H L A. 132 185 nnormalize. … … 135 188 nqed. 136 189 137 nlemma length_ append:190 nlemma length_distributes_append: 138 191 ∀A: Type[0]. 139 192 ∀l, m: List A. … … 160 213 #H L H2. 161 214 nnormalize. 162 napplyS length_append. 163 215 napply (length_distributes_append A (reverse A l) (Cons A H (Empty A))). 216 *) 217 218 (* 164 219 nlemma reverse_reverse: 165 220 ∀A: Type[0]. … … 173 228 nnormalize. 174 229 *) 230 231 nlemma 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 //. 244 nqed. 245 246 nlemma 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 //. 257 nqed.
Note: See TracChangeset
for help on using the changeset viewer.