~/bend-docscommunity

perm.bend checks

raw source on the hub · import bend-mathlib@0.3.0.0/perm.bend as Perm

bend-mathlib/perm.bend: step-list permutations over bendlib-kernel-list, plus sort value defs and proofs. Resolves the unpublished kernel by its real content hash (devlib); see packages/bendlib-kernel-list/README.md.

2 imports
import Base
import 0xb5c8145e53a6a127d611f45f602666ec/list.bend as K

Definitions

def internal_shift source · line 6 · raw

@+s:List<&2, Nat> -> List<&2, Nat>

def internal_apply_app source · line 13 · raw

@-A:Data -> @+s1:List<&2, Nat> -> @+s2:List<&2, Nat> -> @+xs:List<&2, A> -> {0xb5c8145e53a6a127d611f45f602666ec/list.apply(A, List.append(&2, Nat, s1, s2), xs) == 0xb5c8145e53a6a127d611f45f602666ec/list.apply(A, s2, 0xb5c8145e53a6a127d611f45f602666ec/list.apply(A, s1, xs)) : List<&2, A>}

def internal_apply_shift source · line 20 · raw

@-A:Data -> @+s:List<&2, Nat> -> @+x:A -> @+xs:List<&2, A> -> {0xb5c8145e53a6a127d611f45f602666ec/list.apply(A, internal_shift(s), x <> xs) == x <> 0xb5c8145e53a6a127d611f45f602666ec/list.apply(A, s, xs) : List<&2, A>}

def perm_refl source · line 28 · raw

@-A:Data -> @-xs:List<&2, A> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, xs)

Permutation is reflexive.

def perm_nil source · line 32 · raw

@-A:Data -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, [], [])

The empty list is a permutation of itself.

def perm_swap source · line 36 · raw

@-A:Data -> @-x:A -> @-y:A -> @-t:List<&2, A> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, x <> y <> t, y <> x <> t)

Swapping the two leading elements is a permutation.

def internal_trans_eq source · line 39 · raw

@-A:Data -> @+s1:List<&2, Nat> -> @+s2:List<&2, Nat> -> @+xs:List<&2, A> -> @-ys:List<&2, A> -> @-zs:List<&2, A> -> @e1:0xb5c8145e53a6a127d611f45f602666ec/list.perm_steps(A, s1, xs, ys) -> @e2:0xb5c8145e53a6a127d611f45f602666ec/list.perm_steps(A, s2, ys, zs) -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm_steps(A, List.append(&2, Nat, s1, s2), xs, zs)

def perm_trans source · line 45 · raw

@-A:Data -> @+xs:List<&2, A> -> @-ys:List<&2, A> -> @-zs:List<&2, A> -> @h1:0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, ys) -> @h2:0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, ys, zs) -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, zs)

Permutation is transitive.

def internal_cons_eq source · line 52 · raw

@-A:Data -> @+s:List<&2, Nat> -> @+x:A -> @+xs:List<&2, A> -> @-ys:List<&2, A> -> @e:0xb5c8145e53a6a127d611f45f602666ec/list.perm_steps(A, s, xs, ys) -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm_steps(A, internal_shift(s), x <> xs, x <> ys)

def perm_cons source · line 58 · raw

@-A:Data -> @+x:A -> @+xs:List<&2, A> -> @-ys:List<&2, A> -> @h:0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, ys) -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, x <> xs, x <> ys)

Prepending the same element preserves permutation.

def perm_dup source · line 64 · raw

@-A:Data -> @-xs:List<&2, A> -> @-ys:List<&2, A> -> @+h:0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, ys) -> Pair(0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, ys), 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, ys))

A Perm hypothesis in existential form is reusable.

def internal_ins_pick source · line 82 · raw

@-A:Data -> @b:Bool -> @+x:A -> @+y:A -> @+t:List<&2, A> -> @-r:List<&2, A> -> @ih:0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, x <> t, r) -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, x <> y <> t, Bool.pick(List<&2, A>, b, x <> y <> t, y <> r))

def isort_by_perm_nat source · line 106 · raw

@+xs:List<&2, Nat> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(Nat, xs, isort_by(Nat, Nat.is_le, xs))

Closed instance: instantiate at Nat and at String.

def internal_append_nil source · line 109 · raw

@-A:Data -> @+ys:List<&2, A> -> {List.append(&2, A, ys, []) == ys : List<&2, A>}

def perm_append_nil source · line 118 · raw

@-A:Data -> @+xs:List<&2, A> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, List.append(&2, A, xs, []), xs)

Appending Nil is a permutation (steps: none).

def perm_move source · line 122 · raw

@-A:Data -> @+xs:List<&2, A> -> @+y:A -> @+t:List<&2, A> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, List.append(&2, A, xs, y <> t), y <> List.append(&2, A, xs, t))

Moving an element from the middle to the front is a permutation.

def internal_merge_pick source · line 138 · raw

@-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:0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, List.append(&2, A, xt, y <> yt), m1) -> @ih2:0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, x <> List.append(&2, A, xt, yt), m2) -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, x <> List.append(&2, A, xt, y <> yt), Bool.pick(List<&2, A>, b, x <> m1, y <> m2))

def merge_by_perm_nat source · line 155 · raw

@+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(Nat, List.append(&2, Nat, xs, ys), merge_by(Nat, Nat.is_le, xs, ys))

def perm_move_rev source · line 159 · raw

@-A:Data -> @+xs:List<&2, A> -> @+y:A -> @+t:List<&2, A> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, y <> List.append(&2, A, xs, t), List.append(&2, A, xs, y <> t))

Moving the front element into the middle is a permutation.

def perm_append_comm source · line 167 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, List.append(&2, A, xs, ys), List.append(&2, A, ys, xs))

Appending commutes up to permutation (derived without symmetry).

def perm_append_right source · line 175 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @-zs:List<&2, A> -> @h:0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, ys, zs) -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, List.append(&2, A, xs, ys), List.append(&2, A, xs, zs))

Permuting the right operand of an append.

def perm_append source · line 183 · raw

@-A:Data -> @+xs:List<&2, A> -> @+xs2:List<&2, A> -> @+ys:List<&2, A> -> @-ys2:List<&2, A> -> @p:0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, xs2) -> @q:0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, ys, ys2) -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, List.append(&2, A, xs, ys), List.append(&2, A, xs2, ys2))

Permuting both operands of an append.

def evens source · line 186 · raw

@-A:Data -> @xs:List<&2, A> -> List<&2, A>

def odds source · line 197 · raw

@-A:Data -> @xs:List<&2, A> -> List<&2, A>

def split_perm source · line 209 · raw

@-A:Data -> @+xs:List<&2, A> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, List.append(&2, A, evens(A, xs), odds(A, xs)))

Splitting into evens and odds is a permutation.

def sort_by_perm_nat source · line 243 · raw

@+xs:List<&2, Nat> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(Nat, xs, sort_by(Nat, Nat.is_le, xs))

def internal_sort_nat_test source · line 246 · raw

{sort_by(Nat, Nat.is_le, [5n, 1n, 4n, 2n, 3n, 1n]) == [1n, 1n, 2n, 3n, 4n, 5n] : List<&2, Nat>}

def internal_swap_head_invol source · line 249 · raw

@-A:Data -> @xs:List<&2, A> -> {0xb5c8145e53a6a127d611f45f602666ec/list.swap_head(A, 0xb5c8145e53a6a127d611f45f602666ec/list.swap_head(A, xs)) == xs : List<&2, A>}

def internal_swap_at_invol source · line 260 · raw

@-A:Data -> @+i:Nat -> @+xs:List<&2, A> -> {0xb5c8145e53a6a127d611f45f602666ec/list.swap_at(A, i, 0xb5c8145e53a6a127d611f45f602666ec/list.swap_at(A, i, xs)) == xs : List<&2, A>}

def internal_invert source · line 272 · raw

@+s:List<&2, Nat> -> List<&2, Nat>

def internal_apply_invert source · line 279 · raw

@-A:Data -> @+s:List<&2, Nat> -> @+xs:List<&2, A> -> {0xb5c8145e53a6a127d611f45f602666ec/list.apply(A, internal_invert(s), 0xb5c8145e53a6a127d611f45f602666ec/list.apply(A, s, xs)) == xs : List<&2, A>}

def internal_sym_eq source · line 288 · raw

@-A:Data -> @+s:List<&2, Nat> -> @+xs:List<&2, A> -> @-ys:List<&2, A> -> @e:0xb5c8145e53a6a127d611f45f602666ec/list.perm_steps(A, s, xs, ys) -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm_steps(A, internal_invert(s), ys, xs)

def perm_sym source · line 293 · raw

@-A:Data -> @+xs:List<&2, A> -> @-ys:List<&2, A> -> @h:0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, ys) -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, ys, xs)

Permutation is symmetric.

def internal_swap_head_length source · line 299 · raw

@-A:Data -> @xs:List<&2, A> -> {List.length(&2, A, 0xb5c8145e53a6a127d611f45f602666ec/list.swap_head(A, xs)) == List.length(&2, A, xs) : Nat}

Permutation preserves length.

def internal_swap_at_length source · line 310 · raw

@-A:Data -> @+i:Nat -> @+xs:List<&2, A> -> {List.length(&2, A, 0xb5c8145e53a6a127d611f45f602666ec/list.swap_at(A, i, xs)) == List.length(&2, A, xs) : Nat}

def internal_apply_length source · line 322 · raw

@-A:Data -> @+s:List<&2, Nat> -> @+xs:List<&2, A> -> {List.length(&2, A, 0xb5c8145e53a6a127d611f45f602666ec/list.apply(A, s, xs)) == List.length(&2, A, xs) : Nat}

def internal_length_eq source · line 329 · raw

@-A:Data -> @+s:List<&2, Nat> -> @+xs:List<&2, A> -> @-ys:List<&2, A> -> @e:0xb5c8145e53a6a127d611f45f602666ec/list.perm_steps(A, s, xs, ys) -> {List.length(&2, A, ys) == List.length(&2, A, xs) : Nat}

def perm_length source · line 333 · raw

@-A:Data -> @+xs:List<&2, A> -> @-ys:List<&2, A> -> @h:0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, ys) -> {List.length(&2, A, ys) == List.length(&2, A, xs) : Nat}

def internal_perm_nil_nat source · line 337 · raw

0xb5c8145e53a6a127d611f45f602666ec/list.perm(Nat, [], [])

def internal_perm_dup_nat source · line 340 · raw

@+xs:List<&2, Nat> -> @-ys:List<&2, Nat> -> @h:0xb5c8145e53a6a127d611f45f602666ec/list.perm(Nat, xs, ys) -> Pair(0xb5c8145e53a6a127d611f45f602666ec/list.perm(Nat, xs, ys), 0xb5c8145e53a6a127d611f45f602666ec/list.perm(Nat, xs, ys))

def internal_perm_sym_nat source · line 343 · raw

@+xs:List<&2, Nat> -> @-ys:List<&2, Nat> -> @h:0xb5c8145e53a6a127d611f45f602666ec/list.perm(Nat, xs, ys) -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(Nat, ys, xs)

def internal_perm_length_nat source · line 346 · raw

@+xs:List<&2, Nat> -> @-ys:List<&2, Nat> -> @h:0xb5c8145e53a6a127d611f45f602666ec/list.perm(Nat, xs, ys) -> {List.length(&2, Nat, ys) == List.length(&2, Nat, xs) : Nat}

Templates

template insert_by source · line 68 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+x:A -> @xs:List<&2, A> -> List<&2, A>

Insertion into a list, generic comparator (structural, Base-only branching via Bool.pick).

template isort_by source · line 75 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @xs:List<&2, A> -> List<&2, A>

template insert_by_perm source · line 90 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+x:A -> @+xs:List<&2, A> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, x <> xs, insert_by(A, le, x, xs))

Inserting x into xs permutes x <> xs.

template isort_by_perm source · line 98 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+xs:List<&2, A> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, isort_by(A, le, xs))

Insertion sort permutes its input.

template merge_by source · line 129 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @xs:List<&2, A> -> @ys:List<&2, A> -> List<&2, A>

template merge_by_perm source · line 146 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, List.append(&2, A, xs, ys), merge_by(A, le, xs, ys))

Merging permutes the concatenation.

template msort_by source · line 221 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @fuel:Nat -> @+xs:List<&2, A> -> List<&2, A>

Merge sort with fuel (the fuel only bounds recursion; it never affects the permutation).

template msort_by_perm source · line 229 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @fuel:Nat -> @+xs:List<&2, A> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, msort_by(A, le, fuel, xs))

Merge sort permutes its input, for any fuel.

template sort_by source · line 236 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+xs:List<&2, A> -> List<&2, A>

template sort_by_perm source · line 240 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+xs:List<&2, A> -> 0xb5c8145e53a6a127d611f45f602666ec/list.perm(A, xs, sort_by(A, le, xs))

The sort permutes its input.