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