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 # Range(n) has length n. 412 law length_range: 413 for n: Nat 414 {List.length(&2, Nat, List.range(n)) == n : Nat} 415 416 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}: 417 match n: 418 case 0n: 419 {==} 420 case 1n+p: 421 %MNat.add_succ(p, List.length(&2, Nat, acc)) : {List.length(&2, Nat, List.range.go(p, p <> acc)) == _ : Nat} 422 internal_length_range_go(p, p <> acc) 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 # Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs). 514 law map_reverse: 515 for ~A: Type 516 for ~B: Type 517 for ~f: A -> B 518 for xs: List 519 {List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) == List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) : List} 520 521 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}: 522 match xs: 523 case Nil{}: 524 {==} 525 case h <> t: 526 internal_map_reverse_go(~A, ~B, ~f, t, h <> acc) 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 # Filtering an append filters each part. 566 law filter_append: 567 for ~A: Data 568 for ~f: A -> Bool 569 for xs: List<&2, A> 570 for ys: List<&2, A> 571 {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>} 572 573 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>}: 574 match b: 575 case False{}: 576 {==} 577 case True{}: 578 {==} 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 # Filtering never makes a list longer. 608 law length_filter_le: 609 for ~A: Data 610 for ~f: A -> Bool 611 for xs: List<&2, A> 612 {Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)) == True{} : Bool} 613 614 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}: 615 match b: 616 case False{}: 617 MNat.le_succ(List.length(&2, A, r)) 618 case True{}: 619 MNat.le_refl(1n+List.length(&2, A, r)) 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 cons is a member of it. 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 # Membership is preserved when a new 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 # Nothing 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 # Membership on the left of an append. 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 # Membership on the right of an append. 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 list is sorted by any comparator. 732 law sorted_nil: 733 sorted_by(~Nat, ~Nat.is_le, Nil{}) 734 735 def sorted_nil(): 736 {==} 737 738 # A singleton list is sorted by any comparator. 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 sorted tail with an in-order head is sorted. 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 head pair of a sorted cons-cons list is 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 sorted cons-cons list 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 # A sorted list has a sorted tail. 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 # --- generated: _sym twins (tools/mathlib/twins.ts), do not edit --- 1313 1314 # The empty list is a right identity for append: xs ++ [] = xs, reversed to rewrite toward the simple side. 1315 law append_nil_sym: 1316 for -a: Quant 1317 for -A: Kind(a) 1318 for xs: List 1319 {xs == List.append(a, A, xs, Nil{}) : List} 1320 1321 def append_nil_sym(a, A, xs): 1322 Equal.sym(List, List.append(a, A, xs, Nil{}), xs, append_nil(a, A, xs)) 1323 1324 # The empty list is a left identity for append: [] ++ xs = xs, reversed to rewrite toward the simple side. 1325 law nil_append_sym: 1326 for -a: Quant 1327 for -A: Kind(a) 1328 for -xs: List 1329 {xs == List.append(a, A, Nil{}, xs) : List} 1330 1331 def nil_append_sym(a, A, xs): 1332 Equal.sym(List, List.append(a, A, Nil{}, xs), xs, nil_append(a, A, xs)) 1333 1334 # Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs), reversed to rewrite toward the simple side. 1335 law append_assoc_sym: 1336 for -a: Quant 1337 for -A: Kind(a) 1338 for xs: List 1339 for -ys: List 1340 for -zs: List 1341 {List.append(a, A, xs, List.append(a, A, ys, zs)) == List.append(a, A, List.append(a, A, xs, ys), zs) : List} 1342 1343 def append_assoc_sym(a, A, xs, ys, zs): 1344 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)) 1345 1346 # The length of an append is the sum of the lengths, reversed to rewrite toward the simple side. 1347 law length_append_sym: 1348 for -a: Quant 1349 for -A: Kind(a) 1350 for xs: List 1351 for -ys: List 1352 {Nat.add(List.length(a, A, xs), List.length(a, A, ys)) == List.length(a, A, List.append(a, A, xs, ys)) : Nat} 1353 1354 def length_append_sym(a, A, xs, ys): 1355 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)) 1356 1357 # The reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side. 1358 law reverse_go_spec_sym: 1359 for -a: Quant 1360 for -A: Kind(a) 1361 for xs: List 1362 for -acc: List 1363 {List.append(a, A, List.reverse(a, A, xs), acc) == List.reverse.go(a, A, xs, acc) : List} 1364 1365 def reverse_go_spec_sym(a, A, xs, acc): 1366 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)) 1367 1368 # Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side. 1369 law reverse_append_sym: 1370 for -a: Quant 1371 for -A: Kind(a) 1372 for xs: List 1373 for ys: List 1374 {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} 1375 1376 def reverse_append_sym(a, A, xs, ys): 1377 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)) 1378 1379 # Reversing twice gives the list back, reversed to rewrite toward the simple side. 1380 law reverse_reverse_sym: 1381 for -a: Quant 1382 for -A: Kind(a) 1383 for xs: List 1384 {xs == List.reverse(a, A, List.reverse(a, A, xs)) : List} 1385 1386 def reverse_reverse_sym(a, A, xs): 1387 Equal.sym(List, List.reverse(a, A, List.reverse(a, A, xs)), xs, reverse_reverse(a, A, xs)) 1388 1389 # Reversing preserves the length, reversed to rewrite toward the simple side. 1390 law length_reverse_sym: 1391 for -a: Quant 1392 for -A: Kind(a) 1393 for xs: List 1394 {List.length(a, A, xs) == List.length(a, A, List.reverse(a, A, xs)) : Nat} 1395 1396 def length_reverse_sym(a, A, xs): 1397 Equal.sym(Nat, List.length(a, A, List.reverse(a, A, xs)), List.length(a, A, xs), length_reverse(a, A, xs)) 1398 1399 # A right fold over an append folds the first part onto the fold of the second, reversed to rewrite toward the simple side. 1400 law foldr_append_sym: 1401 for ~a: Quant 1402 for ~A: Kind(a) 1403 for ~B: Type 1404 for ~f: A -> B -> B 1405 for xs: List 1406 for -ys: List 1407 for -z: B 1408 {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} 1409 1410 def foldr_append_sym(a, A, B, f, xs, ys, z): 1411 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)) 1412 1413 # Taking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side. 1414 law take_append_drop_sym: 1415 for -a: Quant 1416 for -A: Kind(a) 1417 for xs: List 1418 for n: Nat 1419 {xs == List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) : List} 1420 1421 def take_append_drop_sym(a, A, xs, n): 1422 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)) 1423 1424 # Mapping preserves the length, reversed to rewrite toward the simple side. 1425 law length_map_sym: 1426 for ~A: Type 1427 for ~B: Type 1428 for ~f: A -> B 1429 for xs: List 1430 {List.length(&1, A, xs) == List.length(&1, B, List.map(~A, ~B, ~f, xs)) : Nat} 1431 1432 def length_map_sym(A, B, f, xs): 1433 Equal.sym(Nat, List.length(&1, B, List.map(~A, ~B, ~f, xs)), List.length(&1, A, xs), length_map(~A, ~B, ~f, xs)) 1434 1435 # Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side. 1436 law map_append_sym: 1437 for ~A: Type 1438 for ~B: Type 1439 for ~f: A -> B 1440 for xs: List 1441 for -ys: List 1442 {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} 1443 1444 def map_append_sym(A, B, f, xs, ys): 1445 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)) 1446 1447 # Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs, reversed to rewrite toward the simple side. 1448 law map_map_sym: 1449 for ~A: Type 1450 for ~B: Type 1451 for ~C: Type 1452 for ~f: A -> B 1453 for ~g: B -> C 1454 for xs: List 1455 {List.map(~A, ~C, ~(x => g(f(x))), xs) == List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) : List} 1456 1457 def map_map_sym(A, B, C, f, g, xs): 1458 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)) 1459 1460 # Taking zero elements gives the empty list, reversed to rewrite toward the simple side. 1461 law take_zero_sym: 1462 for -a: Quant 1463 for -A: Kind(a) 1464 for xs: List 1465 {Nil{} == List.take(a, A, xs, 0n) : List} 1466 1467 def take_zero_sym(a, A, xs): 1468 Equal.sym(List, List.take(a, A, xs, 0n), Nil{}, take_zero(a, A, xs)) 1469 1470 # Dropping zero elements gives the list back, reversed to rewrite toward the simple side. 1471 law drop_zero_sym: 1472 for -a: Quant 1473 for -A: Kind(a) 1474 for xs: List 1475 {xs == List.drop(a, A, xs, 0n) : List} 1476 1477 def drop_zero_sym(a, A, xs): 1478 Equal.sym(List, List.drop(a, A, xs, 0n), xs, drop_zero(a, A, xs)) 1479 1480 # Taking from the empty list gives the empty list, reversed to rewrite toward the simple side. 1481 law take_nil_sym: 1482 for -a: Quant 1483 for -A: Kind(a) 1484 for -n: Nat 1485 {Nil{} == List.take(a, A, Nil{}, n) : List} 1486 1487 def take_nil_sym(a, A, n): 1488 Equal.sym(List, List.take(a, A, Nil{}, n), Nil{}, take_nil(a, A, n)) 1489 1490 # Dropping from the empty list gives the empty list, reversed to rewrite toward the simple side. 1491 law drop_nil_sym: 1492 for -a: Quant 1493 for -A: Kind(a) 1494 for -n: Nat 1495 {Nil{} == List.drop(a, A, Nil{}, n) : List} 1496 1497 def drop_nil_sym(a, A, n): 1498 Equal.sym(List, List.drop(a, A, Nil{}, n), Nil{}, drop_nil(a, A, n)) 1499 1500 # Taking n elements leaves min(n, length) of them, reversed to rewrite toward the simple side. 1501 law length_take_sym: 1502 for -a: Quant 1503 for -A: Kind(a) 1504 for xs: List 1505 for n: Nat 1506 {Nat.min(n, List.length(a, A, xs)) == List.length(a, A, List.take(a, A, xs, n)) : Nat} 1507 1508 def length_take_sym(a, A, xs, n): 1509 Equal.sym(Nat, List.length(a, A, List.take(a, A, xs, n)), Nat.min(n, List.length(a, A, xs)), length_take(a, A, xs, n)) 1510 1511 # Dropping n elements leaves length - n of them, reversed to rewrite toward the simple side. 1512 law length_drop_sym: 1513 for -a: Quant 1514 for -A: Kind(a) 1515 for xs: List 1516 for n: Nat 1517 {Nat.sub(List.length(a, A, xs), n) == List.length(a, A, List.drop(a, A, xs, n)) : Nat} 1518 1519 def length_drop_sym(a, A, xs, n): 1520 Equal.sym(Nat, List.length(a, A, List.drop(a, A, xs, n)), Nat.sub(List.length(a, A, xs), n), length_drop(a, A, xs, n)) 1521 1522 # Taking as many elements as the list has gives the list back, reversed to rewrite toward the simple side. 1523 law take_length_sym: 1524 for -A: Data 1525 for +xs: List<&2, A> 1526 {xs == List.take(&2, A, xs, List.length(&2, A, xs)) : List<&2, A>} 1527 1528 def take_length_sym(A, xs): 1529 Equal.sym(List<&2, A>, List.take(&2, A, xs, List.length(&2, A, xs)), xs, take_length(A, xs)) 1530 1531 # Dropping as many elements as the list has gives the empty list, reversed to rewrite toward the simple side. 1532 law drop_length_sym: 1533 for -A: Data 1534 for +xs: List<&2, A> 1535 {Nil{} == List.drop(&2, A, xs, List.length(&2, A, xs)) : List<&2, A>} 1536 1537 def drop_length_sym(A, xs): 1538 Equal.sym(List<&2, A>, List.drop(&2, A, xs, List.length(&2, A, xs)), Nil{}, drop_length(A, xs)) 1539 1540 # Taking m from the first n is taking min(n, m), reversed to rewrite toward the simple side. 1541 law take_take_sym: 1542 for -a: Quant 1543 for -A: Kind(a) 1544 for xs: List 1545 for n: Nat 1546 for m: Nat 1547 {List.take(a, A, xs, Nat.min(n, m)) == List.take(a, A, List.take(a, A, xs, n), m) : List} 1548 1549 def take_take_sym(a, A, xs, n, m): 1550 Equal.sym(List, List.take(a, A, List.take(a, A, xs, n), m), List.take(a, A, xs, Nat.min(n, m)), take_take(a, A, xs, n, m)) 1551 1552 # Dropping m after dropping n is dropping n + m, reversed to rewrite toward the simple side. 1553 law drop_drop_sym: 1554 for -a: Quant 1555 for -A: Kind(a) 1556 for xs: List 1557 for n: Nat 1558 for -m: Nat 1559 {List.drop(a, A, xs, Nat.add(n, m)) == List.drop(a, A, List.drop(a, A, xs, n), m) : List} 1560 1561 def drop_drop_sym(a, A, xs, n, m): 1562 Equal.sym(List, List.drop(a, A, List.drop(a, A, xs, n), m), List.drop(a, A, xs, Nat.add(n, m)), drop_drop(a, A, xs, n, m)) 1563 1564 # Reversing the empty list gives the empty list, reversed to rewrite toward the simple side. 1565 law reverse_nil_sym: 1566 for -a: Quant 1567 for -A: Kind(a) 1568 {Nil{} == List.reverse(a, A, Nil{}) : List} 1569 1570 def reverse_nil_sym(a, A): 1571 Equal.sym(List, List.reverse(a, A, Nil{}), Nil{}, reverse_nil(a, A)) 1572 1573 # Reversing a one-element list gives it back, reversed to rewrite toward the simple side. 1574 law reverse_singleton_sym: 1575 for -a: Quant 1576 for -A: Kind(a) 1577 for -x: A 1578 {[x] == List.reverse(a, A, [x]) : List} 1579 1580 def reverse_singleton_sym(a, A, x): 1581 Equal.sym(List, List.reverse(a, A, [x]), [x], reverse_singleton(a, A, x)) 1582 1583 # Replicating x n times gives a list of length n, reversed to rewrite toward the simple side. 1584 law length_replicate_sym: 1585 for -A: Data 1586 for n: Nat 1587 for -x: A 1588 {n == List.length(&2, A, List.replicate(A, n, x)) : Nat} 1589 1590 def length_replicate_sym(A, n, x): 1591 Equal.sym(Nat, List.length(&2, A, List.replicate(A, n, x)), n, length_replicate(A, n, x)) 1592 1593 # Range(n) has length n, reversed to rewrite toward the simple side. 1594 law length_range_sym: 1595 for n: Nat 1596 {n == List.length(&2, Nat, List.range(n)) : Nat} 1597 1598 def length_range_sym(n): 1599 Equal.sym(Nat, List.length(&2, Nat, List.range(n)), n, length_range(n)) 1600 1601 # Zipping two lists gives the length of the shorter one, reversed to rewrite toward the simple side. 1602 law length_zip_sym: 1603 for -a: Quant 1604 for -A: Kind(a) 1605 for xs: List 1606 for ys: List 1607 {Nat.min(List.length(a, A, xs), List.length(a, A, ys)) == List.length(&1, A & A, List.zip(a, A, a, A, xs, ys)) : Nat} 1608 1609 def length_zip_sym(a, A, xs, ys): 1610 Equal.sym(Nat, 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)), length_zip(a, A, xs, ys)) 1611 1612 # Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys), reversed to rewrite toward the simple side. 1613 law append_cons_sym: 1614 for -a: Quant 1615 for -A: Kind(a) 1616 for -x: A 1617 for -xs: List 1618 for -ys: List 1619 {x <> List.append(a, A, xs, ys) == List.append(a, A, x <> xs, ys) : List} 1620 1621 def append_cons_sym(a, A, x, xs, ys): 1622 Equal.sym(List, List.append(a, A, x <> xs, ys), x <> List.append(a, A, xs, ys), append_cons(a, A, x, xs, ys)) 1623 1624 # The empty list has length zero, reversed to rewrite toward the simple side. 1625 law length_nil_sym: 1626 for -a: Quant 1627 for -A: Kind(a) 1628 {0n == List.length(a, A, Nil{}) : Nat} 1629 1630 def length_nil_sym(a, A): 1631 Equal.sym(Nat, List.length(a, A, Nil{}), 0n, length_nil(a, A)) 1632 1633 # A cons is one longer than its tail, reversed to rewrite toward the simple side. 1634 law length_cons_sym: 1635 for -a: Quant 1636 for -A: Kind(a) 1637 for -x: A 1638 for -xs: List 1639 {1n+List.length(a, A, xs) == List.length(a, A, x <> xs) : Nat} 1640 1641 def length_cons_sym(a, A, x, xs): 1642 Equal.sym(Nat, List.length(a, A, x <> xs), 1n+List.length(a, A, xs), length_cons(a, A, x, xs)) 1643 1644 # Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss, reversed to rewrite toward the simple side. 1645 law concat_append_sym: 1646 for -a: Quant 1647 for -A: Kind(a) 1648 for xss: List> 1649 for -yss: List> 1650 {List.append(a, A, List.concat(a, A, xss), List.concat(a, A, yss)) == List.concat(a, A, List.append(a, List, xss, yss)) : List} 1651 1652 def concat_append_sym(a, A, xss, yss): 1653 Equal.sym(List, List.concat(a, A, List.append(a, List, xss, yss)), List.append(a, A, List.concat(a, A, xss), List.concat(a, A, yss)), concat_append(a, A, xss, yss)) 1654 1655 # A left fold over an append folds the second part from the fold of the first, reversed to rewrite toward the simple side. 1656 law foldl_append_sym: 1657 for ~a: Quant 1658 for ~A: Kind(a) 1659 for ~B: Type 1660 for ~f: B -> A -> B 1661 for xs: List 1662 for -ys: List 1663 for -z: B 1664 {List.foldl(~a, ~A, ~B, ~f, ys, List.foldl(~a, ~A, ~B, ~f, xs, z)) == List.foldl(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) : B} 1665 1666 def foldl_append_sym(a, A, B, f, xs, ys, z): 1667 Equal.sym(B, 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)), foldl_append(~a, ~A, ~B, ~f, xs, ys, z)) 1668 1669 # Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs), reversed to rewrite toward the simple side. 1670 law map_reverse_sym: 1671 for ~A: Type 1672 for ~B: Type 1673 for ~f: A -> B 1674 for xs: List 1675 {List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) : List} 1676 1677 def map_reverse_sym(A, B, f, xs): 1678 Equal.sym(List, List.map(~A, ~B, ~f, List.reverse(&1, A, xs)), List.reverse(&1, B, List.map(~A, ~B, ~f, xs)), map_reverse(~A, ~B, ~f, xs)) 1679 1680 # All over an append is all over each part, joined by and, reversed to rewrite toward the simple side. 1681 law all_append_sym: 1682 for ~a: Quant 1683 for ~A: Kind(a) 1684 for ~f: A -> Bool 1685 for xs: List 1686 for -ys: List 1687 {Bool.and(List.all(~a, ~A, ~f, xs), List.all(~a, ~A, ~f, ys)) == List.all(~a, ~A, ~f, List.append(a, A, xs, ys)) : Bool} 1688 1689 def all_append_sym(a, A, f, xs, ys): 1690 Equal.sym(Bool, 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)), all_append(~a, ~A, ~f, xs, ys)) 1691 1692 # Any over an append is any over each part, joined by or, reversed to rewrite toward the simple side. 1693 law any_append_sym: 1694 for ~a: Quant 1695 for ~A: Kind(a) 1696 for ~f: A -> Bool 1697 for xs: List 1698 for -ys: List 1699 {Bool.or(List.any(~a, ~A, ~f, xs), List.any(~a, ~A, ~f, ys)) == List.any(~a, ~A, ~f, List.append(a, A, xs, ys)) : Bool} 1700 1701 def any_append_sym(a, A, f, xs, ys): 1702 Equal.sym(Bool, 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)), any_append(~a, ~A, ~f, xs, ys)) 1703 1704 # Filtering an append filters each part, reversed to rewrite toward the simple side. 1705 law filter_append_sym: 1706 for ~A: Data 1707 for ~f: A -> Bool 1708 for xs: List<&2, A> 1709 for ys: List<&2, A> 1710 {List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)) == List.filter(~A, ~f, List.append(&2, A, xs, ys)) : List<&2, A>} 1711 1712 def filter_append_sym(A, f, xs, ys): 1713 Equal.sym(List<&2, A>, List.filter(~A, ~f, List.append(&2, A, xs, ys)), List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)), filter_append(~A, ~f, xs, ys)) 1714 1715 # An append contains x iff either part does, reversed to rewrite toward the simple side. 1716 law contains_append_sym: 1717 for ~A: Data 1718 for ~eq: A -> A -> Bool 1719 for xs: List<&2, A> 1720 for -ys: List<&2, A> 1721 for +x: A 1722 {Bool.or(List.contains(~A, ~eq, xs, x), List.contains(~A, ~eq, ys, x)) == List.contains(~A, ~eq, List.append(&2, A, xs, ys), x) : Bool} 1723 1724 def contains_append_sym(A, eq, xs, ys, x): 1725 Equal.sym(Bool, 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)), contains_append(~A, ~eq, xs, ys, x)) 1726 1727 # Filtering never makes a list longer, reversed to rewrite toward the simple side. 1728 law length_filter_le_sym: 1729 for ~A: Data 1730 for ~f: A -> Bool 1731 for xs: List<&2, A> 1732 {True{} == Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)) : Bool} 1733 1734 def length_filter_le_sym(A, f, xs): 1735 Equal.sym(Bool, Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)), True{}, length_filter_le(~A, ~f, xs)) 1736 1737 # Taking the length of the first part of an append gives the first part back, reversed to rewrite toward the simple side. 1738 law take_left_sym: 1739 for -a: Quant 1740 for -A: Kind(a) 1741 for xs: List 1742 for ys: List 1743 {xs == List.take(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) : List} 1744 1745 def take_left_sym(a, A, xs, ys): 1746 Equal.sym(List, List.take(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)), xs, take_left(a, A, xs, ys)) 1747 1748 # Dropping the length of the first part of an append gives the second part, reversed to rewrite toward the simple side. 1749 law drop_left_sym: 1750 for -a: Quant 1751 for -A: Kind(a) 1752 for xs: List 1753 for ys: List 1754 {ys == List.drop(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) : List} 1755 1756 def drop_left_sym(a, A, xs, ys): 1757 Equal.sym(List, List.drop(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)), ys, drop_left(a, A, xs, ys)) 1758 1759 # Taking past the first part of an append keeps it and takes the rest from the second part, reversed to rewrite toward the simple side. 1760 law take_append_sym: 1761 for -a: Quant 1762 for -A: Kind(a) 1763 for xs: List 1764 for -ys: List 1765 for -n: Nat 1766 {List.append(a, A, xs, List.take(a, A, ys, n)) == List.take(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)) : List} 1767 1768 def take_append_sym(a, A, xs, ys, n): 1769 Equal.sym(List, 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)), take_append(a, A, xs, ys, n)) 1770 1771 # Dropping past the first part of an append drops the rest from the second part, reversed to rewrite toward the simple side. 1772 law drop_append_sym: 1773 for -a: Quant 1774 for -A: Kind(a) 1775 for xs: List 1776 for -ys: List 1777 for -n: Nat 1778 {List.drop(a, A, ys, n) == List.drop(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)) : List} 1779 1780 def drop_append_sym(a, A, xs, ys, n): 1781 Equal.sym(List, List.drop(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)), List.drop(a, A, ys, n), drop_append(a, A, xs, ys, n)) 1782 1783 # Taking at most the length of the first part of an append only sees the first part, reversed to rewrite toward the simple side. 1784 law take_append_of_le_length_sym: 1785 for -a: Quant 1786 for -A: Kind(a) 1787 for xs: List 1788 for ys: List 1789 for n: Nat 1790 for h: MNat.le(n, List.length(a, A, xs)) 1791 {List.take(a, A, xs, n) == List.take(a, A, List.append(a, A, xs, ys), n) : List} 1792 1793 def take_append_of_le_length_sym(a, A, xs, ys, n, h): 1794 Equal.sym(List, List.take(a, A, List.append(a, A, xs, ys), n), List.take(a, A, xs, n), take_append_of_le_length(a, A, xs, ys, n, h)) 1795 1796 # Dropping at most the length of the first part of an append drops only from the first part, reversed to rewrite toward the simple side. 1797 law drop_append_of_le_length_sym: 1798 for -a: Quant 1799 for -A: Kind(a) 1800 for xs: List 1801 for ys: List 1802 for n: Nat 1803 for h: MNat.le(n, List.length(a, A, xs)) 1804 {List.append(a, A, List.drop(a, A, xs, n), ys) == List.drop(a, A, List.append(a, A, xs, ys), n) : List} 1805 1806 def drop_append_of_le_length_sym(a, A, xs, ys, n, h): 1807 Equal.sym(List, List.drop(a, A, List.append(a, A, xs, ys), n), List.append(a, A, List.drop(a, A, xs, n), ys), drop_append_of_le_length(a, A, xs, ys, n, h)) 1808 1809 # Mapping commutes with taking: map f (take n xs) = take n (map f xs), reversed to rewrite toward the simple side. 1810 law map_take_sym: 1811 for ~A: Type 1812 for ~B: Type 1813 for ~f: A -> B 1814 for xs: List 1815 for n: Nat 1816 {List.take(&1, B, List.map(~A, ~B, ~f, xs), n) == List.map(~A, ~B, ~f, List.take(&1, A, xs, n)) : List} 1817 1818 def map_take_sym(A, B, f, xs, n): 1819 Equal.sym(List, List.map(~A, ~B, ~f, List.take(&1, A, xs, n)), List.take(&1, B, List.map(~A, ~B, ~f, xs), n), map_take(~A, ~B, ~f, xs, n)) 1820 1821 # Mapping commutes with dropping: map f (drop n xs) = drop n (map f xs), reversed to rewrite toward the simple side. 1822 law map_drop_sym: 1823 for ~A: Type 1824 for ~B: Type 1825 for ~f: A -> B 1826 for xs: List 1827 for n: Nat 1828 {List.drop(&1, B, List.map(~A, ~B, ~f, xs), n) == List.map(~A, ~B, ~f, List.drop(&1, A, xs, n)) : List} 1829 1830 def map_drop_sym(A, B, f, xs, n): 1831 Equal.sym(List, List.map(~A, ~B, ~f, List.drop(&1, A, xs, n)), List.drop(&1, B, List.map(~A, ~B, ~f, xs), n), map_drop(~A, ~B, ~f, xs, n)) 1832 1833 # Taking m from n copies of x gives min(m, n) copies of x, reversed to rewrite toward the simple side. 1834 law take_replicate_sym: 1835 for -A: Data 1836 for n: Nat 1837 for m: Nat 1838 for -x: A 1839 {List.replicate(A, Nat.min(m, n), x) == List.take(&2, A, List.replicate(A, n, x), m) : List<&2, A>} 1840 1841 def take_replicate_sym(A, n, m, x): 1842 Equal.sym(List<&2, A>, List.take(&2, A, List.replicate(A, n, x), m), List.replicate(A, Nat.min(m, n), x), take_replicate(A, n, m, x)) 1843 1844 # Dropping m from n copies of x gives n - m copies of x, reversed to rewrite toward the simple side. 1845 law drop_replicate_sym: 1846 for -A: Data 1847 for n: Nat 1848 for m: Nat 1849 for -x: A 1850 {List.replicate(A, Nat.sub(n, m), x) == List.drop(&2, A, List.replicate(A, n, x), m) : List<&2, A>} 1851 1852 def drop_replicate_sym(A, n, m, x): 1853 Equal.sym(List<&2, A>, List.drop(&2, A, List.replicate(A, n, x), m), List.replicate(A, Nat.sub(n, m), x), drop_replicate(A, n, m, x)) 1854 1855 # The tail is one shorter than the list, or empty: length (tail xs) = length xs - 1, reversed to rewrite toward the simple side. 1856 law length_tail_sym: 1857 for -a: Quant 1858 for -A: Kind(a) 1859 for xs: List 1860 {Nat.sub(List.length(a, A, xs), 1n) == List.length(a, A, List.tail(a, A, xs)) : Nat} 1861 1862 def length_tail_sym(a, A, xs): 1863 Equal.sym(Nat, List.length(a, A, List.tail(a, A, xs)), Nat.sub(List.length(a, A, xs), 1n), length_tail(a, A, xs)) 1864 1865 # Mapping the identity gives the list back, reversed to rewrite toward the simple side. 1866 law map_id_sym: 1867 for ~A: Type 1868 for xs: List 1869 {xs == List.map(~A, ~A, ~(x => x), xs) : List} 1870 1871 def map_id_sym(A, xs): 1872 Equal.sym(List, List.map(~A, ~A, ~(x => x), xs), xs, map_id(~A, xs)) 1873 1874 # A right fold over a map folds with the mapped function: foldr g z (map f xs) = foldr (g . f) z xs, reversed to rewrite toward the simple side. 1875 law foldr_map_sym: 1876 for ~A: Type 1877 for ~B: Type 1878 for ~C: Type 1879 for ~f: A -> B 1880 for ~g: B -> C -> C 1881 for xs: List 1882 for -z: C 1883 {List.foldr(~&1, ~A, ~C, ~(x => y => g(f(x), y)), xs, z) == List.foldr(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, xs), z) : C} 1884 1885 def foldr_map_sym(A, B, C, f, g, xs, z): 1886 Equal.sym(C, 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), foldr_map(~A, ~B, ~C, ~f, ~g, xs, z)) 1887 1888 # 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, reversed to rewrite toward the simple side. 1889 law foldl_map_sym: 1890 for ~A: Type 1891 for ~B: Type 1892 for ~C: Type 1893 for ~f: A -> B 1894 for ~g: C -> B -> C 1895 for xs: List 1896 for -z: C 1897 {List.foldl(~&1, ~A, ~C, ~(x => y => g(x, f(y))), xs, z) == List.foldl(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, xs), z) : C} 1898 1899 def foldl_map_sym(A, B, C, f, g, xs, z): 1900 Equal.sym(C, 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), foldl_map(~A, ~B, ~C, ~f, ~g, xs, z)) 1901 1902 # Replicating m + n times appends m copies to n copies, reversed to rewrite toward the simple side. 1903 law replicate_add_sym: 1904 for -A: Data 1905 for m: Nat 1906 for -n: Nat 1907 for -x: A 1908 {List.append(&2, A, List.replicate(A, m, x), List.replicate(A, n, x)) == List.replicate(A, Nat.add(m, n), x) : List<&2, A>} 1909 1910 def replicate_add_sym(A, m, n, x): 1911 Equal.sym(List<&2, A>, List.replicate(A, Nat.add(m, n), x), List.append(&2, A, List.replicate(A, m, x), List.replicate(A, n, x)), replicate_add(A, m, n, x)) 1912 1913 # Reversing n copies of x gives them back, reversed to rewrite toward the simple side. 1914 law reverse_replicate_sym: 1915 for -A: Data 1916 for n: Nat 1917 for -x: A 1918 {List.replicate(A, n, x) == List.reverse(&2, A, List.replicate(A, n, x)) : List<&2, A>} 1919 1920 def reverse_replicate_sym(A, n, x): 1921 Equal.sym(List<&2, A>, List.reverse(&2, A, List.replicate(A, n, x)), List.replicate(A, n, x), reverse_replicate(A, n, x)) 1922 1923 # Filtering with an always-true predicate gives the list back, reversed to rewrite toward the simple side. 1924 law filter_true_sym: 1925 for ~A: Data 1926 for xs: List<&2, A> 1927 {xs == List.filter(~A, ~(x => True{}), xs) : List<&2, A>} 1928 1929 def filter_true_sym(A, xs): 1930 Equal.sym(List<&2, A>, List.filter(~A, ~(x => True{}), xs), xs, filter_true(~A, xs)) 1931 1932 # Filtering with an always-false predicate gives the empty list, reversed to rewrite toward the simple side. 1933 law filter_false_sym: 1934 for ~A: Data 1935 for xs: List<&2, A> 1936 {Nil{} == List.filter(~A, ~(x => False{}), xs) : List<&2, A>} 1937 1938 def filter_false_sym(A, xs): 1939 Equal.sym(List<&2, A>, List.filter(~A, ~(x => False{}), xs), Nil{}, filter_false(~A, xs)) 1940 1941 # Filtering twice is filtering by both predicates: filter p (filter q xs) = filter (p and q) xs, reversed to rewrite toward the simple side. 1942 law filter_filter_sym: 1943 for ~A: Data 1944 for ~p: A -> Bool 1945 for ~q: A -> Bool 1946 for xs: List<&2, A> 1947 {List.filter(~A, ~(+x => Bool.and(p(x), q(x))), xs) == List.filter(~A, ~p, List.filter(~A, ~q, xs)) : List<&2, A>} 1948 1949 def filter_filter_sym(A, p, q, xs): 1950 Equal.sym(List<&2, A>, List.filter(~A, ~p, List.filter(~A, ~q, xs)), List.filter(~A, ~(+x => Bool.and(p(x), q(x))), xs), filter_filter(~A, ~p, ~q, xs)) 1951 1952 # All over a filter checks q only where p holds: all q (filter p xs) = all (not p or q) xs, reversed to rewrite toward the simple side. 1953 law all_filter_sym: 1954 for ~A: Data 1955 for ~p: A -> Bool 1956 for ~q: A -> Bool 1957 for xs: List<&2, A> 1958 {List.all(~&2, ~A, ~(+x => Bool.or(Bool.not(p(x)), q(x))), xs) == List.all(~&2, ~A, ~q, List.filter(~A, ~p, xs)) : Bool} 1959 1960 def all_filter_sym(A, p, q, xs): 1961 Equal.sym(Bool, List.all(~&2, ~A, ~q, List.filter(~A, ~p, xs)), List.all(~&2, ~A, ~(+x => Bool.or(Bool.not(p(x)), q(x))), xs), all_filter(~A, ~p, ~q, xs)) 1962 1963 # Any over a filter looks for q only where p holds: any q (filter p xs) = any (p and q) xs, reversed to rewrite toward the simple side. 1964 law any_filter_sym: 1965 for ~A: Data 1966 for ~p: A -> Bool 1967 for ~q: A -> Bool 1968 for xs: List<&2, A> 1969 {List.any(~&2, ~A, ~(+x => Bool.and(p(x), q(x))), xs) == List.any(~&2, ~A, ~q, List.filter(~A, ~p, xs)) : Bool} 1970 1971 def any_filter_sym(A, p, q, xs): 1972 Equal.sym(Bool, List.any(~&2, ~A, ~q, List.filter(~A, ~p, xs)), List.any(~&2, ~A, ~(+x => Bool.and(p(x), q(x))), xs), any_filter(~A, ~p, ~q, xs)) 1973 1974 # All over a map checks the composed predicate: all p (map f xs) = all (p . f) xs, reversed to rewrite toward the simple side. 1975 law all_map_sym: 1976 for ~A: Type 1977 for ~B: Type 1978 for ~f: A -> B 1979 for ~p: B -> Bool 1980 for xs: List 1981 {List.all(~&1, ~A, ~(x => p(f(x))), xs) == List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) : Bool} 1982 1983 def all_map_sym(A, B, f, p, xs): 1984 Equal.sym(Bool, List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)), List.all(~&1, ~A, ~(x => p(f(x))), xs), all_map(~A, ~B, ~f, ~p, xs)) 1985 1986 # Any over a map checks the composed predicate: any p (map f xs) = any (p . f) xs, reversed to rewrite toward the simple side. 1987 law any_map_sym: 1988 for ~A: Type 1989 for ~B: Type 1990 for ~f: A -> B 1991 for ~p: B -> Bool 1992 for xs: List 1993 {List.any(~&1, ~A, ~(x => p(f(x))), xs) == List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) : Bool} 1994 1995 def any_map_sym(A, B, f, p, xs): 1996 Equal.sym(Bool, List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)), List.any(~&1, ~A, ~(x => p(f(x))), xs), any_map(~A, ~B, ~f, ~p, xs)) 1997 1998 # Reversing does not change whether all elements satisfy a predicate, reversed to rewrite toward the simple side. 1999 law all_reverse_sym: 2000 for ~a: Quant Lines 1-2000 of 2029. More: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.6.0.0/list.bend&start_line=2001