~/bend-docscommunity

perm.bend checks

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

bend-mathlib/perm.bend: step-list permutations over bendlib-kernel-list, plus sort value defs and proofs. Resolves the published kernel bendlib-kernel-list@1.0.0.0 by its content hash; 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 83 · 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 107 · raw

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

Insertion sort permutes a Nat list.

def internal_append_nil source · line 110 · raw

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

def perm_append_nil source · line 119 · 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 123 · 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 140 · 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 158 · 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))

Merging two Nat lists permutes their concatenation.

def perm_move_rev source · line 162 · 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 170 · 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 178 · 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 gives a permutation of the append.

def perm_append source · line 186 · 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 gives a permutation of the append.

def evens source · line 190 · raw

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

The elements of a list at even positions (0, 2, 4, ...).

def odds source · line 202 · raw

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

The elements of a list at odd positions (1, 3, 5, ...).

def split_perm source · line 214 · 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 250 · raw

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

Merge sort permutes a Nat list.

def internal_sort_nat_test source · line 253 · 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 256 · 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 267 · 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 279 · raw

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

def internal_apply_invert source · line 286 · 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 295 · 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 300 · 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 305 · raw

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

def internal_swap_at_length source · line 316 · 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 328 · 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 335 · 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 340 · 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}

Permutation preserves length.

def internal_perm_nil_nat source · line 344 · raw

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

def internal_perm_dup_nat source · line 347 · 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 350 · 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 353 · 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 76 · raw

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

Insertion sort by the comparator le.

template insert_by_perm source · line 91 · 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 99 · 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 131 · raw

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

Merges two lists, taking the head of xs first whenever le(x, y) holds.

template merge_by_perm source · line 148 · 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 226 · 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 234 · 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 242 · raw

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

Merge sort by the comparator le.

template sort_by_perm source · line 246 · 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.