~/bend-docscommunity

proofs/containers/binary_heap/idx.bend checks

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

4 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../spec/lib/common.bend as SC

Definitions

def kidl source · line 11 · raw

@+i:Nat -> Nat

def kidr source · line 14 · raw

@+i:Nat -> Nat

def half_go source · line 17 · raw

@n:Nat -> @odd:Bool -> Nat

def half source · line 26 · raw

@n:Nat -> Nat

def par source · line 29 · raw

@+j:Nat -> Nat

def hg_false source · line 34 · raw

@+i:Nat -> {half_go(Nat.double(i), False{}) == i : Nat}

def hg_true source · line 41 · raw

@+i:Nat -> {half_go(Nat.double(i), True{}) == i : Nat}

def half_double source · line 48 · raw

@+i:Nat -> {half(Nat.double(i)) == i : Nat}

def half_succ_double source · line 51 · raw

@+i:Nat -> {half(1n+Nat.double(i)) == i : Nat}

def sub0 source · line 54 · raw

@+n:Nat -> {n == Nat.sub(n, 0n) : Nat}

def par_kidl source · line 59 · raw

@+i:Nat -> {par(kidl(i)) == i : Nat}

def par_kidr source · line 63 · raw

@+i:Nat -> {par(kidr(i)) == i : Nat}

def half_even_succ source · line 70 · raw

@+p:Nat -> @+ep:{p == Nat.double(half(p)) : Nat} -> {Nat.is_eq(1n+p, 1n+Nat.double(half(1n+p))) == True{} : Bool}

p = 2h => 1 + p = 1 + 2 * half(1 + p), because half(1 + 2h) = h

def half_odd_succ source · line 77 · raw

@+p:Nat -> @+ep:{p == 1n+Nat.double(half(p)) : Nat} -> {Nat.is_eq(1n+p, Nat.double(half(1n+p))) == True{} : Bool}

p = 1 + 2h => 1 + p = 2 * half(1 + p), because half(2 + 2h) = 1 + h

def half_split_succ source · line 83 · raw

@+p:Nat -> @e:Or({Nat.is_eq(p, Nat.double(half(p))) == True{} : Bool}, {Nat.is_eq(p, 1n+Nat.double(half(p))) == True{} : Bool}) -> Or({Nat.is_eq(1n+p, Nat.double(half(1n+p))) == True{} : Bool}, {Nat.is_eq(1n+p, 1n+Nat.double(half(1n+p))) == True{} : Bool})

def half_split source · line 90 · raw

@+j:Nat -> Or({Nat.is_eq(j, Nat.double(half(j))) == True{} : Bool}, {Nat.is_eq(j, 1n+Nat.double(half(j))) == True{} : Bool})

def kid_left source · line 99 · raw

@+p:Nat -> @+ep:{p == Nat.double(half(p)) : Nat} -> {1n+p == kidl(par(1n+p)) : Nat}

def kid_right source · line 103 · raw

@+p:Nat -> @+ep:{p == 1n+Nat.double(half(p)) : Nat} -> {1n+p == kidr(par(1n+p)) : Nat}

def kid_split_succ source · line 107 · raw

@+p:Nat -> @e:Or({Nat.is_eq(p, Nat.double(half(p))) == True{} : Bool}, {Nat.is_eq(p, 1n+Nat.double(half(p))) == True{} : Bool}) -> Or({1n+p == kidl(par(1n+p)) : Nat}, {1n+p == kidr(par(1n+p)) : Nat})

def kid_split source · line 114 · raw

@+j:Nat -> @+hj:{Nat.is_lt(0n, j) == True{} : Bool} -> Or({j == kidl(par(j)) : Nat}, {j == kidr(par(j)) : Nat})

def double_le source · line 123 · raw

@+i:Nat -> {Nat.is_le(i, Nat.double(i)) == True{} : Bool}

def kidl_gt source · line 130 · raw

@+i:Nat -> {Nat.is_lt(i, kidl(i)) == True{} : Bool}

def kidr_gt source · line 133 · raw

@+i:Nat -> {Nat.is_lt(i, kidr(i)) == True{} : Bool}

def kidl_pos source · line 136 · raw

@+i:Nat -> {Nat.is_lt(0n, kidl(i)) == True{} : Bool}

def kidr_pos source · line 139 · raw

@+i:Nat -> {Nat.is_lt(0n, kidr(i)) == True{} : Bool}

def par_lt_of source · line 142 · raw

@+j:Nat -> @e:Or({j == kidl(par(j)) : Nat}, {j == kidr(par(j)) : Nat}) -> {Nat.is_lt(par(j), j) == True{} : Bool}

def par_lt source · line 149 · raw

@+j:Nat -> @+hj:{Nat.is_lt(0n, j) == True{} : Bool} -> {Nat.is_lt(par(j), j) == True{} : Bool}

def kidl_pos1 source · line 152 · raw

@+y:Nat -> {Nat.is_le(1n, kidl(y)) == True{} : Bool}

def kidr_pos1 source · line 155 · raw

@+y:Nat -> {Nat.is_le(1n, kidr(y)) == True{} : Bool}

def double_le_of source · line 160 · raw

@+j:Nat -> @e:Or({Nat.is_eq(j, Nat.double(half(j))) == True{} : Bool}, {Nat.is_eq(j, 1n+Nat.double(half(j))) == True{} : Bool}) -> {Nat.is_le(Nat.double(half(j)), j) == True{} : Bool}

def double_le_self source · line 167 · raw

@+j:Nat -> {Nat.is_le(Nat.double(half(j)), j) == True{} : Bool}

def double_lt_inj source · line 170 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(Nat.double(a), Nat.double(b)) == True{} : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

def sub_le_self source · line 179 · raw

@+j:Nat -> {Nat.is_le(Nat.sub(j, 1n), j) == True{} : Bool}

def par_bound source · line 188 · raw

@+i:Nat -> @+k:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+k)) == True{} : Bool} -> {Nat.is_lt(par(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool}

the parent of an index below 2^(k+1) is below 2^k

def double_lt source · line 193 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_lt(Nat.double(a), Nat.double(b)) == True{} : Bool}

def double_lt_succ source · line 203 · raw

@+a:Nat -> @+q:Nat -> @+h:{Nat.is_lt(Nat.double(a), Nat.double(q)) == True{} : Bool} -> {Nat.is_lt(1n+Nat.double(a), Nat.double(q)) == True{} : Bool}

one more than an even number below an even number is still below it

def kidl_bound source · line 213 · raw

@+i:Nat -> @+d:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(kidl(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+d)) == True{} : Bool}

a child index of an index below 2^d is below 2^(d+1)

def succ_lt_sub source · line 217 · raw

@+l:Nat -> @+n:Nat -> {Nat.is_lt(1n+l, n) == Nat.is_lt(l, Nat.sub(n, 1n)) : Bool}

l + 1 < n is l < n - 1

def scale source · line 232 · raw

@f:Nat -> @m:Nat -> Nat

def double_le_mono source · line 239 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(Nat.double(a), Nat.double(b)) == True{} : Bool}

def scale_mono source · line 248 · raw

@f:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(scale(f, a), scale(f, b)) == True{} : Bool}

def kid_double_of source · line 255 · raw

@+i:Nat -> @+c:Nat -> @+ep:{par(c) == i : Nat} -> @e:Or({c == kidl(par(c)) : Nat}, {c == kidr(par(c)) : Nat}) -> {Nat.is_le(Nat.double(1n+i), 1n+c) == True{} : Bool}

def kid_double source · line 263 · raw

@+i:Nat -> @+c:Nat -> @+ep:{par(c) == i : Nat} -> @+hcpos:{Nat.is_le(1n, c) == True{} : Bool} -> {Nat.is_le(Nat.double(1n+i), 1n+c) == True{} : Bool}

a child index is at least twice the parent's, so 1 + kid >= 2 * (1 + i)