~/bend-docscommunity

proofs/containers/binary_heap/grow.bend checks

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

12 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/binary_heap.bend as S
import ../../../src/containers/binary_heap.bend as H
import ./idx.bend as IX
import ./slots.bend as SL
import ./vals.bend as V
import ./root.bend as RT

Templates

template slots_grown source · line 18 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.TNode{t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(Maybe<&2, A>, d, None{})}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), None{})) : List<&2, Maybe<&2, A>>}

template slot_left source · line 23 · raw

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

A slot inside the old block reads the same through the appended one.

template lay_grow source · line 26 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+ys:List<&2, Maybe<&2, A>> -> @k:Nat -> @+hk:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, A>, ss)) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ss, k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, A>, ss, ys), k) == True{} : Bool}

template pair_grow source · line 37 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+ys:List<&2, Maybe<&2, A>> -> @m:Nat -> @+hm:{Nat.is_lt(m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, A>, ss)) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, ss, m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, A>, ss, ys), m) == True{} : Bool}

one heap-order pair, read through the appended block

template ho_grow source · line 46 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+ys:List<&2, Maybe<&2, A>> -> @k:Nat -> @+hk:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, A>, ss)) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, ss, k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, A>, ss, ys), k) == True{} : Bool}

template vals_grow source · line 55 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+ys:List<&2, Maybe<&2, A>> -> @k:Nat -> @+hk:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, A>, ss)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, A>, ss, ys), k) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ss, k) : List<&2, A>}

template gtree source · line 65 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>>

template gtree_perfect source · line 68 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, 1n+d, gtree(A, d, t)) == True{} : Bool}

template gtree_real source · line 71 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.grown(A, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, gtree(A, d, t)) : Array<Maybe<&2, A>>}

template gtree_lay source · line 74 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+k:Nat -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hk:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, gtree(A, d, t)), k) == True{} : Bool}

template gtree_ho source · line 79 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+k:Nat -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hk:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, gtree(A, d, t)), k) == True{} : Bool}

template gtree_vals source · line 84 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+k:Nat -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hk:{Nat.is_le(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, gtree(A, d, t)), k) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), k) : List<&2, A>}