~/bend-docscommunity

sort.bend checks

raw source on the hub · import bend-mathlib@0.7.1.0/sort.bend as Sort

bend-mathlib/sort.bend: insertion and merge sort proved sorted over perm.bend's value defs (generic ~le).

4 imports
import Base
import ./nat.bend as MNat
import ./list.bend as MList
import ./perm.bend as MPerm

Definitions

def internal_le_flip_nat source · line 27 · raw

@x:Nat -> @y:Nat -> @e:{Nat.is_le(x, y) == False{} : Bool} -> {Nat.is_le(y, x) == True{} : Bool}

def internal_le_trans_nat source · line 38 · raw

@x:Nat -> @y:Nat -> @z:Nat -> @xy:{Nat.is_le(x, y) == True{} : Bool} -> @yz:{Nat.is_le(y, z) == True{} : Bool} -> {Nat.is_le(x, z) == True{} : Bool}

def isort_by_sorted_nat source · line 79 · raw

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

Insertion sort returns a sorted Nat list.

def merge_by_sorted_nat source · line 150 · raw

@+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> @hx:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(Nat, Nat.is_le, xs) -> @hy:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(Nat, Nat.is_le, ys) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(Nat, Nat.is_le, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.merge_by(Nat, Nat.is_le, xs, ys))

Merging two sorted Nat lists gives a sorted list.

def msort_by_sorted_nat source · line 263 · raw

@+xs:List<&2, Nat> -> @+h:{Nat.is_le(List.length(&2, Nat, xs), 1n+List.length(&2, Nat, xs)) == True{} : Bool} -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(Nat, Nat.is_le, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.msort_by(Nat, Nat.is_le, List.length(&2, Nat, xs), xs))

Merge sort with fuel = length returns a sorted Nat list (h always holds; sort_by_sorted_nat needs no h).

def sort_by_sorted_nat source · line 267 · raw

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

Merge sort returns a sorted Nat list.

Templates

template internal_sorted_single source · line 7 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+x:A -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, [x])

template internal_sorted_cons_cons_intro source · line 10 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+x:A -> @+y:A -> @+t:List<&2, A> -> @hxy:{le(x, y) == True{} : Bool} -> @hyt:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, y <> t) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, x <> y <> t)

template internal_sorted_cons_cons_elim_le source · line 14 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+x:A -> @+y:A -> @+t:List<&2, A> -> @h:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, x <> y <> t) -> {le(x, y) == True{} : Bool}

template internal_sorted_cons_cons_elim_tail source · line 17 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+x:A -> @+y:A -> @+t:List<&2, A> -> @h:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, x <> y <> t) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, y <> t)

template internal_sorted_tail source · line 20 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+x:A -> @+xs:List<&2, A> -> @h:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, x <> xs) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, xs)

template internal_cons_ins_step source · line 41 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_total:(@x:A -> @y:A -> @_:{le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}) -> @b:Bool -> @+y:A -> @+x:A -> @+z:A -> @+u:List<&2, A> -> @e:{le(x, z) == b : Bool} -> @hyx:{le(y, x) == True{} : Bool} -> @+h:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, y <> z <> u) -> @k:(@_:{le(z, x) == True{} : Bool} -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, z <> 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.insert_by(A, le, x, u))) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, y <> Bool.pick(List<&2, A>, b, x <> z <> u, z <> 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.insert_by(A, le, x, u)))

template internal_sorted_cons_ins source · line 48 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_total:(@x:A -> @y:A -> @_:{le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}) -> @+t:List<&2, A> -> @+y:A -> @+x:A -> @hyx:{le(y, x) == True{} : Bool} -> @+h:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, y <> t) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, y <> 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.insert_by(A, le, x, t))

template internal_insert_step source · line 55 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_total:(@x:A -> @y:A -> @_:{le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}) -> @b:Bool -> @+x:A -> @+y:A -> @+t:List<&2, A> -> @e:{le(x, y) == b : Bool} -> @+h:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, y <> t) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, Bool.pick(List<&2, A>, b, x <> y <> t, y <> 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.insert_by(A, le, x, t)))

template insert_by_sorted source · line 63 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_total:(@x:A -> @y:A -> @_:{le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}) -> @+x:A -> @+xs:List<&2, A> -> @+h:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, xs) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.insert_by(A, le, x, xs))

Inserting into a sorted list keeps it sorted, for a total comparator.

template isort_by_sorted source · line 71 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_total:(@x:A -> @y:A -> @_:{le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}) -> @+xs:List<&2, A> -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.isort_by(A, le, xs))

Insertion sort returns a sorted list.

template internal_least source · line 82 · raw

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

template internal_least_intro source · line 85 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+lo:A -> @+h:A -> @+t:List<&2, A> -> @hh:{le(lo, h) == True{} : Bool} -> @ht:internal_least(A, le, lo, t) -> internal_least(A, le, lo, h <> t)

template internal_least_cons_le source · line 89 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+lo:A -> @+h:A -> @+t:List<&2, A> -> @hh:internal_least(A, le, lo, h <> t) -> {le(lo, h) == True{} : Bool}

template internal_least_cons_tail source · line 92 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+lo:A -> @+h:A -> @+t:List<&2, A> -> @hh:internal_least(A, le, lo, h <> t) -> internal_least(A, le, lo, t)

template internal_least_trans source · line 95 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_trans:(@x:A -> @y:A -> @z:A -> @_:{le(x, y) == True{} : Bool} -> @_:{le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}) -> @+a:A -> @+b:A -> @+xs:List<&2, A> -> @+hab:{le(a, b) == True{} : Bool} -> @+hb:internal_least(A, le, b, xs) -> internal_least(A, le, a, xs)

template internal_sorted_least_head source · line 102 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_trans:(@x:A -> @y:A -> @z:A -> @_:{le(x, y) == True{} : Bool} -> @_:{le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}) -> @+xs:List<&2, A> -> @+x:A -> @+h:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, x <> xs) -> internal_least(A, le, x, xs)

template internal_sorted_cons_of_least source · line 109 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+lo:A -> @+m:List<&2, A> -> @hl:internal_least(A, le, lo, m) -> @hm:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, m) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, lo <> m)

template internal_least_merge_pick source · line 116 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+lo:A -> @b:Bool -> @+x:A -> @+xt:List<&2, A> -> @+y:A -> @+yt:List<&2, A> -> @hx:internal_least(A, le, lo, x <> xt) -> @hy:internal_least(A, le, lo, y <> yt) -> @hm1:internal_least(A, le, lo, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.merge_by(A, le, xt, y <> yt)) -> @hm2:internal_least(A, le, lo, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.merge_by(A, le, x <> xt, yt)) -> internal_least(A, le, lo, Bool.pick(List<&2, A>, b, x <> 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.merge_by(A, le, xt, y <> yt), y <> 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.merge_by(A, le, x <> xt, yt)))

template internal_least_merge source · line 123 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+lo:A -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+hx:internal_least(A, le, lo, xs) -> @+hy:internal_least(A, le, lo, ys) -> internal_least(A, le, lo, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.merge_by(A, le, xs, ys))

template internal_merge_sorted_pick source · line 132 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_trans:(@x:A -> @y:A -> @z:A -> @_:{le(x, y) == True{} : Bool} -> @_:{le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}) -> @-le_total:(@x:A -> @y:A -> @_:{le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}) -> @b:Bool -> @+x:A -> @+xt:List<&2, A> -> @+y:A -> @+yt:List<&2, A> -> @+e:{le(x, y) == b : Bool} -> @hx:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, x <> xt) -> @hy:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, y <> yt) -> @hm1:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.merge_by(A, le, xt, y <> yt)) -> @hm2:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.merge_by(A, le, x <> xt, yt)) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, Bool.pick(List<&2, A>, b, x <> 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.merge_by(A, le, xt, y <> yt), y <> 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.merge_by(A, le, x <> xt, yt)))

template merge_by_sorted source · line 140 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_trans:(@x:A -> @y:A -> @z:A -> @_:{le(x, y) == True{} : Bool} -> @_:{le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}) -> @-le_total:(@x:A -> @y:A -> @_:{le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}) -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+hx:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, xs) -> @+hy:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, ys) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.merge_by(A, le, xs, ys))

Merging two sorted lists is sorted (needs transitivity, and totality for the un-taken branch).

template internal_length_zero source · line 153 · raw

@-A:Data -> @+xs:List<&2, A> -> @e:{List.length(&2, A, xs) == 0n : Nat} -> {xs == [] : List<&2, A>}

template internal_sorted_short source · line 160 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+xs:List<&2, A> -> @h:0x3c446c5bcf57d1eef89775ba0b411fc6/nat.le(List.length(&2, A, xs), 1n) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, xs)

template internal_length_evens_le source · line 172 · raw

@-A:Data -> @+xs:List<&2, A> -> {Nat.is_le(List.length(&2, A, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.evens(A, xs)), List.length(&2, A, xs)) == True{} : Bool}

template internal_length_odds_le source · line 183 · raw

@-A:Data -> @+xs:List<&2, A> -> {Nat.is_le(List.length(&2, A, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.odds(A, xs)), List.length(&2, A, xs)) == True{} : Bool}

template internal_least_evens source · line 194 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+xs:List<&2, A> -> @+lo:A -> @+h:internal_least(A, le, lo, xs) -> internal_least(A, le, lo, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.evens(A, xs))

template internal_least_odds source · line 205 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+xs:List<&2, A> -> @+lo:A -> @+h:internal_least(A, le, lo, xs) -> internal_least(A, le, lo, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.odds(A, xs))

template internal_evens_sorted source · line 216 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_trans:(@x:A -> @y:A -> @z:A -> @_:{le(x, y) == True{} : Bool} -> @_:{le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}) -> @+xs:List<&2, A> -> @+h:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, xs) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.evens(A, xs))

template internal_odds_sorted source · line 227 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_trans:(@x:A -> @y:A -> @z:A -> @_:{le(x, y) == True{} : Bool} -> @_:{le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}) -> @+xs:List<&2, A> -> @+h:0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, xs) -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.odds(A, xs))

template msort_by_sorted source · line 239 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_trans:(@x:A -> @y:A -> @z:A -> @_:{le(x, y) == True{} : Bool} -> @_:{le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}) -> @-le_total:(@x:A -> @y:A -> @_:{le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}) -> @fuel:Nat -> @+xs:List<&2, A> -> @+h:{Nat.is_le(List.length(&2, A, xs), 1n+fuel) == True{} : Bool} -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.msort_by(A, le, fuel, xs))

Merge sort returns a sorted list once the fuel reaches the input length (invariant: length <= fuel+1).

template sort_by_sorted source · line 255 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_trans:(@x:A -> @y:A -> @z:A -> @_:{le(x, y) == True{} : Bool} -> @_:{le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}) -> @-le_total:(@x:A -> @y:A -> @_:{le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}) -> @+xs:List<&2, A> -> 0x3c446c5bcf57d1eef89775ba0b411fc6/list.sorted_by(A, le, 0x3c446c5bcf57d1eef89775ba0b411fc6/perm.sort_by(A, le, xs))

Merge sort of the full-length fuel sorts its input.