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. 3 import Base 4 import 0xb5c8145e53a6a127d611f45f602666ec/list.bend as K 5 6 def 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 13 def 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 20 def 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. 28 def 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. 32 def perm_nil(-A: Data) -> K.perm(A, Nil{}, Nil{}): 33 (Nil{}, {==}) 34 35 # Swapping the two leading elements is a permutation. 36 def 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 39 def 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. 45 def 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 52 def 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. 58 def 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. 64 def 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). 68 def 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. 76 def 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 83 def 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. 91 def 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. 99 def 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. 107 def 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 110 def 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. 119 def 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. 123 def 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. 131 def 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 140 def 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. 148 def 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. 158 def 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. 162 def 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). 170 def 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. 178 def 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. 186 def 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, ...). 190 def 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, ...). 202 def 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. 214 def 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). 226 def 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. 234 def 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. 242 def 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. 246 def 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. 250 def 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 253 def 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 256 def 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 267 def 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 279 def 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 286 def 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 295 def 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. 300 def 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 305 def 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 316 def 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 328 def 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 335 def 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. 340 def 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)