perm.bend
bend-mathlib@0.8.0.0 · 342 lines · 0 definitions
1# bend-mathlib/perm.bend: step-list permutations over bendlib-kernel-list, plus sort value defs and proofs.
2# Resolves the published kernel bendlib-kernel-list@1.0.0.0 by its content hash; see packages/bendlib-kernel-list/README.md.
3import Base
4import bendlib-kernel-list@1.0.0.0/list.bend as K
5
6def internal_shift(+s: List<&2, Nat>) -> List<&2, Nat>:
7 match s:
8 case Nil{}:
9 Nil{}
10 case +i <> rest:
11 (1n+i) <> internal_shift(rest)
12
13def internal_apply_app(-A: Data, +s1: List<&2, Nat>, +s2: List<&2, Nat>, +xs: List<&2, A>) -> {K.apply(A, List.append(&2, Nat, s1, s2), xs) == K.apply(A, s2, K.apply(A, s1, xs)) : List<&2, A>}:
14 match s1:
15 case Nil{}:
16 {==}
17 case +i <> rest:
18 internal_apply_app(A, rest, s2, K.swap_at(A, i, xs))
19
20def internal_apply_shift(-A: Data, +s: List<&2, Nat>, +x: A, +xs: List<&2, A>) -> {K.apply(A, internal_shift(s), x <> xs) == x <> K.apply(A, s, xs) : List<&2, A>}:
21 match s:
22 case Nil{}:
23 {==}
24 case +i <> rest:
25 internal_apply_shift(A, rest, x, K.swap_at(A, i, xs))
26
27# Permutation is reflexive.
28def perm_refl(-A: Data, -xs: List<&2, A>) -> K.perm(A, xs, xs):
29 (Nil{}, {==})
30
31# The empty list is a permutation of itself.
32def perm_nil(-A: Data) -> K.perm(A, Nil{}, Nil{}):
33 (Nil{}, {==})
34
35# Swapping the two leading elements is a permutation.
36def perm_swap(-A: Data, -x: A, -y: A, -t: List<&2, A>) -> K.perm(A, x <> y <> t, y <> x <> t):
37 (0n <> Nil{}, {==})
38
39def internal_trans_eq(-A: Data, +s1: List<&2, Nat>, +s2: List<&2, Nat>, +xs: List<&2, A>, -ys: List<&2, A>, -zs: List<&2, A>, e1: K.perm_steps(A, s1, xs, ys), e2: K.perm_steps(A, s2, ys, zs)) -> K.perm_steps(A, List.append(&2, Nat, s1, s2), xs, zs):
40 %Equal.sym(List<&2, A>, K.apply(A, List.append(&2, Nat, s1, s2), xs), K.apply(A, s2, K.apply(A, s1, xs)), internal_apply_app(A, s1, s2, xs)) : {_ == zs : List<&2, A>}
41 %Equal.sym(List<&2, A>, K.apply(A, s1, xs), ys, e1) : {K.apply(A, s2, _) == zs : List<&2, A>}
42 e2
43
44# Permutation is transitive.
45def perm_trans(-A: Data, +xs: List<&2, A>, -ys: List<&2, A>, -zs: List<&2, A>, h1: K.perm(A, xs, ys), h2: K.perm(A, ys, zs)) -> K.perm(A, xs, zs):
46 (s1, e1) = h1
47 (s2, e2) = h2
48 +s1 = s1
49 +s2 = s2
50 (List.append(&2, Nat, s1, s2), internal_trans_eq(A, s1, s2, xs, ys, zs, e1, e2))
51
52def internal_cons_eq(-A: Data, +s: List<&2, Nat>, +x: A, +xs: List<&2, A>, -ys: List<&2, A>, e: K.perm_steps(A, s, xs, ys)) -> K.perm_steps(A, internal_shift(s), x <> xs, x <> ys):
53 %Equal.sym(List<&2, A>, K.apply(A, internal_shift(s), x <> xs), x <> K.apply(A, s, xs), internal_apply_shift(A, s, x, xs)) : {_ == x <> ys : List<&2, A>}
54 %Equal.sym(List<&2, A>, K.apply(A, s, xs), ys, e) : {x <> _ == x <> ys : List<&2, A>}
55 {==}
56
57# Prepending the same element preserves permutation.
58def perm_cons(-A: Data, +x: A, +xs: List<&2, A>, -ys: List<&2, A>, h: K.perm(A, xs, ys)) -> K.perm(A, x <> xs, x <> ys):
59 (s, e) = h
60 +s = s
61 (internal_shift(s), internal_cons_eq(A, s, x, xs, ys, e))
62
63# A Perm hypothesis in existential form is reusable.
64def perm_dup(-A: Data, -xs: List<&2, A>, -ys: List<&2, A>, +h: K.perm(A, xs, ys)) -> K.perm(A, xs, ys) & K.perm(A, xs, ys):
65 (h, h)
66
67# Insertion into a list, generic comparator (structural, Base-only branching via Bool.pick).
68def insert_by(~A: Data, ~le: A -> A -> Bool, +x: A, xs: List<&2, A>) -> List<&2, A>:
69 match xs:
70 case Nil{}:
71 x <> Nil{}
72 case +y <> +t:
73 Bool.pick(List<&2, A>, le(x, y), x <> y <> t, y <> insert_by(~A, ~le, x, t))
74
75# Insertion sort by the comparator le.
76def isort_by(~A: Data, ~le: A -> A -> Bool, xs: List<&2, A>) -> List<&2, A>:
77 match xs:
78 case Nil{}:
79 Nil{}
80 case +x <> t:
81 insert_by(~A, ~le, x, isort_by(~A, ~le, t))
82
83def internal_ins_pick(-A: Data, b: Bool, +x: A, +y: A, +t: List<&2, A>, -r: List<&2, A>, ih: K.perm(A, x <> t, r)) -> K.perm(A, x <> y <> t, Bool.pick(List<&2, A>, b, x <> y <> t, y <> r)):
84 match b:
85 case True{}:
86 perm_refl(A, x <> y <> t)
87 case False{}:
88 perm_trans(A, x <> y <> t, y <> x <> t, y <> r, perm_swap(A, x, y, t), perm_cons(A, y, x <> t, r, ih))
89
90# Inserting x into xs permutes x <> xs.
91def insert_by_perm(~A: Data, ~le: A -> A -> Bool, +x: A, +xs: List<&2, A>) -> K.perm(A, x <> xs, insert_by(~A, ~le, x, xs)):
92 match xs:
93 case Nil{}:
94 perm_refl(A, x <> Nil{})
95 case +y <> t:
96 internal_ins_pick(A, le(x, y), x, y, t, insert_by(~A, ~le, x, t), insert_by_perm(~A, ~le, x, t))
97
98# Insertion sort permutes its input.
99def isort_by_perm(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>) -> K.perm(A, xs, isort_by(~A, ~le, xs)):
100 match xs:
101 case Nil{}:
102 perm_refl(A, Nil{})
103 case +x <> t:
104 perm_trans(A, x <> t, x <> isort_by(~A, ~le, t), isort_by(~A, ~le, x <> t), perm_cons(A, x, t, isort_by(~A, ~le, t), isort_by_perm(~A, ~le, t)), insert_by_perm(~A, ~le, x, isort_by(~A, ~le, t)))
105
106# Insertion sort permutes a Nat list.
107def isort_by_perm_nat(+xs: List<&2, Nat>) -> K.perm(Nat, xs, isort_by(~Nat, ~Nat.is_le, xs)):
108 isort_by_perm(~Nat, ~Nat.is_le, xs)
109
110def internal_append_nil(-A: Data, +ys: List<&2, A>) -> {List.append(&2, A, ys, Nil{}) == ys : List<&2, A>}:
111 match ys:
112 case Nil{}:
113 {==}
114 case +y <> t:
115 %Equal.sym(List<&2, A>, List.append(&2, A, t, Nil{}), t, internal_append_nil(A, t)) : {y <> _ == y <> t : List<&2, A>}
116 {==}
117
118# Appending Nil is a permutation, by the empty step list.
119def perm_append_nil(-A: Data, +xs: List<&2, A>) -> K.perm(A, List.append(&2, A, xs, Nil{}), xs):
120 (Nil{}, internal_append_nil(A, xs))
121
122# Moving an element from the middle to the front is a permutation.
123def perm_move(-A: Data, +xs: List<&2, A>, +y: A, +t: List<&2, A>) -> K.perm(A, List.append(&2, A, xs, y <> t), y <> List.append(&2, A, xs, t)):
124 match xs:
125 case Nil{}:
126 perm_refl(A, y <> t)
127 case +x <> r:
128 perm_trans(A, x <> List.append(&2, A, r, y <> t), x <> y <> List.append(&2, A, r, t), y <> x <> List.append(&2, A, r, t), perm_cons(A, x, List.append(&2, A, r, y <> t), y <> List.append(&2, A, r, t), perm_move(A, r, y, t)), perm_swap(A, x, y, List.append(&2, A, r, t)))
129
130# Merges two lists, taking the head of xs first whenever le(x, y) holds.
131def merge_by(~A: Data, ~le: A -> A -> Bool, xs: List<&2, A>, ys: List<&2, A>) -> List<&2, A>:
132 match xs ys:
133 case Nil{} _:
134 ys
135 case +x <> +xt Nil{}:
136 x <> xt
137 case +x <> +xt +y <> +yt:
138 Bool.pick(List<&2, A>, le(x, y), x <> merge_by(~A, ~le, xt, y <> yt), y <> merge_by(~A, ~le, x <> xt, yt))
139
140def internal_merge_pick(-A: Data, b: Bool, +x: A, +xt: List<&2, A>, +y: A, +yt: List<&2, A>, -m1: List<&2, A>, -m2: List<&2, A>, ih1: K.perm(A, List.append(&2, A, xt, y <> yt), m1), ih2: K.perm(A, x <> List.append(&2, A, xt, yt), m2)) -> K.perm(A, x <> List.append(&2, A, xt, y <> yt), Bool.pick(List<&2, A>, b, x <> m1, y <> m2)):
141 match b:
142 case True{}:
143 perm_cons(A, x, List.append(&2, A, xt, y <> yt), m1, ih1)
144 case False{}:
145 perm_trans(A, x <> List.append(&2, A, xt, y <> yt), y <> x <> List.append(&2, A, xt, yt), y <> m2, perm_move(A, x <> xt, y, yt), perm_cons(A, y, x <> List.append(&2, A, xt, yt), m2, ih2))
146
147# Merging permutes the concatenation.
148def merge_by_perm(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>, +ys: List<&2, A>) -> K.perm(A, List.append(&2, A, xs, ys), merge_by(~A, ~le, xs, ys)):
149 match xs ys:
150 case Nil{} _:
151 perm_refl(A, ys)
152 case +x <> +xt Nil{}:
153 perm_cons(A, x, List.append(&2, A, xt, Nil{}), xt, perm_append_nil(A, xt))
154 case +x <> +xt +y <> +yt:
155 internal_merge_pick(A, le(x, y), x, xt, y, yt, merge_by(~A, ~le, xt, y <> yt), merge_by(~A, ~le, x <> xt, yt), merge_by_perm(~A, ~le, xt, y <> yt), merge_by_perm(~A, ~le, x <> xt, yt))
156
157# Merging two Nat lists permutes their concatenation.
158def merge_by_perm_nat(+xs: List<&2, Nat>, +ys: List<&2, Nat>) -> K.perm(Nat, List.append(&2, Nat, xs, ys), merge_by(~Nat, ~Nat.is_le, xs, ys)):
159 merge_by_perm(~Nat, ~Nat.is_le, xs, ys)
160
161# Moving the front element into the middle is a permutation.
162def perm_move_rev(-A: Data, +xs: List<&2, A>, +y: A, +t: List<&2, A>) -> K.perm(A, y <> List.append(&2, A, xs, t), List.append(&2, A, xs, y <> t)):
163 match xs:
164 case Nil{}:
165 perm_refl(A, y <> t)
166 case +x <> r:
167 perm_trans(A, y <> x <> List.append(&2, A, r, t), x <> y <> List.append(&2, A, r, t), x <> List.append(&2, A, r, y <> t), perm_swap(A, y, x, List.append(&2, A, r, t)), perm_cons(A, x, y <> List.append(&2, A, r, t), List.append(&2, A, r, y <> t), perm_move_rev(A, r, y, t)))
168
169# Appending commutes up to permutation (derived without symmetry).
170def perm_append_comm(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) -> K.perm(A, List.append(&2, A, xs, ys), List.append(&2, A, ys, xs)):
171 match xs:
172 case Nil{}:
173 (Nil{}, Equal.sym(List<&2, A>, List.append(&2, A, ys, Nil{}), ys, internal_append_nil(A, ys)))
174 case +x <> r:
175 perm_trans(A, x <> List.append(&2, A, r, ys), x <> List.append(&2, A, ys, r), List.append(&2, A, ys, x <> r), perm_cons(A, x, List.append(&2, A, r, ys), List.append(&2, A, ys, r), perm_append_comm(A, r, ys)), perm_move_rev(A, ys, x, r))
176
177# Permuting the right operand of an append gives a permutation of the append.
178def perm_append_right(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>, -zs: List<&2, A>, h: K.perm(A, ys, zs)) -> K.perm(A, List.append(&2, A, xs, ys), List.append(&2, A, xs, zs)):
179 match xs:
180 case Nil{}:
181 h
182 case +x <> r:
183 perm_cons(A, x, List.append(&2, A, r, ys), List.append(&2, A, r, zs), perm_append_right(A, r, ys, zs, h))
184
185# Permuting both operands of an append gives a permutation of the append.
186def perm_append(-A: Data, +xs: List<&2, A>, +xs2: List<&2, A>, +ys: List<&2, A>, -ys2: List<&2, A>, p: K.perm(A, xs, xs2), q: K.perm(A, ys, ys2)) -> K.perm(A, List.append(&2, A, xs, ys), List.append(&2, A, xs2, ys2)):
187 perm_trans(A, List.append(&2, A, xs, ys), List.append(&2, A, ys, xs), List.append(&2, A, xs2, ys2), perm_append_comm(A, xs, ys), perm_trans(A, List.append(&2, A, ys, xs), List.append(&2, A, ys, xs2), List.append(&2, A, xs2, ys2), perm_append_right(A, ys, xs, xs2, p), perm_trans(A, List.append(&2, A, ys, xs2), List.append(&2, A, xs2, ys), List.append(&2, A, xs2, ys2), perm_append_comm(A, ys, xs2), perm_append_right(A, xs2, ys, ys2, q))))
188
189# The elements of a list at even positions (0, 2, 4, ...).
190def evens(-A: Data, xs: List<&2, A>) -> List<&2, A>:
191 match xs:
192 case Nil{}:
193 Nil{}
194 case +x <> r:
195 match r:
196 case Nil{}:
197 x <> Nil{}
198 case +y <> t:
199 x <> evens(A, t)
200
201# The elements of a list at odd positions (1, 3, 5, ...).
202def odds(-A: Data, xs: List<&2, A>) -> List<&2, A>:
203 match xs:
204 case Nil{}:
205 Nil{}
206 case +x <> r:
207 match r:
208 case Nil{}:
209 Nil{}
210 case +y <> t:
211 y <> odds(A, t)
212
213# Splitting into evens and odds is a permutation.
214def split_perm(-A: Data, +xs: List<&2, A>) -> K.perm(A, xs, List.append(&2, A, evens(A, xs), odds(A, xs))):
215 match xs:
216 case Nil{}:
217 perm_refl(A, Nil{})
218 case +x <> r:
219 match r:
220 case Nil{}:
221 perm_refl(A, x <> Nil{})
222 case +y <> t:
223 perm_cons(A, x, y <> t, List.append(&2, A, evens(A, t), y <> odds(A, t)), perm_trans(A, y <> t, y <> List.append(&2, A, evens(A, t), odds(A, t)), List.append(&2, A, evens(A, t), y <> odds(A, t)), perm_cons(A, y, t, List.append(&2, A, evens(A, t), odds(A, t)), split_perm(A, t)), perm_move_rev(A, evens(A, t), y, odds(A, t))))
224
225# Merge sort with fuel (the fuel only bounds recursion; it never affects the permutation).
226def msort_by(~A: Data, ~le: A -> A -> Bool, fuel: Nat, +xs: List<&2, A>) -> List<&2, A>:
227 match fuel:
228 case 0n:
229 xs
230 case 1n++f:
231 merge_by(~A, ~le, msort_by(~A, ~le, f, evens(A, xs)), msort_by(~A, ~le, f, odds(A, xs)))
232
233# Merge sort permutes its input, for any fuel.
234def msort_by_perm(~A: Data, ~le: A -> A -> Bool, fuel: Nat, +xs: List<&2, A>) -> K.perm(A, xs, msort_by(~A, ~le, fuel, xs)):
235 match fuel:
236 case 0n:
237 perm_refl(A, xs)
238 case 1n++f:
239 perm_trans(A, xs, List.append(&2, A, evens(A, xs), odds(A, xs)), msort_by(~A, ~le, 1n+f, xs), split_perm(A, xs), perm_trans(A, List.append(&2, A, evens(A, xs), odds(A, xs)), List.append(&2, A, msort_by(~A, ~le, f, evens(A, xs)), msort_by(~A, ~le, f, odds(A, xs))), msort_by(~A, ~le, 1n+f, xs), perm_append(A, evens(A, xs), msort_by(~A, ~le, f, evens(A, xs)), odds(A, xs), msort_by(~A, ~le, f, odds(A, xs)), msort_by_perm(~A, ~le, f, evens(A, xs)), msort_by_perm(~A, ~le, f, odds(A, xs))), merge_by_perm(~A, ~le, msort_by(~A, ~le, f, evens(A, xs)), msort_by(~A, ~le, f, odds(A, xs)))))
240
241# Merge sort by the comparator le.
242def sort_by(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>) -> List<&2, A>:
243 msort_by(~A, ~le, List.length(&2, A, xs), xs)
244
245# The sort permutes its input.
246def sort_by_perm(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>) -> K.perm(A, xs, sort_by(~A, ~le, xs)):
247 msort_by_perm(~A, ~le, List.length(&2, A, xs), xs)
248
249# Merge sort permutes a Nat list.
250def sort_by_perm_nat(+xs: List<&2, Nat>) -> K.perm(Nat, xs, sort_by(~Nat, ~Nat.is_le, xs)):
251 sort_by_perm(~Nat, ~Nat.is_le, xs)
252
253def internal_sort_nat_test() -> {sort_by(~Nat, ~Nat.is_le, [5n, 1n, 4n, 2n, 3n, 1n]) == [1n, 1n, 2n, 3n, 4n, 5n] : List<&2, Nat>}:
254 {==}
255
256def internal_swap_head_invol(-A: Data, xs: List<&2, A>) -> {K.swap_head(A, K.swap_head(A, xs)) == xs : List<&2, A>}:
257 match xs:
258 case Nil{}:
259 {==}
260 case +x <> t:
261 match t:
262 case Nil{}:
263 {==}
264 case +y <> u:
265 {==}
266
267def internal_swap_at_invol(-A: Data, +i: Nat, +xs: List<&2, A>) -> {K.swap_at(A, i, K.swap_at(A, i, xs)) == xs : List<&2, A>}:
268 match i:
269 case 0n:
270 internal_swap_head_invol(A, xs)
271 case 1n+p:
272 match xs:
273 case Nil{}:
274 {==}
275 case +x <> t:
276 %Equal.sym(List<&2, A>, K.swap_at(A, p, K.swap_at(A, p, t)), t, internal_swap_at_invol(A, p, t)) : {x <> _ == x <> t : List<&2, A>}
277 {==}
278
279def internal_invert(+s: List<&2, Nat>) -> List<&2, Nat>:
280 match s:
281 case Nil{}:
282 Nil{}
283 case +i <> rest:
284 List.append(&2, Nat, internal_invert(rest), i <> Nil{})
285
286def internal_apply_invert(-A: Data, +s: List<&2, Nat>, +xs: List<&2, A>) -> {K.apply(A, internal_invert(s), K.apply(A, s, xs)) == xs : List<&2, A>}:
287 match s:
288 case Nil{}:
289 {==}
290 case +i <> rest:
291 %Equal.sym(List<&2, A>, K.apply(A, List.append(&2, Nat, internal_invert(rest), i <> Nil{}), K.apply(A, rest, K.swap_at(A, i, xs))), K.apply(A, i <> Nil{}, K.apply(A, internal_invert(rest), K.apply(A, rest, K.swap_at(A, i, xs)))), internal_apply_app(A, internal_invert(rest), i <> Nil{}, K.apply(A, rest, K.swap_at(A, i, xs)))) : {_ == xs : List<&2, A>}
292 %Equal.sym(List<&2, A>, K.apply(A, internal_invert(rest), K.apply(A, rest, K.swap_at(A, i, xs))), K.swap_at(A, i, xs), internal_apply_invert(A, rest, K.swap_at(A, i, xs))) : {K.apply(A, i <> Nil{}, _) == xs : List<&2, A>}
293 internal_swap_at_invol(A, i, xs)
294
295def internal_sym_eq(-A: Data, +s: List<&2, Nat>, +xs: List<&2, A>, -ys: List<&2, A>, e: K.perm_steps(A, s, xs, ys)) -> K.perm_steps(A, internal_invert(s), ys, xs):
296 %e : {K.apply(A, internal_invert(s), _) == xs : List<&2, A>}
297 internal_apply_invert(A, s, xs)
298
299# Permutation is symmetric.
300def perm_sym(-A: Data, +xs: List<&2, A>, -ys: List<&2, A>, h: K.perm(A, xs, ys)) -> K.perm(A, ys, xs):
301 (s, e) = h
302 +s = s
303 (internal_invert(s), internal_sym_eq(A, s, xs, ys, e))
304
305def internal_swap_head_length(-A: Data, xs: List<&2, A>) -> {List.length(&2, A, K.swap_head(A, xs)) == List.length(&2, A, xs) : Nat}:
306 match xs:
307 case Nil{}:
308 {==}
309 case +x <> t:
310 match t:
311 case Nil{}:
312 {==}
313 case +y <> u:
314 {==}
315
316def internal_swap_at_length(-A: Data, +i: Nat, +xs: List<&2, A>) -> {List.length(&2, A, K.swap_at(A, i, xs)) == List.length(&2, A, xs) : Nat}:
317 match i:
318 case 0n:
319 internal_swap_head_length(A, xs)
320 case 1n+p:
321 match xs:
322 case Nil{}:
323 {==}
324 case +x <> t:
325 %Equal.sym(Nat, List.length(&2, A, K.swap_at(A, p, t)), List.length(&2, A, t), internal_swap_at_length(A, p, t)) : {1n+_ == 1n+List.length(&2, A, t) : Nat}
326 {==}
327
328def internal_apply_length(-A: Data, +s: List<&2, Nat>, +xs: List<&2, A>) -> {List.length(&2, A, K.apply(A, s, xs)) == List.length(&2, A, xs) : Nat}:
329 match s:
330 case Nil{}:
331 {==}
332 case +i <> rest:
333 Equal.trans(Nat, List.length(&2, A, K.apply(A, rest, K.swap_at(A, i, xs))), List.length(&2, A, K.swap_at(A, i, xs)), List.length(&2, A, xs), internal_apply_length(A, rest, K.swap_at(A, i, xs)), internal_swap_at_length(A, i, xs))
334
335def internal_length_eq(-A: Data, +s: List<&2, Nat>, +xs: List<&2, A>, -ys: List<&2, A>, e: K.perm_steps(A, s, xs, ys)) -> {List.length(&2, A, ys) == List.length(&2, A, xs) : Nat}:
336 %e : {List.length(&2, A, _) == List.length(&2, A, xs) : Nat}
337 internal_apply_length(A, s, xs)
338
339# Permutation preserves length.
340def perm_length(-A: Data, +xs: List<&2, A>, -ys: List<&2, A>, h: K.perm(A, xs, ys)) -> {List.length(&2, A, ys) == List.length(&2, A, xs) : Nat}:
341 (s, e) = h
342 internal_length_eq(A, s, xs, ys, e)