~/bend-docscommunity

proofs/containers/binary_heap/root.bend checks

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

11 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 ./idx.bend as IX
import ./slots.bend as SL
import ./vals.bend as V
import ./multiset.bend as M

Templates

template low_all source · line 22 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @n:Nat -> @+x:A -> Bool

template mle_mid source · line 31 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+a:A -> @m:Maybe<&2, A> -> @b:Maybe<&2, A> -> @+y:A -> @+hm:{m == Some{y} : Maybe<&2, A>} -> @+h1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, Some{a}, m) == True{} : Bool} -> @+h2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, m, b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, Some{a}, b) == True{} : Bool}

template root_at source · line 36 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+root:A -> @+c:Nat -> @b:Maybe<&2, A> -> @sig:Sigma<&1, &1, A, v => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(c)) == Some{v} : Maybe<&2, A>}> -> @+h1:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, Some{root}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(c))) == True{} : Bool} -> @+h2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(c)), b) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, Some{root}, b) == True{} : Bool}

template root_le source · line 43 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @fuel:Nat -> @+root:A -> @j:Nat -> @+hj:{Nat.is_lt(j, n) == True{} : Bool} -> @+hjf:{Nat.is_le(j, fuel) == True{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, ss, n) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ss, n) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, 0n) == Some{root} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, Some{root}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, j)) == True{} : Bool}

Walking up the parent chain: the fuel is an upper bound on the index, and the parent of a positive index is strictly smaller.

template low_all_mk source · line 59 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @k:Nat -> @+root:A -> @+hk:{Nat.is_le(k, n) == True{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, ss, n) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ss, n) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, 0n) == Some{root} : Maybe<&2, A>} -> {low_all(A, cmp, ss, k, root) == True{} : Bool}

template all_ge_cons source · line 70 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+z:A -> @m:Maybe<&2, A> -> @+xs:List<&2, A> -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, Some{z}, m) == True{} : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.all_ge(A, cmp, z, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.all_ge(A, cmp, z, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.cons_slot(A, m, xs)) == True{} : Bool}

template all_ge_vals source · line 77 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @n:Nat -> @+z:A -> @+h:{low_all(A, cmp, ss, n, z) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.all_ge(A, cmp, z, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ss, n)) == True{} : Bool}

template all_ge_msort source · line 86 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+z:A -> @xs:List<&2, A> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.all_ge(A, cmp, z, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.all_ge(A, cmp, z, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, xs)) == True{} : Bool}

template front source · line 97 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+k:Nat -> @+z:A -> @+h:{low_all(A, cmp, ss, k, z) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, z, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ss, k))) == z <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ss, k)) : List<&2, A>}

x is not larger than any slot of [0, k) => it comes first in the multiset.

template length_ins_c source · line 103 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+x:A -> @+h:A -> @+t:List<&2, A> -> @+b:Bool -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, h) == b : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, t)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, t) : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, h <> t)) == 2n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, t) : Nat}

template length_ins source · line 112 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+x:A -> @+xs:List<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, x, xs)) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs) : Nat}

template msort_length source · line 119 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @xs:List<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, xs)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs) : Nat}

template vals_length_c source · line 128 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @s:Maybe<&2, A> -> @+es:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, m) == s : Maybe<&2, A>} -> @+hs:{Maybe.is_some(&2, A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, m)) == True{} : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ss, m)) == m : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ss, 1n+m)) == 1n+m : Nat}

template vals_length source · line 136 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @n:Nat -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ss, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ss, n)) == n : Nat}

template model_length source · line 145 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ss, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ss, n))) == n : Nat}

template ins_del_cons source · line 156 · raw

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

template ins_del_top source · line 165 · raw

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

template ins_del source · line 175 · 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 -> @+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/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ss, n)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, old, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ss, i, None{}), n))) : List<&2, A>}

template low_del_at source · line 189 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @j:Nat -> @+root:A -> @+hjn:{Nat.is_lt(j, n) == True{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, ss, n) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ss, n) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, 0n) == Some{root} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.mle(A, cmp, Some{root}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ss, 0n, None{}), j)) == True{} : Bool}

template low_del source · line 198 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @k:Nat -> @+root:A -> @+hk:{Nat.is_le(k, n) == True{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, ss, n) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ss, n) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, 0n) == Some{root} : Maybe<&2, A>} -> {low_all(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ss, 0n, None{}), k, root) == True{} : Bool}

template head_root source · line 207 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @+root:A -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, ss, n) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ss, n) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, 0n) == Some{root} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ss, n)) == root <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ss, 0n, None{}), n)) : List<&2, A>}