list.bend

bend-mathlib@0.8.1.0 · 3,175 lines · 276 definitions

1# bend-mathlib/list.bend: List lemmas (append, reverse, length, take, drop, map, fold, filter, zip,
2# head, last, get, all, any, find, contains, mem, sorted_by).
3import Base
4import bend-mathlib@0.8.1.0/nat.bend as MNat
5import bend-mathlib@0.8.1.0/bool.bend as MBool
6
7# The empty list is a right identity for append: xs ++ [] = xs.
8law append_nil:
9  for -a: Quant
10  for -A: Kind(a)
11  for xs: List<a, A>
12  {List.append(a, A, xs, Nil{}) == xs : List<a, A>}
13
14def append_nil(a, A, xs):
15  match xs:
16    case Nil{}:
17      {==}
18    case h <> t:
19      %append_nil(a, A, t) : {h <> List.append(a, A, t, Nil{}) == h <> _ : List<a, A>}
20      {==}
21
22# The empty list is a left identity for append: [] ++ xs = xs.
23law nil_append:
24  for -a: Quant
25  for -A: Kind(a)
26  for -xs: List<a, A>
27  {List.append(a, A, Nil{}, xs) == xs : List<a, A>}
28
29def nil_append(a, A, xs):
30  {==}
31
32# Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs).
33law append_assoc:
34  for -a: Quant
35  for -A: Kind(a)
36  for xs: List<a, A>
37  for -ys: List<a, A>
38  for -zs: List<a, A>
39  {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>}
40
41def append_assoc(a, A, xs, ys, zs):
42  match xs:
43    case Nil{}:
44      {==}
45    case h <> t:
46      %append_assoc(a, A, t, ys, zs) : {h <> List.append(a, A, List.append(a, A, t, ys), zs) == h <> _ : List<a, A>}
47      {==}
48
49# The length of an append is the sum of the lengths.
50law length_append:
51  for -a: Quant
52  for -A: Kind(a)
53  for xs: List<a, A>
54  for -ys: List<a, A>
55  {List.length(a, A, List.append(a, A, xs, ys)) == Nat.add(List.length(a, A, xs), List.length(a, A, ys)) : Nat}
56
57def length_append(a, A, xs, ys):
58  match xs:
59    case Nil{}:
60      {==}
61    case h <> t:
62      %length_append(a, A, t, ys) : {1n+List.length(a, A, List.append(a, A, t, ys)) == 1n+_ : Nat}
63      {==}
64
65def 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>}:
66  match xs:
67    case Nil{}:
68      {==}
69    case h <> t:
70      internal_reverse_go_append(a, A, t, h <> ys, acc)
71
72# The reverse accumulator loop appends the reversed list to the accumulator.
73law reverse_go_spec:
74  for -a: Quant
75  for -A: Kind(a)
76  for xs: List<a, A>
77  for -acc: List<a, A>
78  {List.reverse.go(a, A, xs, acc) == List.append(a, A, List.reverse(a, A, xs), acc) : List<a, A>}
79
80def reverse_go_spec(a, A, xs, acc):
81  match xs:
82    case Nil{}:
83      {==}
84    case h <> t:
85      internal_reverse_go_append(a, A, t, h <> Nil{}, acc)
86
87def 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>}:
88  match xs:
89    case Nil{}:
90      {==}
91    case h <> t:
92      internal_reverse_append_go(a, A, t, ys, h <> acc)
93
94# Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs.
95law reverse_append:
96  for -a: Quant
97  for -A: Kind(a)
98  for xs: List<a, A>
99  for ys: List<a, A>
100  {List.reverse(a, A, List.append(a, A, xs, ys)) == List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) : List<a, A>}
101
102def reverse_append(a, A, xs, ys):
103  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)))
104
105def 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>}:
106  match xs:
107    case Nil{}:
108      {==}
109    case h <> t:
110      internal_reverse_go_go(a, A, t, h <> acc)
111
112# Reversing twice gives the list back.
113law reverse_reverse:
114  for -a: Quant
115  for -A: Kind(a)
116  for xs: List<a, A>
117  {List.reverse(a, A, List.reverse(a, A, xs)) == xs : List<a, A>}
118
119def reverse_reverse(a, A, xs):
120  internal_reverse_go_go(a, A, xs, Nil{})
121
122def 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}:
123  match xs:
124    case Nil{}:
125      %Equal.sym(Nat, Nat.add(n, 0n), n, MNat.add_zero(n)) : {List.length(a, A, acc) == _ : Nat}
126      e
127    case h <> t:
128      %Equal.sym(Nat, Nat.add(n, 1n+List.length(a, A, t)), 1n+Nat.add(n, List.length(a, A, t)), MNat.add_succ(n, List.length(a, A, t))) : {List.length(a, A, List.reverse.go(a, A, t, h <> acc)) == _ : Nat}
129      internal_length_reverse_go(a, A, t, h <> acc, 1n+n, Equal.cong(Nat, Nat, k => 1n+k, List.length(a, A, acc), n, e))
130
131# Reversing preserves the length.
132law length_reverse:
133  for -a: Quant
134  for -A: Kind(a)
135  for xs: List<a, A>
136  {List.length(a, A, List.reverse(a, A, xs)) == List.length(a, A, xs) : Nat}
137
138def length_reverse(a, A, xs):
139  internal_length_reverse_go(a, A, xs, Nil{}, 0n, {==})
140
141# A right fold over an append folds the first part onto the fold of the second.
142law foldr_append:
143  for ~a: Quant
144  for ~A: Kind(a)
145  for ~B: Type
146  for ~f: A -> B -> B
147  for xs: List<a, A>
148  for -ys: List<a, A>
149  for -z: B
150  {List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) == List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)) : B}
151
152def foldr_append(a, A, B, f, xs, ys, z):
153  match xs:
154    case Nil{}:
155      {==}
156    case h <> t:
157      %foldr_append(~a, ~A, ~B, ~f, t, ys, z) : {f(h, List.foldr(~a, ~A, ~B, ~f, List.append(a, A, t, ys), z)) == f(h, _) : B}
158      {==}
159
160# Taking n elements and appending the rest after dropping n gives the list back.
161law take_append_drop:
162  for -a: Quant
163  for -A: Kind(a)
164  for xs: List<a, A>
165  for n: Nat
166  {List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) == xs : List<a, A>}
167
168def take_append_drop(a, A, xs, n):
169  match xs n:
170    case Nil{} _:
171      {==}
172    case h <> t 0n:
173      {==}
174    case h <> t 1n+p:
175      %take_append_drop(a, A, t, p) : {h <> List.append(a, A, List.take(a, A, t, p), List.drop(a, A, t, p)) == h <> _ : List<a, A>}
176      {==}
177
178# Mapping preserves the length.
179law length_map:
180  for ~A: Type
181  for ~B: Type
182  for ~f: A -> B
183  for xs: List<A>
184  {List.length(&1, B, List.map(~A, ~B, ~f, xs)) == List.length(&1, A, xs) : Nat}
185
186def length_map(A, B, f, xs):
187  match xs:
188    case Nil{}:
189      {==}
190    case h <> t:
191      %length_map(~A, ~B, ~f, t) : {1n+List.length(&1, B, List.map(~A, ~B, ~f, t)) == 1n+_ : Nat}
192      {==}
193
194# Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys.
195law map_append:
196  for ~A: Type
197  for ~B: Type
198  for ~f: A -> B
199  for xs: List<A>
200  for -ys: List<A>
201  {List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)) == List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)) : List<B>}
202
203def map_append(A, B, f, xs, ys):
204  match xs:
205    case Nil{}:
206      {==}
207    case h <> t:
208      %map_append(~A, ~B, ~f, t, ys) : {f(h) <> List.map(~A, ~B, ~f, List.append(&1, A, t, ys)) == f(h) <> _ : List<B>}
209      {==}
210
211# Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs.
212law map_map:
213  for ~A: Type
214  for ~B: Type
215  for ~C: Type
216  for ~f: A -> B
217  for ~g: B -> C
218  for xs: List<A>
219  {List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~C, ~(x => g(f(x))), xs) : List<C>}
220
221def map_map(A, B, C, f, g, xs):
222  match xs:
223    case Nil{}:
224      {==}
225    case h <> t:
226      %map_map(~A, ~B, ~C, ~f, ~g, t) : {g(f(h)) <> List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, t)) == g(f(h)) <> _ : List<C>}
227      {==}
228
229# Taking zero elements gives the empty list.
230law take_zero:
231  for -a: Quant
232  for -A: Kind(a)
233  for xs: List<a, A>
234  {List.take(a, A, xs, 0n) == Nil{} : List<a, A>}
235
236def take_zero(a, A, xs):
237  match xs:
238    case Nil{}:
239      {==}
240    case h <> t:
241      {==}
242
243# Dropping zero elements gives the list back.
244law drop_zero:
245  for -a: Quant
246  for -A: Kind(a)
247  for xs: List<a, A>
248  {List.drop(a, A, xs, 0n) == xs : List<a, A>}
249
250def drop_zero(a, A, xs):
251  match xs:
252    case Nil{}:
253      {==}
254    case h <> t:
255      {==}
256
257# Taking from the empty list gives the empty list.
258law take_nil:
259  for -a: Quant
260  for -A: Kind(a)
261  for -n: Nat
262  {List.take(a, A, Nil{}, n) == Nil{} : List<a, A>}
263
264def take_nil(a, A, n):
265  {==}
266
267# Dropping from the empty list gives the empty list.
268law drop_nil:
269  for -a: Quant
270  for -A: Kind(a)
271  for -n: Nat
272  {List.drop(a, A, Nil{}, n) == Nil{} : List<a, A>}
273
274def drop_nil(a, A, n):
275  {==}
276
277# Taking n elements leaves min(n, length) of them.
278law length_take:
279  for -a: Quant
280  for -A: Kind(a)
281  for xs: List<a, A>
282  for n: Nat
283  {List.length(a, A, List.take(a, A, xs, n)) == Nat.min(n, List.length(a, A, xs)) : Nat}
284
285def length_take(a, A, xs, n):
286  match xs n:
287    case Nil{} _:
288      Equal.sym(Nat, Nat.min(n, 0n), 0n, MNat.min_zero(n))
289    case h <> t 0n:
290      {==}
291    case h <> t 1n+p:
292      %length_take(a, A, t, p) : {1n+List.length(a, A, List.take(a, A, t, p)) == 1n+_ : Nat}
293      {==}
294
295# Dropping n elements leaves length - n of them.
296law length_drop:
297  for -a: Quant
298  for -A: Kind(a)
299  for xs: List<a, A>
300  for n: Nat
301  {List.length(a, A, List.drop(a, A, xs, n)) == Nat.sub(List.length(a, A, xs), n) : Nat}
302
303def length_drop(a, A, xs, n):
304  match xs n:
305    case Nil{} _:
306      Equal.sym(Nat, Nat.sub(0n, n), 0n, MNat.zero_sub(n))
307    case h <> t 0n:
308      {==}
309    case h <> t 1n+p:
310      length_drop(a, A, t, p)
311
312# Taking as many elements as the list has gives the list back.
313law take_length:
314  for -A: Data
315  for +xs: List<&2, A>
316  {List.take(&2, A, xs, List.length(&2, A, xs)) == xs : List<&2, A>}
317
318def take_length(A, xs):
319  match xs:
320    case Nil{}:
321      {==}
322    case h <> t:
323      %take_length(A, t) : {h <> List.take(&2, A, t, List.length(&2, A, t)) == h <> _ : List<&2, A>}
324      {==}
325
326# Dropping as many elements as the list has gives the empty list.
327law drop_length:
328  for -A: Data
329  for +xs: List<&2, A>
330  {List.drop(&2, A, xs, List.length(&2, A, xs)) == Nil{} : List<&2, A>}
331
332def drop_length(A, xs):
333  match xs:
334    case Nil{}:
335      {==}
336    case h <> t:
337      drop_length(A, t)
338
339# Taking m from the first n is taking min(n, m).
340law take_take:
341  for -a: Quant
342  for -A: Kind(a)
343  for xs: List<a, A>
344  for n: Nat
345  for m: Nat
346  {List.take(a, A, List.take(a, A, xs, n), m) == List.take(a, A, xs, Nat.min(n, m)) : List<a, A>}
347
348def take_take(a, A, xs, n, m):
349  match xs n m:
350    case Nil{} _ _:
351      {==}
352    case h <> t 0n _:
353      {==}
354    case h <> t 1n+p 0n:
355      {==}
356    case h <> t 1n+p 1n+q:
357      %take_take(a, A, t, p, q) : {h <> List.take(a, A, List.take(a, A, t, p), q) == h <> _ : List<a, A>}
358      {==}
359
360# Dropping m after dropping n is dropping n + m.
361law drop_drop:
362  for -a: Quant
363  for -A: Kind(a)
364  for xs: List<a, A>
365  for n: Nat
366  for -m: Nat
367  {List.drop(a, A, List.drop(a, A, xs, n), m) == List.drop(a, A, xs, Nat.add(n, m)) : List<a, A>}
368
369def drop_drop(a, A, xs, n, m):
370  match xs n m:
371    case Nil{} _ _:
372      {==}
373    case h <> t 0n _:
374      {==}
375    case h <> t 1n+p _:
376      drop_drop(a, A, t, p, m)
377
378# Reversing the empty list gives the empty list.
379law reverse_nil:
380  for -a: Quant
381  for -A: Kind(a)
382  {List.reverse(a, A, Nil{}) == Nil{} : List<a, A>}
383
384def reverse_nil(a, A):
385  {==}
386
387# Reversing a one-element list gives it back.
388law reverse_singleton:
389  for -a: Quant
390  for -A: Kind(a)
391  for -x: A
392  {List.reverse(a, A, [x]) == [x] : List<a, A>}
393
394def reverse_singleton(a, A, x):
395  {==}
396
397# Replicating x n times gives a list of length n.
398law length_replicate:
399  for -A: Data
400  for n: Nat
401  for -x: A
402  {List.length(&2, A, List.replicate(A, n, x)) == n : Nat}
403
404def length_replicate(A, n, x):
405  match n:
406    case 0n:
407      {==}
408    case 1n+p:
409      %length_replicate(A, p, x) : {1n+List.length(&2, A, List.replicate(A, p, x)) == 1n+_ : Nat}
410      {==}
411
412def internal_length_range_go(+n: Nat, acc: List<&2, Nat>) -> {List.length(&2, Nat, List.range.go(n, acc)) == Nat.add(n, List.length(&2, Nat, acc)) : Nat}:
413  match n:
414    case 0n:
415      {==}
416    case 1n+p:
417      %MNat.add_succ(p, List.length(&2, Nat, acc)) : {List.length(&2, Nat, List.range.go(p, p <> acc)) == _ : Nat}
418      internal_length_range_go(p, p <> acc)
419
420# Range(n) has length n.
421law length_range:
422  for n: Nat
423  {List.length(&2, Nat, List.range(n)) == n : Nat}
424
425def length_range(n):
426  +n = n
427  %Equal.sym(Nat, List.length(&2, Nat, List.range.go(n, Nil{})), Nat.add(n, 0n), internal_length_range_go(n, Nil{})) : {_ == n : Nat}
428  MNat.add_zero(n)
429
430# A zip is as long as the shorter of the two lists.
431law length_zip:
432  for -a: Quant
433  for -A: Kind(a)
434  for xs: List<a, A>
435  for ys: List<a, A>
436  {List.length(&1, A & A, List.zip(a, A, a, A, xs, ys)) == Nat.min(List.length(a, A, xs), List.length(a, A, ys)) : Nat}
437
438def length_zip(a, A, xs, ys):
439  match xs ys:
440    case Nil{} _:
441      {==}
442    case h <> t Nil{}:
443      {==}
444    case h <> t y <> yt:
445      %length_zip(a, A, t, yt) : {1n+List.length(&1, A & A, List.zip(a, A, a, A, t, yt)) == 1n+_ : Nat}
446      {==}
447
448# Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys).
449law append_cons:
450  for -a: Quant
451  for -A: Kind(a)
452  for -x: A
453  for -xs: List<a, A>
454  for -ys: List<a, A>
455  {List.append(a, A, x <> xs, ys) == x <> List.append(a, A, xs, ys) : List<a, A>}
456
457def append_cons(a, A, x, xs, ys):
458  {==}
459
460# The empty list has length zero.
461law length_nil:
462  for -a: Quant
463  for -A: Kind(a)
464  {List.length(a, A, Nil{}) == 0n : Nat}
465
466def length_nil(a, A):
467  {==}
468
469# A cons is one longer than its tail.
470law length_cons:
471  for -a: Quant
472  for -A: Kind(a)
473  for -x: A
474  for -xs: List<a, A>
475  {List.length(a, A, x <> xs) == 1n+List.length(a, A, xs) : Nat}
476
477def length_cons(a, A, x, xs):
478  {==}
479
480# Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss.
481law concat_append:
482  for -a: Quant
483  for -A: Kind(a)
484  for xss: List<a, List<a, A>>
485  for -yss: List<a, List<a, A>>
486  {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>}
487
488def concat_append(a, A, xss, yss):
489  match xss:
490    case Nil{}:
491      {==}
492    case h <> t:
493      %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>}
494      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)))
495
496# A left fold over an append folds the second part from the fold of the first.
497law foldl_append:
498  for ~a: Quant
499  for ~A: Kind(a)
500  for ~B: Type
501  for ~f: B -> A -> B
502  for xs: List<a, A>
503  for -ys: List<a, A>
504  for -z: B
505  {List.foldl(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) == List.foldl(~a, ~A, ~B, ~f, ys, List.foldl(~a, ~A, ~B, ~f, xs, z)) : B}
506
507def foldl_append(a, A, B, f, xs, ys, z):
508  match xs:
509    case Nil{}:
510      {==}
511    case h <> t:
512      foldl_append(~a, ~A, ~B, ~f, t, ys, f(z, h))
513
514def 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>}:
515  match xs:
516    case Nil{}:
517      {==}
518    case h <> t:
519      internal_map_reverse_go(~A, ~B, ~f, t, h <> acc)
520
521# Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs).
522law map_reverse:
523  for ~A: Type
524  for ~B: Type
525  for ~f: A -> B
526  for xs: List<A>
527  {List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) == List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) : List<B>}
528
529def map_reverse(A, B, f, xs):
530  internal_map_reverse_go(~A, ~B, ~f, xs, Nil{})
531
532# Base 2.0.38 short-circuits each through a thunk (List.all.if, List.any.if, List.find.if), so the cons step is proved by cases on the head's test.
533def internal_all_if(b: Bool, -r: Bool) -> {Bool.and(b, r) == List.all.if(u => r, b) : Bool}:
534  match b:
535    case False{}:
536      {==}
537    case True{}:
538      {==}
539
540def internal_any_if(b: Bool, -r: Bool) -> {Bool.or(b, r) == List.any.if(u => r, b) : Bool}:
541  match b:
542    case False{}:
543      {==}
544    case True{}:
545      {==}
546
547# What List.find does with its head: Some{h} on a hit, else the rest (Base until 2.0.37 had it as List.find.put).
548def internal_find_put(-A: Data, h: A, r: Maybe<&2, A>, hit: Bool) -> Maybe<&2, A>:
549  match hit:
550    case False{}:
551      r
552    case True{}:
553      Some{h}
554
555def internal_find_if(-A: Data, h: A, r: Maybe<&2, A>, b: Bool) -> {internal_find_put(A, h, r, b) == List.find.if(A, h, u => r, b) : Maybe<&2, A>}:
556  match b:
557    case False{}:
558      {==}
559    case True{}:
560      {==}
561
562# The cons case of all, any, find and contains as lemmas, so a change to their Base definitions stays in one place (PLAN F39).
563def internal_all_cons(~a: Quant, ~A: Kind(a), ~f: A -> Bool, h: A, -t: List<a, A>) -> {Bool.and(f(h), List.all(~a, ~A, ~f, t)) == List.all(~a, ~A, ~f, h <> t) : Bool}:
564  internal_all_if(f(h), List.all(~a, ~A, ~f, t))
565
566# The cons case of all with the head's test given as a value, for a head that cannot be used twice (a pair under a predicate that reads both parts).
567def internal_all_cons_test(~a: Quant, ~A: Kind(a), ~f: A -> Bool, -h: A, -t: List<a, A>, b: Bool, e: {f(h) == b : Bool}) -> {Bool.and(b, List.all(~a, ~A, ~f, t)) == List.all(~a, ~A, ~f, h <> t) : Bool}:
568  %Equal.sym(Bool, f(h), b, e) : {Bool.and(b, List.all(~a, ~A, ~f, t)) == List.all.if(u => List.all(~a, ~A, ~f, t), _) : Bool}
569  internal_all_if(b, List.all(~a, ~A, ~f, t))
570
571def internal_any_cons(~a: Quant, ~A: Kind(a), ~f: A -> Bool, h: A, -t: List<a, A>) -> {Bool.or(f(h), List.any(~a, ~A, ~f, t)) == List.any(~a, ~A, ~f, h <> t) : Bool}:
572  internal_any_if(f(h), List.any(~a, ~A, ~f, t))
573
574def internal_find_cons(~A: Data, ~f: A -> Bool, +h: A, t: List<&2, A>) -> {internal_find_put(A, h, List.find(~A, ~f, t), f(h)) == List.find(~A, ~f, h <> t) : Maybe<&2, A>}:
575  internal_find_if(A, h, List.find(~A, ~f, t), f(h))
576
577def internal_any_cons_test(~a: Quant, ~A: Kind(a), ~f: A -> Bool, -h: A, -t: List<a, A>, b: Bool, e: {f(h) == b : Bool}) -> {Bool.or(b, List.any(~a, ~A, ~f, t)) == List.any(~a, ~A, ~f, h <> t) : Bool}:
578  %Equal.sym(Bool, f(h), b, e) : {Bool.or(b, List.any(~a, ~A, ~f, t)) == List.any.if(u => List.any(~a, ~A, ~f, t), _) : Bool}
579  internal_any_if(b, List.any(~a, ~A, ~f, t))
580
581def internal_contains_cons(~A: Data, ~eq: A -> A -> Bool, h: A, -t: List<&2, A>, +x: A) -> {Bool.or(eq(h, x), List.contains(~A, ~eq, t, x)) == List.contains(~A, ~eq, h <> t, x) : Bool}:
582  internal_any_if(eq(h, x), List.contains(~A, ~eq, t, x))
583
584# The cons step of all_append, any_append and contains_append, given the step for the tail; proved by cases on the head's test.
585def internal_all_if_and(b: Bool, -r: Bool, -s: Bool, -l: Bool, ih: {l == Bool.and(r, s) : Bool}) -> {List.all.if(u => l, b) == Bool.and(List.all.if(u => r, b), s) : Bool}:
586  match b:
587    case False{}:
588      {==}
589    case True{}:
590      ih
591
592def internal_any_if_or(b: Bool, -r: Bool, -s: Bool, -l: Bool, ih: {l == Bool.or(r, s) : Bool}) -> {List.any.if(u => l, b) == Bool.or(List.any.if(u => r, b), s) : Bool}:
593  match b:
594    case False{}:
595      ih
596    case True{}:
597      {==}
598
599def internal_all_cons_and(~a: Quant, ~A: Kind(a), ~f: A -> Bool, h: A, -t: List<a, A>, -l: List<a, A>, -s: Bool, ih: {List.all(~a, ~A, ~f, l) == Bool.and(List.all(~a, ~A, ~f, t), s) : Bool}) -> {List.all(~a, ~A, ~f, h <> l) == Bool.and(List.all(~a, ~A, ~f, h <> t), s) : Bool}:
600  internal_all_if_and(f(h), List.all(~a, ~A, ~f, t), s, List.all(~a, ~A, ~f, l), ih)
601
602def internal_any_cons_or(~a: Quant, ~A: Kind(a), ~f: A -> Bool, h: A, -t: List<a, A>, -l: List<a, A>, -s: Bool, ih: {List.any(~a, ~A, ~f, l) == Bool.or(List.any(~a, ~A, ~f, t), s) : Bool}) -> {List.any(~a, ~A, ~f, h <> l) == Bool.or(List.any(~a, ~A, ~f, h <> t), s) : Bool}:
603  internal_any_if_or(f(h), List.any(~a, ~A, ~f, t), s, List.any(~a, ~A, ~f, l), ih)
604
605def internal_contains_cons_or(~A: Data, ~eq: A -> A -> Bool, h: A, -t: List<&2, A>, -l: List<&2, A>, +x: A, -s: Bool, ih: {List.contains(~A, ~eq, l, x) == Bool.or(List.contains(~A, ~eq, t, x), s) : Bool}) -> {List.contains(~A, ~eq, h <> l, x) == Bool.or(List.contains(~A, ~eq, h <> t, x), s) : Bool}:
606  internal_any_if_or(eq(h, x), List.contains(~A, ~eq, t, x), s, List.contains(~A, ~eq, l, x), ih)
607
608# All over an append is all over each part, joined by and.
609law all_append:
610  for ~a: Quant
611  for ~A: Kind(a)
612  for ~f: A -> Bool
613  for xs: List<a, A>
614  for -ys: List<a, A>
615  {List.all(~a, ~A, ~f, List.append(a, A, xs, ys)) == Bool.and(List.all(~a, ~A, ~f, xs), List.all(~a, ~A, ~f, ys)) : Bool}
616
617def all_append(a, A, f, xs, ys):
618  match xs:
619    case Nil{}:
620      {==}
621    case h <> t:
622      internal_all_cons_and(~a, ~A, ~f, h, t, List.append(a, A, t, ys), List.all(~a, ~A, ~f, ys), all_append(~a, ~A, ~f, t, ys))
623
624# Any over an append is any over each part, joined by or.
625law any_append:
626  for ~a: Quant
627  for ~A: Kind(a)
628  for ~f: A -> Bool
629  for xs: List<a, A>
630  for -ys: List<a, A>
631  {List.any(~a, ~A, ~f, List.append(a, A, xs, ys)) == Bool.or(List.any(~a, ~A, ~f, xs), List.any(~a, ~A, ~f, ys)) : Bool}
632
633def any_append(a, A, f, xs, ys):
634  match xs:
635    case Nil{}:
636      {==}
637    case h <> t:
638      internal_any_cons_or(~a, ~A, ~f, h, t, List.append(a, A, t, ys), List.any(~a, ~A, ~f, ys), any_append(~a, ~A, ~f, t, ys))
639
640def internal_filter_put_append(-A: Data, h: A, r: List<&2, A>, s: List<&2, A>, b: Bool) -> {List.append(&2, A, List.filter.put(A, h, r, b), s) == List.filter.put(A, h, List.append(&2, A, r, s), b) : List<&2, A>}:
641  match b:
642    case False{}:
643      {==}
644    case True{}:
645      {==}
646
647# Filtering an append filters each part.
648law filter_append:
649  for ~A: Data
650  for ~f: A -> Bool
651  for xs: List<&2, A>
652  for ys: List<&2, A>
653  {List.filter(~A, ~f, List.append(&2, A, xs, ys)) == List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)) : List<&2, A>}
654
655def filter_append(A, f, xs, ys):
656  match xs:
657    case Nil{}:
658      {==}
659    case +h <> t:
660      +ys = ys
661      +t = t
662      %Equal.sym(List<&2, A>, List.filter(~A, ~f, List.append(&2, A, t, ys)), List.append(&2, A, List.filter(~A, ~f, t), List.filter(~A, ~f, ys)), filter_append(~A, ~f, t, ys)) : {List.filter.put(A, h, _, f(h)) == List.append(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h)), List.filter(~A, ~f, ys)) : List<&2, A>}
663      Equal.sym(List<&2, A>, List.append(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h)), List.filter(~A, ~f, ys)), List.filter.put(A, h, List.append(&2, A, List.filter(~A, ~f, t), List.filter(~A, ~f, ys)), f(h)), internal_filter_put_append(A, h, List.filter(~A, ~f, t), List.filter(~A, ~f, ys), f(h)))
664
665# An append contains x iff either part does.
666law contains_append:
667  for ~A: Data
668  for ~eq: A -> A -> Bool
669  for xs: List<&2, A>
670  for -ys: List<&2, A>
671  for +x: A
672  {List.contains(~A, ~eq, List.append(&2, A, xs, ys), x) == Bool.or(List.contains(~A, ~eq, xs, x), List.contains(~A, ~eq, ys, x)) : Bool}
673
674def contains_append(A, eq, xs, ys, x):
675  match xs:
676    case Nil{}:
677      {==}
678    case h <> t:
679      internal_contains_cons_or(~A, ~eq, h, t, List.append(&2, A, t, ys), x, List.contains(~A, ~eq, ys, x), contains_append(~A, ~eq, t, ys, x))
680
681def internal_length_filter_put_le(-A: Data, h: A, r: List<&2, A>, b: Bool) -> {Nat.is_le(List.length(&2, A, List.filter.put(A, h, r, b)), 1n+List.length(&2, A, r)) == True{} : Bool}:
682  match b:
683    case False{}:
684      MNat.le_succ(List.length(&2, A, r))
685    case True{}:
686      MNat.le_refl(1n+List.length(&2, A, r))
687
688# Filtering never makes a list longer.
689law length_filter_le:
690  for ~A: Data
691  for ~f: A -> Bool
692  for xs: List<&2, A>
693  {Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)) == True{} : Bool}
694
695def length_filter_le(A, f, xs):
696  match xs:
697    case Nil{}:
698      {==}
699    case +h <> t:
700      +t = t
701      MNat.le_trans(List.length(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))), 1n+List.length(&2, A, List.filter(~A, ~f, t)), 1n+List.length(&2, A, t), internal_length_filter_put_le(A, h, List.filter(~A, ~f, t), f(h)), MNat.succ_le_succ(List.length(&2, A, List.filter(~A, ~f, t)), List.length(&2, A, t), length_filter_le(~A, ~f, t)))
702
703# Membership in a list, as a reusable proposition.
704def mem(~A: Data, ~eq: A -> A -> Bool, +x: A, xs: List<&2, A>) -> Data:
705  {List.contains(~A, ~eq, xs, x) == True{} : Bool}
706
707# A list is sorted by a comparator when every adjacent pair is in order.
708def sorted_by(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>) -> Data:
709  {List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), List.zip(&2, A, &2, A, xs, List.tail(&2, A, xs))) == True{} : Bool}
710
711def internal_or_of_right(a: Bool, -b: Bool, hb: {b == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}:
712  match a:
713    case False{}:
714      hb
715    case True{}:
716      {==}
717
718def internal_or_of_or(a: Bool, -b: Bool, -c: Bool, h: {Bool.or(a, b) == True{} : Bool}, k: {b == True{} : Bool} -> {c == True{} : Bool}) -> {Bool.or(a, c) == True{} : Bool}:
719  match a:
720    case False{}:
721      k(h)
722    case True{}:
723      {==}
724
725def internal_and_left(a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
726  match a:
727    case False{}:
728      Empty.absurd({False{} == True{} : Bool}, MNat.internal_false_ne_true(h))
729    case True{}:
730      {==}
731
732def internal_and_right(a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
733  match a:
734    case False{}:
735      Empty.absurd({b == True{} : Bool}, MNat.internal_false_ne_true(h))
736    case True{}:
737      h
738
739def internal_mem_append_left(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +x: Nat, h: {List.contains(~Nat, ~Nat.is_eq, xs, x) == True{} : Bool}) -> {List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, xs, ys), x) == True{} : Bool}:
740  match xs:
741    case Nil{}:
742      Empty.absurd({List.contains(~Nat, ~Nat.is_eq, ys, x) == True{} : Bool}, MNat.internal_false_ne_true(h))
743    case hd <> tl:
744      %internal_contains_cons(~Nat, ~Nat.is_eq, hd, List.append(&2, Nat, tl, ys), x) : {_ == True{} : Bool}
745      internal_or_of_or(Nat.is_eq(hd, x), List.contains(~Nat, ~Nat.is_eq, tl, x), List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, tl, ys), x), Equal.trans(Bool, Bool.or(Nat.is_eq(hd, x), List.contains(~Nat, ~Nat.is_eq, tl, x)), List.contains(~Nat, ~Nat.is_eq, hd <> tl, x), True{}, internal_contains_cons(~Nat, ~Nat.is_eq, hd, tl, x), h), internal_mem_append_left(tl, ys, x))
746
747def internal_mem_append_right(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +x: Nat, h: {List.contains(~Nat, ~Nat.is_eq, ys, x) == True{} : Bool}) -> {List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, xs, ys), x) == True{} : Bool}:
748  match xs:
749    case Nil{}:
750      h
751    case hd <> tl:
752      %internal_contains_cons(~Nat, ~Nat.is_eq, hd, List.append(&2, Nat, tl, ys), x) : {_ == True{} : Bool}
753      internal_or_of_right(Nat.is_eq(hd, x), List.contains(~Nat, ~Nat.is_eq, List.append(&2, Nat, tl, ys), x), internal_mem_append_right(tl, ys, x, h))
754
755# The head of a Nat list is a member of it (membership by Nat.is_eq).
756law mem_cons_self:
757  for x: Nat
758  for -xs: List<&2, Nat>
759  mem(~Nat, ~Nat.is_eq, x, x <> xs)
760
761def mem_cons_self(x, xs):
762  +x = x
763  %internal_contains_cons(~Nat, ~Nat.is_eq, x, xs, x) : {_ == True{} : Bool}
764  %Equal.sym(Bool, Nat.is_eq(x, x), True{}, MNat.is_eq_refl(x)) : {Bool.or(_, List.contains(~Nat, ~Nat.is_eq, xs, x)) == True{} : Bool}
765  {==}
766
767# A member of a Nat list stays a member when a head is prepended.
768law mem_cons_of_mem:
769  for x: Nat
770  for y: Nat
771  for -xs: List<&2, Nat>
772  for h: mem(~Nat, ~Nat.is_eq, x, xs)
773  mem(~Nat, ~Nat.is_eq, x, y <> xs)
774
775def mem_cons_of_mem(x, y, xs, h):
776  +x = x
777  +y = y
778  %internal_contains_cons(~Nat, ~Nat.is_eq, y, xs, x) : {_ == True{} : Bool}
779  internal_or_of_right(Nat.is_eq(y, x), List.contains(~Nat, ~Nat.is_eq, xs, x), h)
780
781# No Nat is a member of the empty list.
782law not_mem_nil:
783  for -x: Nat
784  mem(~Nat, ~Nat.is_eq, x, Nil{}) -> Empty
785
786def not_mem_nil(x, h):
787  MNat.internal_false_ne_true(h)
788
789# A member of xs is a member of xs ++ ys (Nat lists).
790law mem_append_left:
791  for xs: List<&2, Nat>
792  for ys: List<&2, Nat>
793  for x: Nat
794  for h: mem(~Nat, ~Nat.is_eq, x, xs)
795  mem(~Nat, ~Nat.is_eq, x, List.append(&2, Nat, xs, ys))
796
797def mem_append_left(xs, ys, x, h):
798  internal_mem_append_left(xs, ys, x, h)
799
800# A member of ys is a member of xs ++ ys (Nat lists).
801law mem_append_right:
802  for xs: List<&2, Nat>
803  for ys: List<&2, Nat>
804  for x: Nat
805  for h: mem(~Nat, ~Nat.is_eq, x, ys)
806  mem(~Nat, ~Nat.is_eq, x, List.append(&2, Nat, xs, ys))
807
808def mem_append_right(xs, ys, x, h):
809  internal_mem_append_right(xs, ys, x, h)
810
811# The empty Nat list is sorted by Nat.is_le.
812law sorted_nil:
813  sorted_by(~Nat, ~Nat.is_le, Nil{})
814
815def sorted_nil():
816  {==}
817
818# A one-element Nat list is sorted by Nat.is_le.
819law sorted_single:
820  for -x: Nat
821  sorted_by(~Nat, ~Nat.is_le, [x])
822
823def sorted_single(x):
824  {==}
825
826# The step of sorted_by, with a literal pair head so the kernel reduces the predicate (PLAN F39).
827def internal_sorted_cons_true(~A: Data, ~le: A -> A -> Bool, -x: A, -y: A, -z: List<&1, A & A>, e: {le(x, y) == True{} : Bool}) -> {List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), z) == List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), (x, y) <> z) : Bool}:
828  %Equal.sym(Bool, le(x, y), True{}, e) : {List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), z) == List.all.if(u => List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), z), _) : Bool}
829  {==}
830
831def internal_sorted_cons_false(~A: Data, ~le: A -> A -> Bool, -x: A, -y: A, z: List<&1, A & A>, e: {le(x, y) == False{} : Bool}) -> {False{} == List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), (x, y) <> z) : Bool}:
832  %Equal.sym(Bool, le(x, y), False{}, e) : {False{} == List.all.if(u => List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), z), _) : Bool}
833  {==}
834
835# The cons step of sorted_by's pairs with the head written as (x, y): internal_all_cons_test at a variable pair head is outside what --verdict can check.
836def internal_sorted_cons_test(~A: Data, ~le: A -> A -> Bool, -x: A, -y: A, -z: List<&1, A & A>, b: Bool, e: {le(x, y) == b : Bool}) -> {Bool.and(b, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), z)) == List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), (x, y) <> z) : Bool}:
837  %Equal.sym(Bool, le(x, y), b, e) : {Bool.and(b, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), z)) == List.all.if(u => List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), z), _) : Bool}
838  internal_all_if(b, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), z))
839
840# A Nat list sorted by Nat.is_le stays sorted under a head that is <= the next element.
841law sorted_cons_cons_intro:
842  for -x: Nat
843  for -y: Nat
844  for -t: List<&2, Nat>
845  for hxy: MNat.le(x, y)
846  for hyt: sorted_by(~Nat, ~Nat.is_le, y <> t)
847  sorted_by(~Nat, ~Nat.is_le, x <> y <> t)
848
849def sorted_cons_cons_intro(x, y, t, hxy, hyt):
850  %internal_sorted_cons_true(~Nat, ~Nat.is_le, x, y, List.zip(&2, Nat, &2, Nat, y <> t, t), hxy) : {_ == True{} : Bool}
851  hyt
852
853def internal_sorted_tail_step(-x: Nat, +y: Nat, +t: List<&2, Nat>, b: Bool, e: {Nat.is_le(x, y) == b : Bool}, h: sorted_by(~Nat, ~Nat.is_le, x <> y <> t)) -> sorted_by(~Nat, ~Nat.is_le, y <> t):
854  match b:
855    case True{}:
856      Equal.trans(Bool, List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), (x, y) <> List.zip(&2, Nat, &2, Nat, y <> t, t)), True{}, internal_sorted_cons_true(~Nat, ~Nat.is_le, x, y, List.zip(&2, Nat, &2, Nat, y <> t, t), e), h)
857    case False{}:
858      Empty.absurd(sorted_by(~Nat, ~Nat.is_le, y <> t), MNat.internal_false_ne_true(Equal.trans(Bool, False{}, List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), (x, y) <> List.zip(&2, Nat, &2, Nat, y <> t, t)), True{}, internal_sorted_cons_false(~Nat, ~Nat.is_le, x, y, List.zip(&2, Nat, &2, Nat, y <> t, t), e), h)))
859
860# The first two elements of a Nat list sorted by Nat.is_le are in order.
861law sorted_cons_cons_elim_le:
862  for x: Nat
863  for y: Nat
864  for -t: List<&2, Nat>
865  for h: sorted_by(~Nat, ~Nat.is_le, x <> y <> t)
866  MNat.le(x, y)
867
868def sorted_cons_cons_elim_le(x, y, t, h):
869  +x = x
870  +y = y
871  internal_and_left(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), Equal.trans(Bool, Bool.and(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t))), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), (x, y) <> List.zip(&2, Nat, &2, Nat, y <> t, t)), True{}, internal_sorted_cons_test(~Nat, ~Nat.is_le, x, y, List.zip(&2, Nat, &2, Nat, y <> t, t), Nat.is_le(x, y), {==}), h))
872
873# The tail of a Nat list of two or more elements sorted by Nat.is_le is sorted.
874law sorted_cons_cons_elim_tail:
875  for x: Nat
876  for y: Nat
877  for -t: List<&2, Nat>
878  for h: sorted_by(~Nat, ~Nat.is_le, x <> y <> t)
879  sorted_by(~Nat, ~Nat.is_le, y <> t)
880
881def sorted_cons_cons_elim_tail(x, y, t, h):
882  +x = x
883  +y = y
884  internal_and_right(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t)), Equal.trans(Bool, Bool.and(Nat.is_le(x, y), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), List.zip(&2, Nat, &2, Nat, y <> t, t))), List.all(~&1, ~(Nat & Nat), ~(p => Nat.is_le(Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p))), (x, y) <> List.zip(&2, Nat, &2, Nat, y <> t, t)), True{}, internal_sorted_cons_test(~Nat, ~Nat.is_le, x, y, List.zip(&2, Nat, &2, Nat, y <> t, t), Nat.is_le(x, y), {==}), h))
885
886# The tail of a nonempty Nat list sorted by Nat.is_le is sorted.
887law sorted_tail:
888  for x: Nat
889  for xs: List<&2, Nat>
890  for h: sorted_by(~Nat, ~Nat.is_le, x <> xs)
891  sorted_by(~Nat, ~Nat.is_le, xs)
892
893def sorted_tail(x, xs, h):
894  match xs:
895    case Nil{}:
896      {==}
897    case +y <> t:
898      +x = x
899      internal_sorted_tail_step(x, y, t, Nat.is_le(x, y), {==}, h)
900
901def internal_sorted_take_cons(t: List<&2, Nat>, n: Nat, +x: Nat, h: sorted_by(~Nat, ~Nat.is_le, x <> t)) -> sorted_by(~Nat, ~Nat.is_le, x <> List.take(&2, Nat, t, n)):
902  match t n:
903    case Nil{} _:
904      {==}
905    case y <> u 0n:
906      {==}
907    case +y <> u 1n+q:
908      +u = u
909      +h = h
910      sorted_cons_cons_intro(x, y, List.take(&2, Nat, u, q), sorted_cons_cons_elim_le(x, y, u, h), internal_sorted_take_cons(u, q, y, sorted_cons_cons_elim_tail(x, y, u, h)))
911
912# A prefix of a Nat list sorted by Nat.is_le is sorted.
913law sorted_take:
914  for xs: List<&2, Nat>
915  for n: Nat
916  for h: sorted_by(~Nat, ~Nat.is_le, xs)
917  sorted_by(~Nat, ~Nat.is_le, List.take(&2, Nat, xs, n))
918
919def sorted_take(xs, n, h):
920  match xs n:
921    case Nil{} _:
922      {==}
923    case x <> t 0n:
924      {==}
925    case x <> t 1n+p:
926      internal_sorted_take_cons(t, p, x, h)
927
928# A suffix of a Nat list sorted by Nat.is_le is sorted.
929law sorted_drop:
930  for xs: List<&2, Nat>
931  for n: Nat
932  for h: sorted_by(~Nat, ~Nat.is_le, xs)
933  sorted_by(~Nat, ~Nat.is_le, List.drop(&2, Nat, xs, n))
934
935def sorted_drop(xs, n, h):
936  match xs n:
937    case Nil{} _:
938      {==}
939    case x <> t 0n:
940      h
941    case x <> t 1n+p:
942      +t = t
943      sorted_drop(t, p, sorted_tail(x, t, h))
944
945def internal_sorted_skip(+x: Nat, +z: Nat, t: List<&2, Nat>, h: sorted_by(~Nat, ~Nat.is_le, x <> z <> t)) -> sorted_by(~Nat, ~Nat.is_le, x <> t):
946  match t:
947    case Nil{}:
948      {==}
949    case +w <> u:
950      +u = u
951      +h = h
952      sorted_cons_cons_intro(x, w, u, MNat.le_trans(x, z, w, sorted_cons_cons_elim_le(x, z, w <> u, h), sorted_cons_cons_elim_le(z, w, u, sorted_cons_cons_elim_tail(x, z, w <> u, h))), sorted_cons_cons_elim_tail(z, w, u, sorted_cons_cons_elim_tail(x, z, w <> u, h)))
953
954def internal_sorted_filter_cons_put(-x: Nat, -z: Nat, -r: List<&2, Nat>, b: Bool, hxz: MNat.le(x, z), hxr: sorted_by(~Nat, ~Nat.is_le, x <> r), hzr: sorted_by(~Nat, ~Nat.is_le, z <> r)) -> sorted_by(~Nat, ~Nat.is_le, x <> List.filter.put(Nat, z, r, b)):
955  match b:
956    case False{}:
957      hxr
958    case True{}:
959      sorted_cons_cons_intro(x, z, r, hxz, hzr)
960
961def internal_sorted_filter_cons(~f: Nat -> Bool, xs: List<&2, Nat>, +x: Nat, h: sorted_by(~Nat, ~Nat.is_le, x <> xs)) -> sorted_by(~Nat, ~Nat.is_le, x <> List.filter(~Nat, ~f, xs)):
962  match xs:
963    case Nil{}:
964      {==}
965    case +z <> t:
966      +t = t
967      +h = h
968      internal_sorted_filter_cons_put(x, z, List.filter(~Nat, ~f, t), f(z), sorted_cons_cons_elim_le(x, z, t, h), internal_sorted_filter_cons(~f, t, x, internal_sorted_skip(x, z, t, h)), internal_sorted_filter_cons(~f, t, z, sorted_cons_cons_elim_tail(x, z, t, h)))
969
970def internal_sorted_filter_put(-x: Nat, -r: List<&2, Nat>, b: Bool, hxr: sorted_by(~Nat, ~Nat.is_le, x <> r), hr: sorted_by(~Nat, ~Nat.is_le, r)) -> sorted_by(~Nat, ~Nat.is_le, List.filter.put(Nat, x, r, b)):
971  match b:
972    case False{}:
973      hr
974    case True{}:
975      hxr
976
977# Filtering a Nat list sorted by Nat.is_le keeps it sorted.
978law sorted_filter:
979  for ~f: Nat -> Bool
980  for xs: List<&2, Nat>
981  for h: sorted_by(~Nat, ~Nat.is_le, xs)
982  sorted_by(~Nat, ~Nat.is_le, List.filter(~Nat, ~f, xs))
983
984def sorted_filter(f, xs, h):
985  match xs:
986    case Nil{}:
987      {==}
988    case +x <> t:
989      +t = t
990      +h = h
991      internal_sorted_filter_put(x, List.filter(~Nat, ~f, t), f(x), internal_sorted_filter_cons(~f, t, x, h), sorted_filter(~f, t, sorted_tail(x, t, h)))
992
993def internal_head_le_mem_step(+x: Nat, +z: Nat, -t: List<&2, Nat>, +y: Nat, b: Bool, e: {Nat.is_eq(z, y) == b : Bool}, hxz: MNat.le(x, z), hm: {Bool.or(b, List.contains(~Nat, ~Nat.is_eq, t, y)) == True{} : Bool}, ih: {List.contains(~Nat, ~Nat.is_eq, t, y) == True{} : Bool} -> MNat.le(z, y)) -> MNat.le(x, y):
994  match b:
995    case True{}:
996      %MNat.eq_of_is_eq(z, y, e) : MNat.le(x, _)
997      hxz
998    case False{}:
999      MNat.le_trans(x, z, y, hxz, ih(hm))
1000
1001def internal_head_le_mem(xs: List<&2, Nat>, x: Nat, y: Nat, hs: sorted_by(~Nat, ~Nat.is_le, x <> xs), hm: mem(~Nat, ~Nat.is_eq, y, xs)) -> MNat.le(x, y):
1002  match xs:
1003    case Nil{}:
1004      Empty.absurd(MNat.le(x, y), MNat.internal_false_ne_true(hm))
1005    case +z <> t:
1006      +x = x
1007      +y = y
1008      +t = t
1009      +hs = hs
1010      internal_head_le_mem_step(x, z, t, y, Nat.is_eq(z, y), {==}, sorted_cons_cons_elim_le(x, z, t, hs), Equal.trans(Bool, Bool.or(Nat.is_eq(z, y), List.contains(~Nat, ~Nat.is_eq, t, y)), List.contains(~Nat, ~Nat.is_eq, z <> t, y), True{}, internal_contains_cons(~Nat, ~Nat.is_eq, z, t, y), hm), k => internal_head_le_mem(t, z, y, sorted_cons_cons_elim_tail(x, z, t, hs), k))
1011
1012# The head of a Nat list sorted by Nat.is_le is <= every member of its tail.
1013law sorted_head_le_mem:
1014  for x: Nat
1015  for xs: List<&2, Nat>
1016  for y: Nat
1017  for hs: sorted_by(~Nat, ~Nat.is_le, x <> xs)
1018  for hm: mem(~Nat, ~Nat.is_eq, y, xs)
1019  MNat.le(x, y)
1020
1021def sorted_head_le_mem(x, xs, y, hs, hm):
1022  internal_head_le_mem(xs, x, y, hs, hm)
1023
1024def internal_le_of_mem_step(+x: Nat, xs: List<&2, Nat>, +y: Nat, b: Bool, e: {Nat.is_eq(x, y) == b : Bool}, hs: sorted_by(~Nat, ~Nat.is_le, x <> xs), hm: {Bool.or(b, List.contains(~Nat, ~Nat.is_eq, xs, y)) == True{} : Bool}) -> MNat.le(x, y):
1025  match b:
1026    case True{}:
1027      %MNat.eq_of_is_eq(x, y, e) : MNat.le(x, _)
1028      MNat.le_refl(x)
1029    case False{}:
1030      sorted_head_le_mem(x, xs, y, hs, hm)
1031
1032# The head of a Nat list sorted by Nat.is_le is <= every member of the list.
1033law sorted_le_of_mem:
1034  for x: Nat
1035  for xs: List<&2, Nat>
1036  for y: Nat
1037  for hs: sorted_by(~Nat, ~Nat.is_le, x <> xs)
1038  for hm: mem(~Nat, ~Nat.is_eq, y, x <> xs)
1039  MNat.le(x, y)
1040
1041def sorted_le_of_mem(x, xs, y, hs, hm):
1042  +x = x
1043  +y = y
1044  +xs = xs
1045  internal_le_of_mem_step(x, xs, y, Nat.is_eq(x, y), {==}, hs, Equal.trans(Bool, Bool.or(Nat.is_eq(x, y), List.contains(~Nat, ~Nat.is_eq, xs, y)), List.contains(~Nat, ~Nat.is_eq, x <> xs, y), True{}, internal_contains_cons(~Nat, ~Nat.is_eq, x, xs, y), hm))
1046
1047def internal_sorted_append_cons(t: List<&2, Nat>, ys: List<&2, Nat>, +x: Nat, bnd: @a: Nat -> @b: Nat -> mem(~Nat, ~Nat.is_eq, a, x <> t) -> mem(~Nat, ~Nat.is_eq, b, ys) -> MNat.le(a, b), hx: sorted_by(~Nat, ~Nat.is_le, x <> t), hy: sorted_by(~Nat, ~Nat.is_le, ys)) -> sorted_by(~Nat, ~Nat.is_le, x <> List.append(&2, Nat, t, ys)):
1048  match t:
1049    case Nil{}:
1050      match ys:
1051        case Nil{}:
1052          {==}
1053        case +y <> u:
1054          +u = u
1055          sorted_cons_cons_intro(x, y, u, bnd(x, y, mem_cons_self(x, Nil{}), mem_cons_self(y, u)), hy)
1056    case +z <> u:
1057      +u = u
1058      +hx = hx
1059      sorted_cons_cons_intro(x, z, List.append(&2, Nat, u, ys), sorted_cons_cons_elim_le(x, z, u, hx), internal_sorted_append_cons(u, ys, z, +a => b => ma => mb => bnd(a, b, mem_cons_of_mem(a, x, z <> u, ma), mb), sorted_cons_cons_elim_tail(x, z, u, hx), hy))
1060
1061# Appending two Nat lists sorted by Nat.is_le, with every element of the first <= every element of the second, gives a sorted list.
1062law sorted_append:
1063  for xs: List<&2, Nat>
1064  for ys: List<&2, Nat>
1065  for bnd: @x: Nat -> @y: Nat -> mem(~Nat, ~Nat.is_eq, x, xs) -> mem(~Nat, ~Nat.is_eq, y, ys) -> MNat.le(x, y)
1066  for hx: sorted_by(~Nat, ~Nat.is_le, xs)
1067  for hy: sorted_by(~Nat, ~Nat.is_le, ys)
1068  sorted_by(~Nat, ~Nat.is_le, List.append(&2, Nat, xs, ys))
1069
1070def sorted_append(xs, ys, bnd, hx, hy):
1071  match xs:
1072    case Nil{}:
1073      hy
1074    case x <> t:
1075      internal_sorted_append_cons(t, ys, x, bnd, hx, hy)
1076
1077# Taking the length of the first part of an append gives the first part back.
1078law take_left:
1079  for -a: Quant
1080  for -A: Kind(a)
1081  for xs: List<a, A>
1082  for ys: List<a, A>
1083  {List.take(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) == xs : List<a, A>}
1084
1085def take_left(a, A, xs, ys):
1086  match xs:
1087    case Nil{}:
1088      take_zero(a, A, ys)
1089    case h <> t:
1090      %take_left(a, A, t, ys) : {h <> List.take(a, A, List.append(a, A, t, ys), List.length(a, A, t)) == h <> _ : List<a, A>}
1091      {==}
1092
1093# Dropping the length of the first part of an append gives the second part.
1094law drop_left:
1095  for -a: Quant
1096  for -A: Kind(a)
1097  for xs: List<a, A>
1098  for ys: List<a, A>
1099  {List.drop(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) == ys : List<a, A>}
1100
1101def drop_left(a, A, xs, ys):
1102  match xs:
1103    case Nil{}:
1104      drop_zero(a, A, ys)
1105    case h <> t:
1106      drop_left(a, A, t, ys)
1107
1108# Taking past the first part of an append keeps it and takes the rest from the second part.
1109law take_append:
1110  for -a: Quant
1111  for -A: Kind(a)
1112  for xs: List<a, A>
1113  for -ys: List<a, A>
1114  for -n: Nat
1115  {List.take(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)) == List.append(a, A, xs, List.take(a, A, ys, n)) : List<a, A>}
1116
1117def take_append(a, A, xs, ys, n):
1118  match xs:
1119    case Nil{}:
1120      {==}
1121    case h <> t:
1122      %take_append(a, A, t, ys, n) : {h <> List.take(a, A, List.append(a, A, t, ys), Nat.add(List.length(a, A, t), n)) == h <> _ : List<a, A>}
1123      {==}
1124
1125# Dropping past the first part of an append drops the rest from the second part.
1126law drop_append:
1127  for -a: Quant
1128  for -A: Kind(a)
1129  for xs: List<a, A>
1130  for -ys: List<a, A>
1131  for -n: Nat
1132  {List.drop(a, A, List.append(a, A, xs, ys), Nat.add(List.length(a, A, xs), n)) == List.drop(a, A, ys, n) : List<a, A>}
1133
1134def drop_append(a, A, xs, ys, n):
1135  match xs:
1136    case Nil{}:
1137      {==}
1138    case h <> t:
1139      drop_append(a, A, t, ys, n)
1140
1141# Taking at most the length of the first part of an append only sees the first part.
1142law take_append_of_le_length:
1143  for -a: Quant
1144  for -A: Kind(a)
1145  for xs: List<a, A>
1146  for ys: List<a, A>
1147  for n: Nat
1148  for h: MNat.le(n, List.length(a, A, xs))
1149  {List.take(a, A, List.append(a, A, xs, ys), n) == List.take(a, A, xs, n) : List<a, A>}
1150
1151def take_append_of_le_length(a, A, xs, ys, n, h):
1152  match xs n:
1153    case Nil{} 0n:
1154      take_zero(a, A, ys)
1155    case Nil{} 1n+p:
1156      Empty.absurd({List.take(a, A, ys, 1n+p) == Nil{} : List<a, A>}, MNat.internal_false_ne_true(h))
1157    case x <> t 0n:
1158      {==}
1159    case x <> t 1n+p:
1160      %take_append_of_le_length(a, A, t, ys, p, h) : {x <> List.take(a, A, List.append(a, A, t, ys), p) == x <> _ : List<a, A>}
1161      {==}
1162
1163# Dropping at most the length of the first part of an append drops only from the first part.
1164law drop_append_of_le_length:
1165  for -a: Quant
1166  for -A: Kind(a)
1167  for xs: List<a, A>
1168  for ys: List<a, A>
1169  for n: Nat
1170  for h: MNat.le(n, List.length(a, A, xs))
1171  {List.drop(a, A, List.append(a, A, xs, ys), n) == List.append(a, A, List.drop(a, A, xs, n), ys) : List<a, A>}
1172
1173def drop_append_of_le_length(a, A, xs, ys, n, h):
1174  match xs n:
1175    case Nil{} 0n:
1176      drop_zero(a, A, ys)
1177    case Nil{} 1n+p:
1178      Empty.absurd({List.drop(a, A, ys, 1n+p) == ys : List<a, A>}, MNat.internal_false_ne_true(h))
1179    case x <> t 0n:
1180      {==}
1181    case x <> t 1n+p:
1182      drop_append_of_le_length(a, A, t, ys, p, h)
1183
1184# Mapping commutes with taking: map f (take n xs) = take n (map f xs).
1185law map_take:
1186  for ~A: Type
1187  for ~B: Type
1188  for ~f: A -> B
1189  for xs: List<A>
1190  for n: Nat
1191  {List.map(~A, ~B, ~f, List.take(&1, A, xs, n)) == List.take(&1, B, List.map(~A, ~B, ~f, xs), n) : List<B>}
1192
1193def map_take(A, B, f, xs, n):
1194  match xs n:
1195    case Nil{} _:
1196      {==}
1197    case h <> t 0n:
1198      {==}
1199    case h <> t 1n+p:
1200      %map_take(~A, ~B, ~f, t, p) : {f(h) <> List.map(~A, ~B, ~f, List.take(&1, A, t, p)) == f(h) <> _ : List<B>}
1201      {==}
1202
1203# Mapping commutes with dropping: map f (drop n xs) = drop n (map f xs).
1204law map_drop:
1205  for ~A: Type
1206  for ~B: Type
1207  for ~f: A -> B
1208  for xs: List<A>
1209  for n: Nat
1210  {List.map(~A, ~B, ~f, List.drop(&1, A, xs, n)) == List.drop(&1, B, List.map(~A, ~B, ~f, xs), n) : List<B>}
1211
1212def map_drop(A, B, f, xs, n):
1213  match xs n:
1214    case Nil{} _:
1215      {==}
1216    case h <> t 0n:
1217      {==}
1218    case h <> t 1n+p:
1219      map_drop(~A, ~B, ~f, t, p)
1220
1221# Taking m from n copies of x gives min(m, n) copies of x.
1222law take_replicate:
1223  for -A: Data
1224  for n: Nat
1225  for m: Nat
1226  for -x: A
1227  {List.take(&2, A, List.replicate(A, n, x), m) == List.replicate(A, Nat.min(m, n), x) : List<&2, A>}
1228
1229def take_replicate(A, n, m, x):
1230  match n m:
1231    case 0n _:
1232      %MNat.min_zero_sym(m) : {Nil{} == List.replicate(A, _, x) : List<&2, A>}
1233      {==}
1234    case 1n+p 0n:
1235      {==}
1236    case 1n+p 1n+q:
1237      %take_replicate(A, p, q, x) : {x <> List.take(&2, A, List.replicate(A, p, x), q) == x <> _ : List<&2, A>}
1238      {==}
1239
1240# Dropping m from n copies of x gives n - m copies of x.
1241law drop_replicate:
1242  for -A: Data
1243  for n: Nat
1244  for m: Nat
1245  for -x: A
1246  {List.drop(&2, A, List.replicate(A, n, x), m) == List.replicate(A, Nat.sub(n, m), x) : List<&2, A>}
1247
1248def drop_replicate(A, n, m, x):
1249  match n m:
1250    case 0n _:
1251      {==}
1252    case 1n+p 0n:
1253      {==}
1254    case 1n+p 1n+q:
1255      drop_replicate(A, p, q, x)
1256
1257# Taking n elements gives at most n of them.
1258law length_take_le:
1259  for -a: Quant
1260  for -A: Kind(a)
1261  for xs: List<a, A>
1262  for n: Nat
1263  MNat.le(List.length(a, A, List.take(a, A, xs, n)), n)
1264
1265def length_take_le(a, A, xs, n):
1266  match xs n:
1267    case Nil{} _:
1268      MNat.zero_le(n)
1269    case h <> t 0n:
1270      {==}
1271    case h <> t 1n+p:
1272      MNat.succ_le_succ(List.length(a, A, List.take(a, A, t, p)), p, length_take_le(a, A, t, p))
1273
1274# The tail is one shorter than the list, or empty: length (tail xs) = length xs - 1.
1275law length_tail:
1276  for -a: Quant
1277  for -A: Kind(a)
1278  for xs: List<a, A>
1279  {List.length(a, A, List.tail(a, A, xs)) == Nat.sub(List.length(a, A, xs), 1n) : Nat}
1280
1281def length_tail(a, A, xs):
1282  match xs:
1283    case Nil{}:
1284      {==}
1285    case h <> t:
1286      MNat.sub_zero_sym(List.length(a, A, t))
1287
1288# Mapping the identity gives the list back.
1289law map_id:
1290  for ~A: Type
1291  for xs: List<A>
1292  {List.map(~A, ~A, ~(x => x), xs) == xs : List<A>}
1293
1294def map_id(A, xs):
1295  match xs:
1296    case Nil{}:
1297      {==}
1298    case h <> t:
1299      %map_id(~A, t) : {h <> List.map(~A, ~A, ~(x => x), t) == h <> _ : List<A>}
1300      {==}
1301
1302# A right fold over a map folds with the mapped function: foldr g z (map f xs) = foldr (g . f) z xs.
1303law foldr_map:
1304  for ~A: Type
1305  for ~B: Type
1306  for ~C: Type
1307  for ~f: A -> B
1308  for ~g: B -> C -> C
1309  for xs: List<A>
1310  for -z: C
1311  {List.foldr(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, xs), z) == List.foldr(~&1, ~A, ~C, ~(x => y => g(f(x), y)), xs, z) : C}
1312
1313def foldr_map(A, B, C, f, g, xs, z):
1314  match xs:
1315    case Nil{}:
1316      {==}
1317    case h <> t:
1318      %foldr_map(~A, ~B, ~C, ~f, ~g, t, z) : {g(f(h), List.foldr(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, t), z)) == g(f(h), _) : C}
1319      {==}
1320
1321# A left fold over a map folds with the mapped function: foldl g z (map f xs) = foldl (fun acc x => g acc (f x)) z xs.
1322law foldl_map:
1323  for ~A: Type
1324  for ~B: Type
1325  for ~C: Type
1326  for ~f: A -> B
1327  for ~g: C -> B -> C
1328  for xs: List<A>
1329  for -z: C
1330  {List.foldl(~&1, ~B, ~C, ~g, List.map(~A, ~B, ~f, xs), z) == List.foldl(~&1, ~A, ~C, ~(x => y => g(x, f(y))), xs, z) : C}
1331
1332def foldl_map(A, B, C, f, g, xs, z):
1333  match xs:
1334    case Nil{}:
1335      {==}
1336    case h <> t:
1337      foldl_map(~A, ~B, ~C, ~f, ~g, t, g(z, f(h)))
1338
1339# Replicating m + n times appends m copies to n copies.
1340law replicate_add:
1341  for -A: Data
1342  for m: Nat
1343  for -n: Nat
1344  for -x: A
1345  {List.replicate(A, Nat.add(m, n), x) == List.append(&2, A, List.replicate(A, m, x), List.replicate(A, n, x)) : List<&2, A>}
1346
1347def replicate_add(A, m, n, x):
1348  match m:
1349    case 0n:
1350      {==}
1351    case 1n+p:
1352      %replicate_add(A, p, n, x) : {x <> List.replicate(A, Nat.add(p, n), x) == x <> _ : List<&2, A>}
1353      {==}
1354
1355def internal_replicate_append_nil(-A: Data, n: Nat, -x: A) -> {List.append(&2, A, List.replicate(A, n, x), Nil{}) == List.replicate(A, n, x) : List<&2, A>}:
1356  match n:
1357    case 0n:
1358      {==}
1359    case 1n+p:
1360      %internal_replicate_append_nil(A, p, x) : {x <> List.append(&2, A, List.replicate(A, p, x), Nil{}) == x <> _ : List<&2, A>}
1361      {==}
1362
1363def internal_replicate_append_cons(-A: Data, n: Nat, -x: A, -acc: List<&2, A>) -> {List.append(&2, A, List.replicate(A, n, x), x <> acc) == x <> List.append(&2, A, List.replicate(A, n, x), acc) : List<&2, A>}:
1364  match n:
1365    case 0n:
1366      {==}
1367    case 1n+p:
1368      %internal_replicate_append_cons(A, p, x, acc) : {x <> List.append(&2, A, List.replicate(A, p, x), x <> acc) == x <> _ : List<&2, A>}
1369      {==}
1370
1371def internal_reverse_go_replicate(-A: Data, n: Nat, -x: A, -acc: List<&2, A>) -> {List.reverse.go(&2, A, List.replicate(A, n, x), acc) == List.append(&2, A, List.replicate(A, n, x), acc) : List<&2, A>}:
1372  match n:
1373    case 0n:
1374      {==}
1375    case 1n+p:
1376      +p = p
1377      Equal.trans(List<&2, A>, List.reverse.go(&2, A, List.replicate(A, p, x), x <> acc), List.append(&2, A, List.replicate(A, p, x), x <> acc), x <> List.append(&2, A, List.replicate(A, p, x), acc), internal_reverse_go_replicate(A, p, x, x <> acc), internal_replicate_append_cons(A, p, x, acc))
1378
1379# Reversing n copies of x gives them back.
1380law reverse_replicate:
1381  for -A: Data
1382  for n: Nat
1383  for -x: A
1384  {List.reverse(&2, A, List.replicate(A, n, x)) == List.replicate(A, n, x) : List<&2, A>}
1385
1386def reverse_replicate(A, n, x):
1387  +n = n
1388  Equal.trans(List<&2, A>, List.reverse(&2, A, List.replicate(A, n, x)), List.append(&2, A, List.replicate(A, n, x), Nil{}), List.replicate(A, n, x), internal_reverse_go_replicate(A, n, x, Nil{}), internal_replicate_append_nil(A, n, x))
1389
1390# Filtering with an always-true predicate gives the list back.
1391law filter_true:
1392  for ~A: Data
1393  for xs: List<&2, A>
1394  {List.filter(~A, ~(x => True{}), xs) == xs : List<&2, A>}
1395
1396def filter_true(A, xs):
1397  match xs:
1398    case Nil{}:
1399      {==}
1400    case h <> t:
1401      %filter_true(~A, t) : {h <> List.filter(~A, ~(x => True{}), t) == h <> _ : List<&2, A>}
1402      {==}
1403
1404# Filtering with an always-false predicate gives the empty list.
1405law filter_false:
1406  for ~A: Data
1407  for xs: List<&2, A>
1408  {List.filter(~A, ~(x => False{}), xs) == Nil{} : List<&2, A>}
1409
1410def filter_false(A, xs):
1411  match xs:
1412    case Nil{}:
1413      {==}
1414    case h <> t:
1415      filter_false(~A, t)
1416
1417def internal_filter_put_filter(~A: Data, ~p: A -> Bool, +h: A, r: List<&2, A>, b: Bool) -> {List.filter(~A, ~p, List.filter.put(A, h, r, b)) == List.filter.put(A, h, List.filter(~A, ~p, r), Bool.and(p(h), b)) : List<&2, A>}:
1418  match b:
1419    case False{}:
1420      %MBool.and_false_sym(p(h)) : {List.filter(~A, ~p, r) == List.filter.put(A, h, List.filter(~A, ~p, r), _) : List<&2, A>}
1421      {==}
1422    case True{}:
1423      %MBool.and_true_sym(p(h)) : {List.filter(~A, ~p, h <> r) == List.filter.put(A, h, List.filter(~A, ~p, r), _) : List<&2, A>}
1424      {==}
1425
1426# Filtering twice is filtering by both predicates: filter p (filter q xs) = filter (p and q) xs.
1427law filter_filter:
1428  for ~A: Data
1429  for ~p: A -> Bool
1430  for ~q: A -> Bool
1431  for xs: List<&2, A>
1432  {List.filter(~A, ~p, List.filter(~A, ~q, xs)) == List.filter(~A, ~(+x => Bool.and(p(x), q(x))), xs) : List<&2, A>}
1433
1434def filter_filter(A, p, q, xs):
1435  match xs:
1436    case Nil{}:
1437      {==}
1438    case +h <> t:
1439      +t = t
1440      %filter_filter(~A, ~p, ~q, t) : {List.filter(~A, ~p, List.filter.put(A, h, List.filter(~A, ~q, t), q(h))) == List.filter.put(A, h, _, Bool.and(p(h), q(h))) : List<&2, A>}
1441      internal_filter_put_filter(~A, ~p, h, List.filter(~A, ~q, t), q(h))
1442
1443def internal_all_filter_put(~A: Data, ~q: A -> Bool, +h: A, r: List<&2, A>, b: Bool) -> {List.all(~&2, ~A, ~q, List.filter.put(A, h, r, b)) == Bool.and(Bool.or(Bool.not(b), q(h)), List.all(~&2, ~A, ~q, r)) : Bool}:
1444  match b:
1445    case False{}:
1446      {==}
1447    case True{}:
1448      Equal.sym(Bool, Bool.and(q(h), List.all(~&2, ~A, ~q, r)), List.all(~&2, ~A, ~q, h <> r), internal_all_cons(~&2, ~A, ~q, h, r))
1449
1450# All over a filter checks q only where p holds: all q (filter p xs) = all (not p or q) xs.
1451law all_filter:
1452  for ~A: Data
1453  for ~p: A -> Bool
1454  for ~q: A -> Bool
1455  for xs: List<&2, A>
1456  {List.all(~&2, ~A, ~q, List.filter(~A, ~p, xs)) == List.all(~&2, ~A, ~(+x => Bool.or(Bool.not(p(x)), q(x))), xs) : Bool}
1457
1458def all_filter(A, p, q, xs):
1459  match xs:
1460    case Nil{}:
1461      {==}
1462    case +h <> t:
1463      +t = t
1464      %internal_all_cons(~&2, ~A, ~(+x => Bool.or(Bool.not(p(x)), q(x))), h, t) : {List.all(~&2, ~A, ~q, List.filter.put(A, h, List.filter(~A, ~p, t), p(h))) == _ : Bool}
1465      %all_filter(~A, ~p, ~q, t) : {List.all(~&2, ~A, ~q, List.filter.put(A, h, List.filter(~A, ~p, t), p(h))) == Bool.and(Bool.or(Bool.not(p(h)), q(h)), _) : Bool}
1466      internal_all_filter_put(~A, ~q, h, List.filter(~A, ~p, t), p(h))
1467
1468def internal_any_filter_put(~A: Data, ~q: A -> Bool, +h: A, r: List<&2, A>, b: Bool) -> {List.any(~&2, ~A, ~q, List.filter.put(A, h, r, b)) == Bool.or(Bool.and(b, q(h)), List.any(~&2, ~A, ~q, r)) : Bool}:
1469  match b:
1470    case False{}:
1471      {==}
1472    case True{}:
1473      Equal.sym(Bool, Bool.or(q(h), List.any(~&2, ~A, ~q, r)), List.any(~&2, ~A, ~q, h <> r), internal_any_cons(~&2, ~A, ~q, h, r))
1474
1475# Any over a filter looks for q only where p holds: any q (filter p xs) = any (p and q) xs.
1476law any_filter:
1477  for ~A: Data
1478  for ~p: A -> Bool
1479  for ~q: A -> Bool
1480  for xs: List<&2, A>
1481  {List.any(~&2, ~A, ~q, List.filter(~A, ~p, xs)) == List.any(~&2, ~A, ~(+x => Bool.and(p(x), q(x))), xs) : Bool}
1482
1483def any_filter(A, p, q, xs):
1484  match xs:
1485    case Nil{}:
1486      {==}
1487    case +h <> t:
1488      +t = t
1489      %internal_any_cons(~&2, ~A, ~(+x => Bool.and(p(x), q(x))), h, t) : {List.any(~&2, ~A, ~q, List.filter.put(A, h, List.filter(~A, ~p, t), p(h))) == _ : Bool}
1490      %any_filter(~A, ~p, ~q, t) : {List.any(~&2, ~A, ~q, List.filter.put(A, h, List.filter(~A, ~p, t), p(h))) == Bool.or(Bool.and(p(h), q(h)), _) : Bool}
1491      internal_any_filter_put(~A, ~q, h, List.filter(~A, ~p, t), p(h))
1492
1493# Unfolds List.all directly, so its proof depends on Base's definition (PLAN F39).
1494def internal_all_map(~A: Type, ~B: Type, ~f: A -> B, ~p: B -> Bool, xs: List<A>) -> {List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) == List.all(~&1, ~A, ~(x => p(f(x))), xs) : Bool}:
1495  match xs:
1496    case Nil{}:
1497      {==}
1498    case h <> t:
1499      %internal_all_map(~A, ~B, ~f, ~p, t) : {List.all.if(u => List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, t)), p(f(h))) == List.all.if(u => _, p(f(h))) : Bool}
1500      {==}
1501
1502def internal_any_map(~A: Type, ~B: Type, ~f: A -> B, ~p: B -> Bool, xs: List<A>) -> {List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) == List.any(~&1, ~A, ~(x => p(f(x))), xs) : Bool}:
1503  match xs:
1504    case Nil{}:
1505      {==}
1506    case h <> t:
1507      %internal_any_map(~A, ~B, ~f, ~p, t) : {List.any.if(u => List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, t)), p(f(h))) == List.any.if(u => _, p(f(h))) : Bool}
1508      {==}
1509
1510# All over a map checks the composed predicate: all p (map f xs) = all (p . f) xs.
1511law all_map:
1512  for ~A: Type
1513  for ~B: Type
1514  for ~f: A -> B
1515  for ~p: B -> Bool
1516  for xs: List<A>
1517  {List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) == List.all(~&1, ~A, ~(x => p(f(x))), xs) : Bool}
1518
1519def all_map(A, B, f, p, xs):
1520  internal_all_map(~A, ~B, ~f, ~p, xs)
1521
1522# Any over a map checks the composed predicate: any p (map f xs) = any (p . f) xs.
1523law any_map:
1524  for ~A: Type
1525  for ~B: Type
1526  for ~f: A -> B
1527  for ~p: B -> Bool
1528  for xs: List<A>
1529  {List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) == List.any(~&1, ~A, ~(x => p(f(x))), xs) : Bool}
1530
1531def any_map(A, B, f, p, xs):
1532  internal_any_map(~A, ~B, ~f, ~p, xs)
1533
1534def 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}:
1535  match xs c:
1536    case Nil{} True{}:
1537      e
1538    case Nil{} False{}:
1539      e
1540    case h <> t True{}:
1541      +v = f(h)
1542      %internal_all_cons_test(~a, ~A, ~f, h, t, v, {==}) : {List.all(~a, ~A, ~f, List.reverse.go(a, A, t, h <> acc)) == _ : Bool}
1543      internal_all_reverse_go(~a, ~A, ~f, t, h <> acc, v, Equal.trans(Bool, List.all(~a, ~A, ~f, h <> acc), Bool.and(v, List.all(~a, ~A, ~f, acc)), v, Equal.sym(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), List.all(~a, ~A, ~f, h <> acc), internal_all_cons_test(~a, ~A, ~f, h, acc, v, {==})), Equal.trans(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), Bool.and(v, True{}), v, Equal.cong(Bool, Bool, k => Bool.and(v, k), List.all(~a, ~A, ~f, acc), True{}, e), MBool.and_true(v))))
1544    case h <> t False{}:
1545      +v = f(h)
1546      internal_all_reverse_go(~a, ~A, ~f, t, h <> acc, False{}, Equal.trans(Bool, List.all(~a, ~A, ~f, h <> acc), Bool.and(v, List.all(~a, ~A, ~f, acc)), False{}, Equal.sym(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), List.all(~a, ~A, ~f, h <> acc), internal_all_cons_test(~a, ~A, ~f, h, acc, v, {==})), Equal.trans(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), Bool.and(v, False{}), False{}, Equal.cong(Bool, Bool, k => Bool.and(v, k), List.all(~a, ~A, ~f, acc), False{}, e), MBool.and_false(v))))
1547
1548# Reversing does not change whether all elements satisfy a predicate.
1549law all_reverse:
1550  for ~a: Quant
1551  for ~A: Kind(a)
1552  for ~f: A -> Bool
1553  for xs: List<a, A>
1554  {List.all(~a, ~A, ~f, List.reverse(a, A, xs)) == List.all(~a, ~A, ~f, xs) : Bool}
1555
1556def all_reverse(a, A, f, xs):
1557  internal_all_reverse_go(~a, ~A, ~f, xs, Nil{}, True{}, {==})
1558
1559def 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}:
1560  match xs c:
1561    case Nil{} True{}:
1562      e
1563    case Nil{} False{}:
1564      e
1565    case h <> t True{}:
1566      +v = f(h)
1567      internal_any_reverse_go(~a, ~A, ~f, t, h <> acc, True{}, Equal.trans(Bool, List.any(~a, ~A, ~f, h <> acc), Bool.or(v, List.any(~a, ~A, ~f, acc)), True{}, Equal.sym(Bool, Bool.or(v, List.any(~a, ~A, ~f, acc)), List.any(~a, ~A, ~f, h <> acc), internal_any_cons_test(~a, ~A, ~f, h, acc, v, {==})), Equal.trans(Bool, Bool.or(v, List.any(~a, ~A, ~f, acc)), Bool.or(v, True{}), True{}, Equal.cong(Bool, Bool, k => Bool.or(v, k), List.any(~a, ~A, ~f, acc), True{}, e), MBool.or_true(v))))
1568    case h <> t False{}:
1569      +v = f(h)
1570      %internal_any_cons_test(~a, ~A, ~f, h, t, v, {==}) : {List.any(~a, ~A, ~f, List.reverse.go(a, A, t, h <> acc)) == _ : Bool}
1571      internal_any_reverse_go(~a, ~A, ~f, t, h <> acc, v, Equal.trans(Bool, List.any(~a, ~A, ~f, h <> acc), Bool.or(v, List.any(~a, ~A, ~f, acc)), v, Equal.sym(Bool, Bool.or(v, List.any(~a, ~A, ~f, acc)), List.any(~a, ~A, ~f, h <> acc), internal_any_cons_test(~a, ~A, ~f, h, acc, v, {==})), Equal.trans(Bool, Bool.or(v, List.any(~a, ~A, ~f, acc)), Bool.or(v, False{}), v, Equal.cong(Bool, Bool, k => Bool.or(v, k), List.any(~a, ~A, ~f, acc), False{}, e), MBool.or_false(v))))
1572
1573# Reversing does not change whether some element satisfies a predicate.
1574law any_reverse:
1575  for ~a: Quant
1576  for ~A: Kind(a)
1577  for ~f: A -> Bool
1578  for xs: List<a, A>
1579  {List.any(~a, ~A, ~f, List.reverse(a, A, xs)) == List.any(~a, ~A, ~f, xs) : Bool}
1580
1581def any_reverse(a, A, f, xs):
1582  internal_any_reverse_go(~a, ~A, ~f, xs, Nil{}, False{}, {==})
1583
1584def internal_contains_reverse_go(~A: Data, ~eq: A -> A -> Bool, xs: List<&2, A>, +acc: List<&2, A>, +x: A, c: Bool, e: {List.contains(~A, ~eq, acc, x) == c : Bool}) -> {List.contains(~A, ~eq, List.reverse.go(&2, A, xs, acc), x) == Bool.or(c, List.contains(~A, ~eq, xs, x)) : Bool}:
1585  match xs c:
1586    case Nil{} True{}:
1587      e
1588    case Nil{} False{}:
1589      e
1590    case +h <> t True{}:
1591      internal_contains_reverse_go(~A, ~eq, t, h <> acc, x, True{}, Equal.trans(Bool, List.contains(~A, ~eq, h <> acc, x), Bool.or(eq(h, x), List.contains(~A, ~eq, acc, x)), True{}, Equal.sym(Bool, Bool.or(eq(h, x), List.contains(~A, ~eq, acc, x)), List.contains(~A, ~eq, h <> acc, x), internal_contains_cons(~A, ~eq, h, acc, x)), Equal.trans(Bool, Bool.or(eq(h, x), List.contains(~A, ~eq, acc, x)), Bool.or(eq(h, x), True{}), True{}, Equal.cong(Bool, Bool, k => Bool.or(eq(h, x), k), List.contains(~A, ~eq, acc, x), True{}, e), MBool.or_true(eq(h, x)))))
1592    case +h <> +t False{}:
1593      +v = eq(h, x)
1594      %internal_contains_cons(~A, ~eq, h, t, x) : {List.contains(~A, ~eq, List.reverse.go(&2, A, t, h <> acc), x) == _ : Bool}
1595      internal_contains_reverse_go(~A, ~eq, t, h <> acc, x, v, Equal.trans(Bool, List.contains(~A, ~eq, h <> acc, x), Bool.or(v, List.contains(~A, ~eq, acc, x)), v, Equal.sym(Bool, Bool.or(eq(h, x), List.contains(~A, ~eq, acc, x)), List.contains(~A, ~eq, h <> acc, x), internal_contains_cons(~A, ~eq, h, acc, x)), Equal.trans(Bool, Bool.or(v, List.contains(~A, ~eq, acc, x)), Bool.or(v, False{}), v, Equal.cong(Bool, Bool, k => Bool.or(v, k), List.contains(~A, ~eq, acc, x), False{}, e), MBool.or_false(v))))
1596
1597# Reversing does not change whether a list contains x.
1598law contains_reverse:
1599  for ~A: Data
1600  for ~eq: A -> A -> Bool
1601  for xs: List<&2, A>
1602  for +x: A
1603  {List.contains(~A, ~eq, List.reverse(&2, A, xs), x) == List.contains(~A, ~eq, xs, x) : Bool}
1604
1605def contains_reverse(A, eq, xs, x):
1606  internal_contains_reverse_go(~A, ~eq, xs, Nil{}, x, False{}, {==})
1607
1608# Zipping the empty list with anything gives the empty list.
1609law zip_nil_left:
1610  for -a: Quant
1611  for -A: Kind(a)
1612  for -b: Quant
1613  for -B: Kind(b)
1614  for -ys: List<b, B>
1615  {List.zip(a, A, b, B, Nil{}, ys) == Nil{} : List<&1, A & B>}
1616
1617def zip_nil_left(a, A, b, B, ys):
1618  {==}
1619
1620# Zipping anything with the empty list gives the empty list.
1621law zip_nil_right:
1622  for -a: Quant
1623  for -A: Kind(a)
1624  for -b: Quant
1625  for -B: Kind(b)
1626  for xs: List<a, A>
1627  {List.zip(a, A, b, B, xs, Nil{}) == Nil{} : List<&1, A & B>}
1628
1629def zip_nil_right(a, A, b, B, xs):
1630  match xs:
1631    case Nil{}:
1632      {==}
1633    case h <> t:
1634      {==}
1635
1636# The head of a cons is its first element.
1637law head_cons:
1638  for -a: Quant
1639  for -A: Kind(a)
1640  for -x: A
1641  for -xs: List<a, A>
1642  {List.head(a, A, x <> xs) == Some{x} : Maybe<a, A>}
1643
1644def head_cons(a, A, x, xs):
1645  {==}
1646
1647# The head of an append is the head of the first part, or else of the second.
1648law head_append:
1649  for -a: Quant
1650  for -A: Kind(a)
1651  for xs: List<a, A>
1652  for -ys: List<a, A>
1653  {List.head(a, A, List.append(a, A, xs, ys)) == Maybe.or(a, A, List.head(a, A, xs), List.head(a, A, ys)) : Maybe<a, A>}
1654
1655def head_append(a, A, xs, ys):
1656  match xs:
1657    case Nil{}:
1658      {==}
1659    case h <> t:
1660      {==}
1661
1662# The head of a map is the mapped head.
1663law head_map:
1664  for ~A: Type
1665  for ~B: Type
1666  for ~f: A -> B
1667  for xs: List<A>
1668  {List.head(&1, B, List.map(~A, ~B, ~f, xs)) == Maybe.map(&1, A, B, f, List.head(&1, A, xs)) : Maybe<&1, B>}
1669
1670def head_map(A, B, f, xs):
1671  match xs:
1672    case Nil{}:
1673      {==}
1674    case h <> t:
1675      {==}
1676
1677# The tail of a map is the map of the tail.
1678law tail_map:
1679  for ~A: Type
1680  for ~B: Type
1681  for ~f: A -> B
1682  for xs: List<A>
1683  {List.tail(&1, B, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~B, ~f, List.tail(&1, A, xs)) : List<B>}
1684
1685def tail_map(A, B, f, xs):
1686  match xs:
1687    case Nil{}:
1688      {==}
1689    case h <> t:
1690      {==}
1691
1692# The element at index zero of a cons is its head.
1693law get_cons_zero:
1694  for -a: Quant
1695  for -A: Kind(a)
1696  for -x: A
1697  for -xs: List<a, A>
1698  {List.get(a, A, x <> xs, 0n) == Some{x} : Maybe<a, A>}
1699
1700def get_cons_zero(a, A, x, xs):
1701  {==}
1702
1703# The element at index n + 1 of a cons is the element at index n of its tail.
1704law get_cons_succ:
1705  for -a: Quant
1706  for -A: Kind(a)
1707  for -x: A
1708  for -xs: List<a, A>
1709  for -n: Nat
1710  {List.get(a, A, x <> xs, 1n+n) == List.get(a, A, xs, n) : Maybe<a, A>}
1711
1712def get_cons_succ(a, A, x, xs, n):
1713  {==}
1714
1715# Indexing a map is mapping the indexed element.
1716law get_map:
1717  for ~A: Type
1718  for ~B: Type
1719  for ~f: A -> B
1720  for xs: List<A>
1721  for n: Nat
1722  {List.get(&1, B, List.map(~A, ~B, ~f, xs), n) == Maybe.map(&1, A, B, f, List.get(&1, A, xs, n)) : Maybe<&1, B>}
1723
1724def get_map(A, B, f, xs, n):
1725  match xs n:
1726    case Nil{} _:
1727      {==}
1728    case h <> t 0n:
1729      {==}
1730    case h <> t 1n+p:
1731      get_map(~A, ~B, ~f, t, p)
1732
1733# Setting an element does not change the length.
1734law length_set:
1735  for -a: Quant
1736  for -A: Kind(a)
1737  for xs: List<a, A>
1738  for n: Nat
1739  for -x: A
1740  {List.length(a, A, List.set(a, A, xs, n, x)) == List.length(a, A, xs) : Nat}
1741
1742def length_set(a, A, xs, n, x):
1743  match xs n:
1744    case Nil{} _:
1745      {==}
1746    case h <> t 0n:
1747      {==}
1748    case h <> t 1n+p:
1749      %length_set(a, A, t, p, x) : {1n+List.length(a, A, List.set(a, A, t, p, x)) == 1n+_ : Nat}
1750      {==}
1751
1752# Reading the index just set gives the new value wherever the index is in range.
1753law get_set_self:
1754  for -a: Quant
1755  for -A: Kind(a)
1756  for xs: List<a, A>
1757  for n: Nat
1758  for -x: A
1759  {List.get(a, A, List.set(a, A, xs, n, x), n) == Maybe.map(a, A, A, y => x, List.get(a, A, xs, n)) : Maybe<a, A>}
1760
1761def get_set_self(a, A, xs, n, x):
1762  match xs n:
1763    case Nil{} _:
1764      {==}
1765    case h <> t 0n:
1766      {==}
1767    case h <> t 1n+p:
1768      get_set_self(a, A, t, p, x)
1769
1770def 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}:
1771  match ys:
1772    case Nil{}:
1773      {==}
1774    case y <> t:
1775      internal_last_go_append_singleton(a, A, t, y, x)
1776
1777# The last element of xs ++ [x] is x.
1778law last_append_singleton:
1779  for -a: Quant
1780  for -A: Kind(a)
1781  for xs: List<a, A>
1782  for -x: A
1783  {List.last(a, A, List.append(a, A, xs, [x])) == Some{x} : Maybe<a, A>}
1784
1785def last_append_singleton(a, A, xs, x):
1786  match xs:
1787    case Nil{}:
1788      {==}
1789    case h <> t:
1790      %internal_last_go_append_singleton(a, A, t, h, x) : {Some{List.last.go(a, A, List.append(a, A, t, [x]), h)} == Some{_} : Maybe<a, A>}
1791      {==}
1792
1793def 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>}:
1794  match xs:
1795    case Nil{}:
1796      {==}
1797    case y <> t:
1798      internal_head_reverse_go(a, A, t, y, h <> acc)
1799
1800# The head of the reverse is the last element.
1801law head_reverse:
1802  for -a: Quant
1803  for -A: Kind(a)
1804  for xs: List<a, A>
1805  {List.head(a, A, List.reverse(a, A, xs)) == List.last(a, A, xs) : Maybe<a, A>}
1806
1807def head_reverse(a, A, xs):
1808  match xs:
1809    case Nil{}:
1810      {==}
1811    case h <> t:
1812      internal_head_reverse_go(a, A, t, h, Nil{})
1813
1814def 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>}:
1815  match xs:
1816    case Nil{}:
1817      {==}
1818    case y <> t:
1819      internal_last_reverse_go(a, A, t, y, h <> acc)
1820
1821# The last element of the reverse is the head.
1822law last_reverse:
1823  for -a: Quant
1824  for -A: Kind(a)
1825  for xs: List<a, A>
1826  {List.last(a, A, List.reverse(a, A, xs)) == List.head(a, A, xs) : Maybe<a, A>}
1827
1828def last_reverse(a, A, xs):
1829  match xs:
1830    case Nil{}:
1831      {==}
1832    case h <> t:
1833      internal_last_reverse_go(a, A, t, h, Nil{})
1834
1835# A list is empty exactly when its length is zero.
1836law is_empty_iff_length_eq_zero:
1837  for -a: Quant
1838  for -A: Kind(a)
1839  for xs: List<a, A>
1840  {List.is_empty(a, A, xs) == Nat.is_eq(List.length(a, A, xs), 0n) : Bool}
1841
1842def is_empty_iff_length_eq_zero(a, A, xs):
1843  match xs:
1844    case Nil{}:
1845      {==}
1846    case h <> t:
1847      {==}
1848
1849# An append is empty exactly when both parts are.
1850law is_empty_append:
1851  for -a: Quant
1852  for -A: Kind(a)
1853  for xs: List<a, A>
1854  for -ys: List<a, A>
1855  {List.is_empty(a, A, List.append(a, A, xs, ys)) == Bool.and(List.is_empty(a, A, xs), List.is_empty(a, A, ys)) : Bool}
1856
1857def is_empty_append(a, A, xs, ys):
1858  match xs:
1859    case Nil{}:
1860      {==}
1861    case h <> t:
1862      {==}
1863
1864def 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}:
1865  match xs:
1866    case Nil{}:
1867      {==}
1868    case y <> t:
1869      internal_is_empty_reverse_go(a, A, t, y, h <> acc)
1870
1871# The reverse is empty exactly when the list is.
1872law is_empty_reverse:
1873  for -a: Quant
1874  for -A: Kind(a)
1875  for xs: List<a, A>
1876  {List.is_empty(a, A, List.reverse(a, A, xs)) == List.is_empty(a, A, xs) : Bool}
1877
1878def is_empty_reverse(a, A, xs):
1879  match xs:
1880    case Nil{}:
1881      {==}
1882    case h <> t:
1883      internal_is_empty_reverse_go(a, A, t, h, Nil{})
1884
1885# A map is empty exactly when the list is.
1886law is_empty_map:
1887  for ~A: Type
1888  for ~B: Type
1889  for ~f: A -> B
1890  for xs: List<A>
1891  {List.is_empty(&1, B, List.map(~A, ~B, ~f, xs)) == List.is_empty(&1, A, xs) : Bool}
1892
1893def is_empty_map(A, B, f, xs):
1894  match xs:
1895    case Nil{}:
1896      {==}
1897    case h <> t:
1898      {==}
1899
1900def internal_reverse_filter_put(-A: Data, -h: A, r: List<&2, A>, b: Bool) -> {List.append(&2, A, List.reverse(&2, A, r), List.filter.put(A, h, Nil{}, b)) == List.reverse(&2, A, List.filter.put(A, h, r, b)) : List<&2, A>}:
1901  match b:
1902    case False{}:
1903      append_nil(&2, A, List.reverse(&2, A, r))
1904    case True{}:
1905      Equal.sym(List<&2, A>, List.reverse.go(&2, A, r, [h]), List.append(&2, A, List.reverse(&2, A, r), [h]), reverse_go_spec(&2, A, r, [h]))
1906
1907# Filtering commutes with reversing: filter p (reverse xs) = reverse (filter p xs).
1908law filter_reverse:
1909  for ~A: Data
1910  for ~f: A -> Bool
1911  for xs: List<&2, A>
1912  {List.filter(~A, ~f, List.reverse(&2, A, xs)) == List.reverse(&2, A, List.filter(~A, ~f, xs)) : List<&2, A>}
1913
1914def filter_reverse(A, f, xs):
1915  match xs:
1916    case Nil{}:
1917      {==}
1918    case +h <> t:
1919      +t = t
1920      %Equal.sym(List<&2, A>, List.reverse.go(&2, A, t, [h]), List.append(&2, A, List.reverse(&2, A, t), [h]), reverse_go_spec(&2, A, t, [h])) : {List.filter(~A, ~f, _) == List.reverse(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))) : List<&2, A>}
1921      %Equal.sym(List<&2, A>, List.filter(~A, ~f, List.append(&2, A, List.reverse(&2, A, t), [h])), List.append(&2, A, List.filter(~A, ~f, List.reverse(&2, A, t)), List.filter(~A, ~f, [h])), filter_append(~A, ~f, List.reverse(&2, A, t), [h])) : {_ == List.reverse(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))) : List<&2, A>}
1922      %Equal.sym(List<&2, A>, List.filter(~A, ~f, List.reverse(&2, A, t)), List.reverse(&2, A, List.filter(~A, ~f, t)), filter_reverse(~A, ~f, t)) : {List.append(&2, A, _, List.filter(~A, ~f, [h])) == List.reverse(&2, A, List.filter.put(A, h, List.filter(~A, ~f, t), f(h))) : List<&2, A>}
1923      internal_reverse_filter_put(A, h, List.filter(~A, ~f, t), f(h))
1924
1925# Folding cons from the right, starting from the empty list, rebuilds the list.
1926law foldr_cons_nil:
1927  for ~a: Quant
1928  for ~A: Kind(a)
1929  for xs: List<a, A>
1930  {List.foldr(~a, ~A, ~List<a, A>, ~(x => acc => x <> acc), xs, Nil{}) == xs : List<a, A>}
1931
1932def foldr_cons_nil(a, A, xs):
1933  match xs:
1934    case Nil{}:
1935      {==}
1936    case h <> t:
1937      %foldr_cons_nil(~a, ~A, t) : {h <> List.foldr(~a, ~A, ~List<a, A>, ~(x => acc => x <> acc), t, Nil{}) == h <> _ : List<a, A>}
1938      {==}
1939
1940def 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}:
1941  match xs:
1942    case Nil{}:
1943      {==}
1944    case h <> t:
1945      internal_foldl_reverse_go(~a, ~A, ~B, ~f, t, h <> acc, z)
1946
1947# A left fold over the reverse is a right fold with the arguments flipped.
1948law foldl_reverse:
1949  for ~a: Quant
1950  for ~A: Kind(a)
1951  for ~B: Type
1952  for ~f: B -> A -> B
1953  for xs: List<a, A>
1954  for -z: B
1955  {List.foldl(~a, ~A, ~B, ~f, List.reverse(a, A, xs), z) == List.foldr(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z) : B}
1956
1957def foldl_reverse(a, A, B, f, xs, z):
1958  internal_foldl_reverse_go(~a, ~A, ~B, ~f, xs, Nil{}, z)
1959
1960def 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}:
1961  match xs:
1962    case Nil{}:
1963      {==}
1964    case h <> t:
1965      internal_foldr_reverse_go(~a, ~A, ~B, ~f, t, h <> acc, z)
1966
1967# A right fold over the reverse is a left fold with the arguments flipped.
1968law foldr_reverse:
1969  for ~a: Quant
1970  for ~A: Kind(a)
1971  for ~B: Type
1972  for ~f: A -> B -> B
1973  for xs: List<a, A>
1974  for -z: B
1975  {List.foldr(~a, ~A, ~B, ~f, List.reverse(a, A, xs), z) == List.foldl(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z) : B}
1976
1977def foldr_reverse(a, A, B, f, xs, z):
1978  internal_foldr_reverse_go(~a, ~A, ~B, ~f, xs, Nil{}, z)
1979
1980def internal_range_go_append(+n: Nat, -ys: List<&2, Nat>, -acc: List<&2, Nat>) -> {List.range.go(n, List.append(&2, Nat, ys, acc)) == List.append(&2, Nat, List.range.go(n, ys), acc) : List<&2, Nat>}:
1981  match n:
1982    case 0n:
1983      {==}
1984    case 1n+p:
1985      internal_range_go_append(p, p <> ys, acc)
1986
1987# Range(n + 1) is range(n) followed by n.
1988law range_succ:
1989  for n: Nat
1990  {List.range(1n+n) == List.append(&2, Nat, List.range(n), [n]) : List<&2, Nat>}
1991
1992def range_succ(n):
1993  +n = n
1994  internal_range_go_append(n, Nil{}, [n])
1995
1996def internal_find_put_or(-A: Data, h: A, r: Maybe<&2, A>, -s: Maybe<&2, A>, b: Bool) -> {Maybe.or(&2, A, internal_find_put(A, h, r, b), s) == internal_find_put(A, h, Maybe.or(&2, A, r, s), b) : Maybe<&2, A>}:
1997  match b:
1998    case False{}:
1999      {==}
2000    case True{}:
2001      {==}
2002
2003# Finding in an append finds in the first part, or else in the second.
2004law find_append:
2005  for ~A: Data
2006  for ~f: A -> Bool
2007  for xs: List<&2, A>
2008  for ys: List<&2, A>
2009  {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>}
2010
2011def find_append(A, f, xs, ys):
2012  match xs:
2013    case Nil{}:
2014      {==}
2015    case +h <> t:
2016      +ys = ys
2017      +t = t
2018      %internal_find_cons(~A, ~f, h, List.append(&2, A, t, ys)) : {_ == Maybe.or(&2, A, List.find(~A, ~f, h <> t), List.find(~A, ~f, ys)) : Maybe<&2, A>}
2019      %internal_find_cons(~A, ~f, h, t) : {internal_find_put(A, h, List.find(~A, ~f, List.append(&2, A, t, ys)), f(h)) == Maybe.or(&2, A, _, List.find(~A, ~f, ys)) : Maybe<&2, A>}
2020      %Equal.sym(Maybe<&2, A>, List.find(~A, ~f, List.append(&2, A, t, ys)), Maybe.or(&2, A, List.find(~A, ~f, t), List.find(~A, ~f, ys)), find_append(~A, ~f, t, ys)) : {internal_find_put(A, h, _, f(h)) == Maybe.or(&2, A, internal_find_put(A, h, List.find(~A, ~f, t), f(h)), List.find(~A, ~f, ys)) : Maybe<&2, A>}
2021      Equal.sym(Maybe<&2, A>, Maybe.or(&2, A, internal_find_put(A, h, List.find(~A, ~f, t), f(h)), List.find(~A, ~f, ys)), internal_find_put(A, h, Maybe.or(&2, A, List.find(~A, ~f, t), List.find(~A, ~f, ys)), f(h)), internal_find_put_or(A, h, List.find(~A, ~f, t), List.find(~A, ~f, ys), f(h)))
2022
2023def 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}:
2024  match b:
2025    case False{}:
2026      {==}
2027    case True{}:
2028      {==}
2029
2030def internal_all_eq_not_any_not(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List<a, A>) -> {List.all(~a, ~A, ~f, xs) == Bool.not(List.any(~a, ~A, ~(x => Bool.not(f(x))), xs)) : Bool}:
2031  match xs:
2032    case Nil{}:
2033      {==}
2034    case h <> t:
2035      +v = f(h)
2036      %internal_all_cons_test(~a, ~A, ~f, h, t, v, {==}) : {_ == Bool.not(List.any(~a, ~A, ~(x => Bool.not(f(x))), h <> t)) : Bool}
2037      %internal_any_cons_test(~a, ~A, ~(x => Bool.not(f(x))), h, t, Bool.not(v), {==}) : {Bool.and(v, List.all(~a, ~A, ~f, t)) == Bool.not(_) : Bool}
2038      %Equal.sym(Bool, List.all(~a, ~A, ~f, t), Bool.not(List.any(~a, ~A, ~(x => Bool.not(f(x))), t)), internal_all_eq_not_any_not(~a, ~A, ~f, t)) : {Bool.and(v, _) == Bool.not(Bool.or(Bool.not(v), List.any(~a, ~A, ~(x => Bool.not(f(x))), t))) : Bool}
2039      internal_and_not_eq_not_or_not(v, List.any(~a, ~A, ~(x => Bool.not(f(x))), t))
2040
2041# All elements satisfy f exactly when no element fails it.
2042law all_eq_not_any_not:
2043  for ~a: Quant
2044  for ~A: Kind(a)
2045  for ~f: A -> Bool
2046  for xs: List<a, A>
2047  {List.all(~a, ~A, ~f, xs) == Bool.not(List.any(~a, ~A, ~(x => Bool.not(f(x))), xs)) : Bool}
2048
2049def all_eq_not_any_not(a, A, f, xs):
2050  internal_all_eq_not_any_not(~a, ~A, ~f, xs)
2051
2052def 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}:
2053  match b:
2054    case False{}:
2055      {==}
2056    case True{}:
2057      {==}
2058
2059def internal_any_eq_not_all_not(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List<a, A>) -> {List.any(~a, ~A, ~f, xs) == Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), xs)) : Bool}:
2060  match xs:
2061    case Nil{}:
2062      {==}
2063    case h <> t:
2064      +v = f(h)
2065      %internal_any_cons_test(~a, ~A, ~f, h, t, v, {==}) : {_ == Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), h <> t)) : Bool}
2066      %internal_all_cons_test(~a, ~A, ~(x => Bool.not(f(x))), h, t, Bool.not(v), {==}) : {Bool.or(v, List.any(~a, ~A, ~f, t)) == Bool.not(_) : Bool}
2067      %Equal.sym(Bool, List.any(~a, ~A, ~f, t), Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), t)), internal_any_eq_not_all_not(~a, ~A, ~f, t)) : {Bool.or(v, _) == Bool.not(Bool.and(Bool.not(v), List.all(~a, ~A, ~(x => Bool.not(f(x))), t))) : Bool}
2068      internal_or_not_eq_not_and_not(v, List.all(~a, ~A, ~(x => Bool.not(f(x))), t))
2069
2070# Some element satisfies f exactly when not all elements fail it.
2071law any_eq_not_all_not:
2072  for ~a: Quant
2073  for ~A: Kind(a)
2074  for ~f: A -> Bool
2075  for xs: List<a, A>
2076  {List.any(~a, ~A, ~f, xs) == Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), xs)) : Bool}
2077
2078def any_eq_not_all_not(a, A, f, xs):
2079  internal_any_eq_not_all_not(~a, ~A, ~f, xs)
2080
2081# A one-element list has length one.
2082law length_singleton:
2083  for -a: Quant
2084  for -A: Kind(a)
2085  for -x: A
2086  {List.length(a, A, [x]) == 1n : Nat}
2087
2088def length_singleton(a, A, x):
2089  {==}
2090
2091# Reversing a cons puts its head last: reverse (x :: xs) = reverse xs ++ [x].
2092law reverse_cons:
2093  for -a: Quant
2094  for -A: Kind(a)
2095  for -x: A
2096  for xs: List<a, A>
2097  {List.reverse(a, A, x <> xs) == List.append(a, A, List.reverse(a, A, xs), [x]) : List<a, A>}
2098
2099def reverse_cons(a, A, x, xs):
2100  reverse_go_spec(a, A, xs, [x])
2101
2102# Taking n + 1 elements of a cons keeps its head and takes n from its tail.
2103law take_succ:
2104  for -a: Quant
2105  for -A: Kind(a)
2106  for -x: A
2107  for -xs: List<a, A>
2108  for -n: Nat
2109  {List.take(a, A, x <> xs, 1n+n) == x <> List.take(a, A, xs, n) : List<a, A>}
2110
2111def take_succ(a, A, x, xs, n):
2112  {==}
2113
2114# Dropping n + 1 elements of a cons drops its head and n from its tail.
2115law drop_succ:
2116  for -a: Quant
2117  for -A: Kind(a)
2118  for -x: A
2119  for -xs: List<a, A>
2120  for -n: Nat
2121  {List.drop(a, A, x <> xs, 1n+n) == List.drop(a, A, xs, n) : List<a, A>}
2122
2123def drop_succ(a, A, x, xs, n):
2124  {==}
2125
2126# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
2127
2128# The empty list is a right identity for append: xs ++ [] = xs, reversed to rewrite toward the simple side.
2129law append_nil_sym:
2130  for -a: Quant
2131  for -A: Kind(a)
2132  for xs: List<a, A>
2133  {xs == List.append(a, A, xs, Nil{}) : List<a, A>}
2134
2135def append_nil_sym(a, A, xs):
2136  Equal.sym(List<a, A>, List.append(a, A, xs, Nil{}), xs, append_nil(a, A, xs))
2137
2138# The empty list is a left identity for append: [] ++ xs = xs, reversed to rewrite toward the simple side.
2139law nil_append_sym:
2140  for -a: Quant
2141  for -A: Kind(a)
2142  for -xs: List<a, A>
2143  {xs == List.append(a, A, Nil{}, xs) : List<a, A>}
2144
2145def nil_append_sym(a, A, xs):
2146  Equal.sym(List<a, A>, List.append(a, A, Nil{}, xs), xs, nil_append(a, A, xs))
2147
2148# Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs), reversed to rewrite toward the simple side.
2149law append_assoc_sym:
2150  for -a: Quant
2151  for -A: Kind(a)
2152  for xs: List<a, A>
2153  for -ys: List<a, A>
2154  for -zs: List<a, A>
2155  {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>}
2156
2157def append_assoc_sym(a, A, xs, ys, zs):
2158  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))
2159
2160# The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.
2161law length_append_sym:
2162  for -a: Quant
2163  for -A: Kind(a)
2164  for xs: List<a, A>
2165  for -ys: List<a, A>
2166  {Nat.add(List.length(a, A, xs), List.length(a, A, ys)) == List.length(a, A, List.append(a, A, xs, ys)) : Nat}
2167
2168def length_append_sym(a, A, xs, ys):
2169  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))
2170
2171# The reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side.
2172law reverse_go_spec_sym:
2173  for -a: Quant
2174  for -A: Kind(a)
2175  for xs: List<a, A>
2176  for -acc: List<a, A>
2177  {List.append(a, A, List.reverse(a, A, xs), acc) == List.reverse.go(a, A, xs, acc) : List<a, A>}
2178
2179def reverse_go_spec_sym(a, A, xs, acc):
2180  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))
2181
2182# Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side.
2183law reverse_append_sym:
2184  for -a: Quant
2185  for -A: Kind(a)
2186  for xs: List<a, A>
2187  for ys: List<a, A>
2188  {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>}
2189
2190def reverse_append_sym(a, A, xs, ys):
2191  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))
2192
2193# Reversing twice gives the list back, reversed to rewrite toward the simple side.
2194law reverse_reverse_sym:
2195  for -a: Quant
2196  for -A: Kind(a)
2197  for xs: List<a, A>
2198  {xs == List.reverse(a, A, List.reverse(a, A, xs)) : List<a, A>}
2199
2200def reverse_reverse_sym(a, A, xs):
2201  Equal.sym(List<a, A>, List.reverse(a, A, List.reverse(a, A, xs)), xs, reverse_reverse(a, A, xs))
2202
2203# Reversing preserves the length, reversed to rewrite toward the simple side.
2204law length_reverse_sym:
2205  for -a: Quant
2206  for -A: Kind(a)
2207  for xs: List<a, A>
2208  {List.length(a, A, xs) == List.length(a, A, List.reverse(a, A, xs)) : Nat}
2209
2210def length_reverse_sym(a, A, xs):
2211  Equal.sym(Nat, List.length(a, A, List.reverse(a, A, xs)), List.length(a, A, xs), length_reverse(a, A, xs))
2212
2213# A right fold over an append folds the first part onto the fold of the second, reversed to rewrite toward the simple side.
2214law foldr_append_sym:
2215  for ~a: Quant
2216  for ~A: Kind(a)
2217  for ~B: Type
2218  for ~f: A -> B -> B
2219  for xs: List<a, A>
2220  for -ys: List<a, A>
2221  for -z: B
2222  {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}
2223
2224def foldr_append_sym(a, A, B, f, xs, ys, z):
2225  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))
2226
2227# Taking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side.
2228law take_append_drop_sym:
2229  for -a: Quant
2230  for -A: Kind(a)
2231  for xs: List<a, A>
2232  for n: Nat
2233  {xs == List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) : List<a, A>}
2234
2235def take_append_drop_sym(a, A, xs, n):
2236  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))
2237
2238# Mapping preserves the length, reversed to rewrite toward the simple side.
2239law length_map_sym:
2240  for ~A: Type
2241  for ~B: Type
2242  for ~f: A -> B
2243  for xs: List<A>
2244  {List.length(&1, A, xs) == List.length(&1, B, List.map(~A, ~B, ~f, xs)) : Nat}
2245
2246def length_map_sym(A, B, f, xs):
2247  Equal.sym(Nat, List.length(&1, B, List.map(~A, ~B, ~f, xs)), List.length(&1, A, xs), length_map(~A, ~B, ~f, xs))
2248
2249# Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side.
2250law map_append_sym:
2251  for ~A: Type
2252  for ~B: Type
2253  for ~f: A -> B
2254  for xs: List<A>
2255  for -ys: List<A>
2256  {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>}
2257
2258def map_append_sym(A, B, f, xs, ys):
2259  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))
2260
2261# Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs, reversed to rewrite toward the simple side.
2262law map_map_sym:
2263  for ~A: Type
2264  for ~B: Type
2265  for ~C: Type
2266  for ~f: A -> B
2267  for ~g: B -> C
2268  for xs: List<A>
2269  {List.map(~A, ~C, ~(x => g(f(x))), xs) == List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) : List<C>}
2270
2271def map_map_sym(A, B, C, f, g, xs):
2272  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))
2273
2274# Taking zero elements gives the empty list, reversed to rewrite toward the simple side.
2275law take_zero_sym:
2276  for -a: Quant
2277  for -A: Kind(a)
2278  for xs: List<a, A>
2279  {Nil{} == List.take(a, A, xs, 0n) : List<a, A>}
2280
2281def take_zero_sym(a, A, xs):
2282  Equal.sym(List<a, A>, List.take(a, A, xs, 0n), Nil{}, take_zero(a, A, xs))
2283
2284# Dropping zero elements gives the list back, reversed to rewrite toward the simple side.
2285law drop_zero_sym:
2286  for -a: Quant
2287  for -A: Kind(a)
2288  for xs: List<a, A>
2289  {xs == List.drop(a, A, xs, 0n) : List<a, A>}
2290
2291def drop_zero_sym(a, A, xs):
2292  Equal.sym(List<a, A>, List.drop(a, A, xs, 0n), xs, drop_zero(a, A, xs))
2293
2294# Taking from the empty list gives the empty list, reversed to rewrite toward the simple side.
2295law take_nil_sym:
2296  for -a: Quant
2297  for -A: Kind(a)
2298  for -n: Nat
2299  {Nil{} == List.take(a, A, Nil{}, n) : List<a, A>}
2300
2301def take_nil_sym(a, A, n):
2302  Equal.sym(List<a, A>, List.take(a, A, Nil{}, n), Nil{}, take_nil(a, A, n))
2303
2304# Dropping from the empty list gives the empty list, reversed to rewrite toward the simple side.
2305law drop_nil_sym:
2306  for -a: Quant
2307  for -A: Kind(a)
2308  for -n: Nat
2309  {Nil{} == List.drop(a, A, Nil{}, n) : List<a, A>}
2310
2311def drop_nil_sym(a, A, n):
2312  Equal.sym(List<a, A>, List.drop(a, A, Nil{}, n), Nil{}, drop_nil(a, A, n))
2313
2314# Taking n elements leaves min(n, length) of them, reversed to rewrite toward the simple side.
2315law length_take_sym:
2316  for -a: Quant
2317  for -A: Kind(a)
2318  for xs: List<a, A>
2319  for n: Nat
2320  {Nat.min(n, List.length(a, A, xs)) == List.length(a, A, List.take(a, A, xs, n)) : Nat}
2321
2322def length_take_sym(a, A, xs, n):
2323  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))
2324
2325# Dropping n elements leaves length - n of them, reversed to rewrite toward the simple side.
2326law length_drop_sym:
2327  for -a: Quant
2328  for -A: Kind(a)
2329  for xs: List<a, A>
2330  for n: Nat
2331  {Nat.sub(List.length(a, A, xs), n) == List.length(a, A, List.drop(a, A, xs, n)) : Nat}
2332
2333def length_drop_sym(a, A, xs, n):
2334  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))
2335
2336# Taking as many elements as the list has gives the list back, reversed to rewrite toward the simple side.
2337law take_length_sym:
2338  for -A: Data
2339  for +xs: List<&2, A>
2340  {xs == List.take(&2, A, xs, List.length(&2, A, xs)) : List<&2, A>}
2341
2342def take_length_sym(A, xs):
2343  Equal.sym(List<&2, A>, List.take(&2, A, xs, List.length(&2, A, xs)), xs, take_length(A, xs))
2344
2345# Dropping as many elements as the list has gives the empty list, reversed to rewrite toward the simple side.
2346law drop_length_sym:
2347  for -A: Data
2348  for +xs: List<&2, A>
2349  {Nil{} == List.drop(&2, A, xs, List.length(&2, A, xs)) : List<&2, A>}
2350
2351def drop_length_sym(A, xs):
2352  Equal.sym(List<&2, A>, List.drop(&2, A, xs, List.length(&2, A, xs)), Nil{}, drop_length(A, xs))
2353
2354# Taking m from the first n is taking min(n, m), reversed to rewrite toward the simple side.
2355law take_take_sym:
2356  for -a: Quant
2357  for -A: Kind(a)
2358  for xs: List<a, A>
2359  for n: Nat
2360  for m: Nat
2361  {List.take(a, A, xs, Nat.min(n, m)) == List.take(a, A, List.take(a, A, xs, n), m) : List<a, A>}
2362
2363def take_take_sym(a, A, xs, n, m):
2364  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))
2365
2366# Dropping m after dropping n is dropping n + m, reversed to rewrite toward the simple side.
2367law drop_drop_sym:
2368  for -a: Quant
2369  for -A: Kind(a)
2370  for xs: List<a, A>
2371  for n: Nat
2372  for -m: Nat
2373  {List.drop(a, A, xs, Nat.add(n, m)) == List.drop(a, A, List.drop(a, A, xs, n), m) : List<a, A>}
2374
2375def drop_drop_sym(a, A, xs, n, m):
2376  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))
2377
2378# Reversing the empty list gives the empty list, reversed to rewrite toward the simple side.
2379law reverse_nil_sym:
2380  for -a: Quant
2381  for -A: Kind(a)
2382  {Nil{} == List.reverse(a, A, Nil{}) : List<a, A>}
2383
2384def reverse_nil_sym(a, A):
2385  Equal.sym(List<a, A>, List.reverse(a, A, Nil{}), Nil{}, reverse_nil(a, A))
2386
2387# Reversing a one-element list gives it back, reversed to rewrite toward the simple side.
2388law reverse_singleton_sym:
2389  for -a: Quant
2390  for -A: Kind(a)
2391  for -x: A
2392  {[x] == List.reverse(a, A, [x]) : List<a, A>}
2393
2394def reverse_singleton_sym(a, A, x):
2395  Equal.sym(List<a, A>, List.reverse(a, A, [x]), [x], reverse_singleton(a, A, x))
2396
2397# Replicating x n times gives a list of length n, reversed to rewrite toward the simple side.
2398law length_replicate_sym:
2399  for -A: Data
2400  for n: Nat
2401  for -x: A
2402  {n == List.length(&2, A, List.replicate(A, n, x)) : Nat}
2403
2404def length_replicate_sym(A, n, x):
2405  Equal.sym(Nat, List.length(&2, A, List.replicate(A, n, x)), n, length_replicate(A, n, x))
2406
2407# Range(n) has length n, reversed to rewrite toward the simple side.
2408law length_range_sym:
2409  for n: Nat
2410  {n == List.length(&2, Nat, List.range(n)) : Nat}
2411
2412def length_range_sym(n):
2413  Equal.sym(Nat, List.length(&2, Nat, List.range(n)), n, length_range(n))
2414
2415# A zip is as long as the shorter of the two lists, reversed to rewrite toward the simple side.
2416law length_zip_sym:
2417  for -a: Quant
2418  for -A: Kind(a)
2419  for xs: List<a, A>
2420  for ys: List<a, A>
2421  {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}
2422
2423def length_zip_sym(a, A, xs, ys):
2424  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))
2425
2426# Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys), reversed to rewrite toward the simple side.
2427law append_cons_sym:
2428  for -a: Quant
2429  for -A: Kind(a)
2430  for -x: A
2431  for -xs: List<a, A>
2432  for -ys: List<a, A>
2433  {x <> List.append(a, A, xs, ys) == List.append(a, A, x <> xs, ys) : List<a, A>}
2434
2435def append_cons_sym(a, A, x, xs, ys):
2436  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))
2437
2438# The empty list has length zero, reversed to rewrite toward the simple side.
2439law length_nil_sym:
2440  for -a: Quant
2441  for -A: Kind(a)
2442  {0n == List.length(a, A, Nil{}) : Nat}
2443
2444def length_nil_sym(a, A):
2445  Equal.sym(Nat, List.length(a, A, Nil{}), 0n, length_nil(a, A))
2446
2447# A cons is one longer than its tail, reversed to rewrite toward the simple side.
2448law length_cons_sym:
2449  for -a: Quant
2450  for -A: Kind(a)
2451  for -x: A
2452  for -xs: List<a, A>
2453  {1n+List.length(a, A, xs) == List.length(a, A, x <> xs) : Nat}
2454
2455def length_cons_sym(a, A, x, xs):
2456  Equal.sym(Nat, List.length(a, A, x <> xs), 1n+List.length(a, A, xs), length_cons(a, A, x, xs))
2457
2458# Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss, reversed to rewrite toward the simple side.
2459law concat_append_sym:
2460  for -a: Quant
2461  for -A: Kind(a)
2462  for xss: List<a, List<a, A>>
2463  for -yss: List<a, List<a, A>>
2464  {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>}
2465
2466def concat_append_sym(a, A, xss, yss):
2467  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))
2468
2469# A left fold over an append folds the second part from the fold of the first, reversed to rewrite toward the simple side.
2470law foldl_append_sym:
2471  for ~a: Quant
2472  for ~A: Kind(a)
2473  for ~B: Type
2474  for ~f: B -> A -> B
2475  for xs: List<a, A>
2476  for -ys: List<a, A>
2477  for -z: B
2478  {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}
2479
2480def foldl_append_sym(a, A, B, f, xs, ys, z):
2481  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))
2482
2483# Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs), reversed to rewrite toward the simple side.
2484law map_reverse_sym:
2485  for ~A: Type
2486  for ~B: Type
2487  for ~f: A -> B
2488  for xs: List<A>
2489  {List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) : List<B>}
2490
2491def map_reverse_sym(A, B, f, xs):
2492  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))
2493
2494# All over an append is all over each part, joined by and, reversed to rewrite toward the simple side.
2495law all_append_sym:
2496  for ~a: Quant
2497  for ~A: Kind(a)
2498  for ~f: A -> Bool
2499  for xs: List<a, A>
2500  for -ys: List<a, A>
2501  {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}
2502
2503def all_append_sym(a, A, f, xs, ys):
2504  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))
2505
2506# Any over an append is any over each part, joined by or, reversed to rewrite toward the simple side.
2507law any_append_sym:
2508  for ~a: Quant
2509  for ~A: Kind(a)
2510  for ~f: A -> Bool
2511  for xs: List<a, A>
2512  for -ys: List<a, A>
2513  {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}
2514
2515def any_append_sym(a, A, f, xs, ys):
2516  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))
2517
2518# Filtering an append filters each part, reversed to rewrite toward the simple side.
2519law filter_append_sym:
2520  for ~A: Data
2521  for ~f: A -> Bool
2522  for xs: List<&2, A>
2523  for ys: List<&2, A>
2524  {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>}
2525
2526def filter_append_sym(A, f, xs, ys):
2527  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))
2528
2529# An append contains x iff either part does, reversed to rewrite toward the simple side.
2530law contains_append_sym:
2531  for ~A: Data
2532  for ~eq: A -> A -> Bool
2533  for xs: List<&2, A>
2534  for -ys: List<&2, A>
2535  for +x: A
2536  {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}
2537
2538def contains_append_sym(A, eq, xs, ys, x):
2539  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))
2540
2541# Filtering never makes a list longer, reversed to rewrite toward the simple side.
2542law length_filter_le_sym:
2543  for ~A: Data
2544  for ~f: A -> Bool
2545  for xs: List<&2, A>
2546  {True{} == Nat.is_le(List.length(&2, A, List.filter(~A, ~f, xs)), List.length(&2, A, xs)) : Bool}
2547
2548def length_filter_le_sym(A, f, xs):
2549  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))
2550
2551# Taking the length of the first part of an append gives the first part back, reversed to rewrite toward the simple side.
2552law take_left_sym:
2553  for -a: Quant
2554  for -A: Kind(a)
2555  for xs: List<a, A>
2556  for ys: List<a, A>
2557  {xs == List.take(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) : List<a, A>}
2558
2559def take_left_sym(a, A, xs, ys):
2560  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))
2561
2562# Dropping the length of the first part of an append gives the second part, reversed to rewrite toward the simple side.
2563law drop_left_sym:
2564  for -a: Quant
2565  for -A: Kind(a)
2566  for xs: List<a, A>
2567  for ys: List<a, A>
2568  {ys == List.drop(a, A, List.append(a, A, xs, ys), List.length(a, A, xs)) : List<a, A>}
2569
2570def drop_left_sym(a, A, xs, ys):
2571  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))
2572
2573# 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.
2574law take_append_sym:
2575  for -a: Quant
2576  for -A: Kind(a)
2577  for xs: List<a, A>
2578  for -ys: List<a, A>
2579  for -n: Nat
2580  {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>}
2581
2582def take_append_sym(a, A, xs, ys, n):
2583  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))
2584
2585# Dropping past the first part of an append drops the rest from the second part, reversed to rewrite toward the simple side.
2586law drop_append_sym:
2587  for -a: Quant
2588  for -A: Kind(a)
2589  for xs: List<a, A>
2590  for -ys: List<a, A>
2591  for -n: Nat
2592  {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>}
2593
2594def drop_append_sym(a, A, xs, ys, n):
2595  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))
2596
2597# Taking at most the length of the first part of an append only sees the first part, reversed to rewrite toward the simple side.
2598law take_append_of_le_length_sym:
2599  for -a: Quant
2600  for -A: Kind(a)
2601  for xs: List<a, A>
2602  for ys: List<a, A>
2603  for n: Nat
2604  for h: MNat.le(n, List.length(a, A, xs))
2605  {List.take(a, A, xs, n) == List.take(a, A, List.append(a, A, xs, ys), n) : List<a, A>}
2606
2607def take_append_of_le_length_sym(a, A, xs, ys, n, h):
2608  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))
2609
2610# 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.
2611law drop_append_of_le_length_sym:
2612  for -a: Quant
2613  for -A: Kind(a)
2614  for xs: List<a, A>
2615  for ys: List<a, A>
2616  for n: Nat
2617  for h: MNat.le(n, List.length(a, A, xs))
2618  {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>}
2619
2620def drop_append_of_le_length_sym(a, A, xs, ys, n, h):
2621  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))
2622
2623# Mapping commutes with taking: map f (take n xs) = take n (map f xs), reversed to rewrite toward the simple side.
2624law map_take_sym:
2625  for ~A: Type
2626  for ~B: Type
2627  for ~f: A -> B
2628  for xs: List<A>
2629  for n: Nat
2630  {List.take(&1, B, List.map(~A, ~B, ~f, xs), n) == List.map(~A, ~B, ~f, List.take(&1, A, xs, n)) : List<B>}
2631
2632def map_take_sym(A, B, f, xs, n):
2633  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))
2634
2635# Mapping commutes with dropping: map f (drop n xs) = drop n (map f xs), reversed to rewrite toward the simple side.
2636law map_drop_sym:
2637  for ~A: Type
2638  for ~B: Type
2639  for ~f: A -> B
2640  for xs: List<A>
2641  for n: Nat
2642  {List.drop(&1, B, List.map(~A, ~B, ~f, xs), n) == List.map(~A, ~B, ~f, List.drop(&1, A, xs, n)) : List<B>}
2643
2644def map_drop_sym(A, B, f, xs, n):
2645  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))
2646
2647# Taking m from n copies of x gives min(m, n) copies of x, reversed to rewrite toward the simple side.
2648law take_replicate_sym:
2649  for -A: Data
2650  for n: Nat
2651  for m: Nat
2652  for -x: A
2653  {List.replicate(A, Nat.min(m, n), x) == List.take(&2, A, List.replicate(A, n, x), m) : List<&2, A>}
2654
2655def take_replicate_sym(A, n, m, x):
2656  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))
2657
2658# Dropping m from n copies of x gives n - m copies of x, reversed to rewrite toward the simple side.
2659law drop_replicate_sym:
2660  for -A: Data
2661  for n: Nat
2662  for m: Nat
2663  for -x: A
2664  {List.replicate(A, Nat.sub(n, m), x) == List.drop(&2, A, List.replicate(A, n, x), m) : List<&2, A>}
2665
2666def drop_replicate_sym(A, n, m, x):
2667  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))
2668
2669# The tail is one shorter than the list, or empty: length (tail xs) = length xs - 1, reversed to rewrite toward the simple side.
2670law length_tail_sym:
2671  for -a: Quant
2672  for -A: Kind(a)
2673  for xs: List<a, A>
2674  {Nat.sub(List.length(a, A, xs), 1n) == List.length(a, A, List.tail(a, A, xs)) : Nat}
2675
2676def length_tail_sym(a, A, xs):
2677  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))
2678
2679# Mapping the identity gives the list back, reversed to rewrite toward the simple side.
2680law map_id_sym:
2681  for ~A: Type
2682  for xs: List<A>
2683  {xs == List.map(~A, ~A, ~(x => x), xs) : List<A>}
2684
2685def map_id_sym(A, xs):
2686  Equal.sym(List<A>, List.map(~A, ~A, ~(x => x), xs), xs, map_id(~A, xs))
2687
2688# 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.
2689law foldr_map_sym:
2690  for ~A: Type
2691  for ~B: Type
2692  for ~C: Type
2693  for ~f: A -> B
2694  for ~g: B -> C -> C
2695  for xs: List<A>
2696  for -z: C
2697  {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}
2698
2699def foldr_map_sym(A, B, C, f, g, xs, z):
2700  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))
2701
2702# 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.
2703law foldl_map_sym:
2704  for ~A: Type
2705  for ~B: Type
2706  for ~C: Type
2707  for ~f: A -> B
2708  for ~g: C -> B -> C
2709  for xs: List<A>
2710  for -z: C
2711  {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}
2712
2713def foldl_map_sym(A, B, C, f, g, xs, z):
2714  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))
2715
2716# Replicating m + n times appends m copies to n copies, reversed to rewrite toward the simple side.
2717law replicate_add_sym:
2718  for -A: Data
2719  for m: Nat
2720  for -n: Nat
2721  for -x: A
2722  {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>}
2723
2724def replicate_add_sym(A, m, n, x):
2725  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))
2726
2727# Reversing n copies of x gives them back, reversed to rewrite toward the simple side.
2728law reverse_replicate_sym:
2729  for -A: Data
2730  for n: Nat
2731  for -x: A
2732  {List.replicate(A, n, x) == List.reverse(&2, A, List.replicate(A, n, x)) : List<&2, A>}
2733
2734def reverse_replicate_sym(A, n, x):
2735  Equal.sym(List<&2, A>, List.reverse(&2, A, List.replicate(A, n, x)), List.replicate(A, n, x), reverse_replicate(A, n, x))
2736
2737# Filtering with an always-true predicate gives the list back, reversed to rewrite toward the simple side.
2738law filter_true_sym:
2739  for ~A: Data
2740  for xs: List<&2, A>
2741  {xs == List.filter(~A, ~(x => True{}), xs) : List<&2, A>}
2742
2743def filter_true_sym(A, xs):
2744  Equal.sym(List<&2, A>, List.filter(~A, ~(x => True{}), xs), xs, filter_true(~A, xs))
2745
2746# Filtering with an always-false predicate gives the empty list, reversed to rewrite toward the simple side.
2747law filter_false_sym:
2748  for ~A: Data
2749  for xs: List<&2, A>
2750  {Nil{} == List.filter(~A, ~(x => False{}), xs) : List<&2, A>}
2751
2752def filter_false_sym(A, xs):
2753  Equal.sym(List<&2, A>, List.filter(~A, ~(x => False{}), xs), Nil{}, filter_false(~A, xs))
2754
2755# Filtering twice is filtering by both predicates: filter p (filter q xs) = filter (p and q) xs, reversed to rewrite toward the simple side.
2756law filter_filter_sym:
2757  for ~A: Data
2758  for ~p: A -> Bool
2759  for ~q: A -> Bool
2760  for xs: List<&2, A>
2761  {List.filter(~A, ~(+x => Bool.and(p(x), q(x))), xs) == List.filter(~A, ~p, List.filter(~A, ~q, xs)) : List<&2, A>}
2762
2763def filter_filter_sym(A, p, q, xs):
2764  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))
2765
2766# 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.
2767law all_filter_sym:
2768  for ~A: Data
2769  for ~p: A -> Bool
2770  for ~q: A -> Bool
2771  for xs: List<&2, A>
2772  {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}
2773
2774def all_filter_sym(A, p, q, xs):
2775  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))
2776
2777# 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.
2778law any_filter_sym:
2779  for ~A: Data
2780  for ~p: A -> Bool
2781  for ~q: A -> Bool
2782  for xs: List<&2, A>
2783  {List.any(~&2, ~A, ~(+x => Bool.and(p(x), q(x))), xs) == List.any(~&2, ~A, ~q, List.filter(~A, ~p, xs)) : Bool}
2784
2785def any_filter_sym(A, p, q, xs):
2786  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))
2787
2788# All over a map checks the composed predicate: all p (map f xs) = all (p . f) xs, reversed to rewrite toward the simple side.
2789law all_map_sym:
2790  for ~A: Type
2791  for ~B: Type
2792  for ~f: A -> B
2793  for ~p: B -> Bool
2794  for xs: List<A>
2795  {List.all(~&1, ~A, ~(x => p(f(x))), xs) == List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) : Bool}
2796
2797def all_map_sym(A, B, f, p, xs):
2798  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))
2799
2800# Any over a map checks the composed predicate: any p (map f xs) = any (p . f) xs, reversed to rewrite toward the simple side.
2801law any_map_sym:
2802  for ~A: Type
2803  for ~B: Type
2804  for ~f: A -> B
2805  for ~p: B -> Bool
2806  for xs: List<A>
2807  {List.any(~&1, ~A, ~(x => p(f(x))), xs) == List.any(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) : Bool}
2808
2809def any_map_sym(A, B, f, p, xs):
2810  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))
2811
2812# Reversing does not change whether all elements satisfy a predicate, reversed to rewrite toward the simple side.
2813law all_reverse_sym:
2814  for ~a: Quant
2815  for ~A: Kind(a)
2816  for ~f: A -> Bool
2817  for xs: List<a, A>
2818  {List.all(~a, ~A, ~f, xs) == List.all(~a, ~A, ~f, List.reverse(a, A, xs)) : Bool}
2819
2820def all_reverse_sym(a, A, f, xs):
2821  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))
2822
2823# Reversing does not change whether some element satisfies a predicate, reversed to rewrite toward the simple side.
2824law any_reverse_sym:
2825  for ~a: Quant
2826  for ~A: Kind(a)
2827  for ~f: A -> Bool
2828  for xs: List<a, A>
2829  {List.any(~a, ~A, ~f, xs) == List.any(~a, ~A, ~f, List.reverse(a, A, xs)) : Bool}
2830
2831def any_reverse_sym(a, A, f, xs):
2832  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))
2833
2834# Reversing does not change whether a list contains x, reversed to rewrite toward the simple side.
2835law contains_reverse_sym:
2836  for ~A: Data
2837  for ~eq: A -> A -> Bool
2838  for xs: List<&2, A>
2839  for +x: A
2840  {List.contains(~A, ~eq, xs, x) == List.contains(~A, ~eq, List.reverse(&2, A, xs), x) : Bool}
2841
2842def contains_reverse_sym(A, eq, xs, x):
2843  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))
2844
2845# Zipping the empty list with anything gives the empty list, reversed to rewrite toward the simple side.
2846law zip_nil_left_sym:
2847  for -a: Quant
2848  for -A: Kind(a)
2849  for -b: Quant
2850  for -B: Kind(b)
2851  for -ys: List<b, B>
2852  {Nil{} == List.zip(a, A, b, B, Nil{}, ys) : List<&1, A & B>}
2853
2854def zip_nil_left_sym(a, A, b, B, ys):
2855  Equal.sym(List<&1, A & B>, List.zip(a, A, b, B, Nil{}, ys), Nil{}, zip_nil_left(a, A, b, B, ys))
2856
2857# Zipping anything with the empty list gives the empty list, reversed to rewrite toward the simple side.
2858law zip_nil_right_sym:
2859  for -a: Quant
2860  for -A: Kind(a)
2861  for -b: Quant
2862  for -B: Kind(b)
2863  for xs: List<a, A>
2864  {Nil{} == List.zip(a, A, b, B, xs, Nil{}) : List<&1, A & B>}
2865
2866def zip_nil_right_sym(a, A, b, B, xs):
2867  Equal.sym(List<&1, A & B>, List.zip(a, A, b, B, xs, Nil{}), Nil{}, zip_nil_right(a, A, b, B, xs))
2868
2869# The head of a cons is its first element, reversed to rewrite toward the simple side.
2870law head_cons_sym:
2871  for -a: Quant
2872  for -A: Kind(a)
2873  for -x: A
2874  for -xs: List<a, A>
2875  {Some{x} == List.head(a, A, x <> xs) : Maybe<a, A>}
2876
2877def head_cons_sym(a, A, x, xs):
2878  Equal.sym(Maybe<a, A>, List.head(a, A, x <> xs), Some{x}, head_cons(a, A, x, xs))
2879
2880# The head of an append is the head of the first part, or else of the second, reversed to rewrite toward the simple side.
2881law head_append_sym:
2882  for -a: Quant
2883  for -A: Kind(a)
2884  for xs: List<a, A>
2885  for -ys: List<a, A>
2886  {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>}
2887
2888def head_append_sym(a, A, xs, ys):
2889  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))
2890
2891# The head of a map is the mapped head, reversed to rewrite toward the simple side.
2892law head_map_sym:
2893  for ~A: Type
2894  for ~B: Type
2895  for ~f: A -> B
2896  for xs: List<A>
2897  {Maybe.map(&1, A, B, f, List.head(&1, A, xs)) == List.head(&1, B, List.map(~A, ~B, ~f, xs)) : Maybe<&1, B>}
2898
2899def head_map_sym(A, B, f, xs):
2900  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))
2901
2902# The tail of a map is the map of the tail, reversed to rewrite toward the simple side.
2903law tail_map_sym:
2904  for ~A: Type
2905  for ~B: Type
2906  for ~f: A -> B
2907  for xs: List<A>
2908  {List.map(~A, ~B, ~f, List.tail(&1, A, xs)) == List.tail(&1, B, List.map(~A, ~B, ~f, xs)) : List<B>}
2909
2910def tail_map_sym(A, B, f, xs):
2911  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))
2912
2913# The element at index zero of a cons is its head, reversed to rewrite toward the simple side.
2914law get_cons_zero_sym:
2915  for -a: Quant
2916  for -A: Kind(a)
2917  for -x: A
2918  for -xs: List<a, A>
2919  {Some{x} == List.get(a, A, x <> xs, 0n) : Maybe<a, A>}
2920
2921def get_cons_zero_sym(a, A, x, xs):
2922  Equal.sym(Maybe<a, A>, List.get(a, A, x <> xs, 0n), Some{x}, get_cons_zero(a, A, x, xs))
2923
2924# 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.
2925law get_cons_succ_sym:
2926  for -a: Quant
2927  for -A: Kind(a)
2928  for -x: A
2929  for -xs: List<a, A>
2930  for -n: Nat
2931  {List.get(a, A, xs, n) == List.get(a, A, x <> xs, 1n+n) : Maybe<a, A>}
2932
2933def get_cons_succ_sym(a, A, x, xs, n):
2934  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))
2935
2936# Indexing a map is mapping the indexed element, reversed to rewrite toward the simple side.
2937law get_map_sym:
2938  for ~A: Type
2939  for ~B: Type
2940  for ~f: A -> B
2941  for xs: List<A>
2942  for n: Nat
2943  {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>}
2944
2945def get_map_sym(A, B, f, xs, n):
2946  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))
2947
2948# Setting an element does not change the length, reversed to rewrite toward the simple side.
2949law length_set_sym:
2950  for -a: Quant
2951  for -A: Kind(a)
2952  for xs: List<a, A>
2953  for n: Nat
2954  for -x: A
2955  {List.length(a, A, xs) == List.length(a, A, List.set(a, A, xs, n, x)) : Nat}
2956
2957def length_set_sym(a, A, xs, n, x):
2958  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))
2959
2960# Reading the index just set gives the new value wherever the index is in range, reversed to rewrite toward the simple side.
2961law get_set_self_sym:
2962  for -a: Quant
2963  for -A: Kind(a)
2964  for xs: List<a, A>
2965  for n: Nat
2966  for -x: A
2967  {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>}
2968
2969def get_set_self_sym(a, A, xs, n, x):
2970  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))
2971
2972# The last element of xs ++ [x] is x, reversed to rewrite toward the simple side.
2973law last_append_singleton_sym:
2974  for -a: Quant
2975  for -A: Kind(a)
2976  for xs: List<a, A>
2977  for -x: A
2978  {Some{x} == List.last(a, A, List.append(a, A, xs, [x])) : Maybe<a, A>}
2979
2980def last_append_singleton_sym(a, A, xs, x):
2981  Equal.sym(Maybe<a, A>, List.last(a, A, List.append(a, A, xs, [x])), Some{x}, last_append_singleton(a, A, xs, x))
2982
2983# The head of the reverse is the last element, reversed to rewrite toward the simple side.
2984law head_reverse_sym:
2985  for -a: Quant
2986  for -A: Kind(a)
2987  for xs: List<a, A>
2988  {List.last(a, A, xs) == List.head(a, A, List.reverse(a, A, xs)) : Maybe<a, A>}
2989
2990def head_reverse_sym(a, A, xs):
2991  Equal.sym(Maybe<a, A>, List.head(a, A, List.reverse(a, A, xs)), List.last(a, A, xs), head_reverse(a, A, xs))
2992
2993# The last element of the reverse is the head, reversed to rewrite toward the simple side.
2994law last_reverse_sym:
2995  for -a: Quant
2996  for -A: Kind(a)
2997  for xs: List<a, A>
2998  {List.head(a, A, xs) == List.last(a, A, List.reverse(a, A, xs)) : Maybe<a, A>}
2999
3000def last_reverse_sym(a, A, xs):
3001  Equal.sym(Maybe<a, A>, List.last(a, A, List.reverse(a, A, xs)), List.head(a, A, xs), last_reverse(a, A, xs))
3002
3003# A list is empty exactly when its length is zero, reversed to rewrite toward the simple side.
3004law is_empty_iff_length_eq_zero_sym:
3005  for -a: Quant
3006  for -A: Kind(a)
3007  for xs: List<a, A>
3008  {Nat.is_eq(List.length(a, A, xs), 0n) == List.is_empty(a, A, xs) : Bool}
3009
3010def is_empty_iff_length_eq_zero_sym(a, A, xs):
3011  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))
3012
3013# An append is empty exactly when both parts are, reversed to rewrite toward the simple side.
3014law is_empty_append_sym:
3015  for -a: Quant
3016  for -A: Kind(a)
3017  for xs: List<a, A>
3018  for -ys: List<a, A>
3019  {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}
3020
3021def is_empty_append_sym(a, A, xs, ys):
3022  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))
3023
3024# The reverse is empty exactly when the list is, reversed to rewrite toward the simple side.
3025law is_empty_reverse_sym:
3026  for -a: Quant
3027  for -A: Kind(a)
3028  for xs: List<a, A>
3029  {List.is_empty(a, A, xs) == List.is_empty(a, A, List.reverse(a, A, xs)) : Bool}
3030
3031def is_empty_reverse_sym(a, A, xs):
3032  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))
3033
3034# A map is empty exactly when the list is, reversed to rewrite toward the simple side.
3035law is_empty_map_sym:
3036  for ~A: Type
3037  for ~B: Type
3038  for ~f: A -> B
3039  for xs: List<A>
3040  {List.is_empty(&1, A, xs) == List.is_empty(&1, B, List.map(~A, ~B, ~f, xs)) : Bool}
3041
3042def is_empty_map_sym(A, B, f, xs):
3043  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))
3044
3045# Filtering commutes with reversing: filter p (reverse xs) = reverse (filter p xs), reversed to rewrite toward the simple side.
3046law filter_reverse_sym:
3047  for ~A: Data
3048  for ~f: A -> Bool
3049  for xs: List<&2, A>
3050  {List.reverse(&2, A, List.filter(~A, ~f, xs)) == List.filter(~A, ~f, List.reverse(&2, A, xs)) : List<&2, A>}
3051
3052def filter_reverse_sym(A, f, xs):
3053  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))
3054
3055# Folding cons from the right, starting from the empty list, rebuilds the list, reversed to rewrite toward the simple side.
3056law foldr_cons_nil_sym:
3057  for ~a: Quant
3058  for ~A: Kind(a)
3059  for xs: List<a, A>
3060  {xs == List.foldr(~a, ~A, ~List<a, A>, ~(x => acc => x <> acc), xs, Nil{}) : List<a, A>}
3061
3062def foldr_cons_nil_sym(a, A, xs):
3063  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))
3064
3065# A left fold over the reverse is a right fold with the arguments flipped, reversed to rewrite toward the simple side.
3066law foldl_reverse_sym:
3067  for ~a: Quant
3068  for ~A: Kind(a)
3069  for ~B: Type
3070  for ~f: B -> A -> B
3071  for xs: List<a, A>
3072  for -z: B
3073  {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}
3074
3075def foldl_reverse_sym(a, A, B, f, xs, z):
3076  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))
3077
3078# A right fold over the reverse is a left fold with the arguments flipped, reversed to rewrite toward the simple side.
3079law foldr_reverse_sym:
3080  for ~a: Quant
3081  for ~A: Kind(a)
3082  for ~B: Type
3083  for ~f: A -> B -> B
3084  for xs: List<a, A>
3085  for -z: B
3086  {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}
3087
3088def foldr_reverse_sym(a, A, B, f, xs, z):
3089  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))
3090
3091# Range(n + 1) is range(n) followed by n, reversed to rewrite toward the simple side.
3092law range_succ_sym:
3093  for n: Nat
3094  {List.append(&2, Nat, List.range(n), [n]) == List.range(1n+n) : List<&2, Nat>}
3095
3096def range_succ_sym(n):
3097  Equal.sym(List<&2, Nat>, List.range(1n+n), List.append(&2, Nat, List.range(n), [n]), range_succ(n))
3098
3099# Finding in an append finds in the first part, or else in the second, reversed to rewrite toward the simple side.
3100law find_append_sym:
3101  for ~A: Data
3102  for ~f: A -> Bool
3103  for xs: List<&2, A>
3104  for ys: List<&2, A>
3105  {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>}
3106
3107def find_append_sym(A, f, xs, ys):
3108  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))
3109
3110# All elements satisfy f exactly when no element fails it, reversed to rewrite toward the simple side.
3111law all_eq_not_any_not_sym:
3112  for ~a: Quant
3113  for ~A: Kind(a)
3114  for ~f: A -> Bool
3115  for xs: List<a, A>
3116  {Bool.not(List.any(~a, ~A, ~(x => Bool.not(f(x))), xs)) == List.all(~a, ~A, ~f, xs) : Bool}
3117
3118def all_eq_not_any_not_sym(a, A, f, xs):
3119  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))
3120
3121# Some element satisfies f exactly when not all elements fail it, reversed to rewrite toward the simple side.
3122law any_eq_not_all_not_sym:
3123  for ~a: Quant
3124  for ~A: Kind(a)
3125  for ~f: A -> Bool
3126  for xs: List<a, A>
3127  {Bool.not(List.all(~a, ~A, ~(x => Bool.not(f(x))), xs)) == List.any(~a, ~A, ~f, xs) : Bool}
3128
3129def any_eq_not_all_not_sym(a, A, f, xs):
3130  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))
3131
3132# A one-element list has length one, reversed to rewrite toward the simple side.
3133law length_singleton_sym:
3134  for -a: Quant
3135  for -A: Kind(a)
3136  for -x: A
3137  {1n == List.length(a, A, [x]) : Nat}
3138
3139def length_singleton_sym(a, A, x):
3140  Equal.sym(Nat, List.length(a, A, [x]), 1n, length_singleton(a, A, x))
3141
3142# Reversing a cons puts its head last: reverse (x :: xs) = reverse xs ++ [x], reversed to rewrite toward the simple side.
3143law reverse_cons_sym:
3144  for -a: Quant
3145  for -A: Kind(a)
3146  for -x: A
3147  for xs: List<a, A>
3148  {List.append(a, A, List.reverse(a, A, xs), [x]) == List.reverse(a, A, x <> xs) : List<a, A>}
3149
3150def reverse_cons_sym(a, A, x, xs):
3151  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))
3152
3153# Taking n + 1 elements of a cons keeps its head and takes n from its tail, reversed to rewrite toward the simple side.
3154law take_succ_sym:
3155  for -a: Quant
3156  for -A: Kind(a)
3157  for -x: A
3158  for -xs: List<a, A>
3159  for -n: Nat
3160  {x <> List.take(a, A, xs, n) == List.take(a, A, x <> xs, 1n+n) : List<a, A>}
3161
3162def take_succ_sym(a, A, x, xs, n):
3163  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))
3164
3165# Dropping n + 1 elements of a cons drops its head and n from its tail, reversed to rewrite toward the simple side.
3166law drop_succ_sym:
3167  for -a: Quant
3168  for -A: Kind(a)
3169  for -x: A
3170  for -xs: List<a, A>
3171  for -n: Nat
3172  {List.drop(a, A, xs, n) == List.drop(a, A, x <> xs, 1n+n) : List<a, A>}
3173
3174def drop_succ_sym(a, A, x, xs, n):
3175  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))