1 # bend-mathlib/list.bend: List lemmas (append, reverse, length, take, drop, map, fold, filter). 2 import Base 3 import ./nat.bend as MNat 4 import ./bool.bend as MBool 5 6 # The empty list is a right identity for append: xs ++ [] = xs. 7 law append_nil: 8 for -a: Quant 9 for -A: Kind(a) 10 for xs: List 11 {List.append(a, A, xs, Nil{}) == xs : List} 12 13 def append_nil(a, A, xs): 14 match xs: 15 case Nil{}: 16 {==} 17 case h <> t: 18 %append_nil(a, A, t) : {h <> List.append(a, A, t, Nil{}) == h <> _ : List} 19 {==} 20 21 # The empty list is a left identity for append: [] ++ xs = xs. 22 law nil_append: 23 for -a: Quant 24 for -A: Kind(a) 25 for -xs: List 26 {List.append(a, A, Nil{}, xs) == xs : List} 27 28 def nil_append(a, A, xs): 29 {==} 30 31 # Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs). 32 law append_assoc: 33 for -a: Quant 34 for -A: Kind(a) 35 for xs: List 36 for -ys: List 37 for -zs: List 38 {List.append(a, A, List.append(a, A, xs, ys), zs) == List.append(a, A, xs, List.append(a, A, ys, zs)) : List} 39 40 def append_assoc(a, A, xs, ys, zs): 41 match xs: 42 case Nil{}: 43 {==} 44 case h <> t: 45 %append_assoc(a, A, t, ys, zs) : {h <> List.append(a, A, List.append(a, A, t, ys), zs) == h <> _ : List} 46 {==} 47 48 # The length of an append is the sum of the lengths. 49 law length_append: 50 for -a: Quant 51 for -A: Kind(a) 52 for xs: List 53 for -ys: List 54 {List.length(a, A, List.append(a, A, xs, ys)) == Nat.add(List.length(a, A, xs), List.length(a, A, ys)) : Nat} 55 56 def length_append(a, A, xs, ys): 57 match xs: 58 case Nil{}: 59 {==} 60 case h <> t: 61 %length_append(a, A, t, ys) : {1n+List.length(a, A, List.append(a, A, t, ys)) == 1n+_ : Nat} 62 {==} 63 64 def internal_reverse_go_append(a, -A: Kind(a), xs: List, -ys: List, -acc: List) -> {List.reverse.go(a, A, xs, List.append(a, A, ys, acc)) == List.append(a, A, List.reverse.go(a, A, xs, ys), acc) : List}: 65 match xs: 66 case Nil{}: 67 {==} 68 case h <> t: 69 internal_reverse_go_append(a, A, t, h <> ys, acc) 70 71 # The reverse accumulator loop appends the reversed list to the accumulator. 72 law reverse_go_spec: 73 for -a: Quant 74 for -A: Kind(a) 75 for xs: List 76 for -acc: List 77 {List.reverse.go(a, A, xs, acc) == List.append(a, A, List.reverse(a, A, xs), acc) : List} 78 79 def reverse_go_spec(a, A, xs, acc): 80 match xs: 81 case Nil{}: 82 {==} 83 case h <> t: 84 internal_reverse_go_append(a, A, t, h <> Nil{}, acc) 85 86 def internal_reverse_append_go(a, -A: Kind(a), xs: List, -ys: List, -acc: List) -> {List.reverse.go(a, A, List.append(a, A, xs, ys), acc) == List.reverse.go(a, A, ys, List.reverse.go(a, A, xs, acc)) : List}: 87 match xs: 88 case Nil{}: 89 {==} 90 case h <> t: 91 internal_reverse_append_go(a, A, t, ys, h <> acc) 92 93 # Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs. 94 law reverse_append: 95 for -a: Quant 96 for -A: Kind(a) 97 for xs: List 98 for ys: List 99 {List.reverse(a, A, List.append(a, A, xs, ys)) == List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) : List} 100 101 def reverse_append(a, A, xs, ys): 102 Equal.trans(List, List.reverse(a, A, List.append(a, A, xs, ys)), List.reverse.go(a, A, ys, List.reverse(a, A, xs)), List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)), internal_reverse_append_go(a, A, xs, ys, Nil{}), reverse_go_spec(a, A, ys, List.reverse(a, A, xs))) 103 104 def internal_reverse_go_go(a, -A: Kind(a), xs: List, -acc: List) -> {List.reverse.go(a, A, List.reverse.go(a, A, xs, acc), Nil{}) == List.reverse.go(a, A, acc, xs) : List}: 105 match xs: 106 case Nil{}: 107 {==} 108 case h <> t: 109 internal_reverse_go_go(a, A, t, h <> acc) 110 111 # Reversing twice gives the list back. 112 law reverse_reverse: 113 for -a: Quant 114 for -A: Kind(a) 115 for xs: List 116 {List.reverse(a, A, List.reverse(a, A, xs)) == xs : List} 117 118 def reverse_reverse(a, A, xs): 119 internal_reverse_go_go(a, A, xs, Nil{}) 120 121 def internal_length_reverse_go(a, -A: Kind(a), xs: List, -acc: List, +n: Nat, e: {List.length(a, A, acc) == n : Nat}) -> {List.length(a, A, List.reverse.go(a, A, xs, acc)) == Nat.add(n, List.length(a, A, xs)) : Nat}: 122 match xs: 123 case Nil{}: 124 %Equal.sym(Nat, Nat.add(n, 0n), n, MNat.add_zero(n)) : {List.length(a, A, acc) == _ : Nat} 125 e 126 case h <> t: 127 %Equal.sym(Nat, Nat.add(n, 1n+List.length(a, A, t)), 1n+Nat.add(n, List.length(a, A, t)), MNat.add_succ(n, List.length(a, A, t))) : {List.length(a, A, List.reverse.go(a, A, t, h <> acc)) == _ : Nat} 128 internal_length_reverse_go(a, A, t, h <> acc, 1n+n, Equal.cong(Nat, Nat, k => 1n+k, List.length(a, A, acc), n, e)) 129 130 # Reversing preserves the length. 131 law length_reverse: 132 for -a: Quant 133 for -A: Kind(a) 134 for xs: List 135 {List.length(a, A, List.reverse(a, A, xs)) == List.length(a, A, xs) : Nat} 136 137 def length_reverse(a, A, xs): 138 internal_length_reverse_go(a, A, xs, Nil{}, 0n, {==}) 139 140 # A right fold over an append folds the first part onto the fold of the second. 141 law foldr_append: 142 for ~a: Quant 143 for ~A: Kind(a) 144 for ~B: Type 145 for ~f: A -> B -> B 146 for xs: List 147 for -ys: List 148 for -z: B 149 {List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) == List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)) : B} 150 151 def foldr_append(a, A, B, f, xs, ys, z): 152 match xs: 153 case Nil{}: 154 {==} 155 case h <> t: 156 %foldr_append(~a, ~A, ~B, ~f, t, ys, z) : {f(h, List.foldr(~a, ~A, ~B, ~f, List.append(a, A, t, ys), z)) == f(h, _) : B} 157 {==} 158 159 # Taking n elements and appending the rest after dropping n gives the list back. 160 law take_append_drop: 161 for -a: Quant 162 for -A: Kind(a) 163 for xs: List 164 for n: Nat 165 {List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) == xs : List} 166 167 def take_append_drop(a, A, xs, n): 168 match xs n: 169 case Nil{} _: 170 {==} 171 case h <> t 0n: 172 {==} 173 case h <> t 1n+p: 174 %take_append_drop(a, A, t, p) : {h <> List.append(a, A, List.take(a, A, t, p), List.drop(a, A, t, p)) == h <> _ : List} 175 {==} 176 177 # Mapping preserves the length. 178 law length_map: 179 for ~A: Type 180 for ~B: Type 181 for ~f: A -> B 182 for xs: List 183 {List.length(&1, B, List.map(~A, ~B, ~f, xs)) == List.length(&1, A, xs) : Nat} 184 185 def length_map(A, B, f, xs): 186 match xs: 187 case Nil{}: 188 {==} 189 case h <> t: 190 %length_map(~A, ~B, ~f, t) : {1n+List.length(&1, B, List.map(~A, ~B, ~f, t)) == 1n+_ : Nat} 191 {==} 192 193 # Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys. 194 law map_append: 195 for ~A: Type 196 for ~B: Type 197 for ~f: A -> B 198 for xs: List 199 for -ys: List 200 {List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)) == List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)) : List} 201 202 def map_append(A, B, f, xs, ys): 203 match xs: 204 case Nil{}: 205 {==} 206 case h <> t: 207 %map_append(~A, ~B, ~f, t, ys) : {f(h) <> List.map(~A, ~B, ~f, List.append(&1, A, t, ys)) == f(h) <> _ : List} 208 {==} 209 210 # Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs. 211 law map_map: 212 for ~A: Type 213 for ~B: Type 214 for ~C: Type 215 for ~f: A -> B 216 for ~g: B -> C 217 for xs: List 218 {List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~C, ~(x => g(f(x))), xs) : List} 219 220 def map_map(A, B, C, f, g, xs): 221 match xs: 222 case Nil{}: 223 {==} 224 case h <> t: 225 %map_map(~A, ~B, ~C, ~f, ~g, t) : {g(f(h)) <> List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, t)) == g(f(h)) <> _ : List} 226 {==} 227 228 # Taking zero elements gives the empty list. 229 law take_zero: 230 for -a: Quant 231 for -A: Kind(a) 232 for xs: List 233 {List.take(a, A, xs, 0n) == Nil{} : List} 234 235 def take_zero(a, A, xs): 236 match xs: 237 case Nil{}: 238 {==} 239 case h <> t: 240 {==} 241 242 # Dropping zero elements gives the list back. 243 law drop_zero: 244 for -a: Quant 245 for -A: Kind(a) 246 for xs: List 247 {List.drop(a, A, xs, 0n) == xs : List} 248 249 def drop_zero(a, A, xs): 250 match xs: 251 case Nil{}: 252 {==} 253 case h <> t: 254 {==} 255 256 # Taking from the empty list gives the empty list. 257 law take_nil: 258 for -a: Quant 259 for -A: Kind(a) 260 for -n: Nat 261 {List.take(a, A, Nil{}, n) == Nil{} : List} 262 263 def take_nil(a, A, n): 264 {==} 265 266 # Dropping from the empty list gives the empty list. 267 law drop_nil: 268 for -a: Quant 269 for -A: Kind(a) 270 for -n: Nat 271 {List.drop(a, A, Nil{}, n) == Nil{} : List} 272 273 def drop_nil(a, A, n): 274 {==} 275 276 # Taking n elements leaves min(n, length) of them. 277 law length_take: 278 for -a: Quant 279 for -A: Kind(a) 280 for xs: List 281 for n: Nat 282 {List.length(a, A, List.take(a, A, xs, n)) == Nat.min(n, List.length(a, A, xs)) : Nat} 283 284 def length_take(a, A, xs, n): 285 match xs n: 286 case Nil{} _: 287 Equal.sym(Nat, Nat.min(n, 0n), 0n, MNat.min_zero(n)) 288 case h <> t 0n: 289 {==} 290 case h <> t 1n+p: 291 %length_take(a, A, t, p) : {1n+List.length(a, A, List.take(a, A, t, p)) == 1n+_ : Nat} 292 {==} 293 294 # Dropping n elements leaves length - n of them. 295 law length_drop: 296 for -a: Quant 297 for -A: Kind(a) 298 for xs: List 299 for n: Nat 300 {List.length(a, A, List.drop(a, A, xs, n)) == Nat.sub(List.length(a, A, xs), n) : Nat} 301 302 def length_drop(a, A, xs, n): 303 match xs n: 304 case Nil{} _: 305 Equal.sym(Nat, Nat.sub(0n, n), 0n, MNat.zero_sub(n)) 306 case h <> t 0n: 307 {==} 308 case h <> t 1n+p: 309 length_drop(a, A, t, p) 310 311 # Taking as many elements as the list has gives the list back. 312 law take_length: 313 for -A: Data 314 for +xs: List<&2, A> 315 {List.take(&2, A, xs, List.length(&2, A, xs)) == xs : List<&2, A>} 316 317 def take_length(A, xs): 318 match xs: 319 case Nil{}: 320 {==} 321 case h <> t: 322 %take_length(A, t) : {h <> List.take(&2, A, t, List.length(&2, A, t)) == h <> _ : List<&2, A>} 323 {==} 324 325 # Dropping as many elements as the list has gives the empty list. 326 law drop_length: 327 for -A: Data 328 for +xs: List<&2, A> 329 {List.drop(&2, A, xs, List.length(&2, A, xs)) == Nil{} : List<&2, A>} 330 331 def drop_length(A, xs): 332 match xs: 333 case Nil{}: 334 {==} 335 case h <> t: 336 drop_length(A, t) 337 338 # Taking m from the first n is taking min(n, m). 339 law take_take: 340 for -a: Quant 341 for -A: Kind(a) 342 for xs: List 343 for n: Nat 344 for m: Nat 345 {List.take(a, A, List.take(a, A, xs, n), m) == List.take(a, A, xs, Nat.min(n, m)) : List} 346 347 def take_take(a, A, xs, n, m): 348 match xs n m: 349 case Nil{} _ _: 350 {==} 351 case h <> t 0n _: 352 {==} 353 case h <> t 1n+p 0n: 354 {==} 355 case h <> t 1n+p 1n+q: 356 %take_take(a, A, t, p, q) : {h <> List.take(a, A, List.take(a, A, t, p), q) == h <> _ : List} 357 {==} 358 359 # Dropping m after dropping n is dropping n + m. 360 law drop_drop: 361 for -a: Quant 362 for -A: Kind(a) 363 for xs: List 364 for n: Nat 365 for -m: Nat 366 {List.drop(a, A, List.drop(a, A, xs, n), m) == List.drop(a, A, xs, Nat.add(n, m)) : List} 367 368 def drop_drop(a, A, xs, n, m): 369 match xs n m: 370 case Nil{} _ _: 371 {==} 372 case h <> t 0n _: 373 {==} 374 case h <> t 1n+p _: 375 drop_drop(a, A, t, p, m) 376 377 # Reversing the empty list gives the empty list. 378 law reverse_nil: 379 for -a: Quant 380 for -A: Kind(a) 381 {List.reverse(a, A, Nil{}) == Nil{} : List} 382 383 def reverse_nil(a, A): 384 {==} 385 386 # Reversing a one-element list gives it back. 387 law reverse_singleton: 388 for -a: Quant 389 for -A: Kind(a) 390 for -x: A 391 {List.reverse(a, A, [x]) == [x] : List} 392 393 def reverse_singleton(a, A, x): 394 {==} 395 396 # Replicating x n times gives a list of length n. 397 law length_replicate: 398 for -A: Data 399 for n: Nat 400 for -x: A 401 {List.length(&2, A, List.replicate(A, n, x)) == n : Nat} 402 403 def length_replicate(A, n, x): 404 match n: 405 case 0n: 406 {==} 407 case 1n+p: 408 %length_replicate(A, p, x) : {1n+List.length(&2, A, List.replicate(A, p, x)) == 1n+_ : Nat} 409 {==} 410 411 def internal_length_range_go(+n: Nat, acc: List<&2, Nat>) -> {List.length(&2, Nat, List.range.go(n, acc)) == Nat.add(n, List.length(&2, Nat, acc)) : Nat}: 412 match n: 413 case 0n: 414 {==} 415 case 1n+p: 416 %MNat.add_succ(p, List.length(&2, Nat, acc)) : {List.length(&2, Nat, List.range.go(p, p <> acc)) == _ : Nat} 417 internal_length_range_go(p, p <> acc) 418 419 # Range(n) has length n. 420 law length_range: 421 for n: Nat 422 {List.length(&2, Nat, List.range(n)) == n : Nat} 423 424 def length_range(n): 425 +n = n 426 %Equal.sym(Nat, List.length(&2, Nat, List.range.go(n, Nil{})), Nat.add(n, 0n), internal_length_range_go(n, Nil{})) : {_ == n : Nat} 427 MNat.add_zero(n) 428 429 # Zipping two lists gives the length of the shorter one. 430 law length_zip: 431 for -a: Quant 432 for -A: Kind(a) 433 for xs: List 434 for ys: List 435 {List.length(&1, A & A, List.zip(a, A, a, A, xs, ys)) == Nat.min(List.length(a, A, xs), List.length(a, A, ys)) : Nat} 436 437 def length_zip(a, A, xs, ys): 438 match xs ys: 439 case Nil{} _: 440 {==} 441 case h <> t Nil{}: 442 {==} 443 case h <> t y <> yt: 444 %length_zip(a, A, t, yt) : {1n+List.length(&1, A & A, List.zip(a, A, a, A, t, yt)) == 1n+_ : Nat} 445 {==} 446 447 # Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys). 448 law append_cons: 449 for -a: Quant 450 for -A: Kind(a) 451 for -x: A 452 for -xs: List 453 for -ys: List 454 {List.append(a, A, x <> xs, ys) == x <> List.append(a, A, xs, ys) : List} 455 456 def append_cons(a, A, x, xs, ys): 457 {==} 458 459 # The empty list has length zero. 460 law length_nil: 461 for -a: Quant 462 for -A: Kind(a) 463 {List.length(a, A, Nil{}) == 0n : Nat} 464 465 def length_nil(a, A): 466 {==} 467 468 # A cons is one longer than its tail. 469 law length_cons: 470 for -a: Quant 471 for -A: Kind(a) 472 for -x: A 473 for -xs: List 474 {List.length(a, A, x <> xs) == 1n+List.length(a, A, xs) : Nat} 475 476 def length_cons(a, A, x, xs): 477 {==} 478 479 # Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss. 480 law concat_append: 481 for -a: Quant 482 for -A: Kind(a) 483 for xss: List> 484 for -yss: List> 485 {List.concat(a, A, List.append(a, List, xss, yss)) == List.append(a, A, List.concat(a, A, xss), List.concat(a, A, yss)) : List} 486 487 def concat_append(a, A, xss, yss): 488 match xss: 489 case Nil{}: 490 {==} 491 case h <> t: 492 %Equal.sym(List, List.concat(a, A, List.append(a, List, t, yss)), List.append(a, A, List.concat(a, A, t), List.concat(a, A, yss)), concat_append(a, A, t, yss)) : {List.append(a, A, h, _) == List.append(a, A, List.append(a, A, h, List.concat(a, A, t)), List.concat(a, A, yss)) : List} 493 Equal.sym(List, List.append(a, A, List.append(a, A, h, List.concat(a, A, t)), List.concat(a, A, yss)), List.append(a, A, h, List.append(a, A, List.concat(a, A, t), List.concat(a, A, yss))), append_assoc(a, A, h, List.concat(a, A, t), List.concat(a, A, yss))) 494 495 # A left fold over an append folds the second part from the fold of the first. 496 law foldl_append: 497 for ~a: Quant 498 for ~A: Kind(a) 499 for ~B: Type 500 for ~f: B -> A -> B 501 for xs: List 502 for -ys: List 503 for -z: B 504 {List.foldl(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) == List.foldl(~a, ~A, ~B, ~f, ys, List.foldl(~a, ~A, ~B, ~f, xs, z)) : B} 505 506 def foldl_append(a, A, B, f, xs, ys, z): 507 match xs: 508 case Nil{}: 509 {==} 510 case h <> t: 511 foldl_append(~a, ~A, ~B, ~f, t, ys, f(z, h)) 512 513 def internal_map_reverse_go(~A: Type, ~B: Type, ~f: A -> B, xs: List, acc: List) -> {List.map(~A, ~B, ~f, List.reverse.go(&1, A, xs, acc)) == List.reverse.go(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, acc)) : List}: 514 match xs: 515 case Nil{}: 516 {==} 517 case h <> t: 518 internal_map_reverse_go(~A, ~B, ~f, t, h <> acc) 519 520 # Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs). 521 law map_reverse: 522 for ~A: Type 523 for ~B: Type 524 for ~f: A -> B 525 for xs: List 526 {List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) == List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) : List} 527 528 def map_reverse(A, B, f, xs): 529 internal_map_reverse_go(~A, ~B, ~f, xs, Nil{}) 530 531 # All over an append is all over each part, joined by and. 532 law all_append: 533 for ~a: Quant 534 for ~A: Kind(a) 535 for ~f: A -> Bool 536 for xs: List 537 for -ys: List 538 {List.all(~a, ~A, ~f, List.append(a, A, xs, ys)) == Bool.and(List.all(~a, ~A, ~f, xs), List.all(~a, ~A, ~f, ys)) : Bool} 539 540 def all_append(a, A, f, xs, ys): 541 match xs: 542 case Nil{}: 543 {==} 544 case h <> t: 545 %Equal.sym(Bool, List.all(~a, ~A, ~f, List.append(a, A, t, ys)), Bool.and(List.all(~a, ~A, ~f, t), List.all(~a, ~A, ~f, ys)), all_append(~a, ~A, ~f, t, ys)) : {Bool.and(f(h), _) == Bool.and(Bool.and(f(h), List.all(~a, ~A, ~f, t)), List.all(~a, ~A, ~f, ys)) : Bool} 546 Equal.sym(Bool, Bool.and(Bool.and(f(h), List.all(~a, ~A, ~f, t)), List.all(~a, ~A, ~f, ys)), Bool.and(f(h), Bool.and(List.all(~a, ~A, ~f, t), List.all(~a, ~A, ~f, ys))), MBool.and_assoc(f(h), List.all(~a, ~A, ~f, t), List.all(~a, ~A, ~f, ys))) 547 548 # Any over an append is any over each part, joined by or. 549 law any_append: 550 for ~a: Quant 551 for ~A: Kind(a) 552 for ~f: A -> Bool 553 for xs: List 554 for -ys: List 555 {List.any(~a, ~A, ~f, List.append(a, A, xs, ys)) == Bool.or(List.any(~a, ~A, ~f, xs), List.any(~a, ~A, ~f, ys)) : Bool} 556 557 def any_append(a, A, f, xs, ys): 558 match xs: 559 case Nil{}: 560 {==} 561 case h <> t: 562 %Equal.sym(Bool, List.any(~a, ~A, ~f, List.append(a, A, t, ys)), Bool.or(List.any(~a, ~A, ~f, t), List.any(~a, ~A, ~f, ys)), any_append(~a, ~A, ~f, t, ys)) : {Bool.or(f(h), _) == Bool.or(Bool.or(f(h), List.any(~a, ~A, ~f, t)), List.any(~a, ~A, ~f, ys)) : Bool} 563 Equal.sym(Bool, Bool.or(Bool.or(f(h), List.any(~a, ~A, ~f, t)), List.any(~a, ~A, ~f, ys)), Bool.or(f(h), Bool.or(List.any(~a, ~A, ~f, t), List.any(~a, ~A, ~f, ys))), MBool.or_assoc(f(h), List.any(~a, ~A, ~f, t), List.any(~a, ~A, ~f, ys))) 564 565 def internal_filter_put_append(-A: Data, h: A, r: List<&2, A>, s: List<&2, A>, b: Bool) -> {List.append(&2, A, List.filter.put(A, h, r, b), s) == List.filter.put(A, h, List.append(&2, A, r, s), b) : List<&2, A>}: 566 match b: 567 case False{}: 568 {==} 569 case True{}: 570 {==} 571 572 # Filtering an append filters each part. 573 law filter_append: 574 for ~A: Data 575 for ~f: A -> Bool 576 for xs: List<&2, A> 577 for ys: List<&2, A> 578 {List.filter(~A, ~f, List.append(&2, A, xs, ys)) == List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)) : List<&2, A>} 579 580 def filter_append(A, f, xs, ys): 581 match xs: 582 case Nil{}: 583 {==} 584 case +h <> t: 585 +ys = ys 586 +t = t 587 %Equal.sym(List<&2, A>, List.filter(~A, ~f, List.append(&2, A, t, ys)), List.append(&2, A, List.filter(~A, ~f, t), List.filter(~A, ~f, ys)), filter_append(~A, ~f, t, ys)) : {List.filter.put(A, h, _, f(h)) == List.append(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h)), List.filter(~A, ~f, ys)) : List<&2, A>} 588 Equal.sym(List<&2, A>, List.append(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h)), List.filter(~A, ~f, ys)), List.filter.put(A, h, List.append(&2, A, List.filter(~A, ~f, t), List.filter(~A, ~f, ys)), f(h)), internal_filter_put_append(A, h, List.filter(~A, ~f, t), List.filter(~A, ~f, ys), f(h))) 589 590 # An append contains x iff either part does. 591 law contains_append: 592 for ~A: Data 593 for ~eq: A -> A -> Bool 594 for xs: List<&2, A> 595 for -ys: List<&2, A> 596 for +x: A 597 {List.contains(~A, ~eq, List.append(&2, A, xs, ys), x) == Bool.or(List.contains(~A, ~eq, xs, x), List.contains(~A, ~eq, ys, x)) : Bool} 598 599 def contains_append(A, eq, xs, ys, x): 600 match xs: 601 case Nil{}: 602 {==} 603 case h <> t: 604 %Equal.sym(Bool, List.contains(~A, ~eq, List.append(&2, A, t, ys), x), Bool.or(List.contains(~A, ~eq, t, x), List.contains(~A, ~eq, ys, x)), contains_append(~A, ~eq, t, ys, x)) : {Bool.or(eq(h, x), _) == Bool.or(Bool.or(eq(h, x), List.contains(~A, ~eq, t, x)), List.contains(~A, ~eq, ys, x)) : Bool} 605 Equal.sym(Bool, Bool.or(Bool.or(eq(h, x), List.contains(~A, ~eq, t, x)), List.contains(~A, ~eq, ys, x)), Bool.or(eq(h, x), Bool.or(List.contains(~A, ~eq, t, x), List.contains(~A, ~eq, ys, x))), MBool.or_assoc(eq(h, x), List.contains(~A, ~eq, t, x), List.contains(~A, ~eq, ys, x))) 606 607 def internal_length_filter_put_le(-A: Data, h: A, r: List<&2, A>, b: Bool) -> {Nat.is_le(List.length(&2, A, List.filter.put(A, h, r, b)), 1n+List.length(&2, A, r)) == True{} : Bool}: 608 match b: 609 case False{}: 610 MNat.le_succ(List.length(&2, A, r)) 611 case True{}: 612 MNat.le_refl(1n+List.length(&2, A, r)) 613 614 # Filtering never makes a list longer. 615 law length_filter_le: 616 for ~A: Data 617 for ~f: A -> Bool 618 for xs: List<&2, A> 619 {Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)) == True{} : Bool} 620 621 def length_filter_le(A, f, xs): 622 match xs: 623 case Nil{}: 624 {==} 625 case +h <> t: 626 +t = t 627 MNat.le_trans(List.length(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))), 1n+List.length(&2, A, List.filter(~A, ~f, t)), 1n+List.length(&2, A, t), internal_length_filter_put_le(A, h, List.filter(~A, ~f, t), f(h)), MNat.succ_le_succ(List.length(&2, A, List.filter(~A, ~f, t)), List.length(&2, A, t), length_filter_le(~A, ~f, t))) 628 629 # Membership in a list, as a reusable proposition. 630 def mem(~A: Data, ~eq: A -> A -> Bool, +x: A, xs: List<&2, A>) -> Data: 631 {List.contains(~A, ~eq, xs, x) == True{} : Bool} 632 633 # A list is sorted by a comparator when every adjacent pair is in order. 634 def sorted_by(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>) -> Data: 635 {List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), List.zip(&2, A, &2, A, xs, List.tail(&2, A, xs))) == True{} : Bool} 636 637 def internal_or_of_right(a: Bool, -b: Bool, hb: {b == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}: 638 match a: 639 case False{}: 640 hb 641 case True{}: 642 {==} 643 644 def internal_or_of_or(a: Bool, -b: Bool, -c: Bool, h: {Bool.or(a, b) == True{} : Bool}, k: {b == True{} : Bool} -> {c == True{} : Bool}) -> {Bool.or(a, c) == True{} : Bool}: 645 match a: 646 case False{}: 647 k(h) 648 case True{}: 649 {==} 650 651 def internal_and_left(a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}: 652 match a: 653 case False{}: 654 Empty.absurd({False{} == True{} : Bool}, MNat.internal_false_ne_true(h)) 655 case True{}: 656 {==} 657 658 def internal_and_right(a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}: 659 match a: 660 case False{}: 661 Empty.absurd({b == True{} : Bool}, MNat.internal_false_ne_true(h)) 662 case True{}: 663 h 664 665 def internal_mem_append_left(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +x: Nat, h: {List.contains(~Nat, ~Nat.is_eq, xs, x) == True{} : Bool}) -> {List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, xs, ys), x) == True{} : Bool}: 666 match xs: 667 case Nil{}: 668 Empty.absurd({List.contains(~Nat, ~Nat.is_eq, ys, x) == True{} : Bool}, MNat.internal_false_ne_true(h)) 669 case hd <> tl: 670 internal_or_of_or(Nat.is_eq(hd, x), List.contains(~Nat, ~Nat.is_eq, tl, x), List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, tl, ys), x), h, internal_mem_append_left(tl, ys, x)) 671 672 def internal_mem_append_right(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +x: Nat, h: {List.contains(~Nat, ~Nat.is_eq, ys, x) == True{} : Bool}) -> {List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, xs, ys), x) == True{} : Bool}: 673 match xs: 674 case Nil{}: 675 h 676 case hd <> tl: 677 internal_or_of_right(Nat.is_eq(hd, x), List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, tl, ys), x), internal_mem_append_right(tl, ys, x, h)) 678 679 # The head of a Nat list is a member of it (membership by Nat.is_eq). 680 law mem_cons_self: 681 for x: Nat 682 for -xs: List<&2, Nat> 683 mem(~Nat, ~Nat.is_eq, x, x <> xs) 684 685 def mem_cons_self(x, xs): 686 %Equal.sym(Bool, Nat.is_eq(x, x), True{}, MNat.is_eq_refl(x)) : {Bool.or(_, List.contains(~Nat, ~Nat.is_eq, xs, x)) == True{} : Bool} 687 {==} 688 689 # A member of a Nat list stays a member when a head is prepended. 690 law mem_cons_of_mem: 691 for x: Nat 692 for y: Nat 693 for -xs: List<&2, Nat> 694 for h: mem(~Nat, ~Nat.is_eq, x, xs) 695 mem(~Nat, ~Nat.is_eq, x, y <> xs) 696 697 def mem_cons_of_mem(x, y, xs, h): 698 +x = x 699 internal_or_of_right(Nat.is_eq(y, x), List.contains(~Nat, ~Nat.is_eq, xs, x), h) 700 701 # No Nat is a member of the empty list. 702 law not_mem_nil: 703 for -x: Nat 704 mem(~Nat, ~Nat.is_eq, x, Nil{}) -> Empty 705 706 def not_mem_nil(x, h): 707 MNat.internal_false_ne_true(h) 708 709 # A member of xs is a member of xs ++ ys (Nat lists). 710 law mem_append_left: 711 for xs: List<&2, Nat> 712 for ys: List<&2, Nat> 713 for x: Nat 714 for h: mem(~Nat, ~Nat.is_eq, x, xs) 715 mem(~Nat, ~Nat.is_eq, x, List.append(&2, Nat, xs, ys)) 716 717 def mem_append_left(xs, ys, x, h): 718 internal_mem_append_left(xs, ys, x, h) 719 720 # A member of ys is a member of xs ++ ys (Nat lists). 721 law mem_append_right: 722 for xs: List<&2, Nat> 723 for ys: List<&2, Nat> 724 for x: Nat 725 for h: mem(~Nat, ~Nat.is_eq, x, ys) 726 mem(~Nat, ~Nat.is_eq, x, List.append(&2, Nat, xs, ys)) 727 728 def mem_append_right(xs, ys, x, h): 729 internal_mem_append_right(xs, ys, x, h) 730 731 # The empty Nat list is sorted by Nat.is_le. 732 law sorted_nil: 733 sorted_by(~Nat, ~Nat.is_le, Nil{}) 734 735 def sorted_nil(): 736 {==} 737 738 # A one-element Nat list is sorted by Nat.is_le. 739 law sorted_single: 740 for -x: Nat 741 sorted_by(~Nat, ~Nat.is_le, [x]) 742 743 def sorted_single(x): 744 {==} 745 746 # A Nat list sorted by Nat.is_le stays sorted under a head that is <= the next element. 747 law sorted_cons_cons_intro: 748 for -x: Nat 749 for -y: Nat 750 for -t: List<&2, Nat> 751 for hxy: MNat.le(x, y) 752 for hyt: sorted_by(~Nat, ~Nat.is_le, y <> t) 753 sorted_by(~Nat, ~Nat.is_le, x <> y <> t) 754 755 def sorted_cons_cons_intro(x, y, t, hxy, hyt): 756 %Equal.sym(Bool, Nat.is_le(x, y), True{}, hxy) : {Bool.and(_, List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t))) == True{} : Bool} 757 hyt 758 759 # The first two elements of a Nat list sorted by Nat.is_le are in order. 760 law sorted_cons_cons_elim_le: 761 for x: Nat 762 for y: Nat 763 for -t: List<&2, Nat> 764 for h: sorted_by(~Nat, ~Nat.is_le, x <> y <> t) 765 MNat.le(x, y) 766 767 def sorted_cons_cons_elim_le(x, y, t, h): 768 internal_and_left(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), h) 769 770 # The tail of a Nat list of two or more elements sorted by Nat.is_le is sorted. 771 law sorted_cons_cons_elim_tail: 772 for x: Nat 773 for y: Nat 774 for -t: List<&2, Nat> 775 for h: sorted_by(~Nat, ~Nat.is_le, x <> y <> t) 776 sorted_by(~Nat, ~Nat.is_le, y <> t) 777 778 def sorted_cons_cons_elim_tail(x, y, t, h): 779 internal_and_right(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), h) 780 781 # The tail of a nonempty Nat list sorted by Nat.is_le is sorted. 782 law sorted_tail: 783 for x: Nat 784 for xs: List<&2, Nat> 785 for h: sorted_by(~Nat, ~Nat.is_le, x <> xs) 786 sorted_by(~Nat, ~Nat.is_le, xs) 787 788 def sorted_tail(x, xs, h): 789 match xs: 790 case Nil{}: 791 {==} 792 case y <> t: 793 internal_and_right(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), h) 794 795 # Taking the length of the first part of an append gives the first part back. 796 law take_left: 797 for -a: Quant 798 for -A: Kind(a) 799 for xs: List 800 for ys: List 801 {List.take(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) == xs : List} 802 803 def take_left(a, A, xs, ys): 804 match xs: 805 case Nil{}: 806 take_zero(a, A, ys) 807 case h <> t: 808 %take_left(a, A, t, ys) : {h <> List.take(a, A, List.append(a, A, t, ys), List.length(a, A, t)) == h <> _ : List} 809 {==} 810 811 # Dropping the length of the first part of an append gives the second part. 812 law drop_left: 813 for -a: Quant 814 for -A: Kind(a) 815 for xs: List 816 for ys: List 817 {List.drop(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) == ys : List} 818 819 def drop_left(a, A, xs, ys): 820 match xs: 821 case Nil{}: 822 drop_zero(a, A, ys) 823 case h <> t: 824 drop_left(a, A, t, ys) 825 826 # Taking past the first part of an append keeps it and takes the rest from the second part. 827 law take_append: 828 for -a: Quant 829 for -A: Kind(a) 830 for xs: List 831 for -ys: List 832 for -n: Nat 833 {List.take(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)) == List.append(a, A, xs, List.take(a, A, ys, n)) : List} 834 835 def take_append(a, A, xs, ys, n): 836 match xs: 837 case Nil{}: 838 {==} 839 case h <> t: 840 %take_append(a, A, t, ys, n) : {h <> List.take(a, A, List.append(a, A, t, ys), Nat.add(List.length(a, A, t), n)) == h <> _ : List} 841 {==} 842 843 # Dropping past the first part of an append drops the rest from the second part. 844 law drop_append: 845 for -a: Quant 846 for -A: Kind(a) 847 for xs: List 848 for -ys: List 849 for -n: Nat 850 {List.drop(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)) == List.drop(a, A, ys, n) : List} 851 852 def drop_append(a, A, xs, ys, n): 853 match xs: 854 case Nil{}: 855 {==} 856 case h <> t: 857 drop_append(a, A, t, ys, n) 858 859 # Taking at most the length of the first part of an append only sees the first part. 860 law take_append_of_le_length: 861 for -a: Quant 862 for -A: Kind(a) 863 for xs: List 864 for ys: List 865 for n: Nat 866 for h: MNat.le(n, List.length(a, A, xs)) 867 {List.take(a, A, List.append(a, A, xs, ys), n) == List.take(a, A, xs, n) : List} 868 869 def take_append_of_le_length(a, A, xs, ys, n, h): 870 match xs n: 871 case Nil{} 0n: 872 take_zero(a, A, ys) 873 case Nil{} 1n+p: 874 Empty.absurd({List.take(a, A, ys, 1n+p) == Nil{} : List}, MNat.internal_false_ne_true(h)) 875 case x <> t 0n: 876 {==} 877 case x <> t 1n+p: 878 %take_append_of_le_length(a, A, t, ys, p, h) : {x <> List.take(a, A, List.append(a, A, t, ys), p) == x <> _ : List} 879 {==} 880 881 # Dropping at most the length of the first part of an append drops only from the first part. 882 law drop_append_of_le_length: 883 for -a: Quant 884 for -A: Kind(a) 885 for xs: List 886 for ys: List 887 for n: Nat 888 for h: MNat.le(n, List.length(a, A, xs)) 889 {List.drop(a, A, List.append(a, A, xs, ys), n) == List.append(a, A, List.drop(a, A, xs, n), ys) : List} 890 891 def drop_append_of_le_length(a, A, xs, ys, n, h): 892 match xs n: 893 case Nil{} 0n: 894 drop_zero(a, A, ys) 895 case Nil{} 1n+p: 896 Empty.absurd({List.drop(a, A, ys, 1n+p) == ys : List}, MNat.internal_false_ne_true(h)) 897 case x <> t 0n: 898 {==} 899 case x <> t 1n+p: 900 drop_append_of_le_length(a, A, t, ys, p, h) 901 902 # Mapping commutes with taking: map f (take n xs) = take n (map f xs). 903 law map_take: 904 for ~A: Type 905 for ~B: Type 906 for ~f: A -> B 907 for xs: List 908 for n: Nat 909 {List.map(~A, ~B, ~f, List.take(&1, A, xs, n)) == List.take(&1, B, List.map(~A, ~B, ~f, xs), n) : List} 910 911 def map_take(A, B, f, xs, n): 912 match xs n: 913 case Nil{} _: 914 {==} 915 case h <> t 0n: 916 {==} 917 case h <> t 1n+p: 918 %map_take(~A, ~B, ~f, t, p) : {f(h) <> List.map(~A, ~B, ~f, List.take(&1, A, t, p)) == f(h) <> _ : List} 919 {==} 920 921 # Mapping commutes with dropping: map f (drop n xs) = drop n (map f xs). 922 law map_drop: 923 for ~A: Type 924 for ~B: Type 925 for ~f: A -> B 926 for xs: List 927 for n: Nat 928 {List.map(~A, ~B, ~f, List.drop(&1, A, xs, n)) == List.drop(&1, B, List.map(~A, ~B, ~f, xs), n) : List} 929 930 def map_drop(A, B, f, xs, n): 931 match xs n: 932 case Nil{} _: 933 {==} 934 case h <> t 0n: 935 {==} 936 case h <> t 1n+p: 937 map_drop(~A, ~B, ~f, t, p) 938 939 # Taking m from n copies of x gives min(m, n) copies of x. 940 law take_replicate: 941 for -A: Data 942 for n: Nat 943 for m: Nat 944 for -x: A 945 {List.take(&2, A, List.replicate(A, n, x), m) == List.replicate(A, Nat.min(m, n), x) : List<&2, A>} 946 947 def take_replicate(A, n, m, x): 948 match n m: 949 case 0n _: 950 %MNat.min_zero_sym(m) : {Nil{} == List.replicate(A, _, x) : List<&2, A>} 951 {==} 952 case 1n+p 0n: 953 {==} 954 case 1n+p 1n+q: 955 %take_replicate(A, p, q, x) : {x <> List.take(&2, A, List.replicate(A, p, x), q) == x <> _ : List<&2, A>} 956 {==} 957 958 # Dropping m from n copies of x gives n - m copies of x. 959 law drop_replicate: 960 for -A: Data 961 for n: Nat 962 for m: Nat 963 for -x: A 964 {List.drop(&2, A, List.replicate(A, n, x), m) == List.replicate(A, Nat.sub(n, m), x) : List<&2, A>} 965 966 def drop_replicate(A, n, m, x): 967 match n m: 968 case 0n _: 969 {==} 970 case 1n+p 0n: 971 {==} 972 case 1n+p 1n+q: 973 drop_replicate(A, p, q, x) 974 975 # Taking n elements gives at most n of them. 976 law length_take_le: 977 for -a: Quant 978 for -A: Kind(a) 979 for xs: List 980 for n: Nat 981 MNat.le(List.length(a, A, List.take(a, A, xs, n)), n) 982 983 def length_take_le(a, A, xs, n): 984 match xs n: 985 case Nil{} _: 986 MNat.zero_le(n) 987 case h <> t 0n: 988 {==} 989 case h <> t 1n+p: 990 MNat.succ_le_succ(List.length(a, A, List.take(a, A, t, p)), p, length_take_le(a, A, t, p)) 991 992 # The tail is one shorter than the list, or empty: length (tail xs) = length xs - 1. 993 law length_tail: 994 for -a: Quant 995 for -A: Kind(a) 996 for xs: List 997 {List.length(a, A, List.tail(a, A, xs)) == Nat.sub(List.length(a, A, xs), 1n) : Nat} 998 999 def length_tail(a, A, xs): 1000 match xs: 1001 case Nil{}: 1002 {==} 1003 case h <> t: 1004 MNat.sub_zero_sym(List.length(a, A, t)) 1005 1006 # Mapping the identity gives the list back. 1007 law map_id: 1008 for ~A: Type 1009 for xs: List 1010 {List.map(~A, ~A, ~(x => x), xs) == xs : List} 1011 1012 def map_id(A, xs): 1013 match xs: 1014 case Nil{}: 1015 {==} 1016 case h <> t: 1017 %map_id(~A, t) : {h <> List.map(~A, ~A, ~(x => x), t) == h <> _ : List} 1018 {==} 1019 1020 # A right fold over a map folds with the mapped function: foldr g z (map f xs) = foldr (g . f) z xs. 1021 law foldr_map: 1022 for ~A: Type 1023 for ~B: Type 1024 for ~C: Type 1025 for ~f: A -> B 1026 for ~g: B -> C -> C 1027 for xs: List 1028 for -z: C 1029 {List.foldr(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, xs), z) == List.foldr(~&1, ~A, ~C, ~(x => y => g(f(x), y)), xs, z) : C} 1030 1031 def foldr_map(A, B, C, f, g, xs, z): 1032 match xs: 1033 case Nil{}: 1034 {==} 1035 case h <> t: 1036 %foldr_map(~A, ~B, ~C, ~f, ~g, t, z) : {g(f(h), List.foldr(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, t), z)) == g(f(h), _) : C} 1037 {==} 1038 1039 # A left fold over a map folds with the mapped function: foldl g z (map f xs) = foldl (fun acc x => g acc (f x)) z xs. 1040 law foldl_map: 1041 for ~A: Type 1042 for ~B: Type 1043 for ~C: Type 1044 for ~f: A -> B 1045 for ~g: C -> B -> C 1046 for xs: List 1047 for -z: C 1048 {List.foldl(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, xs), z) == List.foldl(~&1, ~A, ~C, ~(x => y => g(x, f(y))), xs, z) : C} 1049 1050 def foldl_map(A, B, C, f, g, xs, z): 1051 match xs: 1052 case Nil{}: 1053 {==} 1054 case h <> t: 1055 foldl_map(~A, ~B, ~C, ~f, ~g, t, g(z, f(h))) 1056 1057 # Replicating m + n times appends m copies to n copies. 1058 law replicate_add: 1059 for -A: Data 1060 for m: Nat 1061 for -n: Nat 1062 for -x: A 1063 {List.replicate(A, Nat.add(m, n), x) == List.append(&2, A, List.replicate(A, m, x), List.replicate(A, n, x)) : List<&2, A>} 1064 1065 def replicate_add(A, m, n, x): 1066 match m: 1067 case 0n: 1068 {==} 1069 case 1n+p: 1070 %replicate_add(A, p, n, x) : {x <> List.replicate(A, Nat.add(p, n), x) == x <> _ : List<&2, A>} 1071 {==} 1072 1073 def internal_replicate_append_nil(-A: Data, n: Nat, -x: A) -> {List.append(&2, A, List.replicate(A, n, x), Nil{}) == List.replicate(A, n, x) : List<&2, A>}: 1074 match n: 1075 case 0n: 1076 {==} 1077 case 1n+p: 1078 %internal_replicate_append_nil(A, p, x) : {x <> List.append(&2, A, List.replicate(A, p, x), Nil{}) == x <> _ : List<&2, A>} 1079 {==} 1080 1081 def internal_replicate_append_cons(-A: Data, n: Nat, -x: A, -acc: List<&2, A>) -> {List.append(&2, A, List.replicate(A, n, x), x <> acc) == x <> List.append(&2, A, List.replicate(A, n, x), acc) : List<&2, A>}: 1082 match n: 1083 case 0n: 1084 {==} 1085 case 1n+p: 1086 %internal_replicate_append_cons(A, p, x, acc) : {x <> List.append(&2, A, List.replicate(A, p, x), x <> acc) == x <> _ : List<&2, A>} 1087 {==} 1088 1089 def internal_reverse_go_replicate(-A: Data, n: Nat, -x: A, -acc: List<&2, A>) -> {List.reverse.go(&2, A, List.replicate(A, n, x), acc) == List.append(&2, A, List.replicate(A, n, x), acc) : List<&2, A>}: 1090 match n: 1091 case 0n: 1092 {==} 1093 case 1n+p: 1094 +p = p 1095 Equal.trans(List<&2, A>, List.reverse.go(&2, A, List.replicate(A, p, x), x <> acc), List.append(&2, A, List.replicate(A, p, x), x <> acc), x <> List.append(&2, A, List.replicate(A, p, x), acc), internal_reverse_go_replicate(A, p, x, x <> acc), internal_replicate_append_cons(A, p, x, acc)) 1096 1097 # Reversing n copies of x gives them back. 1098 law reverse_replicate: 1099 for -A: Data 1100 for n: Nat 1101 for -x: A 1102 {List.reverse(&2, A, List.replicate(A, n, x)) == List.replicate(A, n, x) : List<&2, A>} 1103 1104 def reverse_replicate(A, n, x): 1105 +n = n 1106 Equal.trans(List<&2, A>, List.reverse(&2, A, List.replicate(A, n, x)), List.append(&2, A, List.replicate(A, n, x), Nil{}), List.replicate(A, n, x), internal_reverse_go_replicate(A, n, x, Nil{}), internal_replicate_append_nil(A, n, x)) 1107 1108 # Filtering with an always-true predicate gives the list back. 1109 law filter_true: 1110 for ~A: Data 1111 for xs: List<&2, A> 1112 {List.filter(~A, ~(x => True{}), xs) == xs : List<&2, A>} 1113 1114 def filter_true(A, xs): 1115 match xs: 1116 case Nil{}: 1117 {==} 1118 case h <> t: 1119 %filter_true(~A, t) : {h <> List.filter(~A, ~(x => True{}), t) == h <> _ : List<&2, A>} 1120 {==} 1121 1122 # Filtering with an always-false predicate gives the empty list. 1123 law filter_false: 1124 for ~A: Data 1125 for xs: List<&2, A> 1126 {List.filter(~A, ~(x => False{}), xs) == Nil{} : List<&2, A>} 1127 1128 def filter_false(A, xs): 1129 match xs: 1130 case Nil{}: 1131 {==} 1132 case h <> t: 1133 filter_false(~A, t) 1134 1135 def internal_filter_put_filter(~A: Data, ~p: A -> Bool, +h: A, r: List<&2, A>, b: Bool) -> {List.filter(~A, ~p, List.filter.put(A, h, r, b)) == List.filter.put(A, h, List.filter(~A, ~p, r), Bool.and(p(h), b)) : List<&2, A>}: 1136 match b: 1137 case False{}: 1138 %MBool.and_false_sym(p(h)) : {List.filter(~A, ~p, r) == List.filter.put(A, h, List.filter(~A, ~p, r), _) : List<&2, A>} 1139 {==} 1140 case True{}: 1141 %MBool.and_true_sym(p(h)) : {List.filter(~A, ~p, h <> r) == List.filter.put(A, h, List.filter(~A, ~p, r), _) : List<&2, A>} 1142 {==} 1143 1144 # Filtering twice is filtering by both predicates: filter p (filter q xs) = filter (p and q) xs. 1145 law filter_filter: 1146 for ~A: Data 1147 for ~p: A -> Bool 1148 for ~q: A -> Bool 1149 for xs: List<&2, A> 1150 {List.filter(~A, ~p, List.filter(~A, ~q, xs)) == List.filter(~A, ~(+x => Bool.and(p(x), q(x))), xs) : List<&2, A>} 1151 1152 def filter_filter(A, p, q, xs): 1153 match xs: 1154 case Nil{}: 1155 {==} 1156 case +h <> t: 1157 +t = t 1158 %filter_filter(~A, ~p, ~q, t) : {List.filter(~A, ~p, List.filter.put(A, h, List.filter(~A, ~q, t), q(h))) == List.filter.put(A, h, _, Bool.and(p(h), q(h))) : List<&2, A>} 1159 internal_filter_put_filter(~A, ~p, h, List.filter(~A, ~q, t), q(h)) 1160 1161 def internal_all_filter_put(~A: Data, ~q: A -> Bool, -h: A, r: List<&2, A>, b: Bool) -> {List.all(~&2, ~A, ~q, List.filter.put(A, h, r, b)) == Bool.and(Bool.or(Bool.not(b), q(h)), List.all(~&2, ~A, ~q, r)) : Bool}: 1162 match b: 1163 case False{}: 1164 {==} 1165 case True{}: 1166 {==} 1167 1168 # All over a filter checks q only where p holds: all q (filter p xs) = all (not p or q) xs. 1169 law all_filter: 1170 for ~A: Data 1171 for ~p: A -> Bool 1172 for ~q: A -> Bool 1173 for xs: List<&2, A> 1174 {List.all(~&2, ~A, ~q, List.filter(~A, ~p, xs)) == List.all(~&2, ~A, ~(+x => Bool.or(Bool.not(p(x)), q(x))), xs) : Bool} 1175 1176 def all_filter(A, p, q, xs): 1177 match xs: 1178 case Nil{}: 1179 {==} 1180 case +h <> t: 1181 +t = t 1182 %all_filter(~A, ~p, ~q, t) : {List.all(~&2, ~A, ~q, List.filter.put(A, h, List.filter(~A, ~p, t), p(h))) == Bool.and(Bool.or(Bool.not(p(h)), q(h)), _) : Bool} 1183 internal_all_filter_put(~A, ~q, h, List.filter(~A, ~p, t), p(h)) 1184 1185 def internal_any_filter_put(~A: Data, ~q: A -> Bool, -h: A, r: List<&2, A>, b: Bool) -> {List.any(~&2, ~A, ~q, List.filter.put(A, h, r, b)) == Bool.or(Bool.and(b, q(h)), List.any(~&2, ~A, ~q, r)) : Bool}: 1186 match b: 1187 case False{}: 1188 {==} 1189 case True{}: 1190 {==} 1191 1192 # Any over a filter looks for q only where p holds: any q (filter p xs) = any (p and q) xs. 1193 law any_filter: 1194 for ~A: Data 1195 for ~p: A -> Bool 1196 for ~q: A -> Bool 1197 for xs: List<&2, A> 1198 {List.any(~&2, ~A, ~q, List.filter(~A, ~p, xs)) == List.any(~&2, ~A, ~(+x => Bool.and(p(x), q(x))), xs) : Bool} 1199 1200 def any_filter(A, p, q, xs): 1201 match xs: 1202 case Nil{}: 1203 {==} 1204 case +h <> t: 1205 +t = t 1206 %any_filter(~A, ~p, ~q, t) : {List.any(~&2, ~A, ~q, List.filter.put(A, h, List.filter(~A, ~p, t), p(h))) == Bool.or(Bool.and(p(h), q(h)), _) : Bool} 1207 internal_any_filter_put(~A, ~q, h, List.filter(~A, ~p, t), p(h)) 1208 1209 # All over a map checks the composed predicate: all p (map f xs) = all (p . f) xs. 1210 law all_map: 1211 for ~A: Type 1212 for ~B: Type 1213 for ~f: A -> B 1214 for ~p: B -> Bool 1215 for xs: List 1216 {List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) == List.all(~&1, ~A, ~(x => p(f(x))), xs) : Bool} 1217 1218 def all_map(A, B, f, p, xs): 1219 match xs: 1220 case Nil{}: 1221 {==} 1222 case h <> t: 1223 %all_map(~A, ~B, ~f, ~p, t) : {Bool.and(p(f(h)), List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, t))) == Bool.and(p(f(h)), _) : Bool} 1224 {==} 1225 1226 # Any over a map checks the composed predicate: any p (map f xs) = any (p . f) xs. 1227 law any_map: 1228 for ~A: Type 1229 for ~B: Type 1230 for ~f: A -> B 1231 for ~p: B -> Bool 1232 for xs: List 1233 {List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) == List.any(~&1, ~A, ~(x => p(f(x))), xs) : Bool} 1234 1235 def any_map(A, B, f, p, xs): 1236 match xs: 1237 case Nil{}: 1238 {==} 1239 case h <> t: 1240 %any_map(~A, ~B, ~f, ~p, t) : {Bool.or(p(f(h)), List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, t))) == Bool.or(p(f(h)), _) : Bool} 1241 {==} 1242 1243 def internal_all_reverse_go(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List, -acc: List, c: Bool, e: {List.all(~a, ~A, ~f, acc) == c : Bool}) -> {List.all(~a, ~A, ~f, List.reverse.go(a, A, xs, acc)) == Bool.and(c, List.all(~a, ~A, ~f, xs)) : Bool}: 1244 match xs c: 1245 case Nil{} True{}: 1246 e 1247 case Nil{} False{}: 1248 e 1249 case h <> t True{}: 1250 +v = f(h) 1251 internal_all_reverse_go(~a, ~A, ~f, t, h <> acc, v, Equal.trans(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), Bool.and(v, True{}), v, Equal.cong(Bool, Bool, k => Bool.and(v, k), List.all(~a, ~A, ~f, acc), True{}, e), MBool.and_true(v))) 1252 case h <> t False{}: 1253 internal_all_reverse_go(~a, ~A, ~f, t, h <> acc, False{}, Equal.trans(Bool, Bool.and(f(h), List.all(~a, ~A, ~f, acc)), Bool.and(f(h), False{}), False{}, Equal.cong(Bool, Bool, k => Bool.and(f(h), k), List.all(~a, ~A, ~f, acc), False{}, e), MBool.and_false(f(h)))) 1254 1255 # Reversing does not change whether all elements satisfy a predicate. 1256 law all_reverse: 1257 for ~a: Quant 1258 for ~A: Kind(a) 1259 for ~f: A -> Bool 1260 for xs: List 1261 {List.all(~a, ~A, ~f, List.reverse(a, A, xs)) == List.all(~a, ~A, ~f, xs) : Bool} 1262 1263 def all_reverse(a, A, f, xs): 1264 internal_all_reverse_go(~a, ~A, ~f, xs, Nil{}, True{}, {==}) 1265 1266 def internal_any_reverse_go(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List, -acc: List, c: Bool, e: {List.any(~a, ~A, ~f, acc) == c : Bool}) -> {List.any(~a, ~A, ~f, List.reverse.go(a, A, xs, acc)) == Bool.or(c, List.any(~a, ~A, ~f, xs)) : Bool}: 1267 match xs c: 1268 case Nil{} True{}: 1269 e 1270 case Nil{} False{}: 1271 e 1272 case h <> t True{}: 1273 internal_any_reverse_go(~a, ~A, ~f, t, h <> acc, True{}, Equal.trans(Bool, Bool.or(f(h), List.any(~a, ~A, ~f, acc)), Bool.or(f(h), True{}), True{}, Equal.cong(Bool, Bool, k => Bool.or(f(h), k), List.any(~a, ~A, ~f, acc), True{}, e), MBool.or_true(f(h)))) 1274 case h <> t False{}: 1275 +v = f(h) 1276 internal_any_reverse_go(~a, ~A, ~f, t, h <> acc, v, Equal.trans(Bool, Bool.or(v, List.any(~a, ~A, ~f, acc)), Bool.or(v, False{}), v, Equal.cong(Bool, Bool, k => Bool.or(v, k), List.any(~a, ~A, ~f, acc), False{}, e), MBool.or_false(v))) 1277 1278 # Reversing does not change whether some element satisfies a predicate. 1279 law any_reverse: 1280 for ~a: Quant 1281 for ~A: Kind(a) 1282 for ~f: A -> Bool 1283 for xs: List 1284 {List.any(~a, ~A, ~f, List.reverse(a, A, xs)) == List.any(~a, ~A, ~f, xs) : Bool} 1285 1286 def any_reverse(a, A, f, xs): 1287 internal_any_reverse_go(~a, ~A, ~f, xs, Nil{}, False{}, {==}) 1288 1289 def internal_contains_reverse_go(~A: Data, ~eq: A -> A -> Bool, xs: List<&2, A>, -acc: List<&2, A>, +x: A, c: Bool, e: {List.contains(~A, ~eq, acc, x) == c : Bool}) -> {List.contains(~A, ~eq, List.reverse.go(&2, A, xs, acc), x) == Bool.or(c, List.contains(~A, ~eq, xs, x)) : Bool}: 1290 match xs c: 1291 case Nil{} True{}: 1292 e 1293 case Nil{} False{}: 1294 e 1295 case h <> t True{}: 1296 internal_contains_reverse_go(~A, ~eq, t, h <> acc, x, True{}, Equal.trans(Bool, Bool.or(eq(h, x), List.contains(~A, ~eq, acc, x)), Bool.or(eq(h, x), True{}), True{}, Equal.cong(Bool, Bool, k => Bool.or(eq(h, x), k), List.contains(~A, ~eq, acc, x), True{}, e), MBool.or_true(eq(h, x)))) 1297 case h <> t False{}: 1298 +v = eq(h, x) 1299 internal_contains_reverse_go(~A, ~eq, t, h <> acc, x, v, Equal.trans(Bool, Bool.or(v, List.contains(~A, ~eq, acc, x)), Bool.or(v, False{}), v, Equal.cong(Bool, Bool, k => Bool.or(v, k), List.contains(~A, ~eq, acc, x), False{}, e), MBool.or_false(v))) 1300 1301 # Reversing does not change whether a list contains x. 1302 law contains_reverse: 1303 for ~A: Data 1304 for ~eq: A -> A -> Bool 1305 for xs: List<&2, A> 1306 for +x: A 1307 {List.contains(~A, ~eq, List.reverse(&2, A, xs), x) == List.contains(~A, ~eq, xs, x) : Bool} 1308 1309 def contains_reverse(A, eq, xs, x): 1310 internal_contains_reverse_go(~A, ~eq, xs, Nil{}, x, False{}, {==}) 1311 1312 # Zipping the empty list with anything gives the empty list. 1313 law zip_nil_left: 1314 for -a: Quant 1315 for -A: Kind(a) 1316 for -b: Quant 1317 for -B: Kind(b) 1318 for -ys: List 1319 {List.zip(a, A, b, B, Nil{}, ys) == Nil{} : List<&1, A & B>} 1320 1321 def zip_nil_left(a, A, b, B, ys): 1322 {==} 1323 1324 # Zipping anything with the empty list gives the empty list. 1325 law zip_nil_right: 1326 for -a: Quant 1327 for -A: Kind(a) 1328 for -b: Quant 1329 for -B: Kind(b) 1330 for xs: List 1331 {List.zip(a, A, b, B, xs, Nil{}) == Nil{} : List<&1, A & B>} 1332 1333 def zip_nil_right(a, A, b, B, xs): 1334 match xs: 1335 case Nil{}: 1336 {==} 1337 case h <> t: 1338 {==} 1339 1340 # The head of a cons is its first element. 1341 law head_cons: 1342 for -a: Quant 1343 for -A: Kind(a) 1344 for -x: A 1345 for -xs: List 1346 {List.head(a, A, x <> xs) == Some{x} : Maybe} 1347 1348 def head_cons(a, A, x, xs): 1349 {==} 1350 1351 # The head of an append is the head of the first part, or else of the second. 1352 law head_append: 1353 for -a: Quant 1354 for -A: Kind(a) 1355 for xs: List 1356 for -ys: List 1357 {List.head(a, A, List.append(a, A, xs, ys)) == Maybe.or(a, A, List.head(a, A, xs), List.head(a, A, ys)) : Maybe} 1358 1359 def head_append(a, A, xs, ys): 1360 match xs: 1361 case Nil{}: 1362 {==} 1363 case h <> t: 1364 {==} 1365 1366 # The head of a map is the mapped head. 1367 law head_map: 1368 for ~A: Type 1369 for ~B: Type 1370 for ~f: A -> B 1371 for xs: List 1372 {List.head(&1, B, List.map(~A, ~B, ~f, xs)) == Maybe.map(&1, A, B, f, List.head(&1, A, xs)) : Maybe<&1, B>} 1373 1374 def head_map(A, B, f, xs): 1375 match xs: 1376 case Nil{}: 1377 {==} 1378 case h <> t: 1379 {==} 1380 1381 # The tail of a map is the map of the tail. 1382 law tail_map: 1383 for ~A: Type 1384 for ~B: Type 1385 for ~f: A -> B 1386 for xs: List 1387 {List.tail(&1, B, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~B, ~f, List.tail(&1, A, xs)) : List} 1388 1389 def tail_map(A, B, f, xs): 1390 match xs: 1391 case Nil{}: 1392 {==} 1393 case h <> t: 1394 {==} 1395 1396 # The element at index zero of a cons is its head. 1397 law get_cons_zero: 1398 for -a: Quant 1399 for -A: Kind(a) 1400 for -x: A 1401 for -xs: List 1402 {List.get(a, A, x <> xs, 0n) == Some{x} : Maybe} 1403 1404 def get_cons_zero(a, A, x, xs): 1405 {==} 1406 1407 # The element at index n + 1 of a cons is the element at index n of its tail. 1408 law get_cons_succ: 1409 for -a: Quant 1410 for -A: Kind(a) 1411 for -x: A 1412 for -xs: List 1413 for -n: Nat 1414 {List.get(a, A, x <> xs, 1n+n) == List.get(a, A, xs, n) : Maybe} 1415 1416 def get_cons_succ(a, A, x, xs, n): 1417 {==} 1418 1419 # Indexing a map is mapping the indexed element. 1420 law get_map: 1421 for ~A: Type 1422 for ~B: Type 1423 for ~f: A -> B 1424 for xs: List 1425 for n: Nat 1426 {List.get(&1, B, List.map(~A, ~B, ~f, xs), n) == Maybe.map(&1, A, B, f, List.get(&1, A, xs, n)) : Maybe<&1, B>} 1427 1428 def get_map(A, B, f, xs, n): 1429 match xs n: 1430 case Nil{} _: 1431 {==} 1432 case h <> t 0n: 1433 {==} 1434 case h <> t 1n+p: 1435 get_map(~A, ~B, ~f, t, p) 1436 1437 # Setting an element does not change the length. 1438 law length_set: 1439 for -a: Quant 1440 for -A: Kind(a) 1441 for xs: List 1442 for n: Nat 1443 for -x: A 1444 {List.length(a, A, List.set(a, A, xs, n, x)) == List.length(a, A, xs) : Nat} 1445 1446 def length_set(a, A, xs, n, x): 1447 match xs n: 1448 case Nil{} _: 1449 {==} 1450 case h <> t 0n: 1451 {==} 1452 case h <> t 1n+p: 1453 %length_set(a, A, t, p, x) : {1n+List.length(a, A, List.set(a, A, t, p, x)) == 1n+_ : Nat} 1454 {==} 1455 1456 # Reading the index just set gives the new value wherever the index is in range. 1457 law get_set_self: 1458 for -a: Quant 1459 for -A: Kind(a) 1460 for xs: List 1461 for n: Nat 1462 for -x: A 1463 {List.get(a, A, List.set(a, A, xs, n, x), n) == Maybe.map(a, A, A, y => x, List.get(a, A, xs, n)) : Maybe} 1464 1465 def get_set_self(a, A, xs, n, x): 1466 match xs n: 1467 case Nil{} _: 1468 {==} 1469 case h <> t 0n: 1470 {==} 1471 case h <> t 1n+p: 1472 get_set_self(a, A, t, p, x) 1473 1474 def internal_last_go_append_singleton(a, -A: Kind(a), ys: List, -h: A, -x: A) -> {List.last.go(a, A, List.append(a, A, ys, [x]), h) == x : A}: 1475 match ys: 1476 case Nil{}: 1477 {==} 1478 case y <> t: 1479 internal_last_go_append_singleton(a, A, t, y, x) 1480 1481 # The last element of xs ++ [x] is x. 1482 law last_append_singleton: 1483 for -a: Quant 1484 for -A: Kind(a) 1485 for xs: List 1486 for -x: A 1487 {List.last(a, A, List.append(a, A, xs, [x])) == Some{x} : Maybe} 1488 1489 def last_append_singleton(a, A, xs, x): 1490 match xs: 1491 case Nil{}: 1492 {==} 1493 case h <> t: 1494 %internal_last_go_append_singleton(a, A, t, h, x) : {Some{List.last.go(a, A, List.append(a, A, t, [x]), h)} == Some{_} : Maybe} 1495 {==} 1496 1497 def internal_head_reverse_go(a, -A: Kind(a), xs: List, -h: A, -acc: List) -> {List.head(a, A, List.reverse.go(a, A, xs, h <> acc)) == Some{List.last.go(a, A, xs, h)} : Maybe}: 1498 match xs: 1499 case Nil{}: 1500 {==} 1501 case y <> t: 1502 internal_head_reverse_go(a, A, t, y, h <> acc) 1503 1504 # The head of the reverse is the last element. 1505 law head_reverse: 1506 for -a: Quant 1507 for -A: Kind(a) 1508 for xs: List 1509 {List.head(a, A, List.reverse(a, A, xs)) == List.last(a, A, xs) : Maybe} 1510 1511 def head_reverse(a, A, xs): 1512 match xs: 1513 case Nil{}: 1514 {==} 1515 case h <> t: 1516 internal_head_reverse_go(a, A, t, h, Nil{}) 1517 1518 def internal_last_reverse_go(a, -A: Kind(a), xs: List, -h: A, -acc: List) -> {List.last(a, A, List.reverse.go(a, A, xs, h <> acc)) == Some{List.last.go(a, A, acc, h)} : Maybe}: 1519 match xs: 1520 case Nil{}: 1521 {==} 1522 case y <> t: 1523 internal_last_reverse_go(a, A, t, y, h <> acc) 1524 1525 # The last element of the reverse is the head. 1526 law last_reverse: 1527 for -a: Quant 1528 for -A: Kind(a) 1529 for xs: List 1530 {List.last(a, A, List.reverse(a, A, xs)) == List.head(a, A, xs) : Maybe} 1531 1532 def last_reverse(a, A, xs): 1533 match xs: 1534 case Nil{}: 1535 {==} 1536 case h <> t: 1537 internal_last_reverse_go(a, A, t, h, Nil{}) 1538 1539 # A list is empty exactly when its length is zero. 1540 law is_empty_iff_length_eq_zero: 1541 for -a: Quant 1542 for -A: Kind(a) 1543 for xs: List 1544 {List.is_empty(a, A, xs) == Nat.is_eq(List.length(a, A, xs), 0n) : Bool} 1545 1546 def is_empty_iff_length_eq_zero(a, A, xs): 1547 match xs: 1548 case Nil{}: 1549 {==} 1550 case h <> t: 1551 {==} 1552 1553 # An append is empty exactly when both parts are. 1554 law is_empty_append: 1555 for -a: Quant 1556 for -A: Kind(a) 1557 for xs: List 1558 for -ys: List 1559 {List.is_empty(a, A, List.append(a, A, xs, ys)) == Bool.and(List.is_empty(a, A, xs), List.is_empty(a, A, ys)) : Bool} 1560 1561 def is_empty_append(a, A, xs, ys): 1562 match xs: 1563 case Nil{}: 1564 {==} 1565 case h <> t: 1566 {==} 1567 1568 def internal_is_empty_reverse_go(a, -A: Kind(a), xs: List, -h: A, -acc: List) -> {List.is_empty(a, A, List.reverse.go(a, A, xs, h <> acc)) == False{} : Bool}: 1569 match xs: 1570 case Nil{}: 1571 {==} 1572 case y <> t: 1573 internal_is_empty_reverse_go(a, A, t, y, h <> acc) 1574 1575 # The reverse is empty exactly when the list is. 1576 law is_empty_reverse: 1577 for -a: Quant 1578 for -A: Kind(a) 1579 for xs: List 1580 {List.is_empty(a, A, List.reverse(a, A, xs)) == List.is_empty(a, A, xs) : Bool} 1581 1582 def is_empty_reverse(a, A, xs): 1583 match xs: 1584 case Nil{}: 1585 {==} 1586 case h <> t: 1587 internal_is_empty_reverse_go(a, A, t, h, Nil{}) 1588 1589 # A map is empty exactly when the list is. 1590 law is_empty_map: 1591 for ~A: Type 1592 for ~B: Type 1593 for ~f: A -> B 1594 for xs: List 1595 {List.is_empty(&1, B, List.map(~A, ~B, ~f, xs)) == List.is_empty(&1, A, xs) : Bool} 1596 1597 def is_empty_map(A, B, f, xs): 1598 match xs: 1599 case Nil{}: 1600 {==} 1601 case h <> t: 1602 {==} 1603 1604 def internal_reverse_filter_put(-A: Data, -h: A, r: List<&2, A>, b: Bool) -> {List.append(&2, A, List.reverse(&2, A, r), List.filter.put(A, h, Nil{}, b)) == List.reverse(&2, A, List.filter.put(A, h, r, b)) : List<&2, A>}: 1605 match b: 1606 case False{}: 1607 append_nil(&2, A, List.reverse(&2, A, r)) 1608 case True{}: 1609 Equal.sym(List<&2, A>, List.reverse.go(&2, A, r, [h]), List.append(&2, A, List.reverse(&2, A, r), [h]), reverse_go_spec(&2, A, r, [h])) 1610 1611 # Filtering commutes with reversing: filter p (reverse xs) = reverse (filter p xs). 1612 law filter_reverse: 1613 for ~A: Data 1614 for ~f: A -> Bool 1615 for xs: List<&2, A> 1616 {List.filter(~A, ~f, List.reverse(&2, A, xs)) == List.reverse(&2, A, List.filter(~A, ~f, xs)) : List<&2, A>} 1617 1618 def filter_reverse(A, f, xs): 1619 match xs: 1620 case Nil{}: 1621 {==} 1622 case +h <> t: 1623 +t = t 1624 %Equal.sym(List<&2, A>, List.reverse.go(&2, A, t, [h]), List.append(&2, A, List.reverse(&2, A, t), [h]), reverse_go_spec(&2, A, t, [h])) : {List.filter(~A, ~f, _) == List.reverse(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))) : List<&2, A>} 1625 %Equal.sym(List<&2, A>, List.filter(~A, ~f, List.append(&2, A, List.reverse(&2, A, t), [h])), List.append(&2, A, List.filter(~A, ~f, List.reverse(&2, A, t)), List.filter(~A, ~f, [h])), filter_append(~A, ~f, List.reverse(&2, A, t), [h])) : {_ == List.reverse(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))) : List<&2, A>} 1626 %Equal.sym(List<&2, A>, List.filter(~A, ~f, List.reverse(&2, A, t)), List.reverse(&2, A, List.filter(~A, ~f, t)), filter_reverse(~A, ~f, t)) : {List.append(&2, A, _, List.filter(~A, ~f, [h])) == List.reverse(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))) : List<&2, A>} 1627 internal_reverse_filter_put(A, h, List.filter(~A, ~f, t), f(h)) 1628 1629 # Folding cons from the right, starting from the empty list, rebuilds the list. 1630 law foldr_cons_nil: 1631 for ~a: Quant 1632 for ~A: Kind(a) 1633 for xs: List 1634 {List.foldr(~a, ~A, ~List, ~(x => acc => x <> acc), xs, Nil{}) == xs : List} 1635 1636 def foldr_cons_nil(a, A, xs): 1637 match xs: 1638 case Nil{}: 1639 {==} 1640 case h <> t: 1641 %foldr_cons_nil(~a, ~A, t) : {h <> List.foldr(~a, ~A, ~List, ~(x => acc => x <> acc), t, Nil{}) == h <> _ : List} 1642 {==} 1643 1644 def internal_foldl_reverse_go(~a: Quant, ~A: Kind(a), ~B: Type, ~f: B -> A -> B, xs: List, -acc: List, -z: B) -> {List.foldl(~a, ~A, ~B, ~f, List.reverse.go(a, A, xs, acc), z) == List.foldl(~a, ~A, ~B, ~f, acc, List.foldr(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z)) : B}: 1645 match xs: 1646 case Nil{}: 1647 {==} 1648 case h <> t: 1649 internal_foldl_reverse_go(~a, ~A, ~B, ~f, t, h <> acc, z) 1650 1651 # A left fold over the reverse is a right fold with the arguments flipped. 1652 law foldl_reverse: 1653 for ~a: Quant 1654 for ~A: Kind(a) 1655 for ~B: Type 1656 for ~f: B -> A -> B 1657 for xs: List 1658 for -z: B 1659 {List.foldl(~a, ~A, ~B, ~f, List.reverse(a, A, xs), z) == List.foldr(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z) : B} 1660 1661 def foldl_reverse(a, A, B, f, xs, z): 1662 internal_foldl_reverse_go(~a, ~A, ~B, ~f, xs, Nil{}, z) 1663 1664 def internal_foldr_reverse_go(~a: Quant, ~A: Kind(a), ~B: Type, ~f: A -> B -> B, xs: List, -acc: List, -z: B) -> {List.foldr(~a, ~A, ~B, ~f, List.reverse.go(a, A, xs, acc), z) == List.foldl(~a, ~A, ~B, ~(x => y => f(y, x)), xs, List.foldr(~a, ~A, ~B, ~f, acc, z)) : B}: 1665 match xs: 1666 case Nil{}: 1667 {==} 1668 case h <> t: 1669 internal_foldr_reverse_go(~a, ~A, ~B, ~f, t, h <> acc, z) 1670 1671 # A right fold over the reverse is a left fold with the arguments flipped. 1672 law foldr_reverse: 1673 for ~a: Quant 1674 for ~A: Kind(a) 1675 for ~B: Type 1676 for ~f: A -> B -> B 1677 for xs: List 1678 for -z: B 1679 {List.foldr(~a, ~A, ~B, ~f, List.reverse(a, A, xs), z) == List.foldl(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z) : B} 1680 1681 def foldr_reverse(a, A, B, f, xs, z): 1682 internal_foldr_reverse_go(~a, ~A, ~B, ~f, xs, Nil{}, z) 1683 1684 def internal_range_go_append(+n: Nat, -ys: List<&2, Nat>, -acc: List<&2, Nat>) -> {List.range.go(n, List.append(&2, Nat, ys, acc)) == List.append(&2, Nat, List.range.go(n, ys), acc) : List<&2, Nat>}: 1685 match n: 1686 case 0n: 1687 {==} 1688 case 1n+p: 1689 internal_range_go_append(p, p <> ys, acc) 1690 1691 # Range(n + 1) is range(n) followed by n. 1692 law range_succ: 1693 for n: Nat 1694 {List.range(1n+n) == List.append(&2, Nat, List.range(n), [n]) : List<&2, Nat>} 1695 1696 def range_succ(n): 1697 +n = n 1698 internal_range_go_append(n, Nil{}, [n]) 1699 1700 def internal_find_put_or(-A: Data, h: A, r: Maybe<&2, A>, -s: Maybe<&2, A>, b: Bool) -> {Maybe.or(&2, A, List.find.put(A, h, r, b), s) == List.find.put(A, h, Maybe.or(&2, A, r, s), b) : Maybe<&2, A>}: 1701 match b: 1702 case False{}: 1703 {==} 1704 case True{}: 1705 {==} 1706 1707 # Finding in an append finds in the first part, or else in the second. 1708 law find_append: 1709 for ~A: Data 1710 for ~f: A -> Bool 1711 for xs: List<&2, A> 1712 for ys: List<&2, A> 1713 {List.find(~A, ~f, List.append(&2, A, xs, ys)) == Maybe.or(&2, A, List.find(~A, ~f, xs), List.find(~A, ~f, ys)) : Maybe<&2, A>} 1714 1715 def find_append(A, f, xs, ys): 1716 match xs: 1717 case Nil{}: 1718 {==} 1719 case +h <> t: 1720 +ys = ys 1721 +t = t 1722 %Equal.sym(Maybe<&2, A>, List.find(~A, ~f, List.append(&2, A, t, ys)), Maybe.or(&2, A, List.find(~A, ~f, t), List.find(~A, ~f, ys)), find_append(~A, ~f, t, ys)) : {List.find.put(A, h, _, f(h)) == Maybe.or(&2, A, List.find.put(A, h, List.find(~A, ~f, t), f(h)), List.find(~A, ~f, ys)) : Maybe<&2, A>} 1723 Equal.sym(Maybe<&2, A>, Maybe.or(&2, A, List.find.put(A, h, List.find(~A, ~f, t), f(h)), List.find(~A, ~f, ys)), List.find.put(A, h, Maybe.or(&2, A, List.find(~A, ~f, t), List.find(~A, ~f, ys)), f(h)), internal_find_put_or(A, h, List.find(~A, ~f, t), List.find(~A, ~f, ys), f(h))) 1724 1725 def internal_and_not_eq_not_or_not(b: Bool, -s: Bool) -> {Bool.and(b, Bool.not(s)) == Bool.not(Bool.or(Bool.not(b), s)) : Bool}: 1726 match b: 1727 case False{}: 1728 {==} 1729 case True{}: 1730 {==} 1731 1732 # All elements satisfy f exactly when no element fails it. 1733 law all_eq_not_any_not: 1734 for ~a: Quant 1735 for ~A: Kind(a) 1736 for ~f: A -> Bool 1737 for xs: List 1738 {List.all(~a, ~A, ~f, xs) == Bool.not(List.any(~a, ~A, ~(x => Bool.not(f(x))), xs)) : Bool} 1739 1740 def all_eq_not_any_not(a, A, f, xs): 1741 match xs: 1742 case Nil{}: 1743 {==} 1744 case h <> t: 1745 %Equal.sym(Bool, List.all(~a, ~A, ~f, t), Bool.not(List.any(~a, ~A, ~(x => Bool.not(f(x))), t)), all_eq_not_any_not(~a, ~A, ~f, t)) : {Bool.and(f(h), _) == Bool.not(Bool.or(Bool.not(f(h)), List.any(~a, ~A, ~(x => Bool.not(f(x))), t))) : Bool} 1746 internal_and_not_eq_not_or_not(f(h), List.any(~a, ~A, ~(x => Bool.not(f(x))), t)) 1747 1748 def internal_or_not_eq_not_and_not(b: Bool, -s: Bool) -> {Bool.or(b, Bool.not(s)) == Bool.not(Bool.and(Bool.not(b), s)) : Bool}: 1749 match b: 1750 case False{}: 1751 {==} 1752 case True{}: 1753 {==} 1754 1755 # Some element satisfies f exactly when not all elements fail it. 1756 law any_eq_not_all_not: 1757 for ~a: Quant 1758 for ~A: Kind(a) 1759 for ~f: A -> Bool 1760 for xs: List 1761 {List.any(~a, ~A, ~f, xs) == Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), xs)) : Bool} 1762 1763 def any_eq_not_all_not(a, A, f, xs): 1764 match xs: 1765 case Nil{}: 1766 {==} 1767 case h <> t: 1768 %Equal.sym(Bool, List.any(~a, ~A, ~f, t), Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), t)), any_eq_not_all_not(~a, ~A, ~f, t)) : {Bool.or(f(h), _) == Bool.not(Bool.and(Bool.not(f(h)), List.all(~a, ~A, ~(x => Bool.not(f(x))), t))) : Bool} 1769 internal_or_not_eq_not_and_not(f(h), List.all(~a, ~A, ~(x => Bool.not(f(x))), t)) 1770 1771 # A one-element list has length one. 1772 law length_singleton: 1773 for -a: Quant 1774 for -A: Kind(a) 1775 for -x: A 1776 {List.length(a, A, [x]) == 1n : Nat} 1777 1778 def length_singleton(a, A, x): 1779 {==} 1780 1781 # Reversing a cons puts its head last: reverse (x :: xs) = reverse xs ++ [x]. 1782 law reverse_cons: 1783 for -a: Quant 1784 for -A: Kind(a) 1785 for -x: A 1786 for xs: List 1787 {List.reverse(a, A, x <> xs) == List.append(a, A, List.reverse(a, A, xs), [x]) : List} 1788 1789 def reverse_cons(a, A, x, xs): 1790 reverse_go_spec(a, A, xs, [x]) 1791 1792 # Taking n + 1 elements of a cons keeps its head and takes n from its tail. 1793 law take_succ: 1794 for -a: Quant 1795 for -A: Kind(a) 1796 for -x: A 1797 for -xs: List 1798 for -n: Nat 1799 {List.take(a, A, x <> xs, 1n+n) == x <> List.take(a, A, xs, n) : List} 1800 1801 def take_succ(a, A, x, xs, n): 1802 {==} 1803 1804 # Dropping n + 1 elements of a cons drops its head and n from its tail. 1805 law drop_succ: 1806 for -a: Quant 1807 for -A: Kind(a) 1808 for -x: A 1809 for -xs: List 1810 for -n: Nat 1811 {List.drop(a, A, x <> xs, 1n+n) == List.drop(a, A, xs, n) : List} 1812 1813 def drop_succ(a, A, x, xs, n): 1814 {==} 1815 1816 # --- generated: _sym twins (tools/mathlib/twins.ts), do not edit --- 1817 1818 # The empty list is a right identity for append: xs ++ [] = xs, reversed to rewrite toward the simple side. 1819 law append_nil_sym: 1820 for -a: Quant 1821 for -A: Kind(a) 1822 for xs: List 1823 {xs == List.append(a, A, xs, Nil{}) : List} 1824 1825 def append_nil_sym(a, A, xs): 1826 Equal.sym(List, List.append(a, A, xs, Nil{}), xs, append_nil(a, A, xs)) 1827 1828 # The empty list is a left identity for append: [] ++ xs = xs, reversed to rewrite toward the simple side. 1829 law nil_append_sym: 1830 for -a: Quant 1831 for -A: Kind(a) 1832 for -xs: List 1833 {xs == List.append(a, A, Nil{}, xs) : List} 1834 1835 def nil_append_sym(a, A, xs): 1836 Equal.sym(List, List.append(a, A, Nil{}, xs), xs, nil_append(a, A, xs)) 1837 1838 # Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs), reversed to rewrite toward the simple side. 1839 law append_assoc_sym: 1840 for -a: Quant 1841 for -A: Kind(a) 1842 for xs: List 1843 for -ys: List 1844 for -zs: List 1845 {List.append(a, A, xs, List.append(a, A, ys, zs)) == List.append(a, A, List.append(a, A, xs, ys), zs) : List} 1846 1847 def append_assoc_sym(a, A, xs, ys, zs): 1848 Equal.sym(List, List.append(a, A, List.append(a, A, xs, ys), zs), List.append(a, A, xs, List.append(a, A, ys, zs)), append_assoc(a, A, xs, ys, zs)) 1849 1850 # The length of an append is the sum of the lengths, reversed to rewrite toward the simple side. 1851 law length_append_sym: 1852 for -a: Quant 1853 for -A: Kind(a) 1854 for xs: List 1855 for -ys: List 1856 {Nat.add(List.length(a, A, xs), List.length(a, A, ys)) == List.length(a, A, List.append(a, A, xs, ys)) : Nat} 1857 1858 def length_append_sym(a, A, xs, ys): 1859 Equal.sym(Nat, List.length(a, A, List.append(a, A, xs, ys)), Nat.add(List.length(a, A, xs), List.length(a, A, ys)), length_append(a, A, xs, ys)) 1860 1861 # The reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side. 1862 law reverse_go_spec_sym: 1863 for -a: Quant 1864 for -A: Kind(a) 1865 for xs: List 1866 for -acc: List 1867 {List.append(a, A, List.reverse(a, A, xs), acc) == List.reverse.go(a, A, xs, acc) : List} 1868 1869 def reverse_go_spec_sym(a, A, xs, acc): 1870 Equal.sym(List, List.reverse.go(a, A, xs, acc), List.append(a, A, List.reverse(a, A, xs), acc), reverse_go_spec(a, A, xs, acc)) 1871 1872 # Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side. 1873 law reverse_append_sym: 1874 for -a: Quant 1875 for -A: Kind(a) 1876 for xs: List 1877 for ys: List 1878 {List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) == List.reverse(a, A, List.append(a, A, xs, ys)) : List} 1879 1880 def reverse_append_sym(a, A, xs, ys): 1881 Equal.sym(List, List.reverse(a, A, List.append(a, A, xs, ys)), List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)), reverse_append(a, A, xs, ys)) 1882 1883 # Reversing twice gives the list back, reversed to rewrite toward the simple side. 1884 law reverse_reverse_sym: 1885 for -a: Quant 1886 for -A: Kind(a) 1887 for xs: List 1888 {xs == List.reverse(a, A, List.reverse(a, A, xs)) : List} 1889 1890 def reverse_reverse_sym(a, A, xs): 1891 Equal.sym(List, List.reverse(a, A, List.reverse(a, A, xs)), xs, reverse_reverse(a, A, xs)) 1892 1893 # Reversing preserves the length, reversed to rewrite toward the simple side. 1894 law length_reverse_sym: 1895 for -a: Quant 1896 for -A: Kind(a) 1897 for xs: List 1898 {List.length(a, A, xs) == List.length(a, A, List.reverse(a, A, xs)) : Nat} 1899 1900 def length_reverse_sym(a, A, xs): 1901 Equal.sym(Nat, List.length(a, A, List.reverse(a, A, xs)), List.length(a, A, xs), length_reverse(a, A, xs)) 1902 1903 # A right fold over an append folds the first part onto the fold of the second, reversed to rewrite toward the simple side. 1904 law foldr_append_sym: 1905 for ~a: Quant 1906 for ~A: Kind(a) 1907 for ~B: Type 1908 for ~f: A -> B -> B 1909 for xs: List 1910 for -ys: List 1911 for -z: B 1912 {List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)) == List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) : B} 1913 1914 def foldr_append_sym(a, A, B, f, xs, ys, z): 1915 Equal.sym(B, List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z), List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)), foldr_append(~a, ~A, ~B, ~f, xs, ys, z)) 1916 1917 # Taking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side. 1918 law take_append_drop_sym: 1919 for -a: Quant 1920 for -A: Kind(a) 1921 for xs: List 1922 for n: Nat 1923 {xs == List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) : List} 1924 1925 def take_append_drop_sym(a, A, xs, n): 1926 Equal.sym(List, List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)), xs, take_append_drop(a, A, xs, n)) 1927 1928 # Mapping preserves the length, reversed to rewrite toward the simple side. 1929 law length_map_sym: 1930 for ~A: Type 1931 for ~B: Type 1932 for ~f: A -> B 1933 for xs: List 1934 {List.length(&1, A, xs) == List.length(&1, B, List.map(~A, ~B, ~f, xs)) : Nat} 1935 1936 def length_map_sym(A, B, f, xs): 1937 Equal.sym(Nat, List.length(&1, B, List.map(~A, ~B, ~f, xs)), List.length(&1, A, xs), length_map(~A, ~B, ~f, xs)) 1938 1939 # Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side. 1940 law map_append_sym: 1941 for ~A: Type 1942 for ~B: Type 1943 for ~f: A -> B 1944 for xs: List 1945 for -ys: List 1946 {List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)) == List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)) : List} 1947 1948 def map_append_sym(A, B, f, xs, ys): 1949 Equal.sym(List, List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)), List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)), map_append(~A, ~B, ~f, xs, ys)) 1950 1951 # Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs, reversed to rewrite toward the simple side. 1952 law map_map_sym: 1953 for ~A: Type 1954 for ~B: Type 1955 for ~C: Type 1956 for ~f: A -> B 1957 for ~g: B -> C 1958 for xs: List 1959 {List.map(~A, ~C, ~(x => g(f(x))), xs) == List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) : List} 1960 1961 def map_map_sym(A, B, C, f, g, xs): 1962 Equal.sym(List, List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)), List.map(~A, ~C, ~(x => g(f(x))), xs), map_map(~A, ~B, ~C, ~f, ~g, xs)) 1963 1964 # Taking zero elements gives the empty list, reversed to rewrite toward the simple side. 1965 law take_zero_sym: 1966 for -a: Quant 1967 for -A: Kind(a) 1968 for xs: List 1969 {Nil{} == List.take(a, A, xs, 0n) : List} 1970 1971 def take_zero_sym(a, A, xs): 1972 Equal.sym(List, List.take(a, A, xs, 0n), Nil{}, take_zero(a, A, xs)) 1973 1974 # Dropping zero elements gives the list back, reversed to rewrite toward the simple side. 1975 law drop_zero_sym: 1976 for -a: Quant 1977 for -A: Kind(a) 1978 for xs: List 1979 {xs == List.drop(a, A, xs, 0n) : List} 1980 1981 def drop_zero_sym(a, A, xs): 1982 Equal.sym(List, List.drop(a, A, xs, 0n), xs, drop_zero(a, A, xs)) 1983 1984 # Taking from the empty list gives the empty list, reversed to rewrite toward the simple side. 1985 law take_nil_sym: 1986 for -a: Quant 1987 for -A: Kind(a) 1988 for -n: Nat 1989 {Nil{} == List.take(a, A, Nil{}, n) : List} 1990 1991 def take_nil_sym(a, A, n): 1992 Equal.sym(List, List.take(a, A, Nil{}, n), Nil{}, take_nil(a, A, n)) 1993 1994 # Dropping from the empty list gives the empty list, reversed to rewrite toward the simple side. 1995 law drop_nil_sym: 1996 for -a: Quant 1997 for -A: Kind(a) 1998 for -n: Nat 1999 {Nil{} == List.drop(a, A, Nil{}, n) : List} 2000 Lines 1-2000 of 2865. More: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.7.2.0/list.bend&start_line=2001