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 def internal_sorted_take_cons(t: List<&2, Nat>, n: Nat, +x: Nat, h: sorted_by(~Nat, ~Nat.is_le, x <> t)) -> sorted_by(~Nat, ~Nat.is_le, x <> List.take(&2, Nat, t, n)): 902 match t n: 903 case Nil{} _: 904 {==} 905 case y <> u 0n: 906 {==} 907 case +y <> u 1n+q: 908 +u = u 909 +h = h 910 sorted_cons_cons_intro(x, y, List.take(&2, Nat, u, q), sorted_cons_cons_elim_le(x, y, u, h), internal_sorted_take_cons(u, q, y, sorted_cons_cons_elim_tail(x, y, u, h))) 911 912 # A prefix of a Nat list sorted by Nat.is_le is sorted. 913 law sorted_take: 914 for xs: List<&2, Nat> 915 for n: Nat 916 for h: sorted_by(~Nat, ~Nat.is_le, xs) 917 sorted_by(~Nat, ~Nat.is_le, List.take(&2, Nat, xs, n)) 918 919 def sorted_take(xs, n, h): 920 match xs n: 921 case Nil{} _: 922 {==} 923 case x <> t 0n: 924 {==} 925 case x <> t 1n+p: 926 internal_sorted_take_cons(t, p, x, h) 927 928 # A suffix of a Nat list sorted by Nat.is_le is sorted. 929 law sorted_drop: 930 for xs: List<&2, Nat> 931 for n: Nat 932 for h: sorted_by(~Nat, ~Nat.is_le, xs) 933 sorted_by(~Nat, ~Nat.is_le, List.drop(&2, Nat, xs, n)) 934 935 def sorted_drop(xs, n, h): 936 match xs n: 937 case Nil{} _: 938 {==} 939 case x <> t 0n: 940 h 941 case x <> t 1n+p: 942 +t = t 943 sorted_drop(t, p, sorted_tail(x, t, h)) 944 945 def internal_sorted_skip(+x: Nat, +z: Nat, t: List<&2, Nat>, h: sorted_by(~Nat, ~Nat.is_le, x <> z <> t)) -> sorted_by(~Nat, ~Nat.is_le, x <> t): 946 match t: 947 case Nil{}: 948 {==} 949 case +w <> u: 950 +u = u 951 +h = h 952 sorted_cons_cons_intro(x, w, u, MNat.le_trans(x, z, w, sorted_cons_cons_elim_le(x, z, w <> u, h), sorted_cons_cons_elim_le(z, w, u, sorted_cons_cons_elim_tail(x, z, w <> u, h))), sorted_cons_cons_elim_tail(z, w, u, sorted_cons_cons_elim_tail(x, z, w <> u, h))) 953 954 def internal_sorted_filter_cons_put(-x: Nat, -z: Nat, -r: List<&2, Nat>, b: Bool, hxz: MNat.le(x, z), hxr: sorted_by(~Nat, ~Nat.is_le, x <> r), hzr: sorted_by(~Nat, ~Nat.is_le, z <> r)) -> sorted_by(~Nat, ~Nat.is_le, x <> List.filter.put(Nat, z, r, b)): 955 match b: 956 case False{}: 957 hxr 958 case True{}: 959 sorted_cons_cons_intro(x, z, r, hxz, hzr) 960 961 def internal_sorted_filter_cons(~f: Nat -> Bool, xs: List<&2, Nat>, +x: Nat, h: sorted_by(~Nat, ~Nat.is_le, x <> xs)) -> sorted_by(~Nat, ~Nat.is_le, x <> List.filter(~Nat, ~f, xs)): 962 match xs: 963 case Nil{}: 964 {==} 965 case +z <> t: 966 +t = t 967 +h = h 968 internal_sorted_filter_cons_put(x, z, List.filter(~Nat, ~f, t), f(z), sorted_cons_cons_elim_le(x, z, t, h), internal_sorted_filter_cons(~f, t, x, internal_sorted_skip(x, z, t, h)), internal_sorted_filter_cons(~f, t, z, sorted_cons_cons_elim_tail(x, z, t, h))) 969 970 def internal_sorted_filter_put(-x: Nat, -r: List<&2, Nat>, b: Bool, hxr: sorted_by(~Nat, ~Nat.is_le, x <> r), hr: sorted_by(~Nat, ~Nat.is_le, r)) -> sorted_by(~Nat, ~Nat.is_le, List.filter.put(Nat, x, r, b)): 971 match b: 972 case False{}: 973 hr 974 case True{}: 975 hxr 976 977 # Filtering a Nat list sorted by Nat.is_le keeps it sorted. 978 law sorted_filter: 979 for ~f: Nat -> Bool 980 for xs: List<&2, Nat> 981 for h: sorted_by(~Nat, ~Nat.is_le, xs) 982 sorted_by(~Nat, ~Nat.is_le, List.filter(~Nat, ~f, xs)) 983 984 def sorted_filter(f, xs, h): 985 match xs: 986 case Nil{}: 987 {==} 988 case +x <> t: 989 +t = t 990 +h = h 991 internal_sorted_filter_put(x, List.filter(~Nat, ~f, t), f(x), internal_sorted_filter_cons(~f, t, x, h), sorted_filter(~f, t, sorted_tail(x, t, h))) 992 993 def internal_head_le_mem_step(+x: Nat, +z: Nat, -t: List<&2, Nat>, +y: Nat, b: Bool, e: {Nat.is_eq(z, y) == b : Bool}, hxz: MNat.le(x, z), hm: {Bool.or(b, List.contains(~Nat, ~Nat.is_eq, t, y)) == True{} : Bool}, ih: {List.contains(~Nat, ~Nat.is_eq, t, y) == True{} : Bool} -> MNat.le(z, y)) -> MNat.le(x, y): 994 match b: 995 case True{}: 996 %MNat.eq_of_is_eq(z, y, e) : MNat.le(x, _) 997 hxz 998 case False{}: 999 MNat.le_trans(x, z, y, hxz, ih(hm)) 1000 1001 def internal_head_le_mem(xs: List<&2, Nat>, x: Nat, y: Nat, hs: sorted_by(~Nat, ~Nat.is_le, x <> xs), hm: mem(~Nat, ~Nat.is_eq, y, xs)) -> MNat.le(x, y): 1002 match xs: 1003 case Nil{}: 1004 Empty.absurd(MNat.le(x, y), MNat.internal_false_ne_true(hm)) 1005 case +z <> t: 1006 +x = x 1007 +y = y 1008 +t = t 1009 +hs = hs 1010 internal_head_le_mem_step(x, z, t, y, Nat.is_eq(z, y), {==}, sorted_cons_cons_elim_le(x, z, t, hs), Equal.trans(Bool, Bool.or(Nat.is_eq(z, y), List.contains(~Nat, ~Nat.is_eq, t, y)), List.contains(~Nat, ~Nat.is_eq, z <> t, y), True{}, internal_contains_cons(~Nat, ~Nat.is_eq, z, t, y), hm), k => internal_head_le_mem(t, z, y, sorted_cons_cons_elim_tail(x, z, t, hs), k)) 1011 1012 # The head of a Nat list sorted by Nat.is_le is <= every member of its tail. 1013 law sorted_head_le_mem: 1014 for x: Nat 1015 for xs: List<&2, Nat> 1016 for y: Nat 1017 for hs: sorted_by(~Nat, ~Nat.is_le, x <> xs) 1018 for hm: mem(~Nat, ~Nat.is_eq, y, xs) 1019 MNat.le(x, y) 1020 1021 def sorted_head_le_mem(x, xs, y, hs, hm): 1022 internal_head_le_mem(xs, x, y, hs, hm) 1023 1024 def internal_le_of_mem_step(+x: Nat, xs: List<&2, Nat>, +y: Nat, b: Bool, e: {Nat.is_eq(x, y) == b : Bool}, hs: sorted_by(~Nat, ~Nat.is_le, x <> xs), hm: {Bool.or(b, List.contains(~Nat, ~Nat.is_eq, xs, y)) == True{} : Bool}) -> MNat.le(x, y): 1025 match b: 1026 case True{}: 1027 %MNat.eq_of_is_eq(x, y, e) : MNat.le(x, _) 1028 MNat.le_refl(x) 1029 case False{}: 1030 sorted_head_le_mem(x, xs, y, hs, hm) 1031 1032 # The head of a Nat list sorted by Nat.is_le is <= every member of the list. 1033 law sorted_le_of_mem: 1034 for x: Nat 1035 for xs: List<&2, Nat> 1036 for y: Nat 1037 for hs: sorted_by(~Nat, ~Nat.is_le, x <> xs) 1038 for hm: mem(~Nat, ~Nat.is_eq, y, x <> xs) 1039 MNat.le(x, y) 1040 1041 def sorted_le_of_mem(x, xs, y, hs, hm): 1042 +x = x 1043 +y = y 1044 +xs = xs 1045 internal_le_of_mem_step(x, xs, y, Nat.is_eq(x, y), {==}, hs, Equal.trans(Bool, Bool.or(Nat.is_eq(x, y), List.contains(~Nat, ~Nat.is_eq, xs, y)), List.contains(~Nat, ~Nat.is_eq, x <> xs, y), True{}, internal_contains_cons(~Nat, ~Nat.is_eq, x, xs, y), hm)) 1046 1047 def internal_sorted_append_cons(t: List<&2, Nat>, ys: List<&2, Nat>, +x: Nat, bnd: @a: Nat -> @b: Nat -> mem(~Nat, ~Nat.is_eq, a, x <> t) -> mem(~Nat, ~Nat.is_eq, b, ys) -> MNat.le(a, b), hx: sorted_by(~Nat, ~Nat.is_le, x <> t), hy: sorted_by(~Nat, ~Nat.is_le, ys)) -> sorted_by(~Nat, ~Nat.is_le, x <> List.append(&2, Nat, t, ys)): 1048 match t: 1049 case Nil{}: 1050 match ys: 1051 case Nil{}: 1052 {==} 1053 case +y <> u: 1054 +u = u 1055 sorted_cons_cons_intro(x, y, u, bnd(x, y, mem_cons_self(x, Nil{}), mem_cons_self(y, u)), hy) 1056 case +z <> u: 1057 +u = u 1058 +hx = hx 1059 sorted_cons_cons_intro(x, z, List.append(&2, Nat, u, ys), sorted_cons_cons_elim_le(x, z, u, hx), internal_sorted_append_cons(u, ys, z, +a => b => ma => mb => bnd(a, b, mem_cons_of_mem(a, x, z <> u, ma), mb), sorted_cons_cons_elim_tail(x, z, u, hx), hy)) 1060 1061 # Appending two Nat lists sorted by Nat.is_le, with every element of the first <= every element of the second, gives a sorted list. 1062 law sorted_append: 1063 for xs: List<&2, Nat> 1064 for ys: List<&2, Nat> 1065 for bnd: @x: Nat -> @y: Nat -> mem(~Nat, ~Nat.is_eq, x, xs) -> mem(~Nat, ~Nat.is_eq, y, ys) -> MNat.le(x, y) 1066 for hx: sorted_by(~Nat, ~Nat.is_le, xs) 1067 for hy: sorted_by(~Nat, ~Nat.is_le, ys) 1068 sorted_by(~Nat, ~Nat.is_le, List.append(&2, Nat, xs, ys)) 1069 1070 def sorted_append(xs, ys, bnd, hx, hy): 1071 match xs: 1072 case Nil{}: 1073 hy 1074 case x <> t: 1075 internal_sorted_append_cons(t, ys, x, bnd, hx, hy) 1076 1077 # Taking the length of the first part of an append gives the first part back. 1078 law take_left: 1079 for -a: Quant 1080 for -A: Kind(a) 1081 for xs: List 1082 for ys: List 1083 {List.take(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) == xs : List} 1084 1085 def take_left(a, A, xs, ys): 1086 match xs: 1087 case Nil{}: 1088 take_zero(a, A, ys) 1089 case h <> t: 1090 %take_left(a, A, t, ys) : {h <> List.take(a, A, List.append(a, A, t, ys), List.length(a, A, t)) == h <> _ : List} 1091 {==} 1092 1093 # Dropping the length of the first part of an append gives the second part. 1094 law drop_left: 1095 for -a: Quant 1096 for -A: Kind(a) 1097 for xs: List 1098 for ys: List 1099 {List.drop(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) == ys : List} 1100 1101 def drop_left(a, A, xs, ys): 1102 match xs: 1103 case Nil{}: 1104 drop_zero(a, A, ys) 1105 case h <> t: 1106 drop_left(a, A, t, ys) 1107 1108 # Taking past the first part of an append keeps it and takes the rest from the second part. 1109 law take_append: 1110 for -a: Quant 1111 for -A: Kind(a) 1112 for xs: List 1113 for -ys: List 1114 for -n: Nat 1115 {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} 1116 1117 def take_append(a, A, xs, ys, n): 1118 match xs: 1119 case Nil{}: 1120 {==} 1121 case h <> t: 1122 %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} 1123 {==} 1124 1125 # Dropping past the first part of an append drops the rest from the second part. 1126 law drop_append: 1127 for -a: Quant 1128 for -A: Kind(a) 1129 for xs: List 1130 for -ys: List 1131 for -n: Nat 1132 {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} 1133 1134 def drop_append(a, A, xs, ys, n): 1135 match xs: 1136 case Nil{}: 1137 {==} 1138 case h <> t: 1139 drop_append(a, A, t, ys, n) 1140 1141 # Taking at most the length of the first part of an append only sees the first part. 1142 law take_append_of_le_length: 1143 for -a: Quant 1144 for -A: Kind(a) 1145 for xs: List 1146 for ys: List 1147 for n: Nat 1148 for h: MNat.le(n, List.length(a, A, xs)) 1149 {List.take(a, A, List.append(a, A, xs, ys), n) == List.take(a, A, xs, n) : List} 1150 1151 def take_append_of_le_length(a, A, xs, ys, n, h): 1152 match xs n: 1153 case Nil{} 0n: 1154 take_zero(a, A, ys) 1155 case Nil{} 1n+p: 1156 Empty.absurd({List.take(a, A, ys, 1n+p) == Nil{} : List}, MNat.internal_false_ne_true(h)) 1157 case x <> t 0n: 1158 {==} 1159 case x <> t 1n+p: 1160 %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} 1161 {==} 1162 1163 # Dropping at most the length of the first part of an append drops only from the first part. 1164 law drop_append_of_le_length: 1165 for -a: Quant 1166 for -A: Kind(a) 1167 for xs: List 1168 for ys: List 1169 for n: Nat 1170 for h: MNat.le(n, List.length(a, A, xs)) 1171 {List.drop(a, A, List.append(a, A, xs, ys), n) == List.append(a, A, List.drop(a, A, xs, n), ys) : List} 1172 1173 def drop_append_of_le_length(a, A, xs, ys, n, h): 1174 match xs n: 1175 case Nil{} 0n: 1176 drop_zero(a, A, ys) 1177 case Nil{} 1n+p: 1178 Empty.absurd({List.drop(a, A, ys, 1n+p) == ys : List}, MNat.internal_false_ne_true(h)) 1179 case x <> t 0n: 1180 {==} 1181 case x <> t 1n+p: 1182 drop_append_of_le_length(a, A, t, ys, p, h) 1183 1184 # Mapping commutes with taking: map f (take n xs) = take n (map f xs). 1185 law map_take: 1186 for ~A: Type 1187 for ~B: Type 1188 for ~f: A -> B 1189 for xs: List 1190 for n: Nat 1191 {List.map(~A, ~B, ~f, List.take(&1, A, xs, n)) == List.take(&1, B, List.map(~A, ~B, ~f, xs), n) : List} 1192 1193 def map_take(A, B, f, xs, n): 1194 match xs n: 1195 case Nil{} _: 1196 {==} 1197 case h <> t 0n: 1198 {==} 1199 case h <> t 1n+p: 1200 %map_take(~A, ~B, ~f, t, p) : {f(h) <> List.map(~A, ~B, ~f, List.take(&1, A, t, p)) == f(h) <> _ : List} 1201 {==} 1202 1203 # Mapping commutes with dropping: map f (drop n xs) = drop n (map f xs). 1204 law map_drop: 1205 for ~A: Type 1206 for ~B: Type 1207 for ~f: A -> B 1208 for xs: List 1209 for n: Nat 1210 {List.map(~A, ~B, ~f, List.drop(&1, A, xs, n)) == List.drop(&1, B, List.map(~A, ~B, ~f, xs), n) : List} 1211 1212 def map_drop(A, B, f, xs, n): 1213 match xs n: 1214 case Nil{} _: 1215 {==} 1216 case h <> t 0n: 1217 {==} 1218 case h <> t 1n+p: 1219 map_drop(~A, ~B, ~f, t, p) 1220 1221 # Taking m from n copies of x gives min(m, n) copies of x. 1222 law take_replicate: 1223 for -A: Data 1224 for n: Nat 1225 for m: Nat 1226 for -x: A 1227 {List.take(&2, A, List.replicate(A, n, x), m) == List.replicate(A, Nat.min(m, n), x) : List<&2, A>} 1228 1229 def take_replicate(A, n, m, x): 1230 match n m: 1231 case 0n _: 1232 %MNat.min_zero_sym(m) : {Nil{} == List.replicate(A, _, x) : List<&2, A>} 1233 {==} 1234 case 1n+p 0n: 1235 {==} 1236 case 1n+p 1n+q: 1237 %take_replicate(A, p, q, x) : {x <> List.take(&2, A, List.replicate(A, p, x), q) == x <> _ : List<&2, A>} 1238 {==} 1239 1240 # Dropping m from n copies of x gives n - m copies of x. 1241 law drop_replicate: 1242 for -A: Data 1243 for n: Nat 1244 for m: Nat 1245 for -x: A 1246 {List.drop(&2, A, List.replicate(A, n, x), m) == List.replicate(A, Nat.sub(n, m), x) : List<&2, A>} 1247 1248 def drop_replicate(A, n, m, x): 1249 match n m: 1250 case 0n _: 1251 {==} 1252 case 1n+p 0n: 1253 {==} 1254 case 1n+p 1n+q: 1255 drop_replicate(A, p, q, x) 1256 1257 # Taking n elements gives at most n of them. 1258 law length_take_le: 1259 for -a: Quant 1260 for -A: Kind(a) 1261 for xs: List 1262 for n: Nat 1263 MNat.le(List.length(a, A, List.take(a, A, xs, n)), n) 1264 1265 def length_take_le(a, A, xs, n): 1266 match xs n: 1267 case Nil{} _: 1268 MNat.zero_le(n) 1269 case h <> t 0n: 1270 {==} 1271 case h <> t 1n+p: 1272 MNat.succ_le_succ(List.length(a, A, List.take(a, A, t, p)), p, length_take_le(a, A, t, p)) 1273 1274 # The tail is one shorter than the list, or empty: length (tail xs) = length xs - 1. 1275 law length_tail: 1276 for -a: Quant 1277 for -A: Kind(a) 1278 for xs: List 1279 {List.length(a, A, List.tail(a, A, xs)) == Nat.sub(List.length(a, A, xs), 1n) : Nat} 1280 1281 def length_tail(a, A, xs): 1282 match xs: 1283 case Nil{}: 1284 {==} 1285 case h <> t: 1286 MNat.sub_zero_sym(List.length(a, A, t)) 1287 1288 # Mapping the identity gives the list back. 1289 law map_id: 1290 for ~A: Type 1291 for xs: List 1292 {List.map(~A, ~A, ~(x => x), xs) == xs : List} 1293 1294 def map_id(A, xs): 1295 match xs: 1296 case Nil{}: 1297 {==} 1298 case h <> t: 1299 %map_id(~A, t) : {h <> List.map(~A, ~A, ~(x => x), t) == h <> _ : List} 1300 {==} 1301 1302 # A right fold over a map folds with the mapped function: foldr g z (map f xs) = foldr (g . f) z xs. 1303 law foldr_map: 1304 for ~A: Type 1305 for ~B: Type 1306 for ~C: Type 1307 for ~f: A -> B 1308 for ~g: B -> C -> C 1309 for xs: List 1310 for -z: C 1311 {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} 1312 1313 def foldr_map(A, B, C, f, g, xs, z): 1314 match xs: 1315 case Nil{}: 1316 {==} 1317 case h <> t: 1318 %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} 1319 {==} 1320 1321 # 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. 1322 law foldl_map: 1323 for ~A: Type 1324 for ~B: Type 1325 for ~C: Type 1326 for ~f: A -> B 1327 for ~g: C -> B -> C 1328 for xs: List 1329 for -z: C 1330 {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} 1331 1332 def foldl_map(A, B, C, f, g, xs, z): 1333 match xs: 1334 case Nil{}: 1335 {==} 1336 case h <> t: 1337 foldl_map(~A, ~B, ~C, ~f, ~g, t, g(z, f(h))) 1338 1339 # Replicating m + n times appends m copies to n copies. 1340 law replicate_add: 1341 for -A: Data 1342 for m: Nat 1343 for -n: Nat 1344 for -x: A 1345 {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>} 1346 1347 def replicate_add(A, m, n, x): 1348 match m: 1349 case 0n: 1350 {==} 1351 case 1n+p: 1352 %replicate_add(A, p, n, x) : {x <> List.replicate(A, Nat.add(p, n), x) == x <> _ : List<&2, A>} 1353 {==} 1354 1355 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>}: 1356 match n: 1357 case 0n: 1358 {==} 1359 case 1n+p: 1360 %internal_replicate_append_nil(A, p, x) : {x <> List.append(&2, A, List.replicate(A, p, x), Nil{}) == x <> _ : List<&2, A>} 1361 {==} 1362 1363 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>}: 1364 match n: 1365 case 0n: 1366 {==} 1367 case 1n+p: 1368 %internal_replicate_append_cons(A, p, x, acc) : {x <> List.append(&2, A, List.replicate(A, p, x), x <> acc) == x <> _ : List<&2, A>} 1369 {==} 1370 1371 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>}: 1372 match n: 1373 case 0n: 1374 {==} 1375 case 1n+p: 1376 +p = p 1377 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)) 1378 1379 # Reversing n copies of x gives them back. 1380 law reverse_replicate: 1381 for -A: Data 1382 for n: Nat 1383 for -x: A 1384 {List.reverse(&2, A, List.replicate(A, n, x)) == List.replicate(A, n, x) : List<&2, A>} 1385 1386 def reverse_replicate(A, n, x): 1387 +n = n 1388 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)) 1389 1390 # Filtering with an always-true predicate gives the list back. 1391 law filter_true: 1392 for ~A: Data 1393 for xs: List<&2, A> 1394 {List.filter(~A, ~(x => True{}), xs) == xs : List<&2, A>} 1395 1396 def filter_true(A, xs): 1397 match xs: 1398 case Nil{}: 1399 {==} 1400 case h <> t: 1401 %filter_true(~A, t) : {h <> List.filter(~A, ~(x => True{}), t) == h <> _ : List<&2, A>} 1402 {==} 1403 1404 # Filtering with an always-false predicate gives the empty list. 1405 law filter_false: 1406 for ~A: Data 1407 for xs: List<&2, A> 1408 {List.filter(~A, ~(x => False{}), xs) == Nil{} : List<&2, A>} 1409 1410 def filter_false(A, xs): 1411 match xs: 1412 case Nil{}: 1413 {==} 1414 case h <> t: 1415 filter_false(~A, t) 1416 1417 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>}: 1418 match b: 1419 case False{}: 1420 %MBool.and_false_sym(p(h)) : {List.filter(~A, ~p, r) == List.filter.put(A, h, List.filter(~A, ~p, r), _) : List<&2, A>} 1421 {==} 1422 case True{}: 1423 %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>} 1424 {==} 1425 1426 # Filtering twice is filtering by both predicates: filter p (filter q xs) = filter (p and q) xs. 1427 law filter_filter: 1428 for ~A: Data 1429 for ~p: A -> Bool 1430 for ~q: A -> Bool 1431 for xs: List<&2, A> 1432 {List.filter(~A, ~p, List.filter(~A, ~q, xs)) == List.filter(~A, ~(+x => Bool.and(p(x), q(x))), xs) : List<&2, A>} 1433 1434 def filter_filter(A, p, q, xs): 1435 match xs: 1436 case Nil{}: 1437 {==} 1438 case +h <> t: 1439 +t = t 1440 %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>} 1441 internal_filter_put_filter(~A, ~p, h, List.filter(~A, ~q, t), q(h)) 1442 1443 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}: 1444 match b: 1445 case False{}: 1446 {==} 1447 case True{}: 1448 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)) 1449 1450 # All over a filter checks q only where p holds: all q (filter p xs) = all (not p or q) xs. 1451 law all_filter: 1452 for ~A: Data 1453 for ~p: A -> Bool 1454 for ~q: A -> Bool 1455 for xs: List<&2, A> 1456 {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} 1457 1458 def all_filter(A, p, q, xs): 1459 match xs: 1460 case Nil{}: 1461 {==} 1462 case +h <> t: 1463 +t = t 1464 %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} 1465 %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} 1466 internal_all_filter_put(~A, ~q, h, List.filter(~A, ~p, t), p(h)) 1467 1468 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}: 1469 match b: 1470 case False{}: 1471 {==} 1472 case True{}: 1473 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)) 1474 1475 # Any over a filter looks for q only where p holds: any q (filter p xs) = any (p and q) xs. 1476 law any_filter: 1477 for ~A: Data 1478 for ~p: A -> Bool 1479 for ~q: A -> Bool 1480 for xs: List<&2, A> 1481 {List.any(~&2, ~A, ~q, List.filter(~A, ~p, xs)) == List.any(~&2, ~A, ~(+x => Bool.and(p(x), q(x))), xs) : Bool} 1482 1483 def any_filter(A, p, q, xs): 1484 match xs: 1485 case Nil{}: 1486 {==} 1487 case +h <> t: 1488 +t = t 1489 %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} 1490 %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} 1491 internal_any_filter_put(~A, ~q, h, List.filter(~A, ~p, t), p(h)) 1492 1493 # Unfolds List.all directly, so its proof depends on Base's definition (PLAN F39). 1494 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}: 1495 match xs: 1496 case Nil{}: 1497 {==} 1498 case h <> t: 1499 %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} 1500 {==} 1501 1502 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}: 1503 match xs: 1504 case Nil{}: 1505 {==} 1506 case h <> t: 1507 %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} 1508 {==} 1509 1510 # All over a map checks the composed predicate: all p (map f xs) = all (p . f) xs. 1511 law all_map: 1512 for ~A: Type 1513 for ~B: Type 1514 for ~f: A -> B 1515 for ~p: B -> Bool 1516 for xs: List 1517 {List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) == List.all(~&1, ~A, ~(x => p(f(x))), xs) : Bool} 1518 1519 def all_map(A, B, f, p, xs): 1520 internal_all_map(~A, ~B, ~f, ~p, xs) 1521 1522 # Any over a map checks the composed predicate: any p (map f xs) = any (p . f) xs. 1523 law any_map: 1524 for ~A: Type 1525 for ~B: Type 1526 for ~f: A -> B 1527 for ~p: B -> Bool 1528 for xs: List 1529 {List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) == List.any(~&1, ~A, ~(x => p(f(x))), xs) : Bool} 1530 1531 def any_map(A, B, f, p, xs): 1532 internal_any_map(~A, ~B, ~f, ~p, xs) 1533 1534 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}: 1535 match xs c: 1536 case Nil{} True{}: 1537 e 1538 case Nil{} False{}: 1539 e 1540 case h <> t True{}: 1541 +v = f(h) 1542 %internal_all_cons_test(~a, ~A, ~f, h, t, v, {==}) : {List.all(~a, ~A, ~f, List.reverse.go(a, A, t, h <> acc)) == _ : Bool} 1543 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)))) 1544 case h <> t False{}: 1545 +v = f(h) 1546 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)))) 1547 1548 # Reversing does not change whether all elements satisfy a predicate. 1549 law all_reverse: 1550 for ~a: Quant 1551 for ~A: Kind(a) 1552 for ~f: A -> Bool 1553 for xs: List 1554 {List.all(~a, ~A, ~f, List.reverse(a, A, xs)) == List.all(~a, ~A, ~f, xs) : Bool} 1555 1556 def all_reverse(a, A, f, xs): 1557 internal_all_reverse_go(~a, ~A, ~f, xs, Nil{}, True{}, {==}) 1558 1559 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}: 1560 match xs c: 1561 case Nil{} True{}: 1562 e 1563 case Nil{} False{}: 1564 e 1565 case h <> t True{}: 1566 +v = f(h) 1567 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)))) 1568 case h <> t False{}: 1569 +v = f(h) 1570 %internal_any_cons_test(~a, ~A, ~f, h, t, v, {==}) : {List.any(~a, ~A, ~f, List.reverse.go(a, A, t, h <> acc)) == _ : Bool} 1571 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)))) 1572 1573 # Reversing does not change whether some element satisfies a predicate. 1574 law any_reverse: 1575 for ~a: Quant 1576 for ~A: Kind(a) 1577 for ~f: A -> Bool 1578 for xs: List 1579 {List.any(~a, ~A, ~f, List.reverse(a, A, xs)) == List.any(~a, ~A, ~f, xs) : Bool} 1580 1581 def any_reverse(a, A, f, xs): 1582 internal_any_reverse_go(~a, ~A, ~f, xs, Nil{}, False{}, {==}) 1583 1584 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}: 1585 match xs c: 1586 case Nil{} True{}: 1587 e 1588 case Nil{} False{}: 1589 e 1590 case +h <> t True{}: 1591 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))))) 1592 case +h <> +t False{}: 1593 +v = eq(h, x) 1594 %internal_contains_cons(~A, ~eq, h, t, x) : {List.contains(~A, ~eq, List.reverse.go(&2, A, t, h <> acc), x) == _ : Bool} 1595 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)))) 1596 1597 # Reversing does not change whether a list contains x. 1598 law contains_reverse: 1599 for ~A: Data 1600 for ~eq: A -> A -> Bool 1601 for xs: List<&2, A> 1602 for +x: A 1603 {List.contains(~A, ~eq, List.reverse(&2, A, xs), x) == List.contains(~A, ~eq, xs, x) : Bool} 1604 1605 def contains_reverse(A, eq, xs, x): 1606 internal_contains_reverse_go(~A, ~eq, xs, Nil{}, x, False{}, {==}) 1607 1608 # Zipping the empty list with anything gives the empty list. 1609 law zip_nil_left: 1610 for -a: Quant 1611 for -A: Kind(a) 1612 for -b: Quant 1613 for -B: Kind(b) 1614 for -ys: List 1615 {List.zip(a, A, b, B, Nil{}, ys) == Nil{} : List<&1, A & B>} 1616 1617 def zip_nil_left(a, A, b, B, ys): 1618 {==} 1619 1620 # Zipping anything with the empty list gives the empty list. 1621 law zip_nil_right: 1622 for -a: Quant 1623 for -A: Kind(a) 1624 for -b: Quant 1625 for -B: Kind(b) 1626 for xs: List 1627 {List.zip(a, A, b, B, xs, Nil{}) == Nil{} : List<&1, A & B>} 1628 1629 def zip_nil_right(a, A, b, B, xs): 1630 match xs: 1631 case Nil{}: 1632 {==} 1633 case h <> t: 1634 {==} 1635 1636 # The head of a cons is its first element. 1637 law head_cons: 1638 for -a: Quant 1639 for -A: Kind(a) 1640 for -x: A 1641 for -xs: List 1642 {List.head(a, A, x <> xs) == Some{x} : Maybe} 1643 1644 def head_cons(a, A, x, xs): 1645 {==} 1646 1647 # The head of an append is the head of the first part, or else of the second. 1648 law head_append: 1649 for -a: Quant 1650 for -A: Kind(a) 1651 for xs: List 1652 for -ys: List 1653 {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} 1654 1655 def head_append(a, A, xs, ys): 1656 match xs: 1657 case Nil{}: 1658 {==} 1659 case h <> t: 1660 {==} 1661 1662 # The head of a map is the mapped head. 1663 law head_map: 1664 for ~A: Type 1665 for ~B: Type 1666 for ~f: A -> B 1667 for xs: List 1668 {List.head(&1, B, List.map(~A, ~B, ~f, xs)) == Maybe.map(&1, A, B, f, List.head(&1, A, xs)) : Maybe<&1, B>} 1669 1670 def head_map(A, B, f, xs): 1671 match xs: 1672 case Nil{}: 1673 {==} 1674 case h <> t: 1675 {==} 1676 1677 # The tail of a map is the map of the tail. 1678 law tail_map: 1679 for ~A: Type 1680 for ~B: Type 1681 for ~f: A -> B 1682 for xs: List 1683 {List.tail(&1, B, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~B, ~f, List.tail(&1, A, xs)) : List} 1684 1685 def tail_map(A, B, f, xs): 1686 match xs: 1687 case Nil{}: 1688 {==} 1689 case h <> t: 1690 {==} 1691 1692 # The element at index zero of a cons is its head. 1693 law get_cons_zero: 1694 for -a: Quant 1695 for -A: Kind(a) 1696 for -x: A 1697 for -xs: List 1698 {List.get(a, A, x <> xs, 0n) == Some{x} : Maybe} 1699 1700 def get_cons_zero(a, A, x, xs): 1701 {==} 1702 1703 # The element at index n + 1 of a cons is the element at index n of its tail. 1704 law get_cons_succ: 1705 for -a: Quant 1706 for -A: Kind(a) 1707 for -x: A 1708 for -xs: List 1709 for -n: Nat 1710 {List.get(a, A, x <> xs, 1n+n) == List.get(a, A, xs, n) : Maybe} 1711 1712 def get_cons_succ(a, A, x, xs, n): 1713 {==} 1714 1715 # Indexing a map is mapping the indexed element. 1716 law get_map: 1717 for ~A: Type 1718 for ~B: Type 1719 for ~f: A -> B 1720 for xs: List 1721 for n: Nat 1722 {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>} 1723 1724 def get_map(A, B, f, xs, n): 1725 match xs n: 1726 case Nil{} _: 1727 {==} 1728 case h <> t 0n: 1729 {==} 1730 case h <> t 1n+p: 1731 get_map(~A, ~B, ~f, t, p) 1732 1733 # Setting an element does not change the length. 1734 law length_set: 1735 for -a: Quant 1736 for -A: Kind(a) 1737 for xs: List 1738 for n: Nat 1739 for -x: A 1740 {List.length(a, A, List.set(a, A, xs, n, x)) == List.length(a, A, xs) : Nat} 1741 1742 def length_set(a, A, xs, n, x): 1743 match xs n: 1744 case Nil{} _: 1745 {==} 1746 case h <> t 0n: 1747 {==} 1748 case h <> t 1n+p: 1749 %length_set(a, A, t, p, x) : {1n+List.length(a, A, List.set(a, A, t, p, x)) == 1n+_ : Nat} 1750 {==} 1751 1752 # Reading the index just set gives the new value wherever the index is in range. 1753 law get_set_self: 1754 for -a: Quant 1755 for -A: Kind(a) 1756 for xs: List 1757 for n: Nat 1758 for -x: A 1759 {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} 1760 1761 def get_set_self(a, A, xs, n, x): 1762 match xs n: 1763 case Nil{} _: 1764 {==} 1765 case h <> t 0n: 1766 {==} 1767 case h <> t 1n+p: 1768 get_set_self(a, A, t, p, x) 1769 1770 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}: 1771 match ys: 1772 case Nil{}: 1773 {==} 1774 case y <> t: 1775 internal_last_go_append_singleton(a, A, t, y, x) 1776 1777 # The last element of xs ++ [x] is x. 1778 law last_append_singleton: 1779 for -a: Quant 1780 for -A: Kind(a) 1781 for xs: List 1782 for -x: A 1783 {List.last(a, A, List.append(a, A, xs, [x])) == Some{x} : Maybe} 1784 1785 def last_append_singleton(a, A, xs, x): 1786 match xs: 1787 case Nil{}: 1788 {==} 1789 case h <> t: 1790 %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} 1791 {==} 1792 1793 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}: 1794 match xs: 1795 case Nil{}: 1796 {==} 1797 case y <> t: 1798 internal_head_reverse_go(a, A, t, y, h <> acc) 1799 1800 # The head of the reverse is the last element. 1801 law head_reverse: 1802 for -a: Quant 1803 for -A: Kind(a) 1804 for xs: List 1805 {List.head(a, A, List.reverse(a, A, xs)) == List.last(a, A, xs) : Maybe} 1806 1807 def head_reverse(a, A, xs): 1808 match xs: 1809 case Nil{}: 1810 {==} 1811 case h <> t: 1812 internal_head_reverse_go(a, A, t, h, Nil{}) 1813 1814 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}: 1815 match xs: 1816 case Nil{}: 1817 {==} 1818 case y <> t: 1819 internal_last_reverse_go(a, A, t, y, h <> acc) 1820 1821 # The last element of the reverse is the head. 1822 law last_reverse: 1823 for -a: Quant 1824 for -A: Kind(a) 1825 for xs: List 1826 {List.last(a, A, List.reverse(a, A, xs)) == List.head(a, A, xs) : Maybe} 1827 1828 def last_reverse(a, A, xs): 1829 match xs: 1830 case Nil{}: 1831 {==} 1832 case h <> t: 1833 internal_last_reverse_go(a, A, t, h, Nil{}) 1834 1835 # A list is empty exactly when its length is zero. 1836 law is_empty_iff_length_eq_zero: 1837 for -a: Quant 1838 for -A: Kind(a) 1839 for xs: List 1840 {List.is_empty(a, A, xs) == Nat.is_eq(List.length(a, A, xs), 0n) : Bool} 1841 1842 def is_empty_iff_length_eq_zero(a, A, xs): 1843 match xs: 1844 case Nil{}: 1845 {==} 1846 case h <> t: 1847 {==} 1848 1849 # An append is empty exactly when both parts are. 1850 law is_empty_append: 1851 for -a: Quant 1852 for -A: Kind(a) 1853 for xs: List 1854 for -ys: List 1855 {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} 1856 1857 def is_empty_append(a, A, xs, ys): 1858 match xs: 1859 case Nil{}: 1860 {==} 1861 case h <> t: 1862 {==} 1863 1864 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}: 1865 match xs: 1866 case Nil{}: 1867 {==} 1868 case y <> t: 1869 internal_is_empty_reverse_go(a, A, t, y, h <> acc) 1870 1871 # The reverse is empty exactly when the list is. 1872 law is_empty_reverse: 1873 for -a: Quant 1874 for -A: Kind(a) 1875 for xs: List 1876 {List.is_empty(a, A, List.reverse(a, A, xs)) == List.is_empty(a, A, xs) : Bool} 1877 1878 def is_empty_reverse(a, A, xs): 1879 match xs: 1880 case Nil{}: 1881 {==} 1882 case h <> t: 1883 internal_is_empty_reverse_go(a, A, t, h, Nil{}) 1884 1885 # A map is empty exactly when the list is. 1886 law is_empty_map: 1887 for ~A: Type 1888 for ~B: Type 1889 for ~f: A -> B 1890 for xs: List 1891 {List.is_empty(&1, B, List.map(~A, ~B, ~f, xs)) == List.is_empty(&1, A, xs) : Bool} 1892 1893 def is_empty_map(A, B, f, xs): 1894 match xs: 1895 case Nil{}: 1896 {==} 1897 case h <> t: 1898 {==} 1899 1900 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>}: 1901 match b: 1902 case False{}: 1903 append_nil(&2, A, List.reverse(&2, A, r)) 1904 case True{}: 1905 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])) 1906 1907 # Filtering commutes with reversing: filter p (reverse xs) = reverse (filter p xs). 1908 law filter_reverse: 1909 for ~A: Data 1910 for ~f: A -> Bool 1911 for xs: List<&2, A> 1912 {List.filter(~A, ~f, List.reverse(&2, A, xs)) == List.reverse(&2, A, List.filter(~A, ~f, xs)) : List<&2, A>} 1913 1914 def filter_reverse(A, f, xs): 1915 match xs: 1916 case Nil{}: 1917 {==} 1918 case +h <> t: 1919 +t = t 1920 %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>} 1921 %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>} 1922 %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>} 1923 internal_reverse_filter_put(A, h, List.filter(~A, ~f, t), f(h)) 1924 1925 # Folding cons from the right, starting from the empty list, rebuilds the list. 1926 law foldr_cons_nil: 1927 for ~a: Quant 1928 for ~A: Kind(a) 1929 for xs: List 1930 {List.foldr(~a, ~A, ~List, ~(x => acc => x <> acc), xs, Nil{}) == xs : List} 1931 1932 def foldr_cons_nil(a, A, xs): 1933 match xs: 1934 case Nil{}: 1935 {==} 1936 case h <> t: 1937 %foldr_cons_nil(~a, ~A, t) : {h <> List.foldr(~a, ~A, ~List, ~(x => acc => x <> acc), t, Nil{}) == h <> _ : List} 1938 {==} 1939 1940 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}: 1941 match xs: 1942 case Nil{}: 1943 {==} 1944 case h <> t: 1945 internal_foldl_reverse_go(~a, ~A, ~B, ~f, t, h <> acc, z) 1946 1947 # A left fold over the reverse is a right fold with the arguments flipped. 1948 law foldl_reverse: 1949 for ~a: Quant 1950 for ~A: Kind(a) 1951 for ~B: Type 1952 for ~f: B -> A -> B 1953 for xs: List 1954 for -z: B 1955 {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} 1956 1957 def foldl_reverse(a, A, B, f, xs, z): 1958 internal_foldl_reverse_go(~a, ~A, ~B, ~f, xs, Nil{}, z) 1959 1960 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}: 1961 match xs: 1962 case Nil{}: 1963 {==} 1964 case h <> t: 1965 internal_foldr_reverse_go(~a, ~A, ~B, ~f, t, h <> acc, z) 1966 1967 # A right fold over the reverse is a left fold with the arguments flipped. 1968 law foldr_reverse: 1969 for ~a: Quant 1970 for ~A: Kind(a) 1971 for ~B: Type 1972 for ~f: A -> B -> B 1973 for xs: List 1974 for -z: B 1975 {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} 1976 1977 def foldr_reverse(a, A, B, f, xs, z): 1978 internal_foldr_reverse_go(~a, ~A, ~B, ~f, xs, Nil{}, z) 1979 1980 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>}: 1981 match n: 1982 case 0n: 1983 {==} 1984 case 1n+p: 1985 internal_range_go_append(p, p <> ys, acc) 1986 1987 # Range(n + 1) is range(n) followed by n. 1988 law range_succ: 1989 for n: Nat 1990 {List.range(1n+n) == List.append(&2, Nat, List.range(n), [n]) : List<&2, Nat>} 1991 1992 def range_succ(n): 1993 +n = n 1994 internal_range_go_append(n, Nil{}, [n]) 1995 1996 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>}: 1997 match b: 1998 case False{}: 1999 {==} 2000 case True{}: Lines 1-2000 of 3175. More: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/list.bend&start_line=2001