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