list.bend

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