proofs/containers/binary_heap/pop.bend checks

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

20 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 ../../lib/u32.bend as U
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 ../../../src/containers/types/binary_heap.bend as E
import ./idx.bend as IX
import ./u32idx.bend as UX
import ./slots.bend as SL
import ./vals.bend as V
import ./multiset.bend as M
import ./root.bend as RT
import ./up.bend as UPS
import ./down.bend as DN
import ./state.bend as ST

Definitions

def scale_double source · line 28 · raw

@f:Nat -> @+m:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.scale(f, Nat.double(m)) == Nat.double(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.scale(f, m)) : Nat}

def scale_one source · line 35 · raw

@d:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.scale(d, 1n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d) : Nat}

def half_ge1 source · line 44 · raw

@k:Nat -> @+h:{Nat.is_le(2n, k) == True{} : Bool} -> {Nat.is_le(1n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.half(k)) == True{} : Bool}

def par_pos source · line 54 · raw

@j:Nat -> @+hj:{Nat.is_le(1n, j) == True{} : Bool} -> @+hkf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, 0n) == False{} : Bool} -> {Nat.is_le(1n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)) == True{} : Bool}

not a child of the root and positive => the parent is positive too

def round_lt source · line 178 · raw

@+m:Nat -> @+d:Nat -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hm:{Nat.is_lt(m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(U32.to_nat(U32.from_nat(m)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool}

Templates

template hole source · line 67 · raw

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

template hole_at0 source · line 70 · raw

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

template hole_off source · line 73 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+last:A -> @+j:Nat -> @+hj0:{Nat.is_eq(0n, j) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, hole(A, ss, m, last), j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, j) : Maybe<&2, A>}

template pop_pair source · line 78 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+last:A -> @j:Nat -> @+hjm:{Nat.is_lt(j, m) == True{} : Bool} -> @+hkf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, 0n) == False{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, ss, 1n+m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_ok(A, cmp, hole(A, ss, m, last), j) == True{} : Bool}

template pop_skip source · line 88 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+last:A -> @+j:Nat -> @+hjm:{Nat.is_lt(j, m) == True{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, ss, 1n+m) == True{} : Bool} -> @b:Bool -> @+eb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_of(j, 0n) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.pair_skip2(A, cmp, hole(A, ss, m, last), j, 0n) == True{} : Bool}

template pop_exc source · line 95 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+last:A -> @k:Nat -> @+hk:{Nat.is_le(k, m) == True{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, ss, 1n+m) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_exc2(A, cmp, hole(A, ss, m, last), k, 0n) == True{} : Bool}

template pop_some source · line 106 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+last:A -> @j:Nat -> @+hjm:{Nat.is_lt(j, m) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ss, 1n+m) == True{} : Bool} -> @+hlen:{Nat.is_lt(0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, A>, ss)) == True{} : Bool} -> {Maybe.is_some(&2, A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, hole(A, ss, m, last), j)) == True{} : Bool}

template pop_lay source · line 115 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+last:A -> @k:Nat -> @+hk:{Nat.is_le(k, m) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ss, 1n+m) == True{} : Bool} -> @+hlen:{Nat.is_lt(0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, A>, ss)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, hole(A, ss, m, last), k) == True{} : Bool}

template pop_kid source · line 126 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+root:A -> @+c:Nat -> @+hm:{Nat.is_lt(0n, m) == True{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, ss, 1n+m) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, ss, 1n+m) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, 0n) == Some{root} : Maybe<&2, A>} -> @b:Bool -> @+eb:{Nat.is_lt(c, m) == b : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.kid_le(A, cmp, ss, m, 0n, c) == True{} : Bool}

template pop_kids source · line 135 · raw

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

template pop_ms source · line 142 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+root:A -> @+last:A -> @+hm:{Nat.is_lt(0n, m) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, 0n) == Some{root} : Maybe<&2, A>} -> @+hlast:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, m) == Some{last} : 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, root, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, hole(A, ss, m, last), m))) : List<&2, A>}

template pop_low_at source · line 150 · raw

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

template pop_low source · line 160 · raw

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

template pop_split source · line 171 · raw

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

The observation of a pop: the multiset of the heap is the old root followed by the multiset the sift-down is given as its target.

template round_nth source · line 181 · raw

@-A:Data -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+m:Nat -> @+d:Nat -> @+v:A -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hm:{Nat.is_lt(m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), m) == Some{v} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), U32.to_nat(U32.from_nat(m))) == Some{Some{v}} : Maybe<&2, Maybe<&2, A>>}

template get_last source · line 186 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+m:Nat -> @+last:A -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hm:{Nat.is_lt(m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+hlast:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), m) == Some{last} : Maybe<&2, A>} -> {Array.get(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), U32.from_nat(m)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), Some{last}) : Pair(Array<Maybe<&2, A>>, Maybe<&2, A>)}

the last element is read, not cleared

template get_root source · line 189 · raw

@-A:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+root:A -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, d, t) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>} -> {Array.get(Maybe<&2, A>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), 0) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), Some{root}) : Pair(Array<Maybe<&2, A>>, Maybe<&2, A>)}

template pop_to_move source · line 196 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+depth:Nat -> @+m:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+root:A -> @+last:A -> @+hd:{Nat.is_le(depth, 31n) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, depth, t) == True{} : Bool} -> @+hs:{Nat.is_le(1n+m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>} -> @+hlast:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), m) == Some{last} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.pop(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{1n+m, depth, t})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.pop_move(A, cmp, m, U32.from_nat(m), depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(depth), root, last, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), U32.is_eq(U32.from_nat(m), 0)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Error, A>)}

The pop of a nonempty heap, reduced to the move that follows reading the last element. Each step is an explicit substitution rather than a rewrite annotation: the goal is normalised between steps, so naming the redex is the only robust way to transport it.

template pop_sift source · line 218 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+depth:Nat -> @+m:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+root:A -> @+last:A -> @+hd:{Nat.is_le(depth, 31n) == True{} : Bool} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, A>, depth, t) == True{} : Bool} -> @+hs:{Nat.is_le(1n+m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == True{} : Bool} -> @+hho:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.ho_upto(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 1n+m) == True{} : Bool} -> @+hlay:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.lay(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 1n+m) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>} -> @+hlast:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), m) == Some{last} : Maybe<&2, A>} -> @+hm:{Nat.is_lt(0n, m) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/down.SiftDownOK(A, cmp, depth, m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, hole(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), m, last), m)), depth, t, 0n, last)

template PopRes source · line 237 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<A> -> Type

template pop_from source · line 240 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+depth:Nat -> @+m:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+root:A -> @+last:A -> @+tgt:List<&2, A> -> @+hd:{Nat.is_le(depth, 31n) == True{} : Bool} -> @+hs:{Nat.is_le(1n+m, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(depth)) == True{} : Bool} -> @+eq0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.pop(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{1n+m, depth, t})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.pop_move(A, cmp, m, U32.from_nat(m), depth, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32.pow2u(depth), root, last, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, A>, t), False{}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<A>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Error, A>)} -> @+hsplit:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{1n+m, depth, t}) == root <> tgt : List<&2, A>} -> @r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/down.SiftDownOK(A, cmp, depth, m, tgt, depth, t, 0n, last) -> PopRes(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{1n+m, depth, t})

template pop_nonempty source · line 252 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+depth:Nat -> @m:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+root:A -> @+last:A -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{1n+m, depth, t}) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>} -> @+hlast:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), m) == Some{last} : Maybe<&2, A>} -> PopRes(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{1n+m, depth, t})

template pop_with_last source · line 280 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+depth:Nat -> @+m:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+root:A -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{1n+m, depth, t}) == True{} : Bool} -> @+h0:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>} -> @sig:Sigma<&1, &1, A, v => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), m) == Some{v} : Maybe<&2, A>}> -> PopRes(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{1n+m, depth, t})

template pop_with_root source · line 285 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+depth:Nat -> @+m:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{1n+m, depth, t}) == True{} : Bool} -> @sig:Sigma<&1, &1, A, v => {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, A>, t), 0n) == Some{v} : Maybe<&2, A>}> -> PopRes(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{1n+m, depth, t})

template pop_ok source · line 291 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+size:Nat -> @+depth:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, A>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t}) == True{} : Bool} -> PopRes(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Sh{size, depth, t})