def swap_some

bend-collections-laws-math@1.0.0.0 · proofs/math/random/shuffle.bend:80

import Base
import bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend as R
import bend-collections-laws-math@1.0.0.0/spec/math/random/rand.bend as SR
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A

80def swap_some(~A: Data, ~V: Data, ~rel: A -> V -> Bool, +v: V, +xs: List<&2, A>, +i: Nat, +j: Nat, +x: A, +y: A, +hx: {R.nth(A, xs, i) == Some{x} : Maybe<&2, A>}, +hy: {R.nth(A, xs, j) == Some{y} : Maybe<&2, A>}) -> {occ(~A, ~V, ~rel, v, R.put(A, R.put(A, xs, i, y), j, x)) == occ(~A, ~V, ~rel, v, xs) : Nat}:
81  +ys = R.put(A, xs, i, y)
82  A.add_cancel_r(occ(~A, ~V, ~rel, v, R.put(A, ys, j, x)), occ(~A, ~V, ~rel, v, xs), SR.b2n(rel(y, v)),
83    Equal.trans(Nat, Nat.add(occ(~A, ~V, ~rel, v, R.put(A, ys, j, x)), SR.b2n(rel(y, v))), Nat.add(occ(~A, ~V, ~rel, v, ys), SR.b2n(rel(x, v))), Nat.add(occ(~A, ~V, ~rel, v, xs), SR.b2n(rel(y, v))),
84      put_occ(~A, ~V, ~rel, v, ys, j, x, y, nth_put(A, xs, i, j, y, hy)),
85      put_occ(~A, ~V, ~rel, v, xs, i, y, x, hx)))