~/bend-docscommunity

proofs/containers/binary_heap/slots.bend checks

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

8 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

Definitions

def flip_eq source · line 87 · raw

@c:Cmp -> @+h:{Cmp.is_eq(c) == False{} : Bool} -> {Cmp.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.flipc(c)) == False{} : Bool}

def ne_sym source · line 96 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_eq(b, a) == False{} : Bool} -> {Nat.is_eq(a, b) == False{} : Bool}

def kid_of source · line 253 · raw

@+m:Nat -> @+i:Nat -> Bool

def or_false source · line 302 · raw

@a:Bool -> @b:Bool -> @+ea:{a == False{} : Bool} -> @+eb:{b == False{} : Bool} -> {Bool.or(a, b) == False{} : Bool}

Templates

template unwrap source · line 19 · raw

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

template slot source · line 26 · raw

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

template mle source · line 31 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @a:Maybe<&2, A> -> @b:Maybe<&2, A> -> Bool

Order between two slots; vacuously true when a slot is empty (the layout invariant is what says the slots of interest are occupied).

template pair_ok source · line 38 · raw

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

template ho_upto source · line 46 · raw

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

Heap order over the children 0 .. k-1 (index 0 has no parent condition).

template lay source · line 54 · raw

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

Every slot of [0, k) is occupied.

template ho_get_eq source · line 63 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+j:Nat -> @+e:{Nat.is_eq(j, m) == True{} : Bool} -> @+hp:{pair_ok(A, cmp, ss, m) == True{} : Bool} -> {pair_ok(A, cmp, ss, j) == True{} : Bool}

template ho_get source · line 66 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @k:Nat -> @+j:Nat -> @+h:{ho_upto(A, cmp, ss, k) == True{} : Bool} -> @+hj:{Nat.is_lt(j, k) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat.pred(k)) == b : Bool} -> {pair_ok(A, cmp, ss, j) == True{} : Bool}

template ho_at source · line 75 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+k:Nat -> @+j:Nat -> @+h:{ho_upto(A, cmp, ss, k) == True{} : Bool} -> @+hj:{Nat.is_lt(j, k) == True{} : Bool} -> {pair_ok(A, cmp, ss, j) == True{} : Bool}

template slot_same source · line 80 · raw

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

template slot_other source · line 84 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+i:Nat -> @+j:Nat -> @+v:Maybe<&2, A> -> @+ne:{Nat.is_eq(i, j) == False{} : Bool} -> {slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ss, i, v), j) == slot(A, ss, j) : Maybe<&2, A>}

template mle_some source · line 102 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+x:A -> @+y:A -> @+h:{mle(A, cmp, Some{x}, Some{y}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, y) == True{} : Bool}

template mle_mk source · line 105 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+x:A -> @+y:A -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, x, y) == True{} : Bool} -> {mle(A, cmp, Some{x}, Some{y}) == True{} : Bool}

template mle_none_l source · line 108 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+b:Maybe<&2, A> -> {mle(A, cmp, None{}, b) == True{} : Bool}

template mle_none_r source · line 115 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+a:Maybe<&2, A> -> {mle(A, cmp, a, None{}) == True{} : Bool}

template mle_trans source · line 124 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @a:Maybe<&2, A> -> @+y:A -> @c:Maybe<&2, A> -> @+hab:{mle(A, cmp, a, Some{y}) == True{} : Bool} -> @+hbc:{mle(A, cmp, Some{y}, c) == True{} : Bool} -> {mle(A, cmp, a, c) == True{} : Bool}

transitivity through an OCCUPIED middle slot (with an empty middle there is nothing to conclude: mle is vacuous there)

template lay_get_eq source · line 138 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+j:Nat -> @+e:{Nat.is_eq(j, m) == True{} : Bool} -> @+hp:{Maybe.is_some(&2, A, slot(A, ss, m)) == True{} : Bool} -> {Maybe.is_some(&2, A, slot(A, ss, j)) == True{} : Bool}

template lay_get source · line 141 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @k:Nat -> @+j:Nat -> @+h:{lay(A, ss, k) == True{} : Bool} -> @+hj:{Nat.is_lt(j, k) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat.pred(k)) == b : Bool} -> {Maybe.is_some(&2, A, slot(A, ss, j)) == True{} : Bool}

template lay_at source · line 150 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+k:Nat -> @+j:Nat -> @+h:{lay(A, ss, k) == True{} : Bool} -> @+hj:{Nat.is_lt(j, k) == True{} : Bool} -> {Maybe.is_some(&2, A, slot(A, ss, j)) == True{} : Bool}

template slot_some source · line 154 · raw

@-A:Data -> @m:Maybe<&2, A> -> @+h:{Maybe.is_some(&2, A, m) == True{} : Bool} -> Sigma<&1, &1, A, v => {m == Some{v} : Maybe<&2, A>}>

An occupied slot, as a value.

template nth_slot source · line 163 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, A>, ss)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Maybe<&2, A>, ss, j) == Some{slot(A, ss, j)} : Maybe<&2, Maybe<&2, A>>}

template pair_skip source · line 178 · raw

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

template ho_exc source · line 181 · raw

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

template skip_at source · line 188 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+i:Nat -> @+hne:{Nat.is_eq(m, i) == False{} : Bool} -> @+h:{pair_skip(A, cmp, ss, m, i) == True{} : Bool} -> {pair_ok(A, cmp, ss, m) == True{} : Bool}

template skip_eq source · line 191 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+i:Nat -> @+eb:{Nat.is_eq(m, i) == True{} : Bool} -> {pair_skip(A, cmp, ss, m, i) == True{} : Bool}

template skip_ne source · line 195 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+i:Nat -> @+eb:{Nat.is_eq(m, i) == False{} : Bool} -> @+h:{pair_ok(A, cmp, ss, m) == True{} : Bool} -> {pair_skip(A, cmp, ss, m, i) == True{} : Bool}

template exc_get source · line 199 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @k:Nat -> @+i:Nat -> @+j:Nat -> @+h:{ho_exc(A, cmp, ss, k, i) == True{} : Bool} -> @+hj:{Nat.is_lt(j, k) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat.pred(k)) == b : Bool} -> {pair_skip(A, cmp, ss, j, i) == True{} : Bool}

template exc_at source · line 209 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+k:Nat -> @+i:Nat -> @+j:Nat -> @+h:{ho_exc(A, cmp, ss, k, i) == True{} : Bool} -> @+hj:{Nat.is_lt(j, k) == True{} : Bool} -> @+hne:{Nat.is_eq(j, i) == False{} : Bool} -> {pair_ok(A, cmp, ss, j) == True{} : Bool}

one pair out of ho_exc

template pair_of_skip source · line 212 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+i:Nat -> @+hi:{pair_ok(A, cmp, ss, i) == True{} : Bool} -> @+h:{pair_skip(A, cmp, ss, m, i) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(m, i) == b : Bool} -> {pair_ok(A, cmp, ss, m) == True{} : Bool}

template ho_of_exc source · line 220 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @k:Nat -> @+i:Nat -> @+h:{ho_exc(A, cmp, ss, k, i) == True{} : Bool} -> @+hi:{pair_ok(A, cmp, ss, i) == True{} : Bool} -> {ho_upto(A, cmp, ss, k) == True{} : Bool}

ho_upto follows from ho_exc plus the excluded pair

template kid_le source · line 231 · raw

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

template kids_le source · line 234 · raw

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

template kid_le_at source · line 237 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @+u:Nat -> @+c:Nat -> @+hc:{Nat.is_lt(c, n) == True{} : Bool} -> @+h:{kid_le(A, cmp, ss, n, u, c) == True{} : Bool} -> {mle(A, cmp, slot(A, ss, u), slot(A, ss, c)) == True{} : Bool}

template kid_le_in source · line 240 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @+u:Nat -> @+c:Nat -> @+eb:{Nat.is_lt(c, n) == True{} : Bool} -> @+h:{mle(A, cmp, slot(A, ss, u), slot(A, ss, c)) == True{} : Bool} -> {kid_le(A, cmp, ss, n, u, c) == True{} : Bool}

template kid_le_out source · line 244 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @+u:Nat -> @+c:Nat -> @+eb:{Nat.is_lt(c, n) == False{} : Bool} -> {kid_le(A, cmp, ss, n, u, c) == True{} : Bool}

template pair_skip2 source · line 256 · raw

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

template ho_exc2 source · line 259 · raw

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

template skip2_eq source · line 266 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+i:Nat -> @+eb:{kid_of(m, i) == True{} : Bool} -> {pair_skip2(A, cmp, ss, m, i) == True{} : Bool}

template skip2_ne source · line 270 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+i:Nat -> @+eb:{kid_of(m, i) == False{} : Bool} -> @+h:{pair_ok(A, cmp, ss, m) == True{} : Bool} -> {pair_skip2(A, cmp, ss, m, i) == True{} : Bool}

template skip2_at source · line 274 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+m:Nat -> @+i:Nat -> @+hne:{kid_of(m, i) == False{} : Bool} -> @+h:{pair_skip2(A, cmp, ss, m, i) == True{} : Bool} -> {pair_ok(A, cmp, ss, m) == True{} : Bool}

template exc2_get source · line 277 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @k:Nat -> @+i:Nat -> @+j:Nat -> @+h:{ho_exc2(A, cmp, ss, k, i) == True{} : Bool} -> @+hj:{Nat.is_lt(j, k) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat.pred(k)) == b : Bool} -> {pair_skip2(A, cmp, ss, j, i) == True{} : Bool}

template exc2_at source · line 286 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+k:Nat -> @+i:Nat -> @+j:Nat -> @+h:{ho_exc2(A, cmp, ss, k, i) == True{} : Bool} -> @+hj:{Nat.is_lt(j, k) == True{} : Bool} -> @+hne:{kid_of(j, i) == False{} : Bool} -> {pair_ok(A, cmp, ss, j) == True{} : Bool}

template pair_of_kid source · line 289 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @+i:Nat -> @c:Nat -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(c) == i : Nat} -> @+hcpos:{Nat.is_le(1n, c) == True{} : Bool} -> @+h:{mle(A, cmp, slot(A, ss, i), slot(A, ss, c)) == True{} : Bool} -> {pair_ok(A, cmp, ss, c) == True{} : Bool}

template pair_kid_at source · line 298 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @+i:Nat -> @+j:Nat -> @+c:Nat -> @+hjn:{Nat.is_lt(j, n) == True{} : Bool} -> @+ej:{Nat.is_eq(j, c) == True{} : Bool} -> @+epc:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(c) == i : Nat} -> @+hc:{kid_le(A, cmp, ss, n, i, c) == True{} : Bool} -> @+hcpos:{Nat.is_le(1n, c) == True{} : Bool} -> {pair_ok(A, cmp, ss, j) == True{} : Bool}

one excluded pair, from "the hole is not larger than that child"

template ho_of_exc2_at source · line 307 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @+k:Nat -> @+i:Nat -> @+j:Nat -> @+hjk:{Nat.is_lt(j, k) == True{} : Bool} -> @+hjn:{Nat.is_lt(j, n) == True{} : Bool} -> @+h:{ho_exc2(A, cmp, ss, k, i) == True{} : Bool} -> @+hkids:{kids_le(A, cmp, ss, n, i, i) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidl(i)) == b : Bool} -> @c:Bool -> @+ec:{Nat.is_eq(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.kidr(i)) == c : Bool} -> {pair_ok(A, cmp, ss, j) == True{} : Bool}

ho_upto from ho_exc2 plus "the hole is not larger than its children"

template ho_of_exc2 source · line 316 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+ss:List<&2, Maybe<&2, A>> -> @+n:Nat -> @k:Nat -> @+i:Nat -> @+hk:{Nat.is_le(k, n) == True{} : Bool} -> @+h:{ho_exc2(A, cmp, ss, k, i) == True{} : Bool} -> @+hkids:{kids_le(A, cmp, ss, n, i, i) == True{} : Bool} -> {ho_upto(A, cmp, ss, k) == True{} : Bool}