~/bend-docscommunity

proofs/containers/binary_heap/vals.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/vals.bend as Vals

10 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/order.bend as O
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/binary_heap.bend as S
import ./multiset.bend as M
import ./idx.bend as IX
import ./slots.bend as SL

Templates

template cons_slot source · line 17 · raw

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

template vals source · line 24 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @n:Nat -> List<&2, A>

template msort source · line 31 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @xs:List<&2, A> -> List<&2, A>

template vals_above source · line 40 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+i:Nat -> @+v:Maybe<&2, A> -> @m:Nat -> @+h:{Nat.is_le(m, i) == True{} : Bool} -> {vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ss, i, v), m) == vals(A, ss, m) : List<&2, A>}

template none_not_some source · line 50 · raw

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

template nth_of_slot_go source · line 53 · raw

@-A:Data -> @+old:A -> @m:Maybe<&2, Maybe<&2, A>> -> @+hold:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.unwrap(A, m) == Some{old} : Maybe<&2, A>} -> {m == Some{Some{old}} : Maybe<&2, Maybe<&2, A>>}

template nth_of_slot source · line 60 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+i:Nat -> @+old:A -> @+hold:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, i) == Some{old} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Maybe<&2, A>, ss, i) == Some{Some{old}} : Maybe<&2, Maybe<&2, A>>}

template slot_in_range source · line 63 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+i:Nat -> @+old:A -> @+hold:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, i) == Some{old} : Maybe<&2, A>} -> {Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, A>, ss)) == True{} : Bool}

template ins_set_same source · line 66 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+i:Nat -> @+old:A -> @+v:A -> @+hold:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, i) == Some{old} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, old, msort(A, cmp, vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ss, i, Some{v}), 1n+i))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, v, msort(A, cmp, vals(A, ss, 1n+i))) : List<&2, A>}

template ins_set_top source · line 73 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+i:Nat -> @+old:A -> @+v:A -> @+ei:{i == m : Nat} -> @+hold:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, i) == Some{old} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, old, msort(A, cmp, vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ss, i, Some{v}), 1n+m))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, v, msort(A, cmp, vals(A, ss, 1n+m))) : List<&2, A>}

template ins_set_cons source · line 77 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @s:Maybe<&2, A> -> @+old:A -> @+v:A -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, old, msort(A, cmp, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, v, msort(A, cmp, ys)) : List<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, old, msort(A, cmp, cons_slot(A, s, xs))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, v, msort(A, cmp, cons_slot(A, s, ys))) : List<&2, A>}

template ins_set source · line 86 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @n:Nat -> @+i:Nat -> @+old:A -> @+v:A -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> @+hold:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, i) == Some{old} : Maybe<&2, A>} -> @b:Bool -> @+eb:{Nat.is_eq(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat.pred(n)) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, old, msort(A, cmp, vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ss, i, Some{v}), n))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, v, msort(A, cmp, vals(A, ss, n))) : List<&2, A>}