proofs/containers/binary_heap/bag.bend checks

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

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 ./slots.bend as SL
import ./vals.bend as V

Definitions

def not_le_not_eq_c source · line 24 · raw

@c:Cmp -> @+e:{Cmp.is_le(c) == False{} : Bool} -> {Cmp.is_eq(c) == False{} : Bool}

Templates

template del_head source · line 20 · raw

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

The first element that compares EQ to z is removed. b is "does the head compare EQ to z": a loop that branches on a computed value has to carry the decision in its arguments (Bend matches only on parameters). z is removed from a list it was just inserted into.

template not_le_not_eq source · line 33 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+z:A -> @+h:A -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, z, h) == False{} : Bool} -> {Cmp.is_eq(cmp(z, h)) == False{} : Bool}

template del_ins_cons source · line 36 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+z:A -> @+h:A -> @+t:List<&2, A> -> @b:Bool -> @+eb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.le(A, cmp, z, h) == b : Bool} -> @+ih:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.delf(A, cmp, z, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, z, t)) == t : List<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.delf(A, cmp, z, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, z, h <> t)) == h <> t : List<&2, A>}

template del_ins source · line 46 · raw

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

template ins_inj source · line 54 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(A, cmp) -> @+z:A -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, z, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.ins(A, cmp, z, ys) : List<&2, A>} -> {xs == ys : List<&2, A>}

Insertion is injective in the list: the sorted multiset is determined.

template upd_upd_same source · line 63 · raw

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

template slot_l1 source · line 72 · raw

@-A:Data -> @+ss:List<&2, Maybe<&2, A>> -> @+i:Nat -> @+p:Nat -> @+b:A -> @+hne:{Nat.is_eq(i, p) == False{} : Bool} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, p) == Some{b} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ss, i, Some{b}), p) == Some{b} : Maybe<&2, A>}

template all_ge_cons source · line 77 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/order.Order(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} -> @+hxs:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.all_ge(A, cmp, z, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/binary_heap.all_ge(A, cmp, z, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.cons_slot(A, m, xs))) == True{} : Bool}

template low_all source · line 85 · raw

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

template all_ge_vals source · line 92 · raw

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

template vals_swap source · line 103 · 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 -> @+p:Nat -> @+a:A -> @+b:A -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> @+hp:{Nat.is_lt(p, n) == True{} : Bool} -> @+hne:{Nat.is_eq(i, p) == False{} : Bool} -> @+ha:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, i) == Some{a} : Maybe<&2, A>} -> @+hb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/slots.slot(A, ss, p) == Some{b} : Maybe<&2, A>} -> {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>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, A>, ss, i, Some{b}), p, Some{a}), n)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.msort(A, cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/vals.vals(A, ss, n)) : List<&2, A>}

Exchanging the values of two occupied slots leaves the sorted multiset unchanged: two applications of ins_set and one cancellation.