list.bend

bend-mathlib@0.7.2.0 · 2,865 lines · 0 definitions

1# bend-mathlib/list.bend: List lemmas (append, reverse, length, take, drop, map, fold, filter).
2import Base
3import bend-mathlib@0.7.2.0/nat.bend as MNat
4import bend-mathlib@0.7.2.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
411def internal_length_range_go(+n: Nat, acc: List<&2, Nat>) -> {List.length(&2, Nat, List.range.go(n, acc)) == Nat.add(n, List.length(&2, Nat, acc)) : Nat}:
412  match n:
413    case 0n:
414      {==}
415    case 1n+p:
416      %MNat.add_succ(p, List.length(&2, Nat, acc)) : {List.length(&2, Nat, List.range.go(p, p <> acc)) == _ : Nat}
417      internal_length_range_go(p, p <> acc)
418
419# Range(n) has length n.
420law length_range:
421  for n: Nat
422  {List.length(&2, Nat, List.range(n)) == n : Nat}
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
513def 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>}:
514  match xs:
515    case Nil{}:
516      {==}
517    case h <> t:
518      internal_map_reverse_go(~A, ~B, ~f, t, h <> acc)
519
520# Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs).
521law map_reverse:
522  for ~A: Type
523  for ~B: Type
524  for ~f: A -> B
525  for xs: List<A>
526  {List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) == List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) : List<B>}
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
565def internal_filter_put_append(-A: Data, h: A, r: List<&2, A>, s: List<&2, A>, b: Bool) -> {List.append(&2, A, List.filter.put(A, h, r, b), s) == List.filter.put(A, h, List.append(&2, A, r, s), b) : List<&2, A>}:
566  match b:
567    case False{}:
568      {==}
569    case True{}:
570      {==}
571
572# Filtering an append filters each part.
573law filter_append:
574  for ~A: Data
575  for ~f: A -> Bool
576  for xs: List<&2, A>
577  for ys: List<&2, A>
578  {List.filter(~A, ~f, List.append(&2, A, xs, ys)) == List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)) : List<&2, A>}
579
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
607def internal_length_filter_put_le(-A: Data, h: A, r: List<&2, A>, b: Bool) -> {Nat.is_le(List.length(&2, A, List.filter.put(A, h, r, b)), 1n+List.length(&2, A, r)) == True{} : Bool}:
608  match b:
609    case False{}:
610      MNat.le_succ(List.length(&2, A, r))
611    case True{}:
612      MNat.le_refl(1n+List.length(&2, A, r))
613
614# Filtering never makes a list longer.
615law length_filter_le:
616  for ~A: Data
617  for ~f: A -> Bool
618  for xs: List<&2, A>
619  {Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)) == True{} : Bool}
620
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 Nat list is a member of it (membership by Nat.is_eq).
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# A member of a Nat list stays a member when a 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# No Nat 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# A member of xs is a member of xs ++ ys (Nat lists).
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# A member of ys is a member of xs ++ ys (Nat lists).
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 Nat list is sorted by Nat.is_le.
732law sorted_nil:
733  sorted_by(~Nat, ~Nat.is_le, Nil{})
734
735def sorted_nil():
736  {==}
737
738# A one-element Nat list is sorted by Nat.is_le.
739law sorted_single:
740  for -x: Nat
741  sorted_by(~Nat, ~Nat.is_le, [x])
742
743def sorted_single(x):
744  {==}
745
746# A Nat list sorted by Nat.is_le stays sorted under a head that is <= the next element.
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 first two elements of a Nat list sorted by Nat.is_le are 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 Nat list of two or more elements sorted by Nat.is_le 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# The tail of a nonempty Nat list sorted by Nat.is_le is sorted.
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# Taking the length of the first part of an append gives the first part back.
796law take_left:
797  for -a: Quant
798  for -A: Kind(a)
799  for xs: List<a, A>
800  for ys: List<a, A>
801  {List.take(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) == xs : List<a, A>}
802
803def take_left(a, A, xs, ys):
804  match xs:
805    case Nil{}:
806      take_zero(a, A, ys)
807    case h <> t:
808      %take_left(a, A, t, ys) : {h <> List.take(a, A, List.append(a, A, t, ys), List.length(a, A, t)) == h <> _ : List<a, A>}
809      {==}
810
811# Dropping the length of the first part of an append gives the second part.
812law drop_left:
813  for -a: Quant
814  for -A: Kind(a)
815  for xs: List<a, A>
816  for ys: List<a, A>
817  {List.drop(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) == ys : List<a, A>}
818
819def drop_left(a, A, xs, ys):
820  match xs:
821    case Nil{}:
822      drop_zero(a, A, ys)
823    case h <> t:
824      drop_left(a, A, t, ys)
825
826# Taking past the first part of an append keeps it and takes the rest from the second part.
827law take_append:
828  for -a: Quant
829  for -A: Kind(a)
830  for xs: List<a, A>
831  for -ys: List<a, A>
832  for -n: Nat
833  {List.take(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)) == List.append(a, A, xs, List.take(a, A, ys, n)) : List<a, A>}
834
835def take_append(a, A, xs, ys, n):
836  match xs:
837    case Nil{}:
838      {==}
839    case h <> t:
840      %take_append(a, A, t, ys, n) : {h <> List.take(a, A, List.append(a, A, t, ys), Nat.add(List.length(a, A, t), n)) == h <> _ : List<a, A>}
841      {==}
842
843# Dropping past the first part of an append drops the rest from the second part.
844law drop_append:
845  for -a: Quant
846  for -A: Kind(a)
847  for xs: List<a, A>
848  for -ys: List<a, A>
849  for -n: Nat
850  {List.drop(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)) == List.drop(a, A, ys, n) : List<a, A>}
851
852def drop_append(a, A, xs, ys, n):
853  match xs:
854    case Nil{}:
855      {==}
856    case h <> t:
857      drop_append(a, A, t, ys, n)
858
859# Taking at most the length of the first part of an append only sees the first part.
860law take_append_of_le_length:
861  for -a: Quant
862  for -A: Kind(a)
863  for xs: List<a, A>
864  for ys: List<a, A>
865  for n: Nat
866  for h: MNat.le(n, List.length(a, A, xs))
867  {List.take(a, A, List.append(a, A, xs, ys), n) == List.take(a, A, xs, n) : List<a, A>}
868
869def take_append_of_le_length(a, A, xs, ys, n, h):
870  match xs n:
871    case Nil{} 0n:
872      take_zero(a, A, ys)
873    case Nil{} 1n+p:
874      Empty.absurd({List.take(a, A, ys, 1n+p) == Nil{} : List<a, A>}, MNat.internal_false_ne_true(h))
875    case x <> t 0n:
876      {==}
877    case x <> t 1n+p:
878      %take_append_of_le_length(a, A, t, ys, p, h) : {x <> List.take(a, A, List.append(a, A, t, ys), p) == x <> _ : List<a, A>}
879      {==}
880
881# Dropping at most the length of the first part of an append drops only from the first part.
882law drop_append_of_le_length:
883  for -a: Quant
884  for -A: Kind(a)
885  for xs: List<a, A>
886  for ys: List<a, A>
887  for n: Nat
888  for h: MNat.le(n, List.length(a, A, xs))
889  {List.drop(a, A, List.append(a, A, xs, ys), n) == List.append(a, A, List.drop(a, A, xs, n), ys) : List<a, A>}
890
891def drop_append_of_le_length(a, A, xs, ys, n, h):
892  match xs n:
893    case Nil{} 0n:
894      drop_zero(a, A, ys)
895    case Nil{} 1n+p:
896      Empty.absurd({List.drop(a, A, ys, 1n+p) == ys : List<a, A>}, MNat.internal_false_ne_true(h))
897    case x <> t 0n:
898      {==}
899    case x <> t 1n+p:
900      drop_append_of_le_length(a, A, t, ys, p, h)
901
902# Mapping commutes with taking: map f (take n xs) = take n (map f xs).
903law map_take:
904  for ~A: Type
905  for ~B: Type
906  for ~f: A -> B
907  for xs: List<A>
908  for n: Nat
909  {List.map(~A, ~B, ~f, List.take(&1, A, xs, n)) == List.take(&1, B, List.map(~A, ~B, ~f, xs), n) : List<B>}
910
911def map_take(A, B, f, xs, n):
912  match xs n:
913    case Nil{} _:
914      {==}
915    case h <> t 0n:
916      {==}
917    case h <> t 1n+p:
918      %map_take(~A, ~B, ~f, t, p) : {f(h) <> List.map(~A, ~B, ~f, List.take(&1, A, t, p)) == f(h) <> _ : List<B>}
919      {==}
920
921# Mapping commutes with dropping: map f (drop n xs) = drop n (map f xs).
922law map_drop:
923  for ~A: Type
924  for ~B: Type
925  for ~f: A -> B
926  for xs: List<A>
927  for n: Nat
928  {List.map(~A, ~B, ~f, List.drop(&1, A, xs, n)) == List.drop(&1, B, List.map(~A, ~B, ~f, xs), n) : List<B>}
929
930def map_drop(A, B, f, xs, n):
931  match xs n:
932    case Nil{} _:
933      {==}
934    case h <> t 0n:
935      {==}
936    case h <> t 1n+p:
937      map_drop(~A, ~B, ~f, t, p)
938
939# Taking m from n copies of x gives min(m, n) copies of x.
940law take_replicate:
941  for -A: Data
942  for n: Nat
943  for m: Nat
944  for -x: A
945  {List.take(&2, A, List.replicate(A, n, x), m) == List.replicate(A, Nat.min(m, n), x) : List<&2, A>}
946
947def take_replicate(A, n, m, x):
948  match n m:
949    case 0n _:
950      %MNat.min_zero_sym(m) : {Nil{} == List.replicate(A, _, x) : List<&2, A>}
951      {==}
952    case 1n+p 0n:
953      {==}
954    case 1n+p 1n+q:
955      %take_replicate(A, p, q, x) : {x <> List.take(&2, A, List.replicate(A, p, x), q) == x <> _ : List<&2, A>}
956      {==}
957
958# Dropping m from n copies of x gives n - m copies of x.
959law drop_replicate:
960  for -A: Data
961  for n: Nat
962  for m: Nat
963  for -x: A
964  {List.drop(&2, A, List.replicate(A, n, x), m) == List.replicate(A, Nat.sub(n, m), x) : List<&2, A>}
965
966def drop_replicate(A, n, m, x):
967  match n m:
968    case 0n _:
969      {==}
970    case 1n+p 0n:
971      {==}
972    case 1n+p 1n+q:
973      drop_replicate(A, p, q, x)
974
975# Taking n elements gives at most n of them.
976law length_take_le:
977  for -a: Quant
978  for -A: Kind(a)
979  for xs: List<a, A>
980  for n: Nat
981  MNat.le(List.length(a, A, List.take(a, A, xs, n)), n)
982
983def length_take_le(a, A, xs, n):
984  match xs n:
985    case Nil{} _:
986      MNat.zero_le(n)
987    case h <> t 0n:
988      {==}
989    case h <> t 1n+p:
990      MNat.succ_le_succ(List.length(a, A, List.take(a, A, t, p)), p, length_take_le(a, A, t, p))
991
992# The tail is one shorter than the list, or empty: length (tail xs) = length xs - 1.
993law length_tail:
994  for -a: Quant
995  for -A: Kind(a)
996  for xs: List<a, A>
997  {List.length(a, A, List.tail(a, A, xs)) == Nat.sub(List.length(a, A, xs), 1n) : Nat}
998
999def length_tail(a, A, xs):
1000  match xs:
1001    case Nil{}:
1002      {==}
1003    case h <> t:
1004      MNat.sub_zero_sym(List.length(a, A, t))
1005
1006# Mapping the identity gives the list back.
1007law map_id:
1008  for ~A: Type
1009  for xs: List<A>
1010  {List.map(~A, ~A, ~(x => x), xs) == xs : List<A>}
1011
1012def map_id(A, xs):
1013  match xs:
1014    case Nil{}:
1015      {==}
1016    case h <> t:
1017      %map_id(~A, t) : {h <> List.map(~A, ~A, ~(x => x), t) == h <> _ : List<A>}
1018      {==}
1019
1020# A right fold over a map folds with the mapped function: foldr g z (map f xs) = foldr (g . f) z xs.
1021law foldr_map:
1022  for ~A: Type
1023  for ~B: Type
1024  for ~C: Type
1025  for ~f: A -> B
1026  for ~g: B -> C -> C
1027  for xs: List<A>
1028  for -z: C
1029  {List.foldr(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, xs), z) == List.foldr(~&1, ~A, ~C, ~(x => y => g(f(x), y)), xs, z) : C}
1030
1031def foldr_map(A, B, C, f, g, xs, z):
1032  match xs:
1033    case Nil{}:
1034      {==}
1035    case h <> t:
1036      %foldr_map(~A, ~B, ~C, ~f, ~g, t, z) : {g(f(h), List.foldr(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, t), z)) == g(f(h), _) : C}
1037      {==}
1038
1039# A left fold over a map folds with the mapped function: foldl g z (map f xs) = foldl (fun acc x => g acc (f x)) z xs.
1040law foldl_map:
1041  for ~A: Type
1042  for ~B: Type
1043  for ~C: Type
1044  for ~f: A -> B
1045  for ~g: C -> B -> C
1046  for xs: List<A>
1047  for -z: C
1048  {List.foldl(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, xs), z) == List.foldl(~&1, ~A, ~C, ~(x => y => g(x, f(y))), xs, z) : C}
1049
1050def foldl_map(A, B, C, f, g, xs, z):
1051  match xs:
1052    case Nil{}:
1053      {==}
1054    case h <> t:
1055      foldl_map(~A, ~B, ~C, ~f, ~g, t, g(z, f(h)))
1056
1057# Replicating m + n times appends m copies to n copies.
1058law replicate_add:
1059  for -A: Data
1060  for m: Nat
1061  for -n: Nat
1062  for -x: A
1063  {List.replicate(A, Nat.add(m, n), x) == List.append(&2, A, List.replicate(A, m, x), List.replicate(A, n, x)) : List<&2, A>}
1064
1065def replicate_add(A, m, n, x):
1066  match m:
1067    case 0n:
1068      {==}
1069    case 1n+p:
1070      %replicate_add(A, p, n, x) : {x <> List.replicate(A, Nat.add(p, n), x) == x <> _ : List<&2, A>}
1071      {==}
1072
1073def internal_replicate_append_nil(-A: Data, n: Nat, -x: A) -> {List.append(&2, A, List.replicate(A, n, x), Nil{}) == List.replicate(A, n, x) : List<&2, A>}:
1074  match n:
1075    case 0n:
1076      {==}
1077    case 1n+p:
1078      %internal_replicate_append_nil(A, p, x) : {x <> List.append(&2, A, List.replicate(A, p, x), Nil{}) == x <> _ : List<&2, A>}
1079      {==}
1080
1081def internal_replicate_append_cons(-A: Data, n: Nat, -x: A, -acc: List<&2, A>) -> {List.append(&2, A, List.replicate(A, n, x), x <> acc) == x <> List.append(&2, A, List.replicate(A, n, x), acc) : List<&2, A>}:
1082  match n:
1083    case 0n:
1084      {==}
1085    case 1n+p:
1086      %internal_replicate_append_cons(A, p, x, acc) : {x <> List.append(&2, A, List.replicate(A, p, x), x <> acc) == x <> _ : List<&2, A>}
1087      {==}
1088
1089def internal_reverse_go_replicate(-A: Data, n: Nat, -x: A, -acc: List<&2, A>) -> {List.reverse.go(&2, A, List.replicate(A, n, x), acc) == List.append(&2, A, List.replicate(A, n, x), acc) : List<&2, A>}:
1090  match n:
1091    case 0n:
1092      {==}
1093    case 1n+p:
1094      +p = p
1095      Equal.trans(List<&2, A>, List.reverse.go(&2, A, List.replicate(A, p, x), x <> acc), List.append(&2, A, List.replicate(A, p, x), x <> acc), x <> List.append(&2, A, List.replicate(A, p, x), acc), internal_reverse_go_replicate(A, p, x, x <> acc), internal_replicate_append_cons(A, p, x, acc))
1096
1097# Reversing n copies of x gives them back.
1098law reverse_replicate:
1099  for -A: Data
1100  for n: Nat
1101  for -x: A
1102  {List.reverse(&2, A, List.replicate(A, n, x)) == List.replicate(A, n, x) : List<&2, A>}
1103
1104def reverse_replicate(A, n, x):
1105  +n = n
1106  Equal.trans(List<&2, A>, List.reverse(&2, A, List.replicate(A, n, x)), List.append(&2, A, List.replicate(A, n, x), Nil{}), List.replicate(A, n, x), internal_reverse_go_replicate(A, n, x, Nil{}), internal_replicate_append_nil(A, n, x))
1107
1108# Filtering with an always-true predicate gives the list back.
1109law filter_true:
1110  for ~A: Data
1111  for xs: List<&2, A>
1112  {List.filter(~A, ~(x => True{}), xs) == xs : List<&2, A>}
1113
1114def filter_true(A, xs):
1115  match xs:
1116    case Nil{}:
1117      {==}
1118    case h <> t:
1119      %filter_true(~A, t) : {h <> List.filter(~A, ~(x => True{}), t) == h <> _ : List<&2, A>}
1120      {==}
1121
1122# Filtering with an always-false predicate gives the empty list.
1123law filter_false:
1124  for ~A: Data
1125  for xs: List<&2, A>
1126  {List.filter(~A, ~(x => False{}), xs) == Nil{} : List<&2, A>}
1127
1128def filter_false(A, xs):
1129  match xs:
1130    case Nil{}:
1131      {==}
1132    case h <> t:
1133      filter_false(~A, t)
1134
1135def internal_filter_put_filter(~A: Data, ~p: A -> Bool, +h: A, r: List<&2, A>, b: Bool) -> {List.filter(~A, ~p, List.filter.put(A, h, r, b)) == List.filter.put(A, h, List.filter(~A, ~p, r), Bool.and(p(h), b)) : List<&2, A>}:
1136  match b:
1137    case False{}:
1138      %MBool.and_false_sym(p(h)) : {List.filter(~A, ~p, r) == List.filter.put(A, h, List.filter(~A, ~p, r), _) : List<&2, A>}
1139      {==}
1140    case True{}:
1141      %MBool.and_true_sym(p(h)) : {List.filter(~A, ~p, h <> r) == List.filter.put(A, h, List.filter(~A, ~p, r), _) : List<&2, A>}
1142      {==}
1143
1144# Filtering twice is filtering by both predicates: filter p (filter q xs) = filter (p and q) xs.
1145law filter_filter:
1146  for ~A: Data
1147  for ~p: A -> Bool
1148  for ~q: A -> Bool
1149  for xs: List<&2, A>
1150  {List.filter(~A, ~p, List.filter(~A, ~q, xs)) == List.filter(~A, ~(+x => Bool.and(p(x), q(x))), xs) : List<&2, A>}
1151
1152def filter_filter(A, p, q, xs):
1153  match xs:
1154    case Nil{}:
1155      {==}
1156    case +h <> t:
1157      +t = t
1158      %filter_filter(~A, ~p, ~q, t) : {List.filter(~A, ~p, List.filter.put(A, h, List.filter(~A, ~q, t), q(h))) == List.filter.put(A, h, _, Bool.and(p(h), q(h))) : List<&2, A>}
1159      internal_filter_put_filter(~A, ~p, h, List.filter(~A, ~q, t), q(h))
1160
1161def internal_all_filter_put(~A: Data, ~q: A -> Bool, -h: A, r: List<&2, A>, b: Bool) -> {List.all(~&2, ~A, ~q, List.filter.put(A, h, r, b)) == Bool.and(Bool.or(Bool.not(b), q(h)), List.all(~&2, ~A, ~q, r)) : Bool}:
1162  match b:
1163    case False{}:
1164      {==}
1165    case True{}:
1166      {==}
1167
1168# All over a filter checks q only where p holds: all q (filter p xs) = all (not p or q) xs.
1169law all_filter:
1170  for ~A: Data
1171  for ~p: A -> Bool
1172  for ~q: A -> Bool
1173  for xs: List<&2, A>
1174  {List.all(~&2, ~A, ~q, List.filter(~A, ~p, xs)) == List.all(~&2, ~A, ~(+x => Bool.or(Bool.not(p(x)), q(x))), xs) : Bool}
1175
1176def all_filter(A, p, q, xs):
1177  match xs:
1178    case Nil{}:
1179      {==}
1180    case +h <> t:
1181      +t = t
1182      %all_filter(~A, ~p, ~q, t) : {List.all(~&2, ~A, ~q, List.filter.put(A, h, List.filter(~A, ~p, t), p(h))) == Bool.and(Bool.or(Bool.not(p(h)), q(h)), _) : Bool}
1183      internal_all_filter_put(~A, ~q, h, List.filter(~A, ~p, t), p(h))
1184
1185def internal_any_filter_put(~A: Data, ~q: A -> Bool, -h: A, r: List<&2, A>, b: Bool) -> {List.any(~&2, ~A, ~q, List.filter.put(A, h, r, b)) == Bool.or(Bool.and(b, q(h)), List.any(~&2, ~A, ~q, r)) : Bool}:
1186  match b:
1187    case False{}:
1188      {==}
1189    case True{}:
1190      {==}
1191
1192# Any over a filter looks for q only where p holds: any q (filter p xs) = any (p and q) xs.
1193law any_filter:
1194  for ~A: Data
1195  for ~p: A -> Bool
1196  for ~q: A -> Bool
1197  for xs: List<&2, A>
1198  {List.any(~&2, ~A, ~q, List.filter(~A, ~p, xs)) == List.any(~&2, ~A, ~(+x => Bool.and(p(x), q(x))), xs) : Bool}
1199
1200def any_filter(A, p, q, xs):
1201  match xs:
1202    case Nil{}:
1203      {==}
1204    case +h <> t:
1205      +t = t
1206      %any_filter(~A, ~p, ~q, t) : {List.any(~&2, ~A, ~q, List.filter.put(A, h, List.filter(~A, ~p, t), p(h))) == Bool.or(Bool.and(p(h), q(h)), _) : Bool}
1207      internal_any_filter_put(~A, ~q, h, List.filter(~A, ~p, t), p(h))
1208
1209# All over a map checks the composed predicate: all p (map f xs) = all (p . f) xs.
1210law all_map:
1211  for ~A: Type
1212  for ~B: Type
1213  for ~f: A -> B
1214  for ~p: B -> Bool
1215  for xs: List<A>
1216  {List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) == List.all(~&1, ~A, ~(x => p(f(x))), xs) : Bool}
1217
1218def all_map(A, B, f, p, xs):
1219  match xs:
1220    case Nil{}:
1221      {==}
1222    case h <> t:
1223      %all_map(~A, ~B, ~f, ~p, t) : {Bool.and(p(f(h)), List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, t))) == Bool.and(p(f(h)), _) : Bool}
1224      {==}
1225
1226# Any over a map checks the composed predicate: any p (map f xs) = any (p . f) xs.
1227law any_map:
1228  for ~A: Type
1229  for ~B: Type
1230  for ~f: A -> B
1231  for ~p: B -> Bool
1232  for xs: List<A>
1233  {List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) == List.any(~&1, ~A, ~(x => p(f(x))), xs) : Bool}
1234
1235def any_map(A, B, f, p, xs):
1236  match xs:
1237    case Nil{}:
1238      {==}
1239    case h <> t:
1240      %any_map(~A, ~B, ~f, ~p, t) : {Bool.or(p(f(h)), List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, t))) == Bool.or(p(f(h)), _) : Bool}
1241      {==}
1242
1243def internal_all_reverse_go(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List<a, A>, -acc: List<a, A>, c: Bool, e: {List.all(~a, ~A, ~f, acc) == c : Bool}) -> {List.all(~a, ~A, ~f, List.reverse.go(a, A, xs, acc)) == Bool.and(c, List.all(~a, ~A, ~f, xs)) : Bool}:
1244  match xs c:
1245    case Nil{} True{}:
1246      e
1247    case Nil{} False{}:
1248      e
1249    case h <> t True{}:
1250      +v = f(h)
1251      internal_all_reverse_go(~a, ~A, ~f, t, h <> acc, v, Equal.trans(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), Bool.and(v, True{}), v, Equal.cong(Bool, Bool, k => Bool.and(v, k), List.all(~a, ~A, ~f, acc), True{}, e), MBool.and_true(v)))
1252    case h <> t False{}:
1253      internal_all_reverse_go(~a, ~A, ~f, t, h <> acc, False{}, Equal.trans(Bool, Bool.and(f(h), List.all(~a, ~A, ~f, acc)), Bool.and(f(h), False{}), False{}, Equal.cong(Bool, Bool, k => Bool.and(f(h), k), List.all(~a, ~A, ~f, acc), False{}, e), MBool.and_false(f(h))))
1254
1255# Reversing does not change whether all elements satisfy a predicate.
1256law all_reverse:
1257  for ~a: Quant
1258  for ~A: Kind(a)
1259  for ~f: A -> Bool
1260  for xs: List<a, A>
1261  {List.all(~a, ~A, ~f, List.reverse(a, A, xs)) == List.all(~a, ~A, ~f, xs) : Bool}
1262
1263def all_reverse(a, A, f, xs):
1264  internal_all_reverse_go(~a, ~A, ~f, xs, Nil{}, True{}, {==})
1265
1266def internal_any_reverse_go(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List<a, A>, -acc: List<a, A>, c: Bool, e: {List.any(~a, ~A, ~f, acc) == c : Bool}) -> {List.any(~a, ~A, ~f, List.reverse.go(a, A, xs, acc)) == Bool.or(c, List.any(~a, ~A, ~f, xs)) : Bool}:
1267  match xs c:
1268    case Nil{} True{}:
1269      e
1270    case Nil{} False{}:
1271      e
1272    case h <> t True{}:
1273      internal_any_reverse_go(~a, ~A, ~f, t, h <> acc, True{}, Equal.trans(Bool, Bool.or(f(h), List.any(~a, ~A, ~f, acc)), Bool.or(f(h), True{}), True{}, Equal.cong(Bool, Bool, k => Bool.or(f(h), k), List.any(~a, ~A, ~f, acc), True{}, e), MBool.or_true(f(h))))
1274    case h <> t False{}:
1275      +v = f(h)
1276      internal_any_reverse_go(~a, ~A, ~f, t, h <> acc, v, Equal.trans(Bool, Bool.or(v, List.any(~a, ~A, ~f, acc)), Bool.or(v, False{}), v, Equal.cong(Bool, Bool, k => Bool.or(v, k), List.any(~a, ~A, ~f, acc), False{}, e), MBool.or_false(v)))
1277
1278# Reversing does not change whether some element satisfies a predicate.
1279law any_reverse:
1280  for ~a: Quant
1281  for ~A: Kind(a)
1282  for ~f: A -> Bool
1283  for xs: List<a, A>
1284  {List.any(~a, ~A, ~f, List.reverse(a, A, xs)) == List.any(~a, ~A, ~f, xs) : Bool}
1285
1286def any_reverse(a, A, f, xs):
1287  internal_any_reverse_go(~a, ~A, ~f, xs, Nil{}, False{}, {==})
1288
1289def internal_contains_reverse_go(~A: Data, ~eq: A -> A -> Bool, xs: List<&2, A>, -acc: List<&2, A>, +x: A, c: Bool, e: {List.contains(~A, ~eq, acc, x) == c : Bool}) -> {List.contains(~A, ~eq, List.reverse.go(&2, A, xs, acc), x) == Bool.or(c, List.contains(~A, ~eq, xs, x)) : Bool}:
1290  match xs c:
1291    case Nil{} True{}:
1292      e
1293    case Nil{} False{}:
1294      e
1295    case h <> t True{}:
1296      internal_contains_reverse_go(~A, ~eq, t, h <> acc, x, True{}, Equal.trans(Bool, Bool.or(eq(h, x), List.contains(~A, ~eq, acc, x)), Bool.or(eq(h, x), True{}), True{}, Equal.cong(Bool, Bool, k => Bool.or(eq(h, x), k), List.contains(~A, ~eq, acc, x), True{}, e), MBool.or_true(eq(h, x))))
1297    case h <> t False{}:
1298      +v = eq(h, x)
1299      internal_contains_reverse_go(~A, ~eq, t, h <> acc, x, v, Equal.trans(Bool, Bool.or(v, List.contains(~A, ~eq, acc, x)), Bool.or(v, False{}), v, Equal.cong(Bool, Bool, k => Bool.or(v, k), List.contains(~A, ~eq, acc, x), False{}, e), MBool.or_false(v)))
1300
1301# Reversing does not change whether a list contains x.
1302law contains_reverse:
1303  for ~A: Data
1304  for ~eq: A -> A -> Bool
1305  for xs: List<&2, A>
1306  for +x: A
1307  {List.contains(~A, ~eq, List.reverse(&2, A, xs), x) == List.contains(~A, ~eq, xs, x) : Bool}
1308
1309def contains_reverse(A, eq, xs, x):
1310  internal_contains_reverse_go(~A, ~eq, xs, Nil{}, x, False{}, {==})
1311
1312# Zipping the empty list with anything gives the empty list.
1313law zip_nil_left:
1314  for -a: Quant
1315  for -A: Kind(a)
1316  for -b: Quant
1317  for -B: Kind(b)
1318  for -ys: List<b, B>
1319  {List.zip(a, A, b, B, Nil{}, ys) == Nil{} : List<&1, A & B>}
1320
1321def zip_nil_left(a, A, b, B, ys):
1322  {==}
1323
1324# Zipping anything with the empty list gives the empty list.
1325law zip_nil_right:
1326  for -a: Quant
1327  for -A: Kind(a)
1328  for -b: Quant
1329  for -B: Kind(b)
1330  for xs: List<a, A>
1331  {List.zip(a, A, b, B, xs, Nil{}) == Nil{} : List<&1, A & B>}
1332
1333def zip_nil_right(a, A, b, B, xs):
1334  match xs:
1335    case Nil{}:
1336      {==}
1337    case h <> t:
1338      {==}
1339
1340# The head of a cons is its first element.
1341law head_cons:
1342  for -a: Quant
1343  for -A: Kind(a)
1344  for -x: A
1345  for -xs: List<a, A>
1346  {List.head(a, A, x <> xs) == Some{x} : Maybe<a, A>}
1347
1348def head_cons(a, A, x, xs):
1349  {==}
1350
1351# The head of an append is the head of the first part, or else of the second.
1352law head_append:
1353  for -a: Quant
1354  for -A: Kind(a)
1355  for xs: List<a, A>
1356  for -ys: List<a, A>
1357  {List.head(a, A, List.append(a, A, xs, ys)) == Maybe.or(a, A, List.head(a, A, xs), List.head(a, A, ys)) : Maybe<a, A>}
1358
1359def head_append(a, A, xs, ys):
1360  match xs:
1361    case Nil{}:
1362      {==}
1363    case h <> t:
1364      {==}
1365
1366# The head of a map is the mapped head.
1367law head_map:
1368  for ~A: Type
1369  for ~B: Type
1370  for ~f: A -> B
1371  for xs: List<A>
1372  {List.head(&1, B, List.map(~A, ~B, ~f, xs)) == Maybe.map(&1, A, B, f, List.head(&1, A, xs)) : Maybe<&1, B>}
1373
1374def head_map(A, B, f, xs):
1375  match xs:
1376    case Nil{}:
1377      {==}
1378    case h <> t:
1379      {==}
1380
1381# The tail of a map is the map of the tail.
1382law tail_map:
1383  for ~A: Type
1384  for ~B: Type
1385  for ~f: A -> B
1386  for xs: List<A>
1387  {List.tail(&1, B, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~B, ~f, List.tail(&1, A, xs)) : List<B>}
1388
1389def tail_map(A, B, f, xs):
1390  match xs:
1391    case Nil{}:
1392      {==}
1393    case h <> t:
1394      {==}
1395
1396# The element at index zero of a cons is its head.
1397law get_cons_zero:
1398  for -a: Quant
1399  for -A: Kind(a)
1400  for -x: A
1401  for -xs: List<a, A>
1402  {List.get(a, A, x <> xs, 0n) == Some{x} : Maybe<a, A>}
1403
1404def get_cons_zero(a, A, x, xs):
1405  {==}
1406
1407# The element at index n + 1 of a cons is the element at index n of its tail.
1408law get_cons_succ:
1409  for -a: Quant
1410  for -A: Kind(a)
1411  for -x: A
1412  for -xs: List<a, A>
1413  for -n: Nat
1414  {List.get(a, A, x <> xs, 1n+n) == List.get(a, A, xs, n) : Maybe<a, A>}
1415
1416def get_cons_succ(a, A, x, xs, n):
1417  {==}
1418
1419# Indexing a map is mapping the indexed element.
1420law get_map:
1421  for ~A: Type
1422  for ~B: Type
1423  for ~f: A -> B
1424  for xs: List<A>
1425  for n: Nat
1426  {List.get(&1, B, List.map(~A, ~B, ~f, xs), n) == Maybe.map(&1, A, B, f, List.get(&1, A, xs, n)) : Maybe<&1, B>}
1427
1428def get_map(A, B, f, xs, n):
1429  match xs n:
1430    case Nil{} _:
1431      {==}
1432    case h <> t 0n:
1433      {==}
1434    case h <> t 1n+p:
1435      get_map(~A, ~B, ~f, t, p)
1436
1437# Setting an element does not change the length.
1438law length_set:
1439  for -a: Quant
1440  for -A: Kind(a)
1441  for xs: List<a, A>
1442  for n: Nat
1443  for -x: A
1444  {List.length(a, A, List.set(a, A, xs, n, x)) == List.length(a, A, xs) : Nat}
1445
1446def length_set(a, A, xs, n, x):
1447  match xs n:
1448    case Nil{} _:
1449      {==}
1450    case h <> t 0n:
1451      {==}
1452    case h <> t 1n+p:
1453      %length_set(a, A, t, p, x) : {1n+List.length(a, A, List.set(a, A, t, p, x)) == 1n+_ : Nat}
1454      {==}
1455
1456# Reading the index just set gives the new value wherever the index is in range.
1457law get_set_self:
1458  for -a: Quant
1459  for -A: Kind(a)
1460  for xs: List<a, A>
1461  for n: Nat
1462  for -x: A
1463  {List.get(a, A, List.set(a, A, xs, n, x), n) == Maybe.map(a, A, A, y => x, List.get(a, A, xs, n)) : Maybe<a, A>}
1464
1465def get_set_self(a, A, xs, n, x):
1466  match xs n:
1467    case Nil{} _:
1468      {==}
1469    case h <> t 0n:
1470      {==}
1471    case h <> t 1n+p:
1472      get_set_self(a, A, t, p, x)
1473
1474def internal_last_go_append_singleton(a, -A: Kind(a), ys: List<a, A>, -h: A, -x: A) -> {List.last.go(a, A, List.append(a, A, ys, [x]), h) == x : A}:
1475  match ys:
1476    case Nil{}:
1477      {==}
1478    case y <> t:
1479      internal_last_go_append_singleton(a, A, t, y, x)
1480
1481# The last element of xs ++ [x] is x.
1482law last_append_singleton:
1483  for -a: Quant
1484  for -A: Kind(a)
1485  for xs: List<a, A>
1486  for -x: A
1487  {List.last(a, A, List.append(a, A, xs, [x])) == Some{x} : Maybe<a, A>}
1488
1489def last_append_singleton(a, A, xs, x):
1490  match xs:
1491    case Nil{}:
1492      {==}
1493    case h <> t:
1494      %internal_last_go_append_singleton(a, A, t, h, x) : {Some{List.last.go(a, A, List.append(a, A, t, [x]), h)} == Some{_} : Maybe<a, A>}
1495      {==}
1496
1497def internal_head_reverse_go(a, -A: Kind(a), xs: List<a, A>, -h: A, -acc: List<a, A>) -> {List.head(a, A, List.reverse.go(a, A, xs, h <> acc)) == Some{List.last.go(a, A, xs, h)} : Maybe<a, A>}:
1498  match xs:
1499    case Nil{}:
1500      {==}
1501    case y <> t:
1502      internal_head_reverse_go(a, A, t, y, h <> acc)
1503
1504# The head of the reverse is the last element.
1505law head_reverse:
1506  for -a: Quant
1507  for -A: Kind(a)
1508  for xs: List<a, A>
1509  {List.head(a, A, List.reverse(a, A, xs)) == List.last(a, A, xs) : Maybe<a, A>}
1510
1511def head_reverse(a, A, xs):
1512  match xs:
1513    case Nil{}:
1514      {==}
1515    case h <> t:
1516      internal_head_reverse_go(a, A, t, h, Nil{})
1517
1518def internal_last_reverse_go(a, -A: Kind(a), xs: List<a, A>, -h: A, -acc: List<a, A>) -> {List.last(a, A, List.reverse.go(a, A, xs, h <> acc)) == Some{List.last.go(a, A, acc, h)} : Maybe<a, A>}:
1519  match xs:
1520    case Nil{}:
1521      {==}
1522    case y <> t:
1523      internal_last_reverse_go(a, A, t, y, h <> acc)
1524
1525# The last element of the reverse is the head.
1526law last_reverse:
1527  for -a: Quant
1528  for -A: Kind(a)
1529  for xs: List<a, A>
1530  {List.last(a, A, List.reverse(a, A, xs)) == List.head(a, A, xs) : Maybe<a, A>}
1531
1532def last_reverse(a, A, xs):
1533  match xs:
1534    case Nil{}:
1535      {==}
1536    case h <> t:
1537      internal_last_reverse_go(a, A, t, h, Nil{})
1538
1539# A list is empty exactly when its length is zero.
1540law is_empty_iff_length_eq_zero:
1541  for -a: Quant
1542  for -A: Kind(a)
1543  for xs: List<a, A>
1544  {List.is_empty(a, A, xs) == Nat.is_eq(List.length(a, A, xs), 0n) : Bool}
1545
1546def is_empty_iff_length_eq_zero(a, A, xs):
1547  match xs:
1548    case Nil{}:
1549      {==}
1550    case h <> t:
1551      {==}
1552
1553# An append is empty exactly when both parts are.
1554law is_empty_append:
1555  for -a: Quant
1556  for -A: Kind(a)
1557  for xs: List<a, A>
1558  for -ys: List<a, A>
1559  {List.is_empty(a, A, List.append(a, A, xs, ys)) == Bool.and(List.is_empty(a, A, xs), List.is_empty(a, A, ys)) : Bool}
1560
1561def is_empty_append(a, A, xs, ys):
1562  match xs:
1563    case Nil{}:
1564      {==}
1565    case h <> t:
1566      {==}
1567
1568def internal_is_empty_reverse_go(a, -A: Kind(a), xs: List<a, A>, -h: A, -acc: List<a, A>) -> {List.is_empty(a, A, List.reverse.go(a, A, xs, h <> acc)) == False{} : Bool}:
1569  match xs:
1570    case Nil{}:
1571      {==}
1572    case y <> t:
1573      internal_is_empty_reverse_go(a, A, t, y, h <> acc)
1574
1575# The reverse is empty exactly when the list is.
1576law is_empty_reverse:
1577  for -a: Quant
1578  for -A: Kind(a)
1579  for xs: List<a, A>
1580  {List.is_empty(a, A, List.reverse(a, A, xs)) == List.is_empty(a, A, xs) : Bool}
1581
1582def is_empty_reverse(a, A, xs):
1583  match xs:
1584    case Nil{}:
1585      {==}
1586    case h <> t:
1587      internal_is_empty_reverse_go(a, A, t, h, Nil{})
1588
1589# A map is empty exactly when the list is.
1590law is_empty_map:
1591  for ~A: Type
1592  for ~B: Type
1593  for ~f: A -> B
1594  for xs: List<A>
1595  {List.is_empty(&1, B, List.map(~A, ~B, ~f, xs)) == List.is_empty(&1, A, xs) : Bool}
1596
1597def is_empty_map(A, B, f, xs):
1598  match xs:
1599    case Nil{}:
1600      {==}
1601    case h <> t:
1602      {==}
1603
1604def internal_reverse_filter_put(-A: Data, -h: A, r: List<&2, A>, b: Bool) -> {List.append(&2, A, List.reverse(&2, A, r), List.filter.put(A, h, Nil{}, b)) == List.reverse(&2, A, List.filter.put(A, h, r, b)) : List<&2, A>}:
1605  match b:
1606    case False{}:
1607      append_nil(&2, A, List.reverse(&2, A, r))
1608    case True{}:
1609      Equal.sym(List<&2, A>, List.reverse.go(&2, A, r, [h]), List.append(&2, A, List.reverse(&2, A, r), [h]), reverse_go_spec(&2, A, r, [h]))
1610
1611# Filtering commutes with reversing: filter p (reverse xs) = reverse (filter p xs).
1612law filter_reverse:
1613  for ~A: Data
1614  for ~f: A -> Bool
1615  for xs: List<&2, A>
1616  {List.filter(~A, ~f, List.reverse(&2, A, xs)) == List.reverse(&2, A, List.filter(~A, ~f, xs)) : List<&2, A>}
1617
1618def filter_reverse(A, f, xs):
1619  match xs:
1620    case Nil{}:
1621      {==}
1622    case +h <> t:
1623      +t = t
1624      %Equal.sym(List<&2, A>, List.reverse.go(&2, A, t, [h]), List.append(&2, A, List.reverse(&2, A, t), [h]), reverse_go_spec(&2, A, t, [h])) : {List.filter(~A, ~f, _) == List.reverse(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))) : List<&2, A>}
1625      %Equal.sym(List<&2, A>, List.filter(~A, ~f, List.append(&2, A, List.reverse(&2, A, t), [h])), List.append(&2, A, List.filter(~A, ~f, List.reverse(&2, A, t)), List.filter(~A, ~f, [h])), filter_append(~A, ~f, List.reverse(&2, A, t), [h])) : {_ == List.reverse(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))) : List<&2, A>}
1626      %Equal.sym(List<&2, A>, List.filter(~A, ~f, List.reverse(&2, A, t)), List.reverse(&2, A, List.filter(~A, ~f, t)), filter_reverse(~A, ~f, t)) : {List.append(&2, A, _, List.filter(~A, ~f, [h])) == List.reverse(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))) : List<&2, A>}
1627      internal_reverse_filter_put(A, h, List.filter(~A, ~f, t), f(h))
1628
1629# Folding cons from the right, starting from the empty list, rebuilds the list.
1630law foldr_cons_nil:
1631  for ~a: Quant
1632  for ~A: Kind(a)
1633  for xs: List<a, A>
1634  {List.foldr(~a, ~A, ~List<a, A>, ~(x => acc => x <> acc), xs, Nil{}) == xs : List<a, A>}
1635
1636def foldr_cons_nil(a, A, xs):
1637  match xs:
1638    case Nil{}:
1639      {==}
1640    case h <> t:
1641      %foldr_cons_nil(~a, ~A, t) : {h <> List.foldr(~a, ~A, ~List<a, A>, ~(x => acc => x <> acc), t, Nil{}) == h <> _ : List<a, A>}
1642      {==}
1643
1644def internal_foldl_reverse_go(~a: Quant, ~A: Kind(a), ~B: Type, ~f: B -> A -> B, xs: List<a, A>, -acc: List<a, A>, -z: B) -> {List.foldl(~a, ~A, ~B, ~f, List.reverse.go(a, A, xs, acc), z) == List.foldl(~a, ~A, ~B, ~f, acc, List.foldr(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z)) : B}:
1645  match xs:
1646    case Nil{}:
1647      {==}
1648    case h <> t:
1649      internal_foldl_reverse_go(~a, ~A, ~B, ~f, t, h <> acc, z)
1650
1651# A left fold over the reverse is a right fold with the arguments flipped.
1652law foldl_reverse:
1653  for ~a: Quant
1654  for ~A: Kind(a)
1655  for ~B: Type
1656  for ~f: B -> A -> B
1657  for xs: List<a, A>
1658  for -z: B
1659  {List.foldl(~a, ~A, ~B, ~f, List.reverse(a, A, xs), z) == List.foldr(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z) : B}
1660
1661def foldl_reverse(a, A, B, f, xs, z):
1662  internal_foldl_reverse_go(~a, ~A, ~B, ~f, xs, Nil{}, z)
1663
1664def internal_foldr_reverse_go(~a: Quant, ~A: Kind(a), ~B: Type, ~f: A -> B -> B, xs: List<a, A>, -acc: List<a, A>, -z: B) -> {List.foldr(~a, ~A, ~B, ~f, List.reverse.go(a, A, xs, acc), z) == List.foldl(~a, ~A, ~B, ~(x => y => f(y, x)), xs, List.foldr(~a, ~A, ~B, ~f, acc, z)) : B}:
1665  match xs:
1666    case Nil{}:
1667      {==}
1668    case h <> t:
1669      internal_foldr_reverse_go(~a, ~A, ~B, ~f, t, h <> acc, z)
1670
1671# A right fold over the reverse is a left fold with the arguments flipped.
1672law foldr_reverse:
1673  for ~a: Quant
1674  for ~A: Kind(a)
1675  for ~B: Type
1676  for ~f: A -> B -> B
1677  for xs: List<a, A>
1678  for -z: B
1679  {List.foldr(~a, ~A, ~B, ~f, List.reverse(a, A, xs), z) == List.foldl(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z) : B}
1680
1681def foldr_reverse(a, A, B, f, xs, z):
1682  internal_foldr_reverse_go(~a, ~A, ~B, ~f, xs, Nil{}, z)
1683
1684def internal_range_go_append(+n: Nat, -ys: List<&2, Nat>, -acc: List<&2, Nat>) -> {List.range.go(n, List.append(&2, Nat, ys, acc)) == List.append(&2, Nat, List.range.go(n, ys), acc) : List<&2, Nat>}:
1685  match n:
1686    case 0n:
1687      {==}
1688    case 1n+p:
1689      internal_range_go_append(p, p <> ys, acc)
1690
1691# Range(n + 1) is range(n) followed by n.
1692law range_succ:
1693  for n: Nat
1694  {List.range(1n+n) == List.append(&2, Nat, List.range(n), [n]) : List<&2, Nat>}
1695
1696def range_succ(n):
1697  +n = n
1698  internal_range_go_append(n, Nil{}, [n])
1699
1700def internal_find_put_or(-A: Data, h: A, r: Maybe<&2, A>, -s: Maybe<&2, A>, b: Bool) -> {Maybe.or(&2, A, List.find.put(A, h, r, b), s) == List.find.put(A, h, Maybe.or(&2, A, r, s), b) : Maybe<&2, A>}:
1701  match b:
1702    case False{}:
1703      {==}
1704    case True{}:
1705      {==}
1706
1707# Finding in an append finds in the first part, or else in the second.
1708law find_append:
1709  for ~A: Data
1710  for ~f: A -> Bool
1711  for xs: List<&2, A>
1712  for ys: List<&2, A>
1713  {List.find(~A, ~f, List.append(&2, A, xs, ys)) == Maybe.or(&2, A, List.find(~A, ~f, xs), List.find(~A, ~f, ys)) : Maybe<&2, A>}
1714
1715def find_append(A, f, xs, ys):
1716  match xs:
1717    case Nil{}:
1718      {==}
1719    case +h <> t:
1720      +ys = ys
1721      +t = t
1722      %Equal.sym(Maybe<&2, A>, List.find(~A, ~f, List.append(&2, A, t, ys)), Maybe.or(&2, A, List.find(~A, ~f, t), List.find(~A, ~f, ys)), find_append(~A, ~f, t, ys)) : {List.find.put(A, h, _, f(h)) == Maybe.or(&2, A, List.find.put(A, h, List.find(~A, ~f, t), f(h)), List.find(~A, ~f, ys)) : Maybe<&2, A>}
1723      Equal.sym(Maybe<&2, A>, Maybe.or(&2, A, List.find.put(A, h, List.find(~A, ~f, t), f(h)), List.find(~A, ~f, ys)), List.find.put(A, h, Maybe.or(&2, A, List.find(~A, ~f, t), List.find(~A, ~f, ys)), f(h)), internal_find_put_or(A, h, List.find(~A, ~f, t), List.find(~A, ~f, ys), f(h)))
1724
1725def internal_and_not_eq_not_or_not(b: Bool, -s: Bool) -> {Bool.and(b, Bool.not(s)) == Bool.not(Bool.or(Bool.not(b), s)) : Bool}:
1726  match b:
1727    case False{}:
1728      {==}
1729    case True{}:
1730      {==}
1731
1732# All elements satisfy f exactly when no element fails it.
1733law all_eq_not_any_not:
1734  for ~a: Quant
1735  for ~A: Kind(a)
1736  for ~f: A -> Bool
1737  for xs: List<a, A>
1738  {List.all(~a, ~A, ~f, xs) == Bool.not(List.any(~a, ~A, ~(x => Bool.not(f(x))), xs)) : Bool}
1739
1740def all_eq_not_any_not(a, A, f, xs):
1741  match xs:
1742    case Nil{}:
1743      {==}
1744    case h <> t:
1745      %Equal.sym(Bool, List.all(~a, ~A, ~f, t), Bool.not(List.any(~a, ~A, ~(x => Bool.not(f(x))), t)), all_eq_not_any_not(~a, ~A, ~f, t)) : {Bool.and(f(h), _) == Bool.not(Bool.or(Bool.not(f(h)), List.any(~a, ~A, ~(x => Bool.not(f(x))), t))) : Bool}
1746      internal_and_not_eq_not_or_not(f(h), List.any(~a, ~A, ~(x => Bool.not(f(x))), t))
1747
1748def internal_or_not_eq_not_and_not(b: Bool, -s: Bool) -> {Bool.or(b, Bool.not(s)) == Bool.not(Bool.and(Bool.not(b), s)) : Bool}:
1749  match b:
1750    case False{}:
1751      {==}
1752    case True{}:
1753      {==}
1754
1755# Some element satisfies f exactly when not all elements fail it.
1756law any_eq_not_all_not:
1757  for ~a: Quant
1758  for ~A: Kind(a)
1759  for ~f: A -> Bool
1760  for xs: List<a, A>
1761  {List.any(~a, ~A, ~f, xs) == Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), xs)) : Bool}
1762
1763def any_eq_not_all_not(a, A, f, xs):
1764  match xs:
1765    case Nil{}:
1766      {==}
1767    case h <> t:
1768      %Equal.sym(Bool, List.any(~a, ~A, ~f, t), Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), t)), any_eq_not_all_not(~a, ~A, ~f, t)) : {Bool.or(f(h), _) == Bool.not(Bool.and(Bool.not(f(h)), List.all(~a, ~A, ~(x => Bool.not(f(x))), t))) : Bool}
1769      internal_or_not_eq_not_and_not(f(h), List.all(~a, ~A, ~(x => Bool.not(f(x))), t))
1770
1771# A one-element list has length one.
1772law length_singleton:
1773  for -a: Quant
1774  for -A: Kind(a)
1775  for -x: A
1776  {List.length(a, A, [x]) == 1n : Nat}
1777
1778def length_singleton(a, A, x):
1779  {==}
1780
1781# Reversing a cons puts its head last: reverse (x :: xs) = reverse xs ++ [x].
1782law reverse_cons:
1783  for -a: Quant
1784  for -A: Kind(a)
1785  for -x: A
1786  for xs: List<a, A>
1787  {List.reverse(a, A, x <> xs) == List.append(a, A, List.reverse(a, A, xs), [x]) : List<a, A>}
1788
1789def reverse_cons(a, A, x, xs):
1790  reverse_go_spec(a, A, xs, [x])
1791
1792# Taking n + 1 elements of a cons keeps its head and takes n from its tail.
1793law take_succ:
1794  for -a: Quant
1795  for -A: Kind(a)
1796  for -x: A
1797  for -xs: List<a, A>
1798  for -n: Nat
1799  {List.take(a, A, x <> xs, 1n+n) == x <> List.take(a, A, xs, n) : List<a, A>}
1800
1801def take_succ(a, A, x, xs, n):
1802  {==}
1803
1804# Dropping n + 1 elements of a cons drops its head and n from its tail.
1805law drop_succ:
1806  for -a: Quant
1807  for -A: Kind(a)
1808  for -x: A
1809  for -xs: List<a, A>
1810  for -n: Nat
1811  {List.drop(a, A, x <> xs, 1n+n) == List.drop(a, A, xs, n) : List<a, A>}
1812
1813def drop_succ(a, A, x, xs, n):
1814  {==}
1815
1816# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
1817
1818# The empty list is a right identity for append: xs ++ [] = xs, reversed to rewrite toward the simple side.
1819law append_nil_sym:
1820  for -a: Quant
1821  for -A: Kind(a)
1822  for xs: List<a, A>
1823  {xs == List.append(a, A, xs, Nil{}) : List<a, A>}
1824
1825def append_nil_sym(a, A, xs):
1826  Equal.sym(List<a, A>, List.append(a, A, xs, Nil{}), xs, append_nil(a, A, xs))
1827
1828# The empty list is a left identity for append: [] ++ xs = xs, reversed to rewrite toward the simple side.
1829law nil_append_sym:
1830  for -a: Quant
1831  for -A: Kind(a)
1832  for -xs: List<a, A>
1833  {xs == List.append(a, A, Nil{}, xs) : List<a, A>}
1834
1835def nil_append_sym(a, A, xs):
1836  Equal.sym(List<a, A>, List.append(a, A, Nil{}, xs), xs, nil_append(a, A, xs))
1837
1838# Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs), reversed to rewrite toward the simple side.
1839law append_assoc_sym:
1840  for -a: Quant
1841  for -A: Kind(a)
1842  for xs: List<a, A>
1843  for -ys: List<a, A>
1844  for -zs: List<a, A>
1845  {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>}
1846
1847def append_assoc_sym(a, A, xs, ys, zs):
1848  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))
1849
1850# The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.
1851law length_append_sym:
1852  for -a: Quant
1853  for -A: Kind(a)
1854  for xs: List<a, A>
1855  for -ys: List<a, A>
1856  {Nat.add(List.length(a, A, xs), List.length(a, A, ys)) == List.length(a, A, List.append(a, A, xs, ys)) : Nat}
1857
1858def length_append_sym(a, A, xs, ys):
1859  Equal.sym(Nat, List.length(a, A, List.append(a, A, xs, ys)), Nat.add(List.length(a, A, xs), List.length(a, A, ys)), length_append(a, A, xs, ys))
1860
1861# The reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side.
1862law reverse_go_spec_sym:
1863  for -a: Quant
1864  for -A: Kind(a)
1865  for xs: List<a, A>
1866  for -acc: List<a, A>
1867  {List.append(a, A, List.reverse(a, A, xs), acc) == List.reverse.go(a, A, xs, acc) : List<a, A>}
1868
1869def reverse_go_spec_sym(a, A, xs, acc):
1870  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))
1871
1872# Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side.
1873law reverse_append_sym:
1874  for -a: Quant
1875  for -A: Kind(a)
1876  for xs: List<a, A>
1877  for ys: List<a, A>
1878  {List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) == List.reverse(a, A, List.append(a, A, xs, ys)) : List<a, A>}
1879
1880def reverse_append_sym(a, A, xs, ys):
1881  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))
1882
1883# Reversing twice gives the list back, reversed to rewrite toward the simple side.
1884law reverse_reverse_sym:
1885  for -a: Quant
1886  for -A: Kind(a)
1887  for xs: List<a, A>
1888  {xs == List.reverse(a, A, List.reverse(a, A, xs)) : List<a, A>}
1889
1890def reverse_reverse_sym(a, A, xs):
1891  Equal.sym(List<a, A>, List.reverse(a, A, List.reverse(a, A, xs)), xs, reverse_reverse(a, A, xs))
1892
1893# Reversing preserves the length, reversed to rewrite toward the simple side.
1894law length_reverse_sym:
1895  for -a: Quant
1896  for -A: Kind(a)
1897  for xs: List<a, A>
1898  {List.length(a, A, xs) == List.length(a, A, List.reverse(a, A, xs)) : Nat}
1899
1900def length_reverse_sym(a, A, xs):
1901  Equal.sym(Nat, List.length(a, A, List.reverse(a, A, xs)), List.length(a, A, xs), length_reverse(a, A, xs))
1902
1903# A right fold over an append folds the first part onto the fold of the second, reversed to rewrite toward the simple side.
1904law foldr_append_sym:
1905  for ~a: Quant
1906  for ~A: Kind(a)
1907  for ~B: Type
1908  for ~f: A -> B -> B
1909  for xs: List<a, A>
1910  for -ys: List<a, A>
1911  for -z: B
1912  {List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)) == List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) : B}
1913
1914def foldr_append_sym(a, A, B, f, xs, ys, z):
1915  Equal.sym(B, List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z), List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)), foldr_append(~a, ~A, ~B, ~f, xs, ys, z))
1916
1917# Taking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side.
1918law take_append_drop_sym:
1919  for -a: Quant
1920  for -A: Kind(a)
1921  for xs: List<a, A>
1922  for n: Nat
1923  {xs == List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) : List<a, A>}
1924
1925def take_append_drop_sym(a, A, xs, n):
1926  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))
1927
1928# Mapping preserves the length, reversed to rewrite toward the simple side.
1929law length_map_sym:
1930  for ~A: Type
1931  for ~B: Type
1932  for ~f: A -> B
1933  for xs: List<A>
1934  {List.length(&1, A, xs) == List.length(&1, B, List.map(~A, ~B, ~f, xs)) : Nat}
1935
1936def length_map_sym(A, B, f, xs):
1937  Equal.sym(Nat, List.length(&1, B, List.map(~A, ~B, ~f, xs)), List.length(&1, A, xs), length_map(~A, ~B, ~f, xs))
1938
1939# Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side.
1940law map_append_sym:
1941  for ~A: Type
1942  for ~B: Type
1943  for ~f: A -> B
1944  for xs: List<A>
1945  for -ys: List<A>
1946  {List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)) == List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)) : List<B>}
1947
1948def map_append_sym(A, B, f, xs, ys):
1949  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))
1950
1951# Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs, reversed to rewrite toward the simple side.
1952law map_map_sym:
1953  for ~A: Type
1954  for ~B: Type
1955  for ~C: Type
1956  for ~f: A -> B
1957  for ~g: B -> C
1958  for xs: List<A>
1959  {List.map(~A, ~C, ~(x => g(f(x))), xs) == List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) : List<C>}
1960
1961def map_map_sym(A, B, C, f, g, xs):
1962  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))
1963
1964# Taking zero elements gives the empty list, reversed to rewrite toward the simple side.
1965law take_zero_sym:
1966  for -a: Quant
1967  for -A: Kind(a)
1968  for xs: List<a, A>
1969  {Nil{} == List.take(a, A, xs, 0n) : List<a, A>}
1970
1971def take_zero_sym(a, A, xs):
1972  Equal.sym(List<a, A>, List.take(a, A, xs, 0n), Nil{}, take_zero(a, A, xs))
1973
1974# Dropping zero elements gives the list back, reversed to rewrite toward the simple side.
1975law drop_zero_sym:
1976  for -a: Quant
1977  for -A: Kind(a)
1978  for xs: List<a, A>
1979  {xs == List.drop(a, A, xs, 0n) : List<a, A>}
1980
1981def drop_zero_sym(a, A, xs):
1982  Equal.sym(List<a, A>, List.drop(a, A, xs, 0n), xs, drop_zero(a, A, xs))
1983
1984# Taking from the empty list gives the empty list, reversed to rewrite toward the simple side.
1985law take_nil_sym:
1986  for -a: Quant
1987  for -A: Kind(a)
1988  for -n: Nat
1989  {Nil{} == List.take(a, A, Nil{}, n) : List<a, A>}
1990
1991def take_nil_sym(a, A, n):
1992  Equal.sym(List<a, A>, List.take(a, A, Nil{}, n), Nil{}, take_nil(a, A, n))
1993
1994# Dropping from the empty list gives the empty list, reversed to rewrite toward the simple side.
1995law drop_nil_sym:
1996  for -a: Quant
1997  for -A: Kind(a)
1998  for -n: Nat
1999  {Nil{} == List.drop(a, A, Nil{}, n) : List<a, A>}
2000
2001def drop_nil_sym(a, A, n):
2002  Equal.sym(List<a, A>, List.drop(a, A, Nil{}, n), Nil{}, drop_nil(a, A, n))
2003
2004# Taking n elements leaves min(n, length) of them, reversed to rewrite toward the simple side.
2005law length_take_sym:
2006  for -a: Quant
2007  for -A: Kind(a)
2008  for xs: List<a, A>
2009  for n: Nat
2010  {Nat.min(n, List.length(a, A, xs)) == List.length(a, A, List.take(a, A, xs, n)) : Nat}
2011
2012def length_take_sym(a, A, xs, n):
2013  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))
2014
2015# Dropping n elements leaves length - n of them, reversed to rewrite toward the simple side.
2016law length_drop_sym:
2017  for -a: Quant
2018  for -A: Kind(a)
2019  for xs: List<a, A>
2020  for n: Nat
2021  {Nat.sub(List.length(a, A, xs), n) == List.length(a, A, List.drop(a, A, xs, n)) : Nat}
2022
2023def length_drop_sym(a, A, xs, n):
2024  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))
2025
2026# Taking as many elements as the list has gives the list back, reversed to rewrite toward the simple side.
2027law take_length_sym:
2028  for -A: Data
2029  for +xs: List<&2, A>
2030  {xs == List.take(&2, A, xs, List.length(&2, A, xs)) : List<&2, A>}
2031
2032def take_length_sym(A, xs):
2033  Equal.sym(List<&2, A>, List.take(&2, A, xs, List.length(&2, A, xs)), xs, take_length(A, xs))
2034
2035# Dropping as many elements as the list has gives the empty list, reversed to rewrite toward the simple side.
2036law drop_length_sym:
2037  for -A: Data
2038  for +xs: List<&2, A>
2039  {Nil{} == List.drop(&2, A, xs, List.length(&2, A, xs)) : List<&2, A>}
2040
2041def drop_length_sym(A, xs):
2042  Equal.sym(List<&2, A>, List.drop(&2, A, xs, List.length(&2, A, xs)), Nil{}, drop_length(A, xs))
2043
2044# Taking m from the first n is taking min(n, m), reversed to rewrite toward the simple side.
2045law take_take_sym:
2046  for -a: Quant
2047  for -A: Kind(a)
2048  for xs: List<a, A>
2049  for n: Nat
2050  for m: Nat
2051  {List.take(a, A, xs, Nat.min(n, m)) == List.take(a, A, List.take(a, A, xs, n), m) : List<a, A>}
2052
2053def take_take_sym(a, A, xs, n, m):
2054  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))
2055
2056# Dropping m after dropping n is dropping n + m, reversed to rewrite toward the simple side.
2057law drop_drop_sym:
2058  for -a: Quant
2059  for -A: Kind(a)
2060  for xs: List<a, A>
2061  for n: Nat
2062  for -m: Nat
2063  {List.drop(a, A, xs, Nat.add(n, m)) == List.drop(a, A, List.drop(a, A, xs, n), m) : List<a, A>}
2064
2065def drop_drop_sym(a, A, xs, n, m):
2066  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))
2067
2068# Reversing the empty list gives the empty list, reversed to rewrite toward the simple side.
2069law reverse_nil_sym:
2070  for -a: Quant
2071  for -A: Kind(a)
2072  {Nil{} == List.reverse(a, A, Nil{}) : List<a, A>}
2073
2074def reverse_nil_sym(a, A):
2075  Equal.sym(List<a, A>, List.reverse(a, A, Nil{}), Nil{}, reverse_nil(a, A))
2076
2077# Reversing a one-element list gives it back, reversed to rewrite toward the simple side.
2078law reverse_singleton_sym:
2079  for -a: Quant
2080  for -A: Kind(a)
2081  for -x: A
2082  {[x] == List.reverse(a, A, [x]) : List<a, A>}
2083
2084def reverse_singleton_sym(a, A, x):
2085  Equal.sym(List<a, A>, List.reverse(a, A, [x]), [x], reverse_singleton(a, A, x))
2086
2087# Replicating x n times gives a list of length n, reversed to rewrite toward the simple side.
2088law length_replicate_sym:
2089  for -A: Data
2090  for n: Nat
2091  for -x: A
2092  {n == List.length(&2, A, List.replicate(A, n, x)) : Nat}
2093
2094def length_replicate_sym(A, n, x):
2095  Equal.sym(Nat, List.length(&2, A, List.replicate(A, n, x)), n, length_replicate(A, n, x))
2096
2097# Range(n) has length n, reversed to rewrite toward the simple side.
2098law length_range_sym:
2099  for n: Nat
2100  {n == List.length(&2, Nat, List.range(n)) : Nat}
2101
2102def length_range_sym(n):
2103  Equal.sym(Nat, List.length(&2, Nat, List.range(n)), n, length_range(n))
2104
2105# Zipping two lists gives the length of the shorter one, reversed to rewrite toward the simple side.
2106law length_zip_sym:
2107  for -a: Quant
2108  for -A: Kind(a)
2109  for xs: List<a, A>
2110  for ys: List<a, A>
2111  {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}
2112
2113def length_zip_sym(a, A, xs, ys):
2114  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))
2115
2116# Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys), reversed to rewrite toward the simple side.
2117law append_cons_sym:
2118  for -a: Quant
2119  for -A: Kind(a)
2120  for -x: A
2121  for -xs: List<a, A>
2122  for -ys: List<a, A>
2123  {x <> List.append(a, A, xs, ys) == List.append(a, A, x <> xs, ys) : List<a, A>}
2124
2125def append_cons_sym(a, A, x, xs, ys):
2126  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))
2127
2128# The empty list has length zero, reversed to rewrite toward the simple side.
2129law length_nil_sym:
2130  for -a: Quant
2131  for -A: Kind(a)
2132  {0n == List.length(a, A, Nil{}) : Nat}
2133
2134def length_nil_sym(a, A):
2135  Equal.sym(Nat, List.length(a, A, Nil{}), 0n, length_nil(a, A))
2136
2137# A cons is one longer than its tail, reversed to rewrite toward the simple side.
2138law length_cons_sym:
2139  for -a: Quant
2140  for -A: Kind(a)
2141  for -x: A
2142  for -xs: List<a, A>
2143  {1n+List.length(a, A, xs) == List.length(a, A, x <> xs) : Nat}
2144
2145def length_cons_sym(a, A, x, xs):
2146  Equal.sym(Nat, List.length(a, A, x <> xs), 1n+List.length(a, A, xs), length_cons(a, A, x, xs))
2147
2148# Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss, reversed to rewrite toward the simple side.
2149law concat_append_sym:
2150  for -a: Quant
2151  for -A: Kind(a)
2152  for xss: List<a, List<a, A>>
2153  for -yss: List<a, List<a, A>>
2154  {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>}
2155
2156def concat_append_sym(a, A, xss, yss):
2157  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))
2158
2159# A left fold over an append folds the second part from the fold of the first, reversed to rewrite toward the simple side.
2160law foldl_append_sym:
2161  for ~a: Quant
2162  for ~A: Kind(a)
2163  for ~B: Type
2164  for ~f: B -> A -> B
2165  for xs: List<a, A>
2166  for -ys: List<a, A>
2167  for -z: B
2168  {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}
2169
2170def foldl_append_sym(a, A, B, f, xs, ys, z):
2171  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))
2172
2173# Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs), reversed to rewrite toward the simple side.
2174law map_reverse_sym:
2175  for ~A: Type
2176  for ~B: Type
2177  for ~f: A -> B
2178  for xs: List<A>
2179  {List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) : List<B>}
2180
2181def map_reverse_sym(A, B, f, xs):
2182  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))
2183
2184# All over an append is all over each part, joined by and, reversed to rewrite toward the simple side.
2185law all_append_sym:
2186  for ~a: Quant
2187  for ~A: Kind(a)
2188  for ~f: A -> Bool
2189  for xs: List<a, A>
2190  for -ys: List<a, A>
2191  {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}
2192
2193def all_append_sym(a, A, f, xs, ys):
2194  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))
2195
2196# Any over an append is any over each part, joined by or, reversed to rewrite toward the simple side.
2197law any_append_sym:
2198  for ~a: Quant
2199  for ~A: Kind(a)
2200  for ~f: A -> Bool
2201  for xs: List<a, A>
2202  for -ys: List<a, A>
2203  {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}
2204
2205def any_append_sym(a, A, f, xs, ys):
2206  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))
2207
2208# Filtering an append filters each part, reversed to rewrite toward the simple side.
2209law filter_append_sym:
2210  for ~A: Data
2211  for ~f: A -> Bool
2212  for xs: List<&2, A>
2213  for ys: List<&2, A>
2214  {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>}
2215
2216def filter_append_sym(A, f, xs, ys):
2217  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))
2218
2219# An append contains x iff either part does, reversed to rewrite toward the simple side.
2220law contains_append_sym:
2221  for ~A: Data
2222  for ~eq: A -> A -> Bool
2223  for xs: List<&2, A>
2224  for -ys: List<&2, A>
2225  for +x: A
2226  {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}
2227
2228def contains_append_sym(A, eq, xs, ys, x):
2229  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))
2230
2231# Filtering never makes a list longer, reversed to rewrite toward the simple side.
2232law length_filter_le_sym:
2233  for ~A: Data
2234  for ~f: A -> Bool
2235  for xs: List<&2, A>
2236  {True{} == Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)) : Bool}
2237
2238def length_filter_le_sym(A, f, xs):
2239  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))
2240
2241# Taking the length of the first part of an append gives the first part back, reversed to rewrite toward the simple side.
2242law take_left_sym:
2243  for -a: Quant
2244  for -A: Kind(a)
2245  for xs: List<a, A>
2246  for ys: List<a, A>
2247  {xs == List.take(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) : List<a, A>}
2248
2249def take_left_sym(a, A, xs, ys):
2250  Equal.sym(List<a, A>, List.take(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)), xs, take_left(a, A, xs, ys))
2251
2252# Dropping the length of the first part of an append gives the second part, reversed to rewrite toward the simple side.
2253law drop_left_sym:
2254  for -a: Quant
2255  for -A: Kind(a)
2256  for xs: List<a, A>
2257  for ys: List<a, A>
2258  {ys == List.drop(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) : List<a, A>}
2259
2260def drop_left_sym(a, A, xs, ys):
2261  Equal.sym(List<a, A>, List.drop(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)), ys, drop_left(a, A, xs, ys))
2262
2263# Taking past the first part of an append keeps it and takes the rest from the second part, reversed to rewrite toward the simple side.
2264law take_append_sym:
2265  for -a: Quant
2266  for -A: Kind(a)
2267  for xs: List<a, A>
2268  for -ys: List<a, A>
2269  for -n: Nat
2270  {List.append(a, A, xs, List.take(a, A, ys, n)) == List.take(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)) : List<a, A>}
2271
2272def take_append_sym(a, A, xs, ys, n):
2273  Equal.sym(List<a, A>, List.take(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)), List.append(a, A, xs, List.take(a, A, ys, n)), take_append(a, A, xs, ys, n))
2274
2275# Dropping past the first part of an append drops the rest from the second part, reversed to rewrite toward the simple side.
2276law drop_append_sym:
2277  for -a: Quant
2278  for -A: Kind(a)
2279  for xs: List<a, A>
2280  for -ys: List<a, A>
2281  for -n: Nat
2282  {List.drop(a, A, ys, n) == List.drop(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)) : List<a, A>}
2283
2284def drop_append_sym(a, A, xs, ys, n):
2285  Equal.sym(List<a, A>, List.drop(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)), List.drop(a, A, ys, n), drop_append(a, A, xs, ys, n))
2286
2287# Taking at most the length of the first part of an append only sees the first part, reversed to rewrite toward the simple side.
2288law take_append_of_le_length_sym:
2289  for -a: Quant
2290  for -A: Kind(a)
2291  for xs: List<a, A>
2292  for ys: List<a, A>
2293  for n: Nat
2294  for h: MNat.le(n, List.length(a, A, xs))
2295  {List.take(a, A, xs, n) == List.take(a, A, List.append(a, A, xs, ys), n) : List<a, A>}
2296
2297def take_append_of_le_length_sym(a, A, xs, ys, n, h):
2298  Equal.sym(List<a, A>, List.take(a, A, List.append(a, A, xs, ys), n), List.take(a, A, xs, n), take_append_of_le_length(a, A, xs, ys, n, h))
2299
2300# Dropping at most the length of the first part of an append drops only from the first part, reversed to rewrite toward the simple side.
2301law drop_append_of_le_length_sym:
2302  for -a: Quant
2303  for -A: Kind(a)
2304  for xs: List<a, A>
2305  for ys: List<a, A>
2306  for n: Nat
2307  for h: MNat.le(n, List.length(a, A, xs))
2308  {List.append(a, A, List.drop(a, A, xs, n), ys) == List.drop(a, A, List.append(a, A, xs, ys), n) : List<a, A>}
2309
2310def drop_append_of_le_length_sym(a, A, xs, ys, n, h):
2311  Equal.sym(List<a, A>, List.drop(a, A, List.append(a, A, xs, ys), n), List.append(a, A, List.drop(a, A, xs, n), ys), drop_append_of_le_length(a, A, xs, ys, n, h))
2312
2313# Mapping commutes with taking: map f (take n xs) = take n (map f xs), reversed to rewrite toward the simple side.
2314law map_take_sym:
2315  for ~A: Type
2316  for ~B: Type
2317  for ~f: A -> B
2318  for xs: List<A>
2319  for n: Nat
2320  {List.take(&1, B, List.map(~A, ~B, ~f, xs), n) == List.map(~A, ~B, ~f, List.take(&1, A, xs, n)) : List<B>}
2321
2322def map_take_sym(A, B, f, xs, n):
2323  Equal.sym(List<B>, List.map(~A, ~B, ~f, List.take(&1, A, xs, n)), List.take(&1, B, List.map(~A, ~B, ~f, xs), n), map_take(~A, ~B, ~f, xs, n))
2324
2325# Mapping commutes with dropping: map f (drop n xs) = drop n (map f xs), reversed to rewrite toward the simple side.
2326law map_drop_sym:
2327  for ~A: Type
2328  for ~B: Type
2329  for ~f: A -> B
2330  for xs: List<A>
2331  for n: Nat
2332  {List.drop(&1, B, List.map(~A, ~B, ~f, xs), n) == List.map(~A, ~B, ~f, List.drop(&1, A, xs, n)) : List<B>}
2333
2334def map_drop_sym(A, B, f, xs, n):
2335  Equal.sym(List<B>, List.map(~A, ~B, ~f, List.drop(&1, A, xs, n)), List.drop(&1, B, List.map(~A, ~B, ~f, xs), n), map_drop(~A, ~B, ~f, xs, n))
2336
2337# Taking m from n copies of x gives min(m, n) copies of x, reversed to rewrite toward the simple side.
2338law take_replicate_sym:
2339  for -A: Data
2340  for n: Nat
2341  for m: Nat
2342  for -x: A
2343  {List.replicate(A, Nat.min(m, n), x) == List.take(&2, A, List.replicate(A, n, x), m) : List<&2, A>}
2344
2345def take_replicate_sym(A, n, m, x):
2346  Equal.sym(List<&2, A>, List.take(&2, A, List.replicate(A, n, x), m), List.replicate(A, Nat.min(m, n), x), take_replicate(A, n, m, x))
2347
2348# Dropping m from n copies of x gives n - m copies of x, reversed to rewrite toward the simple side.
2349law drop_replicate_sym:
2350  for -A: Data
2351  for n: Nat
2352  for m: Nat
2353  for -x: A
2354  {List.replicate(A, Nat.sub(n, m), x) == List.drop(&2, A, List.replicate(A, n, x), m) : List<&2, A>}
2355
2356def drop_replicate_sym(A, n, m, x):
2357  Equal.sym(List<&2, A>, List.drop(&2, A, List.replicate(A, n, x), m), List.replicate(A, Nat.sub(n, m), x), drop_replicate(A, n, m, x))
2358
2359# The tail is one shorter than the list, or empty: length (tail xs) = length xs - 1, reversed to rewrite toward the simple side.
2360law length_tail_sym:
2361  for -a: Quant
2362  for -A: Kind(a)
2363  for xs: List<a, A>
2364  {Nat.sub(List.length(a, A, xs), 1n) == List.length(a, A, List.tail(a, A, xs)) : Nat}
2365
2366def length_tail_sym(a, A, xs):
2367  Equal.sym(Nat, List.length(a, A, List.tail(a, A, xs)), Nat.sub(List.length(a, A, xs), 1n), length_tail(a, A, xs))
2368
2369# Mapping the identity gives the list back, reversed to rewrite toward the simple side.
2370law map_id_sym:
2371  for ~A: Type
2372  for xs: List<A>
2373  {xs == List.map(~A, ~A, ~(x => x), xs) : List<A>}
2374
2375def map_id_sym(A, xs):
2376  Equal.sym(List<A>, List.map(~A, ~A, ~(x => x), xs), xs, map_id(~A, xs))
2377
2378# A right fold over a map folds with the mapped function: foldr g z (map f xs) = foldr (g . f) z xs, reversed to rewrite toward the simple side.
2379law foldr_map_sym:
2380  for ~A: Type
2381  for ~B: Type
2382  for ~C: Type
2383  for ~f: A -> B
2384  for ~g: B -> C -> C
2385  for xs: List<A>
2386  for -z: C
2387  {List.foldr(~&1, ~A, ~C, ~(x => y => g(f(x), y)), xs, z) == List.foldr(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, xs), z) : C}
2388
2389def foldr_map_sym(A, B, C, f, g, xs, z):
2390  Equal.sym(C, List.foldr(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, xs), z), List.foldr(~&1, ~A, ~C, ~(x => y => g(f(x), y)), xs, z), foldr_map(~A, ~B, ~C, ~f, ~g, xs, z))
2391
2392# A left fold over a map folds with the mapped function: foldl g z (map f xs) = foldl (fun acc x => g acc (f x)) z xs, reversed to rewrite toward the simple side.
2393law foldl_map_sym:
2394  for ~A: Type
2395  for ~B: Type
2396  for ~C: Type
2397  for ~f: A -> B
2398  for ~g: C -> B -> C
2399  for xs: List<A>
2400  for -z: C
2401  {List.foldl(~&1, ~A, ~C, ~(x => y => g(x, f(y))), xs, z) == List.foldl(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, xs), z) : C}
2402
2403def foldl_map_sym(A, B, C, f, g, xs, z):
2404  Equal.sym(C, List.foldl(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, xs), z), List.foldl(~&1, ~A, ~C, ~(x => y => g(x, f(y))), xs, z), foldl_map(~A, ~B, ~C, ~f, ~g, xs, z))
2405
2406# Replicating m + n times appends m copies to n copies, reversed to rewrite toward the simple side.
2407law replicate_add_sym:
2408  for -A: Data
2409  for m: Nat
2410  for -n: Nat
2411  for -x: A
2412  {List.append(&2, A, List.replicate(A, m, x), List.replicate(A, n, x)) == List.replicate(A, Nat.add(m, n), x) : List<&2, A>}
2413
2414def replicate_add_sym(A, m, n, x):
2415  Equal.sym(List<&2, A>, List.replicate(A, Nat.add(m, n), x), List.append(&2, A, List.replicate(A, m, x), List.replicate(A, n, x)), replicate_add(A, m, n, x))
2416
2417# Reversing n copies of x gives them back, reversed to rewrite toward the simple side.
2418law reverse_replicate_sym:
2419  for -A: Data
2420  for n: Nat
2421  for -x: A
2422  {List.replicate(A, n, x) == List.reverse(&2, A, List.replicate(A, n, x)) : List<&2, A>}
2423
2424def reverse_replicate_sym(A, n, x):
2425  Equal.sym(List<&2, A>, List.reverse(&2, A, List.replicate(A, n, x)), List.replicate(A, n, x), reverse_replicate(A, n, x))
2426
2427# Filtering with an always-true predicate gives the list back, reversed to rewrite toward the simple side.
2428law filter_true_sym:
2429  for ~A: Data
2430  for xs: List<&2, A>
2431  {xs == List.filter(~A, ~(x => True{}), xs) : List<&2, A>}
2432
2433def filter_true_sym(A, xs):
2434  Equal.sym(List<&2, A>, List.filter(~A, ~(x => True{}), xs), xs, filter_true(~A, xs))
2435
2436# Filtering with an always-false predicate gives the empty list, reversed to rewrite toward the simple side.
2437law filter_false_sym:
2438  for ~A: Data
2439  for xs: List<&2, A>
2440  {Nil{} == List.filter(~A, ~(x => False{}), xs) : List<&2, A>}
2441
2442def filter_false_sym(A, xs):
2443  Equal.sym(List<&2, A>, List.filter(~A, ~(x => False{}), xs), Nil{}, filter_false(~A, xs))
2444
2445# Filtering twice is filtering by both predicates: filter p (filter q xs) = filter (p and q) xs, reversed to rewrite toward the simple side.
2446law filter_filter_sym:
2447  for ~A: Data
2448  for ~p: A -> Bool
2449  for ~q: A -> Bool
2450  for xs: List<&2, A>
2451  {List.filter(~A, ~(+x => Bool.and(p(x), q(x))), xs) == List.filter(~A, ~p, List.filter(~A, ~q, xs)) : List<&2, A>}
2452
2453def filter_filter_sym(A, p, q, xs):
2454  Equal.sym(List<&2, A>, List.filter(~A, ~p, List.filter(~A, ~q, xs)), List.filter(~A, ~(+x => Bool.and(p(x), q(x))), xs), filter_filter(~A, ~p, ~q, xs))
2455
2456# All over a filter checks q only where p holds: all q (filter p xs) = all (not p or q) xs, reversed to rewrite toward the simple side.
2457law all_filter_sym:
2458  for ~A: Data
2459  for ~p: A -> Bool
2460  for ~q: A -> Bool
2461  for xs: List<&2, A>
2462  {List.all(~&2, ~A, ~(+x => Bool.or(Bool.not(p(x)), q(x))), xs) == List.all(~&2, ~A, ~q, List.filter(~A, ~p, xs)) : Bool}
2463
2464def all_filter_sym(A, p, q, xs):
2465  Equal.sym(Bool, List.all(~&2, ~A, ~q, List.filter(~A, ~p, xs)), List.all(~&2, ~A, ~(+x => Bool.or(Bool.not(p(x)), q(x))), xs), all_filter(~A, ~p, ~q, xs))
2466
2467# Any over a filter looks for q only where p holds: any q (filter p xs) = any (p and q) xs, reversed to rewrite toward the simple side.
2468law any_filter_sym:
2469  for ~A: Data
2470  for ~p: A -> Bool
2471  for ~q: A -> Bool
2472  for xs: List<&2, A>
2473  {List.any(~&2, ~A, ~(+x => Bool.and(p(x), q(x))), xs) == List.any(~&2, ~A, ~q, List.filter(~A, ~p, xs)) : Bool}
2474
2475def any_filter_sym(A, p, q, xs):
2476  Equal.sym(Bool, List.any(~&2, ~A, ~q, List.filter(~A, ~p, xs)), List.any(~&2, ~A, ~(+x => Bool.and(p(x), q(x))), xs), any_filter(~A, ~p, ~q, xs))
2477
2478# All over a map checks the composed predicate: all p (map f xs) = all (p . f) xs, reversed to rewrite toward the simple side.
2479law all_map_sym:
2480  for ~A: Type
2481  for ~B: Type
2482  for ~f: A -> B
2483  for ~p: B -> Bool
2484  for xs: List<A>
2485  {List.all(~&1, ~A, ~(x => p(f(x))), xs) == List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) : Bool}
2486
2487def all_map_sym(A, B, f, p, xs):
2488  Equal.sym(Bool, List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)), List.all(~&1, ~A, ~(x => p(f(x))), xs), all_map(~A, ~B, ~f, ~p, xs))
2489
2490# Any over a map checks the composed predicate: any p (map f xs) = any (p . f) xs, reversed to rewrite toward the simple side.
2491law any_map_sym:
2492  for ~A: Type
2493  for ~B: Type
2494  for ~f: A -> B
2495  for ~p: B -> Bool
2496  for xs: List<A>
2497  {List.any(~&1, ~A, ~(x => p(f(x))), xs) == List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) : Bool}
2498
2499def any_map_sym(A, B, f, p, xs):
2500  Equal.sym(Bool, List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)), List.any(~&1, ~A, ~(x => p(f(x))), xs), any_map(~A, ~B, ~f, ~p, xs))
2501
2502# Reversing does not change whether all elements satisfy a predicate, reversed to rewrite toward the simple side.
2503law all_reverse_sym:
2504  for ~a: Quant
2505  for ~A: Kind(a)
2506  for ~f: A -> Bool
2507  for xs: List<a, A>
2508  {List.all(~a, ~A, ~f, xs) == List.all(~a, ~A, ~f, List.reverse(a, A, xs)) : Bool}
2509
2510def all_reverse_sym(a, A, f, xs):
2511  Equal.sym(Bool, List.all(~a, ~A, ~f, List.reverse(a, A, xs)), List.all(~a, ~A, ~f, xs), all_reverse(~a, ~A, ~f, xs))
2512
2513# Reversing does not change whether some element satisfies a predicate, reversed to rewrite toward the simple side.
2514law any_reverse_sym:
2515  for ~a: Quant
2516  for ~A: Kind(a)
2517  for ~f: A -> Bool
2518  for xs: List<a, A>
2519  {List.any(~a, ~A, ~f, xs) == List.any(~a, ~A, ~f, List.reverse(a, A, xs)) : Bool}
2520
2521def any_reverse_sym(a, A, f, xs):
2522  Equal.sym(Bool, List.any(~a, ~A, ~f, List.reverse(a, A, xs)), List.any(~a, ~A, ~f, xs), any_reverse(~a, ~A, ~f, xs))
2523
2524# Reversing does not change whether a list contains x, reversed to rewrite toward the simple side.
2525law contains_reverse_sym:
2526  for ~A: Data
2527  for ~eq: A -> A -> Bool
2528  for xs: List<&2, A>
2529  for +x: A
2530  {List.contains(~A, ~eq, xs, x) == List.contains(~A, ~eq, List.reverse(&2, A, xs), x) : Bool}
2531
2532def contains_reverse_sym(A, eq, xs, x):
2533  Equal.sym(Bool, List.contains(~A, ~eq, List.reverse(&2, A, xs), x), List.contains(~A, ~eq, xs, x), contains_reverse(~A, ~eq, xs, x))
2534
2535# Zipping the empty list with anything gives the empty list, reversed to rewrite toward the simple side.
2536law zip_nil_left_sym:
2537  for -a: Quant
2538  for -A: Kind(a)
2539  for -b: Quant
2540  for -B: Kind(b)
2541  for -ys: List<b, B>
2542  {Nil{} == List.zip(a, A, b, B, Nil{}, ys) : List<&1, A & B>}
2543
2544def zip_nil_left_sym(a, A, b, B, ys):
2545  Equal.sym(List<&1, A & B>, List.zip(a, A, b, B, Nil{}, ys), Nil{}, zip_nil_left(a, A, b, B, ys))
2546
2547# Zipping anything with the empty list gives the empty list, reversed to rewrite toward the simple side.
2548law zip_nil_right_sym:
2549  for -a: Quant
2550  for -A: Kind(a)
2551  for -b: Quant
2552  for -B: Kind(b)
2553  for xs: List<a, A>
2554  {Nil{} == List.zip(a, A, b, B, xs, Nil{}) : List<&1, A & B>}
2555
2556def zip_nil_right_sym(a, A, b, B, xs):
2557  Equal.sym(List<&1, A & B>, List.zip(a, A, b, B, xs, Nil{}), Nil{}, zip_nil_right(a, A, b, B, xs))
2558
2559# The head of a cons is its first element, reversed to rewrite toward the simple side.
2560law head_cons_sym:
2561  for -a: Quant
2562  for -A: Kind(a)
2563  for -x: A
2564  for -xs: List<a, A>
2565  {Some{x} == List.head(a, A, x <> xs) : Maybe<a, A>}
2566
2567def head_cons_sym(a, A, x, xs):
2568  Equal.sym(Maybe<a, A>, List.head(a, A, x <> xs), Some{x}, head_cons(a, A, x, xs))
2569
2570# The head of an append is the head of the first part, or else of the second, reversed to rewrite toward the simple side.
2571law head_append_sym:
2572  for -a: Quant
2573  for -A: Kind(a)
2574  for xs: List<a, A>
2575  for -ys: List<a, A>
2576  {Maybe.or(a, A, List.head(a, A, xs), List.head(a, A, ys)) == List.head(a, A, List.append(a, A, xs, ys)) : Maybe<a, A>}
2577
2578def head_append_sym(a, A, xs, ys):
2579  Equal.sym(Maybe<a, A>, List.head(a, A, List.append(a, A, xs, ys)), Maybe.or(a, A, List.head(a, A, xs), List.head(a, A, ys)), head_append(a, A, xs, ys))
2580
2581# The head of a map is the mapped head, reversed to rewrite toward the simple side.
2582law head_map_sym:
2583  for ~A: Type
2584  for ~B: Type
2585  for ~f: A -> B
2586  for xs: List<A>
2587  {Maybe.map(&1, A, B, f, List.head(&1, A, xs)) == List.head(&1, B, List.map(~A, ~B, ~f, xs)) : Maybe<&1, B>}
2588
2589def head_map_sym(A, B, f, xs):
2590  Equal.sym(Maybe<&1, B>, List.head(&1, B, List.map(~A, ~B, ~f, xs)), Maybe.map(&1, A, B, f, List.head(&1, A, xs)), head_map(~A, ~B, ~f, xs))
2591
2592# The tail of a map is the map of the tail, reversed to rewrite toward the simple side.
2593law tail_map_sym:
2594  for ~A: Type
2595  for ~B: Type
2596  for ~f: A -> B
2597  for xs: List<A>
2598  {List.map(~A, ~B, ~f, List.tail(&1, A, xs)) == List.tail(&1, B, List.map(~A, ~B, ~f, xs)) : List<B>}
2599
2600def tail_map_sym(A, B, f, xs):
2601  Equal.sym(List<B>, List.tail(&1, B, List.map(~A, ~B, ~f, xs)), List.map(~A, ~B, ~f, List.tail(&1, A, xs)), tail_map(~A, ~B, ~f, xs))
2602
2603# The element at index zero of a cons is its head, reversed to rewrite toward the simple side.
2604law get_cons_zero_sym:
2605  for -a: Quant
2606  for -A: Kind(a)
2607  for -x: A
2608  for -xs: List<a, A>
2609  {Some{x} == List.get(a, A, x <> xs, 0n) : Maybe<a, A>}
2610
2611def get_cons_zero_sym(a, A, x, xs):
2612  Equal.sym(Maybe<a, A>, List.get(a, A, x <> xs, 0n), Some{x}, get_cons_zero(a, A, x, xs))
2613
2614# The element at index n + 1 of a cons is the element at index n of its tail, reversed to rewrite toward the simple side.
2615law get_cons_succ_sym:
2616  for -a: Quant
2617  for -A: Kind(a)
2618  for -x: A
2619  for -xs: List<a, A>
2620  for -n: Nat
2621  {List.get(a, A, xs, n) == List.get(a, A, x <> xs, 1n+n) : Maybe<a, A>}
2622
2623def get_cons_succ_sym(a, A, x, xs, n):
2624  Equal.sym(Maybe<a, A>, List.get(a, A, x <> xs, 1n+n), List.get(a, A, xs, n), get_cons_succ(a, A, x, xs, n))
2625
2626# Indexing a map is mapping the indexed element, reversed to rewrite toward the simple side.
2627law get_map_sym:
2628  for ~A: Type
2629  for ~B: Type
2630  for ~f: A -> B
2631  for xs: List<A>
2632  for n: Nat
2633  {Maybe.map(&1, A, B, f, List.get(&1, A, xs, n)) == List.get(&1, B, List.map(~A, ~B, ~f, xs), n) : Maybe<&1, B>}
2634
2635def get_map_sym(A, B, f, xs, n):
2636  Equal.sym(Maybe<&1, B>, List.get(&1, B, List.map(~A, ~B, ~f, xs), n), Maybe.map(&1, A, B, f, List.get(&1, A, xs, n)), get_map(~A, ~B, ~f, xs, n))
2637
2638# Setting an element does not change the length, reversed to rewrite toward the simple side.
2639law length_set_sym:
2640  for -a: Quant
2641  for -A: Kind(a)
2642  for xs: List<a, A>
2643  for n: Nat
2644  for -x: A
2645  {List.length(a, A, xs) == List.length(a, A, List.set(a, A, xs, n, x)) : Nat}
2646
2647def length_set_sym(a, A, xs, n, x):
2648  Equal.sym(Nat, List.length(a, A, List.set(a, A, xs, n, x)), List.length(a, A, xs), length_set(a, A, xs, n, x))
2649
2650# Reading the index just set gives the new value wherever the index is in range, reversed to rewrite toward the simple side.
2651law get_set_self_sym:
2652  for -a: Quant
2653  for -A: Kind(a)
2654  for xs: List<a, A>
2655  for n: Nat
2656  for -x: A
2657  {Maybe.map(a, A, A, y => x, List.get(a, A, xs, n)) == List.get(a, A, List.set(a, A, xs, n, x), n) : Maybe<a, A>}
2658
2659def get_set_self_sym(a, A, xs, n, x):
2660  Equal.sym(Maybe<a, A>, 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)), get_set_self(a, A, xs, n, x))
2661
2662# The last element of xs ++ [x] is x, reversed to rewrite toward the simple side.
2663law last_append_singleton_sym:
2664  for -a: Quant
2665  for -A: Kind(a)
2666  for xs: List<a, A>
2667  for -x: A
2668  {Some{x} == List.last(a, A, List.append(a, A, xs, [x])) : Maybe<a, A>}
2669
2670def last_append_singleton_sym(a, A, xs, x):
2671  Equal.sym(Maybe<a, A>, List.last(a, A, List.append(a, A, xs, [x])), Some{x}, last_append_singleton(a, A, xs, x))
2672
2673# The head of the reverse is the last element, reversed to rewrite toward the simple side.
2674law head_reverse_sym:
2675  for -a: Quant
2676  for -A: Kind(a)
2677  for xs: List<a, A>
2678  {List.last(a, A, xs) == List.head(a, A, List.reverse(a, A, xs)) : Maybe<a, A>}
2679
2680def head_reverse_sym(a, A, xs):
2681  Equal.sym(Maybe<a, A>, List.head(a, A, List.reverse(a, A, xs)), List.last(a, A, xs), head_reverse(a, A, xs))
2682
2683# The last element of the reverse is the head, reversed to rewrite toward the simple side.
2684law last_reverse_sym:
2685  for -a: Quant
2686  for -A: Kind(a)
2687  for xs: List<a, A>
2688  {List.head(a, A, xs) == List.last(a, A, List.reverse(a, A, xs)) : Maybe<a, A>}
2689
2690def last_reverse_sym(a, A, xs):
2691  Equal.sym(Maybe<a, A>, List.last(a, A, List.reverse(a, A, xs)), List.head(a, A, xs), last_reverse(a, A, xs))
2692
2693# A list is empty exactly when its length is zero, reversed to rewrite toward the simple side.
2694law is_empty_iff_length_eq_zero_sym:
2695  for -a: Quant
2696  for -A: Kind(a)
2697  for xs: List<a, A>
2698  {Nat.is_eq(List.length(a, A, xs), 0n) == List.is_empty(a, A, xs) : Bool}
2699
2700def is_empty_iff_length_eq_zero_sym(a, A, xs):
2701  Equal.sym(Bool, List.is_empty(a, A, xs), Nat.is_eq(List.length(a, A, xs), 0n), is_empty_iff_length_eq_zero(a, A, xs))
2702
2703# An append is empty exactly when both parts are, reversed to rewrite toward the simple side.
2704law is_empty_append_sym:
2705  for -a: Quant
2706  for -A: Kind(a)
2707  for xs: List<a, A>
2708  for -ys: List<a, A>
2709  {Bool.and(List.is_empty(a, A, xs), List.is_empty(a, A, ys)) == List.is_empty(a, A, List.append(a, A, xs, ys)) : Bool}
2710
2711def is_empty_append_sym(a, A, xs, ys):
2712  Equal.sym(Bool, 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)), is_empty_append(a, A, xs, ys))
2713
2714# The reverse is empty exactly when the list is, reversed to rewrite toward the simple side.
2715law is_empty_reverse_sym:
2716  for -a: Quant
2717  for -A: Kind(a)
2718  for xs: List<a, A>
2719  {List.is_empty(a, A, xs) == List.is_empty(a, A, List.reverse(a, A, xs)) : Bool}
2720
2721def is_empty_reverse_sym(a, A, xs):
2722  Equal.sym(Bool, List.is_empty(a, A, List.reverse(a, A, xs)), List.is_empty(a, A, xs), is_empty_reverse(a, A, xs))
2723
2724# A map is empty exactly when the list is, reversed to rewrite toward the simple side.
2725law is_empty_map_sym:
2726  for ~A: Type
2727  for ~B: Type
2728  for ~f: A -> B
2729  for xs: List<A>
2730  {List.is_empty(&1, A, xs) == List.is_empty(&1, B, List.map(~A, ~B, ~f, xs)) : Bool}
2731
2732def is_empty_map_sym(A, B, f, xs):
2733  Equal.sym(Bool, List.is_empty(&1, B, List.map(~A, ~B, ~f, xs)), List.is_empty(&1, A, xs), is_empty_map(~A, ~B, ~f, xs))
2734
2735# Filtering commutes with reversing: filter p (reverse xs) = reverse (filter p xs), reversed to rewrite toward the simple side.
2736law filter_reverse_sym:
2737  for ~A: Data
2738  for ~f: A -> Bool
2739  for xs: List<&2, A>
2740  {List.reverse(&2, A, List.filter(~A, ~f, xs)) == List.filter(~A, ~f, List.reverse(&2, A, xs)) : List<&2, A>}
2741
2742def filter_reverse_sym(A, f, xs):
2743  Equal.sym(List<&2, A>, List.filter(~A, ~f, List.reverse(&2, A, xs)), List.reverse(&2, A, List.filter(~A, ~f, xs)), filter_reverse(~A, ~f, xs))
2744
2745# Folding cons from the right, starting from the empty list, rebuilds the list, reversed to rewrite toward the simple side.
2746law foldr_cons_nil_sym:
2747  for ~a: Quant
2748  for ~A: Kind(a)
2749  for xs: List<a, A>
2750  {xs == List.foldr(~a, ~A, ~List<a, A>, ~(x => acc => x <> acc), xs, Nil{}) : List<a, A>}
2751
2752def foldr_cons_nil_sym(a, A, xs):
2753  Equal.sym(List<a, A>, List.foldr(~a, ~A, ~List<a, A>, ~(x => acc => x <> acc), xs, Nil{}), xs, foldr_cons_nil(~a, ~A, xs))
2754
2755# A left fold over the reverse is a right fold with the arguments flipped, reversed to rewrite toward the simple side.
2756law foldl_reverse_sym:
2757  for ~a: Quant
2758  for ~A: Kind(a)
2759  for ~B: Type
2760  for ~f: B -> A -> B
2761  for xs: List<a, A>
2762  for -z: B
2763  {List.foldr(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z) == List.foldl(~a, ~A, ~B, ~f, List.reverse(a, A, xs), z) : B}
2764
2765def foldl_reverse_sym(a, A, B, f, xs, z):
2766  Equal.sym(B, List.foldl(~a, ~A, ~B, ~f, List.reverse(a, A, xs), z), List.foldr(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z), foldl_reverse(~a, ~A, ~B, ~f, xs, z))
2767
2768# A right fold over the reverse is a left fold with the arguments flipped, reversed to rewrite toward the simple side.
2769law foldr_reverse_sym:
2770  for ~a: Quant
2771  for ~A: Kind(a)
2772  for ~B: Type
2773  for ~f: A -> B -> B
2774  for xs: List<a, A>
2775  for -z: B
2776  {List.foldl(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z) == List.foldr(~a, ~A, ~B, ~f, List.reverse(a, A, xs), z) : B}
2777
2778def foldr_reverse_sym(a, A, B, f, xs, z):
2779  Equal.sym(B, List.foldr(~a, ~A, ~B, ~f, List.reverse(a, A, xs), z), List.foldl(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z), foldr_reverse(~a, ~A, ~B, ~f, xs, z))
2780
2781# Range(n + 1) is range(n) followed by n, reversed to rewrite toward the simple side.
2782law range_succ_sym:
2783  for n: Nat
2784  {List.append(&2, Nat, List.range(n), [n]) == List.range(1n+n) : List<&2, Nat>}
2785
2786def range_succ_sym(n):
2787  Equal.sym(List<&2, Nat>, List.range(1n+n), List.append(&2, Nat, List.range(n), [n]), range_succ(n))
2788
2789# Finding in an append finds in the first part, or else in the second, reversed to rewrite toward the simple side.
2790law find_append_sym:
2791  for ~A: Data
2792  for ~f: A -> Bool
2793  for xs: List<&2, A>
2794  for ys: List<&2, A>
2795  {Maybe.or(&2, A, List.find(~A, ~f, xs), List.find(~A, ~f, ys)) == List.find(~A, ~f, List.append(&2, A, xs, ys)) : Maybe<&2, A>}
2796
2797def find_append_sym(A, f, xs, ys):
2798  Equal.sym(Maybe<&2, A>, List.find(~A, ~f, List.append(&2, A, xs, ys)), Maybe.or(&2, A, List.find(~A, ~f, xs), List.find(~A, ~f, ys)), find_append(~A, ~f, xs, ys))
2799
2800# All elements satisfy f exactly when no element fails it, reversed to rewrite toward the simple side.
2801law all_eq_not_any_not_sym:
2802  for ~a: Quant
2803  for ~A: Kind(a)
2804  for ~f: A -> Bool
2805  for xs: List<a, A>
2806  {Bool.not(List.any(~a, ~A, ~(x => Bool.not(f(x))), xs)) == List.all(~a, ~A, ~f, xs) : Bool}
2807
2808def all_eq_not_any_not_sym(a, A, f, xs):
2809  Equal.sym(Bool, List.all(~a, ~A, ~f, xs), Bool.not(List.any(~a, ~A, ~(x => Bool.not(f(x))), xs)), all_eq_not_any_not(~a, ~A, ~f, xs))
2810
2811# Some element satisfies f exactly when not all elements fail it, reversed to rewrite toward the simple side.
2812law any_eq_not_all_not_sym:
2813  for ~a: Quant
2814  for ~A: Kind(a)
2815  for ~f: A -> Bool
2816  for xs: List<a, A>
2817  {Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), xs)) == List.any(~a, ~A, ~f, xs) : Bool}
2818
2819def any_eq_not_all_not_sym(a, A, f, xs):
2820  Equal.sym(Bool, List.any(~a, ~A, ~f, xs), Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), xs)), any_eq_not_all_not(~a, ~A, ~f, xs))
2821
2822# A one-element list has length one, reversed to rewrite toward the simple side.
2823law length_singleton_sym:
2824  for -a: Quant
2825  for -A: Kind(a)
2826  for -x: A
2827  {1n == List.length(a, A, [x]) : Nat}
2828
2829def length_singleton_sym(a, A, x):
2830  Equal.sym(Nat, List.length(a, A, [x]), 1n, length_singleton(a, A, x))
2831
2832# Reversing a cons puts its head last: reverse (x :: xs) = reverse xs ++ [x], reversed to rewrite toward the simple side.
2833law reverse_cons_sym:
2834  for -a: Quant
2835  for -A: Kind(a)
2836  for -x: A
2837  for xs: List<a, A>
2838  {List.append(a, A, List.reverse(a, A, xs), [x]) == List.reverse(a, A, x <> xs) : List<a, A>}
2839
2840def reverse_cons_sym(a, A, x, xs):
2841  Equal.sym(List<a, A>, List.reverse(a, A, x <> xs), List.append(a, A, List.reverse(a, A, xs), [x]), reverse_cons(a, A, x, xs))
2842
2843# Taking n + 1 elements of a cons keeps its head and takes n from its tail, reversed to rewrite toward the simple side.
2844law take_succ_sym:
2845  for -a: Quant
2846  for -A: Kind(a)
2847  for -x: A
2848  for -xs: List<a, A>
2849  for -n: Nat
2850  {x <> List.take(a, A, xs, n) == List.take(a, A, x <> xs, 1n+n) : List<a, A>}
2851
2852def take_succ_sym(a, A, x, xs, n):
2853  Equal.sym(List<a, A>, List.take(a, A, x <> xs, 1n+n), x <> List.take(a, A, xs, n), take_succ(a, A, x, xs, n))
2854
2855# Dropping n + 1 elements of a cons drops its head and n from its tail, reversed to rewrite toward the simple side.
2856law drop_succ_sym:
2857  for -a: Quant
2858  for -A: Kind(a)
2859  for -x: A
2860  for -xs: List<a, A>
2861  for -n: Nat
2862  {List.drop(a, A, xs, n) == List.drop(a, A, x <> xs, 1n+n) : List<a, A>}
2863
2864def drop_succ_sym(a, A, x, xs, n):
2865  Equal.sym(List<a, A>, List.drop(a, A, x <> xs, 1n+n), List.drop(a, A, xs, n), drop_succ(a, A, x, xs, n))