list.bend
bend-mathlib@0.3.0.0 · 1,218 lines · 0 definitions
1# bend-mathlib/list.bend: List lemmas (append, reverse, length, take, drop, map, fold, filter).
2import Base
3import bend-mathlib@0.3.0.0/nat.bend as MNat
4import bend-mathlib@0.3.0.0/bool.bend as MBool
5
6# The empty list is a right identity for append: xs ++ [] = xs.
7law append_nil:
8 for -a: Quant
9 for -A: Kind(a)
10 for xs: List<a, A>
11 {List.append(a, A, xs, Nil{}) == xs : List<a, A>}
12
13def append_nil(a, A, xs):
14 match xs:
15 case Nil{}:
16 {==}
17 case h <> t:
18 %append_nil(a, A, t) : {h <> List.append(a, A, t, Nil{}) == h <> _ : List<a, A>}
19 {==}
20
21# The empty list is a left identity for append: [] ++ xs = xs.
22law nil_append:
23 for -a: Quant
24 for -A: Kind(a)
25 for -xs: List<a, A>
26 {List.append(a, A, Nil{}, xs) == xs : List<a, A>}
27
28def nil_append(a, A, xs):
29 {==}
30
31# Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs).
32law append_assoc:
33 for -a: Quant
34 for -A: Kind(a)
35 for xs: List<a, A>
36 for -ys: List<a, A>
37 for -zs: List<a, A>
38 {List.append(a, A, List.append(a, A, xs, ys), zs) == List.append(a, A, xs, List.append(a, A, ys, zs)) : List<a, A>}
39
40def append_assoc(a, A, xs, ys, zs):
41 match xs:
42 case Nil{}:
43 {==}
44 case h <> t:
45 %append_assoc(a, A, t, ys, zs) : {h <> List.append(a, A, List.append(a, A, t, ys), zs) == h <> _ : List<a, A>}
46 {==}
47
48# The length of an append is the sum of the lengths.
49law length_append:
50 for -a: Quant
51 for -A: Kind(a)
52 for xs: List<a, A>
53 for -ys: List<a, A>
54 {List.length(a, A, List.append(a, A, xs, ys)) == Nat.add(List.length(a, A, xs), List.length(a, A, ys)) : Nat}
55
56def length_append(a, A, xs, ys):
57 match xs:
58 case Nil{}:
59 {==}
60 case h <> t:
61 %length_append(a, A, t, ys) : {1n+List.length(a, A, List.append(a, A, t, ys)) == 1n+_ : Nat}
62 {==}
63
64def internal_reverse_go_append(a, -A: Kind(a), xs: List<a, A>, -ys: List<a, A>, -acc: List<a, A>) -> {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<a, A>}:
65 match xs:
66 case Nil{}:
67 {==}
68 case h <> t:
69 internal_reverse_go_append(a, A, t, h <> ys, acc)
70
71# The reverse accumulator loop appends the reversed list to the accumulator.
72law reverse_go_spec:
73 for -a: Quant
74 for -A: Kind(a)
75 for xs: List<a, A>
76 for -acc: List<a, A>
77 {List.reverse.go(a, A, xs, acc) == List.append(a, A, List.reverse(a, A, xs), acc) : List<a, A>}
78
79def reverse_go_spec(a, A, xs, acc):
80 match xs:
81 case Nil{}:
82 {==}
83 case h <> t:
84 internal_reverse_go_append(a, A, t, h <> Nil{}, acc)
85
86def internal_reverse_append_go(a, -A: Kind(a), xs: List<a, A>, -ys: List<a, A>, -acc: List<a, A>) -> {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<a, A>}:
87 match xs:
88 case Nil{}:
89 {==}
90 case h <> t:
91 internal_reverse_append_go(a, A, t, ys, h <> acc)
92
93# Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs.
94law reverse_append:
95 for -a: Quant
96 for -A: Kind(a)
97 for xs: List<a, A>
98 for ys: List<a, A>
99 {List.reverse(a, A, List.append(a, A, xs, ys)) == List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) : List<a, A>}
100
101def reverse_append(a, A, xs, ys):
102 Equal.trans(List<a, A>, List.reverse(a, A, List.append(a, A, xs, ys)), List.reverse.go(a, A, ys, List.reverse(a, A, xs)), List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)), internal_reverse_append_go(a, A, xs, ys, Nil{}), reverse_go_spec(a, A, ys, List.reverse(a, A, xs)))
103
104def internal_reverse_go_go(a, -A: Kind(a), xs: List<a, A>, -acc: List<a, A>) -> {List.reverse.go(a, A, List.reverse.go(a, A, xs, acc), Nil{}) == List.reverse.go(a, A, acc, xs) : List<a, A>}:
105 match xs:
106 case Nil{}:
107 {==}
108 case h <> t:
109 internal_reverse_go_go(a, A, t, h <> acc)
110
111# Reversing twice gives the list back.
112law reverse_reverse:
113 for -a: Quant
114 for -A: Kind(a)
115 for xs: List<a, A>
116 {List.reverse(a, A, List.reverse(a, A, xs)) == xs : List<a, A>}
117
118def reverse_reverse(a, A, xs):
119 internal_reverse_go_go(a, A, xs, Nil{})
120
121def internal_length_reverse_go(a, -A: Kind(a), xs: List<a, A>, -acc: List<a, A>, +n: Nat, e: {List.length(a, A, acc) == n : Nat}) -> {List.length(a, A, List.reverse.go(a, A, xs, acc)) == Nat.add(n, List.length(a, A, xs)) : Nat}:
122 match xs:
123 case Nil{}:
124 %Equal.sym(Nat, Nat.add(n, 0n), n, MNat.add_zero(n)) : {List.length(a, A, acc) == _ : Nat}
125 e
126 case h <> t:
127 %Equal.sym(Nat, Nat.add(n, 1n+List.length(a, A, t)), 1n+Nat.add(n, List.length(a, A, t)), MNat.add_succ(n, List.length(a, A, t))) : {List.length(a, A, List.reverse.go(a, A, t, h <> acc)) == _ : Nat}
128 internal_length_reverse_go(a, A, t, h <> acc, 1n+n, Equal.cong(Nat, Nat, k => 1n+k, List.length(a, A, acc), n, e))
129
130# Reversing preserves the length.
131law length_reverse:
132 for -a: Quant
133 for -A: Kind(a)
134 for xs: List<a, A>
135 {List.length(a, A, List.reverse(a, A, xs)) == List.length(a, A, xs) : Nat}
136
137def length_reverse(a, A, xs):
138 internal_length_reverse_go(a, A, xs, Nil{}, 0n, {==})
139
140# A right fold over an append folds the first part onto the fold of the second.
141law foldr_append:
142 for ~a: Quant
143 for ~A: Kind(a)
144 for ~B: Type
145 for ~f: A -> B -> B
146 for xs: List<a, A>
147 for -ys: List<a, A>
148 for -z: B
149 {List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) == List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)) : B}
150
151def foldr_append(a, A, B, f, xs, ys, z):
152 match xs:
153 case Nil{}:
154 {==}
155 case h <> t:
156 %foldr_append(~a, ~A, ~B, ~f, t, ys, z) : {f(h, List.foldr(~a, ~A, ~B, ~f, List.append(a, A, t, ys), z)) == f(h, _) : B}
157 {==}
158
159# Taking n elements and appending the rest after dropping n gives the list back.
160law take_append_drop:
161 for -a: Quant
162 for -A: Kind(a)
163 for xs: List<a, A>
164 for n: Nat
165 {List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) == xs : List<a, A>}
166
167def take_append_drop(a, A, xs, n):
168 match xs n:
169 case Nil{} _:
170 {==}
171 case h <> t 0n:
172 {==}
173 case h <> t 1n+p:
174 %take_append_drop(a, A, t, p) : {h <> List.append(a, A, List.take(a, A, t, p), List.drop(a, A, t, p)) == h <> _ : List<a, A>}
175 {==}
176
177# Mapping preserves the length.
178law length_map:
179 for ~A: Type
180 for ~B: Type
181 for ~f: A -> B
182 for xs: List<A>
183 {List.length(&1, B, List.map(~A, ~B, ~f, xs)) == List.length(&1, A, xs) : Nat}
184
185def length_map(A, B, f, xs):
186 match xs:
187 case Nil{}:
188 {==}
189 case h <> t:
190 %length_map(~A, ~B, ~f, t) : {1n+List.length(&1, B, List.map(~A, ~B, ~f, t)) == 1n+_ : Nat}
191 {==}
192
193# Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys.
194law map_append:
195 for ~A: Type
196 for ~B: Type
197 for ~f: A -> B
198 for xs: List<A>
199 for -ys: List<A>
200 {List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)) == List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)) : List<B>}
201
202def map_append(A, B, f, xs, ys):
203 match xs:
204 case Nil{}:
205 {==}
206 case h <> t:
207 %map_append(~A, ~B, ~f, t, ys) : {f(h) <> List.map(~A, ~B, ~f, List.append(&1, A, t, ys)) == f(h) <> _ : List<B>}
208 {==}
209
210# Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs.
211law map_map:
212 for ~A: Type
213 for ~B: Type
214 for ~C: Type
215 for ~f: A -> B
216 for ~g: B -> C
217 for xs: List<A>
218 {List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~C, ~(x => g(f(x))), xs) : List<C>}
219
220def map_map(A, B, C, f, g, xs):
221 match xs:
222 case Nil{}:
223 {==}
224 case h <> t:
225 %map_map(~A, ~B, ~C, ~f, ~g, t) : {g(f(h)) <> List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, t)) == g(f(h)) <> _ : List<C>}
226 {==}
227
228# Taking zero elements gives the empty list.
229law take_zero:
230 for -a: Quant
231 for -A: Kind(a)
232 for xs: List<a, A>
233 {List.take(a, A, xs, 0n) == Nil{} : List<a, A>}
234
235def take_zero(a, A, xs):
236 match xs:
237 case Nil{}:
238 {==}
239 case h <> t:
240 {==}
241
242# Dropping zero elements gives the list back.
243law drop_zero:
244 for -a: Quant
245 for -A: Kind(a)
246 for xs: List<a, A>
247 {List.drop(a, A, xs, 0n) == xs : List<a, A>}
248
249def drop_zero(a, A, xs):
250 match xs:
251 case Nil{}:
252 {==}
253 case h <> t:
254 {==}
255
256# Taking from the empty list gives the empty list.
257law take_nil:
258 for -a: Quant
259 for -A: Kind(a)
260 for -n: Nat
261 {List.take(a, A, Nil{}, n) == Nil{} : List<a, A>}
262
263def take_nil(a, A, n):
264 {==}
265
266# Dropping from the empty list gives the empty list.
267law drop_nil:
268 for -a: Quant
269 for -A: Kind(a)
270 for -n: Nat
271 {List.drop(a, A, Nil{}, n) == Nil{} : List<a, A>}
272
273def drop_nil(a, A, n):
274 {==}
275
276# Taking n elements leaves min(n, length) of them.
277law length_take:
278 for -a: Quant
279 for -A: Kind(a)
280 for xs: List<a, A>
281 for n: Nat
282 {List.length(a, A, List.take(a, A, xs, n)) == Nat.min(n, List.length(a, A, xs)) : Nat}
283
284def length_take(a, A, xs, n):
285 match xs n:
286 case Nil{} _:
287 Equal.sym(Nat, Nat.min(n, 0n), 0n, MNat.min_zero(n))
288 case h <> t 0n:
289 {==}
290 case h <> t 1n+p:
291 %length_take(a, A, t, p) : {1n+List.length(a, A, List.take(a, A, t, p)) == 1n+_ : Nat}
292 {==}
293
294# Dropping n elements leaves length - n of them.
295law length_drop:
296 for -a: Quant
297 for -A: Kind(a)
298 for xs: List<a, A>
299 for n: Nat
300 {List.length(a, A, List.drop(a, A, xs, n)) == Nat.sub(List.length(a, A, xs), n) : Nat}
301
302def length_drop(a, A, xs, n):
303 match xs n:
304 case Nil{} _:
305 Equal.sym(Nat, Nat.sub(0n, n), 0n, MNat.zero_sub(n))
306 case h <> t 0n:
307 {==}
308 case h <> t 1n+p:
309 length_drop(a, A, t, p)
310
311# Taking as many elements as the list has gives the list back.
312law take_length:
313 for -A: Data
314 for +xs: List<&2, A>
315 {List.take(&2, A, xs, List.length(&2, A, xs)) == xs : List<&2, A>}
316
317def take_length(A, xs):
318 match xs:
319 case Nil{}:
320 {==}
321 case h <> t:
322 %take_length(A, t) : {h <> List.take(&2, A, t, List.length(&2, A, t)) == h <> _ : List<&2, A>}
323 {==}
324
325# Dropping as many elements as the list has gives the empty list.
326law drop_length:
327 for -A: Data
328 for +xs: List<&2, A>
329 {List.drop(&2, A, xs, List.length(&2, A, xs)) == Nil{} : List<&2, A>}
330
331def drop_length(A, xs):
332 match xs:
333 case Nil{}:
334 {==}
335 case h <> t:
336 drop_length(A, t)
337
338# Taking m from the first n is taking min(n, m).
339law take_take:
340 for -a: Quant
341 for -A: Kind(a)
342 for xs: List<a, A>
343 for n: Nat
344 for m: Nat
345 {List.take(a, A, List.take(a, A, xs, n), m) == List.take(a, A, xs, Nat.min(n, m)) : List<a, A>}
346
347def take_take(a, A, xs, n, m):
348 match xs n m:
349 case Nil{} _ _:
350 {==}
351 case h <> t 0n _:
352 {==}
353 case h <> t 1n+p 0n:
354 {==}
355 case h <> t 1n+p 1n+q:
356 %take_take(a, A, t, p, q) : {h <> List.take(a, A, List.take(a, A, t, p), q) == h <> _ : List<a, A>}
357 {==}
358
359# Dropping m after dropping n is dropping n + m.
360law drop_drop:
361 for -a: Quant
362 for -A: Kind(a)
363 for xs: List<a, A>
364 for n: Nat
365 for -m: Nat
366 {List.drop(a, A, List.drop(a, A, xs, n), m) == List.drop(a, A, xs, Nat.add(n, m)) : List<a, A>}
367
368def drop_drop(a, A, xs, n, m):
369 match xs n m:
370 case Nil{} _ _:
371 {==}
372 case h <> t 0n _:
373 {==}
374 case h <> t 1n+p _:
375 drop_drop(a, A, t, p, m)
376
377# Reversing the empty list gives the empty list.
378law reverse_nil:
379 for -a: Quant
380 for -A: Kind(a)
381 {List.reverse(a, A, Nil{}) == Nil{} : List<a, A>}
382
383def reverse_nil(a, A):
384 {==}
385
386# Reversing a one-element list gives it back.
387law reverse_singleton:
388 for -a: Quant
389 for -A: Kind(a)
390 for -x: A
391 {List.reverse(a, A, [x]) == [x] : List<a, A>}
392
393def reverse_singleton(a, A, x):
394 {==}
395
396# Replicating x n times gives a list of length n.
397law length_replicate:
398 for -A: Data
399 for n: Nat
400 for -x: A
401 {List.length(&2, A, List.replicate(A, n, x)) == n : Nat}
402
403def length_replicate(A, n, x):
404 match n:
405 case 0n:
406 {==}
407 case 1n+p:
408 %length_replicate(A, p, x) : {1n+List.length(&2, A, List.replicate(A, p, x)) == 1n+_ : Nat}
409 {==}
410
411# Range(n) has length n.
412law length_range:
413 for n: Nat
414 {List.length(&2, Nat, List.range(n)) == n : Nat}
415
416def internal_length_range_go(+n: Nat, acc: List<&2, Nat>) -> {List.length(&2, Nat, List.range.go(n, acc)) == Nat.add(n, List.length(&2, Nat, acc)) : Nat}:
417 match n:
418 case 0n:
419 {==}
420 case 1n+p:
421 %MNat.add_succ(p, List.length(&2, Nat, acc)) : {List.length(&2, Nat, List.range.go(p, p <> acc)) == _ : Nat}
422 internal_length_range_go(p, p <> acc)
423
424def length_range(n):
425 +n = n
426 %Equal.sym(Nat, List.length(&2, Nat, List.range.go(n, Nil{})), Nat.add(n, 0n), internal_length_range_go(n, Nil{})) : {_ == n : Nat}
427 MNat.add_zero(n)
428
429# Zipping two lists gives the length of the shorter one.
430law length_zip:
431 for -a: Quant
432 for -A: Kind(a)
433 for xs: List<a, A>
434 for ys: List<a, A>
435 {List.length(&1, A & A, List.zip(a, A, a, A, xs, ys)) == Nat.min(List.length(a, A, xs), List.length(a, A, ys)) : Nat}
436
437def length_zip(a, A, xs, ys):
438 match xs ys:
439 case Nil{} _:
440 {==}
441 case h <> t Nil{}:
442 {==}
443 case h <> t y <> yt:
444 %length_zip(a, A, t, yt) : {1n+List.length(&1, A & A, List.zip(a, A, a, A, t, yt)) == 1n+_ : Nat}
445 {==}
446
447# Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys).
448law append_cons:
449 for -a: Quant
450 for -A: Kind(a)
451 for -x: A
452 for -xs: List<a, A>
453 for -ys: List<a, A>
454 {List.append(a, A, x <> xs, ys) == x <> List.append(a, A, xs, ys) : List<a, A>}
455
456def append_cons(a, A, x, xs, ys):
457 {==}
458
459# The empty list has length zero.
460law length_nil:
461 for -a: Quant
462 for -A: Kind(a)
463 {List.length(a, A, Nil{}) == 0n : Nat}
464
465def length_nil(a, A):
466 {==}
467
468# A cons is one longer than its tail.
469law length_cons:
470 for -a: Quant
471 for -A: Kind(a)
472 for -x: A
473 for -xs: List<a, A>
474 {List.length(a, A, x <> xs) == 1n+List.length(a, A, xs) : Nat}
475
476def length_cons(a, A, x, xs):
477 {==}
478
479# Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss.
480law concat_append:
481 for -a: Quant
482 for -A: Kind(a)
483 for xss: List<a, List<a, A>>
484 for -yss: List<a, List<a, A>>
485 {List.concat(a, A, List.append(a, List<a, A>, xss, yss)) == List.append(a, A, List.concat(a, A, xss), List.concat(a, A, yss)) : List<a, A>}
486
487def concat_append(a, A, xss, yss):
488 match xss:
489 case Nil{}:
490 {==}
491 case h <> t:
492 %Equal.sym(List<a, A>, List.concat(a, A, List.append(a, List<a, A>, 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<a, A>}
493 Equal.sym(List<a, A>, List.append(a, A, List.append(a, A, h, List.concat(a, A, t)), List.concat(a, A, yss)), List.append(a, A, h, List.append(a, A, List.concat(a, A, t), List.concat(a, A, yss))), append_assoc(a, A, h, List.concat(a, A, t), List.concat(a, A, yss)))
494
495# A left fold over an append folds the second part from the fold of the first.
496law foldl_append:
497 for ~a: Quant
498 for ~A: Kind(a)
499 for ~B: Type
500 for ~f: B -> A -> B
501 for xs: List<a, A>
502 for -ys: List<a, A>
503 for -z: B
504 {List.foldl(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) == List.foldl(~a, ~A, ~B, ~f, ys, List.foldl(~a, ~A, ~B, ~f, xs, z)) : B}
505
506def foldl_append(a, A, B, f, xs, ys, z):
507 match xs:
508 case Nil{}:
509 {==}
510 case h <> t:
511 foldl_append(~a, ~A, ~B, ~f, t, ys, f(z, h))
512
513# Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs).
514law map_reverse:
515 for ~A: Type
516 for ~B: Type
517 for ~f: A -> B
518 for xs: List<A>
519 {List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) == List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) : List<B>}
520
521def internal_map_reverse_go(~A: Type, ~B: Type, ~f: A -> B, xs: List<A>, acc: List<A>) -> {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<B>}:
522 match xs:
523 case Nil{}:
524 {==}
525 case h <> t:
526 internal_map_reverse_go(~A, ~B, ~f, t, h <> acc)
527
528def map_reverse(A, B, f, xs):
529 internal_map_reverse_go(~A, ~B, ~f, xs, Nil{})
530
531# All over an append is all over each part, joined by and.
532law all_append:
533 for ~a: Quant
534 for ~A: Kind(a)
535 for ~f: A -> Bool
536 for xs: List<a, A>
537 for -ys: List<a, A>
538 {List.all(~a, ~A, ~f, List.append(a, A, xs, ys)) == Bool.and(List.all(~a, ~A, ~f, xs), List.all(~a, ~A, ~f, ys)) : Bool}
539
540def all_append(a, A, f, xs, ys):
541 match xs:
542 case Nil{}:
543 {==}
544 case h <> t:
545 %Equal.sym(Bool, List.all(~a, ~A, ~f, List.append(a, A, t, ys)), Bool.and(List.all(~a, ~A, ~f, t), List.all(~a, ~A, ~f, ys)), all_append(~a, ~A, ~f, t, ys)) : {Bool.and(f(h), _) == Bool.and(Bool.and(f(h), List.all(~a, ~A, ~f, t)), List.all(~a, ~A, ~f, ys)) : Bool}
546 Equal.sym(Bool, Bool.and(Bool.and(f(h), List.all(~a, ~A, ~f, t)), List.all(~a, ~A, ~f, ys)), Bool.and(f(h), Bool.and(List.all(~a, ~A, ~f, t), List.all(~a, ~A, ~f, ys))), MBool.and_assoc(f(h), List.all(~a, ~A, ~f, t), List.all(~a, ~A, ~f, ys)))
547
548# Any over an append is any over each part, joined by or.
549law any_append:
550 for ~a: Quant
551 for ~A: Kind(a)
552 for ~f: A -> Bool
553 for xs: List<a, A>
554 for -ys: List<a, A>
555 {List.any(~a, ~A, ~f, List.append(a, A, xs, ys)) == Bool.or(List.any(~a, ~A, ~f, xs), List.any(~a, ~A, ~f, ys)) : Bool}
556
557def any_append(a, A, f, xs, ys):
558 match xs:
559 case Nil{}:
560 {==}
561 case h <> t:
562 %Equal.sym(Bool, List.any(~a, ~A, ~f, List.append(a, A, t, ys)), Bool.or(List.any(~a, ~A, ~f, t), List.any(~a, ~A, ~f, ys)), any_append(~a, ~A, ~f, t, ys)) : {Bool.or(f(h), _) == Bool.or(Bool.or(f(h), List.any(~a, ~A, ~f, t)), List.any(~a, ~A, ~f, ys)) : Bool}
563 Equal.sym(Bool, Bool.or(Bool.or(f(h), List.any(~a, ~A, ~f, t)), List.any(~a, ~A, ~f, ys)), Bool.or(f(h), Bool.or(List.any(~a, ~A, ~f, t), List.any(~a, ~A, ~f, ys))), MBool.or_assoc(f(h), List.any(~a, ~A, ~f, t), List.any(~a, ~A, ~f, ys)))
564
565# Filtering an append filters each part.
566law filter_append:
567 for ~A: Data
568 for ~f: A -> Bool
569 for xs: List<&2, A>
570 for ys: List<&2, A>
571 {List.filter(~A, ~f, List.append(&2, A, xs, ys)) == List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)) : List<&2, A>}
572
573def internal_filter_put_append(-A: Data, h: A, r: List<&2, A>, s: List<&2, A>, b: Bool) -> {List.append(&2, A, List.filter.put(A, h, r, b), s) == List.filter.put(A, h, List.append(&2, A, r, s), b) : List<&2, A>}:
574 match b:
575 case False{}:
576 {==}
577 case True{}:
578 {==}
579
580def filter_append(A, f, xs, ys):
581 match xs:
582 case Nil{}:
583 {==}
584 case +h <> t:
585 +ys = ys
586 +t = t
587 %Equal.sym(List<&2, A>, List.filter(~A, ~f, List.append(&2, A, t, ys)), List.append(&2, A, List.filter(~A, ~f, t), List.filter(~A, ~f, ys)), filter_append(~A, ~f, t, ys)) : {List.filter.put(A, h, _, f(h)) == List.append(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h)), List.filter(~A, ~f, ys)) : List<&2, A>}
588 Equal.sym(List<&2, A>, List.append(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h)), List.filter(~A, ~f, ys)), List.filter.put(A, h, List.append(&2, A, List.filter(~A, ~f, t), List.filter(~A, ~f, ys)), f(h)), internal_filter_put_append(A, h, List.filter(~A, ~f, t), List.filter(~A, ~f, ys), f(h)))
589
590# An append contains x iff either part does.
591law contains_append:
592 for ~A: Data
593 for ~eq: A -> A -> Bool
594 for xs: List<&2, A>
595 for -ys: List<&2, A>
596 for +x: A
597 {List.contains(~A, ~eq, List.append(&2, A, xs, ys), x) == Bool.or(List.contains(~A, ~eq, xs, x), List.contains(~A, ~eq, ys, x)) : Bool}
598
599def contains_append(A, eq, xs, ys, x):
600 match xs:
601 case Nil{}:
602 {==}
603 case h <> t:
604 %Equal.sym(Bool, List.contains(~A, ~eq, List.append(&2, A, t, ys), x), Bool.or(List.contains(~A, ~eq, t, x), List.contains(~A, ~eq, ys, x)), contains_append(~A, ~eq, t, ys, x)) : {Bool.or(eq(h, x), _) == Bool.or(Bool.or(eq(h, x), List.contains(~A, ~eq, t, x)), List.contains(~A, ~eq, ys, x)) : Bool}
605 Equal.sym(Bool, Bool.or(Bool.or(eq(h, x), List.contains(~A, ~eq, t, x)), List.contains(~A, ~eq, ys, x)), Bool.or(eq(h, x), Bool.or(List.contains(~A, ~eq, t, x), List.contains(~A, ~eq, ys, x))), MBool.or_assoc(eq(h, x), List.contains(~A, ~eq, t, x), List.contains(~A, ~eq, ys, x)))
606
607# Filtering never makes a list longer.
608law length_filter_le:
609 for ~A: Data
610 for ~f: A -> Bool
611 for xs: List<&2, A>
612 {Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)) == True{} : Bool}
613
614def internal_length_filter_put_le(-A: Data, h: A, r: List<&2, A>, b: Bool) -> {Nat.is_le(List.length(&2, A, List.filter.put(A, h, r, b)), 1n+List.length(&2, A, r)) == True{} : Bool}:
615 match b:
616 case False{}:
617 MNat.le_succ(List.length(&2, A, r))
618 case True{}:
619 MNat.le_refl(1n+List.length(&2, A, r))
620
621def length_filter_le(A, f, xs):
622 match xs:
623 case Nil{}:
624 {==}
625 case +h <> t:
626 +t = t
627 MNat.le_trans(List.length(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))), 1n+List.length(&2, A, List.filter(~A, ~f, t)), 1n+List.length(&2, A, t), internal_length_filter_put_le(A, h, List.filter(~A, ~f, t), f(h)), MNat.succ_le_succ(List.length(&2, A, List.filter(~A, ~f, t)), List.length(&2, A, t), length_filter_le(~A, ~f, t)))
628
629# Membership in a list, as a reusable proposition.
630def mem(~A: Data, ~eq: A -> A -> Bool, +x: A, xs: List<&2, A>) -> Data:
631 {List.contains(~A, ~eq, xs, x) == True{} : Bool}
632
633# A list is sorted by a comparator when every adjacent pair is in order.
634def sorted_by(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>) -> Data:
635 {List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), List.zip(&2, A, &2, A, xs, List.tail(&2, A, xs))) == True{} : Bool}
636
637def internal_or_of_right(a: Bool, -b: Bool, hb: {b == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}:
638 match a:
639 case False{}:
640 hb
641 case True{}:
642 {==}
643
644def internal_or_of_or(a: Bool, -b: Bool, -c: Bool, h: {Bool.or(a, b) == True{} : Bool}, k: {b == True{} : Bool} -> {c == True{} : Bool}) -> {Bool.or(a, c) == True{} : Bool}:
645 match a:
646 case False{}:
647 k(h)
648 case True{}:
649 {==}
650
651def internal_and_left(a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
652 match a:
653 case False{}:
654 Empty.absurd({False{} == True{} : Bool}, MNat.internal_false_ne_true(h))
655 case True{}:
656 {==}
657
658def internal_and_right(a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
659 match a:
660 case False{}:
661 Empty.absurd({b == True{} : Bool}, MNat.internal_false_ne_true(h))
662 case True{}:
663 h
664
665def internal_mem_append_left(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +x: Nat, h: {List.contains(~Nat, ~Nat.is_eq, xs, x) == True{} : Bool}) -> {List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, xs, ys), x) == True{} : Bool}:
666 match xs:
667 case Nil{}:
668 Empty.absurd({List.contains(~Nat, ~Nat.is_eq, ys, x) == True{} : Bool}, MNat.internal_false_ne_true(h))
669 case hd <> tl:
670 internal_or_of_or(Nat.is_eq(hd, x), List.contains(~Nat, ~Nat.is_eq, tl, x), List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, tl, ys), x), h, internal_mem_append_left(tl, ys, x))
671
672def internal_mem_append_right(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +x: Nat, h: {List.contains(~Nat, ~Nat.is_eq, ys, x) == True{} : Bool}) -> {List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, xs, ys), x) == True{} : Bool}:
673 match xs:
674 case Nil{}:
675 h
676 case hd <> tl:
677 internal_or_of_right(Nat.is_eq(hd, x), List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, tl, ys), x), internal_mem_append_right(tl, ys, x, h))
678
679# The head of a cons is a member of it.
680law mem_cons_self:
681 for x: Nat
682 for -xs: List<&2, Nat>
683 mem(~Nat, ~Nat.is_eq, x, x <> xs)
684
685def mem_cons_self(x, xs):
686 %Equal.sym(Bool, Nat.is_eq(x, x), True{}, MNat.is_eq_refl(x)) : {Bool.or(_, List.contains(~Nat, ~Nat.is_eq, xs, x)) == True{} : Bool}
687 {==}
688
689# Membership is preserved when a new head is prepended.
690law mem_cons_of_mem:
691 for x: Nat
692 for y: Nat
693 for -xs: List<&2, Nat>
694 for h: mem(~Nat, ~Nat.is_eq, x, xs)
695 mem(~Nat, ~Nat.is_eq, x, y <> xs)
696
697def mem_cons_of_mem(x, y, xs, h):
698 +x = x
699 internal_or_of_right(Nat.is_eq(y, x), List.contains(~Nat, ~Nat.is_eq, xs, x), h)
700
701# Nothing is a member of the empty list.
702law not_mem_nil:
703 for -x: Nat
704 mem(~Nat, ~Nat.is_eq, x, Nil{}) -> Empty
705
706def not_mem_nil(x, h):
707 MNat.internal_false_ne_true(h)
708
709# Membership on the left of an append.
710law mem_append_left:
711 for xs: List<&2, Nat>
712 for ys: List<&2, Nat>
713 for x: Nat
714 for h: mem(~Nat, ~Nat.is_eq, x, xs)
715 mem(~Nat, ~Nat.is_eq, x, List.append(&2, Nat, xs, ys))
716
717def mem_append_left(xs, ys, x, h):
718 internal_mem_append_left(xs, ys, x, h)
719
720# Membership on the right of an append.
721law mem_append_right:
722 for xs: List<&2, Nat>
723 for ys: List<&2, Nat>
724 for x: Nat
725 for h: mem(~Nat, ~Nat.is_eq, x, ys)
726 mem(~Nat, ~Nat.is_eq, x, List.append(&2, Nat, xs, ys))
727
728def mem_append_right(xs, ys, x, h):
729 internal_mem_append_right(xs, ys, x, h)
730
731# The empty list is sorted by any comparator.
732law sorted_nil:
733 sorted_by(~Nat, ~Nat.is_le, Nil{})
734
735def sorted_nil():
736 {==}
737
738# A singleton list is sorted by any comparator.
739law sorted_single:
740 for -x: Nat
741 sorted_by(~Nat, ~Nat.is_le, [x])
742
743def sorted_single(x):
744 {==}
745
746# A sorted tail with an in-order head is sorted.
747law sorted_cons_cons_intro:
748 for -x: Nat
749 for -y: Nat
750 for -t: List<&2, Nat>
751 for hxy: MNat.le(x, y)
752 for hyt: sorted_by(~Nat, ~Nat.is_le, y <> t)
753 sorted_by(~Nat, ~Nat.is_le, x <> y <> t)
754
755def sorted_cons_cons_intro(x, y, t, hxy, hyt):
756 %Equal.sym(Bool, Nat.is_le(x, y), True{}, hxy) : {Bool.and(_, List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t))) == True{} : Bool}
757 hyt
758
759# The head pair of a sorted cons-cons list is in order.
760law sorted_cons_cons_elim_le:
761 for x: Nat
762 for y: Nat
763 for -t: List<&2, Nat>
764 for h: sorted_by(~Nat, ~Nat.is_le, x <> y <> t)
765 MNat.le(x, y)
766
767def sorted_cons_cons_elim_le(x, y, t, h):
768 internal_and_left(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), h)
769
770# The tail of a sorted cons-cons list is sorted.
771law sorted_cons_cons_elim_tail:
772 for x: Nat
773 for y: Nat
774 for -t: List<&2, Nat>
775 for h: sorted_by(~Nat, ~Nat.is_le, x <> y <> t)
776 sorted_by(~Nat, ~Nat.is_le, y <> t)
777
778def sorted_cons_cons_elim_tail(x, y, t, h):
779 internal_and_right(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), h)
780
781# A sorted list has a sorted tail.
782law sorted_tail:
783 for x: Nat
784 for xs: List<&2, Nat>
785 for h: sorted_by(~Nat, ~Nat.is_le, x <> xs)
786 sorted_by(~Nat, ~Nat.is_le, xs)
787
788def sorted_tail(x, xs, h):
789 match xs:
790 case Nil{}:
791 {==}
792 case y <> t:
793 internal_and_right(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), h)
794
795# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
796
797# The empty list is a right identity for append: xs ++ [] = xs, reversed to rewrite toward the simple side.
798law append_nil_sym:
799 for -a: Quant
800 for -A: Kind(a)
801 for xs: List<a, A>
802 {xs == List.append(a, A, xs, Nil{}) : List<a, A>}
803
804def append_nil_sym(a, A, xs):
805 Equal.sym(List<a, A>, List.append(a, A, xs, Nil{}), xs, append_nil(a, A, xs))
806
807# The empty list is a left identity for append: [] ++ xs = xs, reversed to rewrite toward the simple side.
808law nil_append_sym:
809 for -a: Quant
810 for -A: Kind(a)
811 for -xs: List<a, A>
812 {xs == List.append(a, A, Nil{}, xs) : List<a, A>}
813
814def nil_append_sym(a, A, xs):
815 Equal.sym(List<a, A>, List.append(a, A, Nil{}, xs), xs, nil_append(a, A, xs))
816
817# Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs), reversed to rewrite toward the simple side.
818law append_assoc_sym:
819 for -a: Quant
820 for -A: Kind(a)
821 for xs: List<a, A>
822 for -ys: List<a, A>
823 for -zs: List<a, A>
824 {List.append(a, A, xs, List.append(a, A, ys, zs)) == List.append(a, A, List.append(a, A, xs, ys), zs) : List<a, A>}
825
826def append_assoc_sym(a, A, xs, ys, zs):
827 Equal.sym(List<a, A>, 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))
828
829# The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.
830law length_append_sym:
831 for -a: Quant
832 for -A: Kind(a)
833 for xs: List<a, A>
834 for -ys: List<a, A>
835 {Nat.add(List.length(a, A, xs), List.length(a, A, ys)) == List.length(a, A, List.append(a, A, xs, ys)) : Nat}
836
837def length_append_sym(a, A, xs, ys):
838 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))
839
840# The reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side.
841law reverse_go_spec_sym:
842 for -a: Quant
843 for -A: Kind(a)
844 for xs: List<a, A>
845 for -acc: List<a, A>
846 {List.append(a, A, List.reverse(a, A, xs), acc) == List.reverse.go(a, A, xs, acc) : List<a, A>}
847
848def reverse_go_spec_sym(a, A, xs, acc):
849 Equal.sym(List<a, A>, List.reverse.go(a, A, xs, acc), List.append(a, A, List.reverse(a, A, xs), acc), reverse_go_spec(a, A, xs, acc))
850
851# Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side.
852law reverse_append_sym:
853 for -a: Quant
854 for -A: Kind(a)
855 for xs: List<a, A>
856 for ys: List<a, A>
857 {List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) == List.reverse(a, A, List.append(a, A, xs, ys)) : List<a, A>}
858
859def reverse_append_sym(a, A, xs, ys):
860 Equal.sym(List<a, A>, List.reverse(a, A, List.append(a, A, xs, ys)), List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)), reverse_append(a, A, xs, ys))
861
862# Reversing twice gives the list back, reversed to rewrite toward the simple side.
863law reverse_reverse_sym:
864 for -a: Quant
865 for -A: Kind(a)
866 for xs: List<a, A>
867 {xs == List.reverse(a, A, List.reverse(a, A, xs)) : List<a, A>}
868
869def reverse_reverse_sym(a, A, xs):
870 Equal.sym(List<a, A>, List.reverse(a, A, List.reverse(a, A, xs)), xs, reverse_reverse(a, A, xs))
871
872# Reversing preserves the length, reversed to rewrite toward the simple side.
873law length_reverse_sym:
874 for -a: Quant
875 for -A: Kind(a)
876 for xs: List<a, A>
877 {List.length(a, A, xs) == List.length(a, A, List.reverse(a, A, xs)) : Nat}
878
879def length_reverse_sym(a, A, xs):
880 Equal.sym(Nat, List.length(a, A, List.reverse(a, A, xs)), List.length(a, A, xs), length_reverse(a, A, xs))
881
882# A right fold over an append folds the first part onto the fold of the second, reversed to rewrite toward the simple side.
883law foldr_append_sym:
884 for ~a: Quant
885 for ~A: Kind(a)
886 for ~B: Type
887 for ~f: A -> B -> B
888 for xs: List<a, A>
889 for -ys: List<a, A>
890 for -z: B
891 {List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)) == List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) : B}
892
893def foldr_append_sym(a, A, B, f, xs, ys, z):
894 Equal.sym(B, List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z), List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)), foldr_append(~a, ~A, ~B, ~f, xs, ys, z))
895
896# Taking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side.
897law take_append_drop_sym:
898 for -a: Quant
899 for -A: Kind(a)
900 for xs: List<a, A>
901 for n: Nat
902 {xs == List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) : List<a, A>}
903
904def take_append_drop_sym(a, A, xs, n):
905 Equal.sym(List<a, A>, List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)), xs, take_append_drop(a, A, xs, n))
906
907# Mapping preserves the length, reversed to rewrite toward the simple side.
908law length_map_sym:
909 for ~A: Type
910 for ~B: Type
911 for ~f: A -> B
912 for xs: List<A>
913 {List.length(&1, A, xs) == List.length(&1, B, List.map(~A, ~B, ~f, xs)) : Nat}
914
915def length_map_sym(A, B, f, xs):
916 Equal.sym(Nat, List.length(&1, B, List.map(~A, ~B, ~f, xs)), List.length(&1, A, xs), length_map(~A, ~B, ~f, xs))
917
918# Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side.
919law map_append_sym:
920 for ~A: Type
921 for ~B: Type
922 for ~f: A -> B
923 for xs: List<A>
924 for -ys: List<A>
925 {List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)) == List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)) : List<B>}
926
927def map_append_sym(A, B, f, xs, ys):
928 Equal.sym(List<B>, List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)), List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)), map_append(~A, ~B, ~f, xs, ys))
929
930# Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs, reversed to rewrite toward the simple side.
931law map_map_sym:
932 for ~A: Type
933 for ~B: Type
934 for ~C: Type
935 for ~f: A -> B
936 for ~g: B -> C
937 for xs: List<A>
938 {List.map(~A, ~C, ~(x => g(f(x))), xs) == List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) : List<C>}
939
940def map_map_sym(A, B, C, f, g, xs):
941 Equal.sym(List<C>, List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)), List.map(~A, ~C, ~(x => g(f(x))), xs), map_map(~A, ~B, ~C, ~f, ~g, xs))
942
943# Taking zero elements gives the empty list, reversed to rewrite toward the simple side.
944law take_zero_sym:
945 for -a: Quant
946 for -A: Kind(a)
947 for xs: List<a, A>
948 {Nil{} == List.take(a, A, xs, 0n) : List<a, A>}
949
950def take_zero_sym(a, A, xs):
951 Equal.sym(List<a, A>, List.take(a, A, xs, 0n), Nil{}, take_zero(a, A, xs))
952
953# Dropping zero elements gives the list back, reversed to rewrite toward the simple side.
954law drop_zero_sym:
955 for -a: Quant
956 for -A: Kind(a)
957 for xs: List<a, A>
958 {xs == List.drop(a, A, xs, 0n) : List<a, A>}
959
960def drop_zero_sym(a, A, xs):
961 Equal.sym(List<a, A>, List.drop(a, A, xs, 0n), xs, drop_zero(a, A, xs))
962
963# Taking from the empty list gives the empty list, reversed to rewrite toward the simple side.
964law take_nil_sym:
965 for -a: Quant
966 for -A: Kind(a)
967 for -n: Nat
968 {Nil{} == List.take(a, A, Nil{}, n) : List<a, A>}
969
970def take_nil_sym(a, A, n):
971 Equal.sym(List<a, A>, List.take(a, A, Nil{}, n), Nil{}, take_nil(a, A, n))
972
973# Dropping from the empty list gives the empty list, reversed to rewrite toward the simple side.
974law drop_nil_sym:
975 for -a: Quant
976 for -A: Kind(a)
977 for -n: Nat
978 {Nil{} == List.drop(a, A, Nil{}, n) : List<a, A>}
979
980def drop_nil_sym(a, A, n):
981 Equal.sym(List<a, A>, List.drop(a, A, Nil{}, n), Nil{}, drop_nil(a, A, n))
982
983# Taking n elements leaves min(n, length) of them, reversed to rewrite toward the simple side.
984law length_take_sym:
985 for -a: Quant
986 for -A: Kind(a)
987 for xs: List<a, A>
988 for n: Nat
989 {Nat.min(n, List.length(a, A, xs)) == List.length(a, A, List.take(a, A, xs, n)) : Nat}
990
991def length_take_sym(a, A, xs, n):
992 Equal.sym(Nat, List.length(a, A, List.take(a, A, xs, n)), Nat.min(n, List.length(a, A, xs)), length_take(a, A, xs, n))
993
994# Dropping n elements leaves length - n of them, reversed to rewrite toward the simple side.
995law length_drop_sym:
996 for -a: Quant
997 for -A: Kind(a)
998 for xs: List<a, A>
999 for n: Nat
1000 {Nat.sub(List.length(a, A, xs), n) == List.length(a, A, List.drop(a, A, xs, n)) : Nat}
1001
1002def length_drop_sym(a, A, xs, n):
1003 Equal.sym(Nat, List.length(a, A, List.drop(a, A, xs, n)), Nat.sub(List.length(a, A, xs), n), length_drop(a, A, xs, n))
1004
1005# Taking as many elements as the list has gives the list back, reversed to rewrite toward the simple side.
1006law take_length_sym:
1007 for -A: Data
1008 for +xs: List<&2, A>
1009 {xs == List.take(&2, A, xs, List.length(&2, A, xs)) : List<&2, A>}
1010
1011def take_length_sym(A, xs):
1012 Equal.sym(List<&2, A>, List.take(&2, A, xs, List.length(&2, A, xs)), xs, take_length(A, xs))
1013
1014# Dropping as many elements as the list has gives the empty list, reversed to rewrite toward the simple side.
1015law drop_length_sym:
1016 for -A: Data
1017 for +xs: List<&2, A>
1018 {Nil{} == List.drop(&2, A, xs, List.length(&2, A, xs)) : List<&2, A>}
1019
1020def drop_length_sym(A, xs):
1021 Equal.sym(List<&2, A>, List.drop(&2, A, xs, List.length(&2, A, xs)), Nil{}, drop_length(A, xs))
1022
1023# Taking m from the first n is taking min(n, m), reversed to rewrite toward the simple side.
1024law take_take_sym:
1025 for -a: Quant
1026 for -A: Kind(a)
1027 for xs: List<a, A>
1028 for n: Nat
1029 for m: Nat
1030 {List.take(a, A, xs, Nat.min(n, m)) == List.take(a, A, List.take(a, A, xs, n), m) : List<a, A>}
1031
1032def take_take_sym(a, A, xs, n, m):
1033 Equal.sym(List<a, A>, List.take(a, A, List.take(a, A, xs, n), m), List.take(a, A, xs, Nat.min(n, m)), take_take(a, A, xs, n, m))
1034
1035# Dropping m after dropping n is dropping n + m, reversed to rewrite toward the simple side.
1036law drop_drop_sym:
1037 for -a: Quant
1038 for -A: Kind(a)
1039 for xs: List<a, A>
1040 for n: Nat
1041 for -m: Nat
1042 {List.drop(a, A, xs, Nat.add(n, m)) == List.drop(a, A, List.drop(a, A, xs, n), m) : List<a, A>}
1043
1044def drop_drop_sym(a, A, xs, n, m):
1045 Equal.sym(List<a, A>, List.drop(a, A, List.drop(a, A, xs, n), m), List.drop(a, A, xs, Nat.add(n, m)), drop_drop(a, A, xs, n, m))
1046
1047# Reversing the empty list gives the empty list, reversed to rewrite toward the simple side.
1048law reverse_nil_sym:
1049 for -a: Quant
1050 for -A: Kind(a)
1051 {Nil{} == List.reverse(a, A, Nil{}) : List<a, A>}
1052
1053def reverse_nil_sym(a, A):
1054 Equal.sym(List<a, A>, List.reverse(a, A, Nil{}), Nil{}, reverse_nil(a, A))
1055
1056# Reversing a one-element list gives it back, reversed to rewrite toward the simple side.
1057law reverse_singleton_sym:
1058 for -a: Quant
1059 for -A: Kind(a)
1060 for -x: A
1061 {[x] == List.reverse(a, A, [x]) : List<a, A>}
1062
1063def reverse_singleton_sym(a, A, x):
1064 Equal.sym(List<a, A>, List.reverse(a, A, [x]), [x], reverse_singleton(a, A, x))
1065
1066# Replicating x n times gives a list of length n, reversed to rewrite toward the simple side.
1067law length_replicate_sym:
1068 for -A: Data
1069 for n: Nat
1070 for -x: A
1071 {n == List.length(&2, A, List.replicate(A, n, x)) : Nat}
1072
1073def length_replicate_sym(A, n, x):
1074 Equal.sym(Nat, List.length(&2, A, List.replicate(A, n, x)), n, length_replicate(A, n, x))
1075
1076# Range(n) has length n, reversed to rewrite toward the simple side.
1077law length_range_sym:
1078 for n: Nat
1079 {n == List.length(&2, Nat, List.range(n)) : Nat}
1080
1081def length_range_sym(n):
1082 Equal.sym(Nat, List.length(&2, Nat, List.range(n)), n, length_range(n))
1083
1084# Zipping two lists gives the length of the shorter one, reversed to rewrite toward the simple side.
1085law length_zip_sym:
1086 for -a: Quant
1087 for -A: Kind(a)
1088 for xs: List<a, A>
1089 for ys: List<a, A>
1090 {Nat.min(List.length(a, A, xs), List.length(a, A, ys)) == List.length(&1, A & A, List.zip(a, A, a, A, xs, ys)) : Nat}
1091
1092def length_zip_sym(a, A, xs, ys):
1093 Equal.sym(Nat, List.length(&1, A & A, List.zip(a, A, a, A, xs, ys)), Nat.min(List.length(a, A, xs), List.length(a, A, ys)), length_zip(a, A, xs, ys))
1094
1095# Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys), reversed to rewrite toward the simple side.
1096law append_cons_sym:
1097 for -a: Quant
1098 for -A: Kind(a)
1099 for -x: A
1100 for -xs: List<a, A>
1101 for -ys: List<a, A>
1102 {x <> List.append(a, A, xs, ys) == List.append(a, A, x <> xs, ys) : List<a, A>}
1103
1104def append_cons_sym(a, A, x, xs, ys):
1105 Equal.sym(List<a, A>, List.append(a, A, x <> xs, ys), x <> List.append(a, A, xs, ys), append_cons(a, A, x, xs, ys))
1106
1107# The empty list has length zero, reversed to rewrite toward the simple side.
1108law length_nil_sym:
1109 for -a: Quant
1110 for -A: Kind(a)
1111 {0n == List.length(a, A, Nil{}) : Nat}
1112
1113def length_nil_sym(a, A):
1114 Equal.sym(Nat, List.length(a, A, Nil{}), 0n, length_nil(a, A))
1115
1116# A cons is one longer than its tail, reversed to rewrite toward the simple side.
1117law length_cons_sym:
1118 for -a: Quant
1119 for -A: Kind(a)
1120 for -x: A
1121 for -xs: List<a, A>
1122 {1n+List.length(a, A, xs) == List.length(a, A, x <> xs) : Nat}
1123
1124def length_cons_sym(a, A, x, xs):
1125 Equal.sym(Nat, List.length(a, A, x <> xs), 1n+List.length(a, A, xs), length_cons(a, A, x, xs))
1126
1127# Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss, reversed to rewrite toward the simple side.
1128law concat_append_sym:
1129 for -a: Quant
1130 for -A: Kind(a)
1131 for xss: List<a, List<a, A>>
1132 for -yss: List<a, List<a, A>>
1133 {List.append(a, A, List.concat(a, A, xss), List.concat(a, A, yss)) == List.concat(a, A, List.append(a, List<a, A>, xss, yss)) : List<a, A>}
1134
1135def concat_append_sym(a, A, xss, yss):
1136 Equal.sym(List<a, A>, List.concat(a, A, List.append(a, List<a, A>, xss, yss)), List.append(a, A, List.concat(a, A, xss), List.concat(a, A, yss)), concat_append(a, A, xss, yss))
1137
1138# A left fold over an append folds the second part from the fold of the first, reversed to rewrite toward the simple side.
1139law foldl_append_sym:
1140 for ~a: Quant
1141 for ~A: Kind(a)
1142 for ~B: Type
1143 for ~f: B -> A -> B
1144 for xs: List<a, A>
1145 for -ys: List<a, A>
1146 for -z: B
1147 {List.foldl(~a, ~A, ~B, ~f, ys, List.foldl(~a, ~A, ~B, ~f, xs, z)) == List.foldl(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) : B}
1148
1149def foldl_append_sym(a, A, B, f, xs, ys, z):
1150 Equal.sym(B, List.foldl(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z), List.foldl(~a, ~A, ~B, ~f, ys, List.foldl(~a, ~A, ~B, ~f, xs, z)), foldl_append(~a, ~A, ~B, ~f, xs, ys, z))
1151
1152# Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs), reversed to rewrite toward the simple side.
1153law map_reverse_sym:
1154 for ~A: Type
1155 for ~B: Type
1156 for ~f: A -> B
1157 for xs: List<A>
1158 {List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) : List<B>}
1159
1160def map_reverse_sym(A, B, f, xs):
1161 Equal.sym(List<B>, List.map(~A, ~B, ~f, List.reverse(&1, A, xs)), List.reverse(&1, B, List.map(~A, ~B, ~f, xs)), map_reverse(~A, ~B, ~f, xs))
1162
1163# All over an append is all over each part, joined by and, reversed to rewrite toward the simple side.
1164law all_append_sym:
1165 for ~a: Quant
1166 for ~A: Kind(a)
1167 for ~f: A -> Bool
1168 for xs: List<a, A>
1169 for -ys: List<a, A>
1170 {Bool.and(List.all(~a, ~A, ~f, xs), List.all(~a, ~A, ~f, ys)) == List.all(~a, ~A, ~f, List.append(a, A, xs, ys)) : Bool}
1171
1172def all_append_sym(a, A, f, xs, ys):
1173 Equal.sym(Bool, List.all(~a, ~A, ~f, List.append(a, A, xs, ys)), Bool.and(List.all(~a, ~A, ~f, xs), List.all(~a, ~A, ~f, ys)), all_append(~a, ~A, ~f, xs, ys))
1174
1175# Any over an append is any over each part, joined by or, reversed to rewrite toward the simple side.
1176law any_append_sym:
1177 for ~a: Quant
1178 for ~A: Kind(a)
1179 for ~f: A -> Bool
1180 for xs: List<a, A>
1181 for -ys: List<a, A>
1182 {Bool.or(List.any(~a, ~A, ~f, xs), List.any(~a, ~A, ~f, ys)) == List.any(~a, ~A, ~f, List.append(a, A, xs, ys)) : Bool}
1183
1184def any_append_sym(a, A, f, xs, ys):
1185 Equal.sym(Bool, List.any(~a, ~A, ~f, List.append(a, A, xs, ys)), Bool.or(List.any(~a, ~A, ~f, xs), List.any(~a, ~A, ~f, ys)), any_append(~a, ~A, ~f, xs, ys))
1186
1187# Filtering an append filters each part, reversed to rewrite toward the simple side.
1188law filter_append_sym:
1189 for ~A: Data
1190 for ~f: A -> Bool
1191 for xs: List<&2, A>
1192 for ys: List<&2, A>
1193 {List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)) == List.filter(~A, ~f, List.append(&2, A, xs, ys)) : List<&2, A>}
1194
1195def filter_append_sym(A, f, xs, ys):
1196 Equal.sym(List<&2, A>, List.filter(~A, ~f, List.append(&2, A, xs, ys)), List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)), filter_append(~A, ~f, xs, ys))
1197
1198# An append contains x iff either part does, reversed to rewrite toward the simple side.
1199law contains_append_sym:
1200 for ~A: Data
1201 for ~eq: A -> A -> Bool
1202 for xs: List<&2, A>
1203 for -ys: List<&2, A>
1204 for +x: A
1205 {Bool.or(List.contains(~A, ~eq, xs, x), List.contains(~A, ~eq, ys, x)) == List.contains(~A, ~eq, List.append(&2, A, xs, ys), x) : Bool}
1206
1207def contains_append_sym(A, eq, xs, ys, x):
1208 Equal.sym(Bool, List.contains(~A, ~eq, List.append(&2, A, xs, ys), x), Bool.or(List.contains(~A, ~eq, xs, x), List.contains(~A, ~eq, ys, x)), contains_append(~A, ~eq, xs, ys, x))
1209
1210# Filtering never makes a list longer, reversed to rewrite toward the simple side.
1211law length_filter_le_sym:
1212 for ~A: Data
1213 for ~f: A -> Bool
1214 for xs: List<&2, A>
1215 {True{} == Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)) : Bool}
1216
1217def length_filter_le_sym(A, f, xs):
1218 Equal.sym(Bool, Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)), True{}, length_filter_le(~A, ~f, xs))