list.bend
bend-mathlib@0.1.0.1 · 372 lines · 0 definitions
1import Base
2import bend-mathlib@0.1.0.1/nat.bend as MNat
3
4# The empty list is a right identity for append: xs ++ [] = xs.
5law append_nil:
6 for -a: Quant
7 for -A: Kind(a)
8 for xs: List<a, A>
9 {List.append(a, A, xs, Nil{}) == xs : List<a, A>}
10
11def append_nil(a, A, xs):
12 match xs:
13 case Nil{}:
14 {==}
15 case h <> t:
16 %append_nil(a, A, t) : {h <> List.append(a, A, t, Nil{}) == h <> _ : List<a, A>}
17 {==}
18
19# The empty list is a left identity for append: [] ++ xs = xs.
20law nil_append:
21 for -a: Quant
22 for -A: Kind(a)
23 for -xs: List<a, A>
24 {List.append(a, A, Nil{}, xs) == xs : List<a, A>}
25
26def nil_append(a, A, xs):
27 {==}
28
29# Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs).
30law append_assoc:
31 for -a: Quant
32 for -A: Kind(a)
33 for xs: List<a, A>
34 for -ys: List<a, A>
35 for -zs: List<a, A>
36 {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>}
37
38def append_assoc(a, A, xs, ys, zs):
39 match xs:
40 case Nil{}:
41 {==}
42 case h <> t:
43 %append_assoc(a, A, t, ys, zs) : {h <> List.append(a, A, List.append(a, A, t, ys), zs) == h <> _ : List<a, A>}
44 {==}
45
46# The length of an append is the sum of the lengths.
47law length_append:
48 for -a: Quant
49 for -A: Kind(a)
50 for xs: List<a, A>
51 for -ys: List<a, A>
52 {List.length(a, A, List.append(a, A, xs, ys)) == Nat.add(List.length(a, A, xs), List.length(a, A, ys)) : Nat}
53
54def length_append(a, A, xs, ys):
55 match xs:
56 case Nil{}:
57 {==}
58 case h <> t:
59 %length_append(a, A, t, ys) : {1n+List.length(a, A, List.append(a, A, t, ys)) == 1n+_ : Nat}
60 {==}
61
62def 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>}:
63 match xs:
64 case Nil{}:
65 {==}
66 case h <> t:
67 internal_reverse_go_append(a, A, t, h <> ys, acc)
68
69# The reverse accumulator loop appends the reversed list to the accumulator.
70law reverse_go_spec:
71 for -a: Quant
72 for -A: Kind(a)
73 for xs: List<a, A>
74 for -acc: List<a, A>
75 {List.reverse.go(a, A, xs, acc) == List.append(a, A, List.reverse(a, A, xs), acc) : List<a, A>}
76
77def reverse_go_spec(a, A, xs, acc):
78 match xs:
79 case Nil{}:
80 {==}
81 case h <> t:
82 internal_reverse_go_append(a, A, t, h <> Nil{}, acc)
83
84def 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>}:
85 match xs:
86 case Nil{}:
87 {==}
88 case h <> t:
89 internal_reverse_append_go(a, A, t, ys, h <> acc)
90
91# Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs.
92law reverse_append:
93 for -a: Quant
94 for -A: Kind(a)
95 for xs: List<a, A>
96 for ys: List<a, A>
97 {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>}
98
99def reverse_append(a, A, xs, ys):
100 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)))
101
102def 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>}:
103 match xs:
104 case Nil{}:
105 {==}
106 case h <> t:
107 internal_reverse_go_go(a, A, t, h <> acc)
108
109# Reversing twice gives the list back.
110law reverse_reverse:
111 for -a: Quant
112 for -A: Kind(a)
113 for xs: List<a, A>
114 {List.reverse(a, A, List.reverse(a, A, xs)) == xs : List<a, A>}
115
116def reverse_reverse(a, A, xs):
117 internal_reverse_go_go(a, A, xs, Nil{})
118
119def 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}:
120 match xs:
121 case Nil{}:
122 %Equal.sym(Nat, Nat.add(n, 0n), n, MNat.add_zero(n)) : {List.length(a, A, acc) == _ : Nat}
123 e
124 case h <> t:
125 %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}
126 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))
127
128# Reversing preserves the length.
129law length_reverse:
130 for -a: Quant
131 for -A: Kind(a)
132 for xs: List<a, A>
133 {List.length(a, A, List.reverse(a, A, xs)) == List.length(a, A, xs) : Nat}
134
135def length_reverse(a, A, xs):
136 internal_length_reverse_go(a, A, xs, Nil{}, 0n, {==})
137
138# A right fold over an append folds the first part onto the fold of the second.
139law foldr_append:
140 for ~a: Quant
141 for ~A: Kind(a)
142 for ~B: Type
143 for ~f: A -> B -> B
144 for xs: List<a, A>
145 for -ys: List<a, A>
146 for -z: B
147 {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}
148
149def foldr_append(a, A, B, f, xs, ys, z):
150 match xs:
151 case Nil{}:
152 {==}
153 case h <> t:
154 %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}
155 {==}
156
157# Taking n elements and appending the rest after dropping n gives the list back.
158law take_append_drop:
159 for -a: Quant
160 for -A: Kind(a)
161 for xs: List<a, A>
162 for n: Nat
163 {List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) == xs : List<a, A>}
164
165def take_append_drop(a, A, xs, n):
166 match xs n:
167 case Nil{} _:
168 {==}
169 case h <> t 0n:
170 {==}
171 case h <> t 1n+p:
172 %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>}
173 {==}
174
175# Mapping preserves the length.
176law length_map:
177 for ~A: Type
178 for ~B: Type
179 for ~f: A -> B
180 for xs: List<A>
181 {List.length(&1, B, List.map(~A, ~B, ~f, xs)) == List.length(&1, A, xs) : Nat}
182
183def length_map(A, B, f, xs):
184 match xs:
185 case Nil{}:
186 {==}
187 case h <> t:
188 %length_map(~A, ~B, ~f, t) : {1n+List.length(&1, B, List.map(~A, ~B, ~f, t)) == 1n+_ : Nat}
189 {==}
190
191# Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys.
192law map_append:
193 for ~A: Type
194 for ~B: Type
195 for ~f: A -> B
196 for xs: List<A>
197 for -ys: List<A>
198 {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>}
199
200def map_append(A, B, f, xs, ys):
201 match xs:
202 case Nil{}:
203 {==}
204 case h <> t:
205 %map_append(~A, ~B, ~f, t, ys) : {f(h) <> List.map(~A, ~B, ~f, List.append(&1, A, t, ys)) == f(h) <> _ : List<B>}
206 {==}
207
208# Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs.
209law map_map:
210 for ~A: Type
211 for ~B: Type
212 for ~C: Type
213 for ~f: A -> B
214 for ~g: B -> C
215 for xs: List<A>
216 {List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~C, ~(x => g(f(x))), xs) : List<C>}
217
218def map_map(A, B, C, f, g, xs):
219 match xs:
220 case Nil{}:
221 {==}
222 case h <> t:
223 %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>}
224 {==}
225
226# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
227
228# The empty list is a right identity for append: xs ++ [] = xs, reversed to rewrite toward the simple side.
229law append_nil_sym:
230 for -a: Quant
231 for -A: Kind(a)
232 for xs: List<a, A>
233 {xs == List.append(a, A, xs, Nil{}) : List<a, A>}
234
235def append_nil_sym(a, A, xs):
236 Equal.sym(List<a, A>, List.append(a, A, xs, Nil{}), xs, append_nil(a, A, xs))
237
238# The empty list is a left identity for append: [] ++ xs = xs, reversed to rewrite toward the simple side.
239law nil_append_sym:
240 for -a: Quant
241 for -A: Kind(a)
242 for -xs: List<a, A>
243 {xs == List.append(a, A, Nil{}, xs) : List<a, A>}
244
245def nil_append_sym(a, A, xs):
246 Equal.sym(List<a, A>, List.append(a, A, Nil{}, xs), xs, nil_append(a, A, xs))
247
248# Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs), reversed to rewrite toward the simple side.
249law append_assoc_sym:
250 for -a: Quant
251 for -A: Kind(a)
252 for xs: List<a, A>
253 for -ys: List<a, A>
254 for -zs: List<a, A>
255 {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>}
256
257def append_assoc_sym(a, A, xs, ys, zs):
258 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))
259
260# The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.
261law length_append_sym:
262 for -a: Quant
263 for -A: Kind(a)
264 for xs: List<a, A>
265 for -ys: List<a, A>
266 {Nat.add(List.length(a, A, xs), List.length(a, A, ys)) == List.length(a, A, List.append(a, A, xs, ys)) : Nat}
267
268def length_append_sym(a, A, xs, ys):
269 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))
270
271# The reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side.
272law reverse_go_spec_sym:
273 for -a: Quant
274 for -A: Kind(a)
275 for xs: List<a, A>
276 for -acc: List<a, A>
277 {List.append(a, A, List.reverse(a, A, xs), acc) == List.reverse.go(a, A, xs, acc) : List<a, A>}
278
279def reverse_go_spec_sym(a, A, xs, acc):
280 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))
281
282# Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side.
283law reverse_append_sym:
284 for -a: Quant
285 for -A: Kind(a)
286 for xs: List<a, A>
287 for ys: List<a, A>
288 {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>}
289
290def reverse_append_sym(a, A, xs, ys):
291 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))
292
293# Reversing twice gives the list back, reversed to rewrite toward the simple side.
294law reverse_reverse_sym:
295 for -a: Quant
296 for -A: Kind(a)
297 for xs: List<a, A>
298 {xs == List.reverse(a, A, List.reverse(a, A, xs)) : List<a, A>}
299
300def reverse_reverse_sym(a, A, xs):
301 Equal.sym(List<a, A>, List.reverse(a, A, List.reverse(a, A, xs)), xs, reverse_reverse(a, A, xs))
302
303# Reversing preserves the length, reversed to rewrite toward the simple side.
304law length_reverse_sym:
305 for -a: Quant
306 for -A: Kind(a)
307 for xs: List<a, A>
308 {List.length(a, A, xs) == List.length(a, A, List.reverse(a, A, xs)) : Nat}
309
310def length_reverse_sym(a, A, xs):
311 Equal.sym(Nat, List.length(a, A, List.reverse(a, A, xs)), List.length(a, A, xs), length_reverse(a, A, xs))
312
313# A right fold over an append folds the first part onto the fold of the second, reversed to rewrite toward the simple side.
314law foldr_append_sym:
315 for ~a: Quant
316 for ~A: Kind(a)
317 for ~B: Type
318 for ~f: A -> B -> B
319 for xs: List<a, A>
320 for -ys: List<a, A>
321 for -z: B
322 {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}
323
324def foldr_append_sym(a, A, B, f, xs, ys, z):
325 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))
326
327# Taking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side.
328law take_append_drop_sym:
329 for -a: Quant
330 for -A: Kind(a)
331 for xs: List<a, A>
332 for n: Nat
333 {xs == List.append(a, A, List.take(a, A, xs, n), List.drop(a, A, xs, n)) : List<a, A>}
334
335def take_append_drop_sym(a, A, xs, n):
336 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))
337
338# Mapping preserves the length, reversed to rewrite toward the simple side.
339law length_map_sym:
340 for ~A: Type
341 for ~B: Type
342 for ~f: A -> B
343 for xs: List<A>
344 {List.length(&1, A, xs) == List.length(&1, B, List.map(~A, ~B, ~f, xs)) : Nat}
345
346def length_map_sym(A, B, f, xs):
347 Equal.sym(Nat, List.length(&1, B, List.map(~A, ~B, ~f, xs)), List.length(&1, A, xs), length_map(~A, ~B, ~f, xs))
348
349# Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side.
350law map_append_sym:
351 for ~A: Type
352 for ~B: Type
353 for ~f: A -> B
354 for xs: List<A>
355 for -ys: List<A>
356 {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>}
357
358def map_append_sym(A, B, f, xs, ys):
359 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))
360
361# Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs, reversed to rewrite toward the simple side.
362law map_map_sym:
363 for ~A: Type
364 for ~B: Type
365 for ~C: Type
366 for ~f: A -> B
367 for ~g: B -> C
368 for xs: List<A>
369 {List.map(~A, ~C, ~(x => g(f(x))), xs) == List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) : List<C>}
370
371def map_map_sym(A, B, C, f, g, xs):
372 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))