~/bend-docscommunity

proofs/math/random/shuffle.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/random/shuffle.bend as Shuffle

8 imports
import Base
import ../../../src/math/u64.bend as W
import ../../../src/math/w64.bend as X
import ../../../src/math/random/rand.bend as R
import ../../../spec/math/random/rand.bend as SR
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32alg.bend as A

Definitions

def some_or source · line 19 · raw

@-A:Data -> @m:Maybe<&2, A> -> @+d:A -> A

def is_some source · line 26 · raw

@-A:Data -> @m:Maybe<&2, A> -> Bool

def none_some source · line 33 · raw

@-A:Data -> @+y:A -> @e:{None{} == Some{y} : Maybe<&2, A>} -> Empty

def some_inj source · line 37 · raw

@-A:Data -> @+x:A -> @+y:A -> @e:{Some{x} == Some{y} : Maybe<&2, A>} -> {x == y : A}

def swap_ends source · line 41 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(b, c), a) : Nat}

(a + c) + b == (b + c) + a

def assoc3 source · line 49 · raw

@+h:Nat -> @+x:Nat -> @+y:Nat -> @+z:Nat -> @+e:{Nat.add(x, y) == z : Nat} -> {Nat.add(Nat.add(h, x), y) == Nat.add(h, z) : Nat}

(h + x) + y == h + (x + y), stated for the step of put_occ

def nth_put source · line 67 · raw

@-A:Data -> @+xs:List<&2, A> -> @+i:Nat -> @+j:Nat -> @+y:A -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.nth(A, xs, j) == Some{y} : Maybe<&2, A>} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.nth(A, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.put(A, xs, i, y), j) == Some{y} : Maybe<&2, A>}

writing y at i keeps an element y at j

def lt_succ_split source · line 119 · raw

@+v:Nat -> @+p:Nat -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.b2n(Nat.is_eq(p, v)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.b2n(Nat.is_lt(v, p))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.b2n(Nat.is_lt(v, 1n+p)) : Nat}

[p == v] + [v < p] == [v < p + 1]

def range_occ source · line 133 · raw

@+n:Nat -> @+acc:List<&2, Nat> -> @+v:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.occurrences(Nat, Nat, Nat.is_eq, v, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.range_go(n, acc)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.occurrences(Nat, Nat, Nat.is_eq, v, acc), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.b2n(Nat.is_lt(v, n))) : Nat}

range_go(n, acc) = [0, 1, ..., n - 1] ++ acc holds v as often as acc, plus once when v < n

Templates

template occ source · line 16 · raw

@-A:Data -> @-V:Data -> @-rel:(@_:A -> @_:V -> Bool) -> @+v:V -> @+xs:List<&2, A> -> Nat

template put_occ source · line 54 · raw

@-A:Data -> @-V:Data -> @-rel:(@_:A -> @_:V -> Bool) -> @+v:V -> @+xs:List<&2, A> -> @+i:Nat -> @+x:A -> @+y:A -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.nth(A, xs, i) == Some{y} : Maybe<&2, A>} -> {Nat.add(occ(A, V, rel, v, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.put(A, xs, i, x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.b2n(rel(y, v))) == Nat.add(occ(A, V, rel, v, xs), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.b2n(rel(x, v))) : Nat}

writing x over the element y at i: occ + [y] == old occ + [x]

template swap_some source · line 80 · raw

@-A:Data -> @-V:Data -> @-rel:(@_:A -> @_:V -> Bool) -> @+v:V -> @+xs:List<&2, A> -> @+i:Nat -> @+j:Nat -> @+x:A -> @+y:A -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.nth(A, xs, i) == Some{x} : Maybe<&2, A>} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.nth(A, xs, j) == Some{y} : Maybe<&2, A>} -> {occ(A, V, rel, v, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.put(A, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.put(A, xs, i, y), j, x)) == occ(A, V, rel, v, xs) : Nat}

template swap_m_occ source · line 87 · raw

@-A:Data -> @-V:Data -> @-rel:(@_:A -> @_:V -> Bool) -> @+v:V -> @+xs:List<&2, A> -> @+i:Nat -> @+j:Nat -> @+a:Maybe<&2, A> -> @+b:Maybe<&2, A> -> @+ha:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.nth(A, xs, i) == a : Maybe<&2, A>} -> @+hb:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.nth(A, xs, j) == b : Maybe<&2, A>} -> {occ(A, V, rel, v, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.swap_m(A, xs, i, j, a, b)) == occ(A, V, rel, v, xs) : Nat}

template swap_occ source · line 97 · raw

@-A:Data -> @-V:Data -> @-rel:(@_:A -> @_:V -> Bool) -> @+v:V -> @+xs:List<&2, A> -> @+i:Nat -> @+j:Nat -> {occ(A, V, rel, v, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.swap(A, xs, i, j)) == occ(A, V, rel, v, xs) : Nat}

THEOREM: a swap keeps every count

template swap_at_occ source · line 100 · raw

@-A:Data -> @-V:Data -> @-rel:(@_:A -> @_:V -> Bool) -> @-S:Data -> @+v:V -> @+xs:List<&2, A> -> @+i:Nat -> @r:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S) -> {occ(A, V, rel, v, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.fst(List<&2, A>, S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.swap_at(A, S, xs, i, r))) == occ(A, V, rel, v, xs) : Nat}

template go_occ source · line 105 · raw

@-A:Data -> @-V:Data -> @-rel:(@_:A -> @_:V -> Bool) -> @-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+v:V -> @+k:Nat -> @+n:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @st:Pair(List<&2, A>, S) -> {occ(A, V, rel, v, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.fst(List<&2, A>, S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.shuffle_go(A, S, next, k, n, st))) == occ(A, V, rel, v, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.fst(List<&2, A>, S, st)) : Nat}

template shuffle_perm source · line 115 · raw

@-A:Data -> @-V:Data -> @-rel:(@_:A -> @_:V -> Bool) -> @-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+xs:List<&2, A> -> @+v:V -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.occurrences(A, V, rel, v, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.fst(List<&2, A>, S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.shuffle(A, S, next, s, xs))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.occurrences(A, V, rel, v, xs) : Nat}

THEOREM (Shuffle.permutation)

template perm_perm source · line 151 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @+s:S -> @+n:Nat -> @+i:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.occurrences(Nat, Nat, Nat.is_eq, i, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.fst(List<&2, Nat>, S, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/random/rand.perm(S, next, s, n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/random/rand.b2n(Nat.is_lt(i, n)) : Nat}

THEOREM (Perm.permutation)