~/bend-docscommunity

proofs/lib/vec.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/vec.bend as Vec

7 imports
import Base
import ./logic.bend as L
import ./nat.bend as N
import ./list.bend as LL
import ../../spec/lib/common.bend as SC
import ../../src/containers/internal/vec.bend as V
import ./lemmas/proofs/nat_algebra.bend as NA

Definitions

def slots source · line 13 · raw

@-T:Data -> @t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> List<&2, T>

def perfect source · line 20 · raw

@-T:Data -> @+d:Nat -> @t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> Bool

def pf_left source · line 31 · raw

@-T:Data -> @+p:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> @+pf:{perfect(T, 1n+p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.VNode{l, r}) == True{} : Bool} -> {perfect(T, p, l) == True{} : Bool}

def pf_right source · line 34 · raw

@-T:Data -> @+p:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> @+r:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> @+pf:{perfect(T, 1n+p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.VNode{l, r}) == True{} : Bool} -> {perfect(T, p, r) == True{} : Bool}

def slots_length source · line 37 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, slots(T, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(d) : Nat}

def upper_lt source · line 51 · raw

@+j:Nat -> @+p:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(1n+p)) == True{} : Bool} -> @+le:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(p), j) == True{} : Bool} -> {Nat.is_lt(Nat.sub(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(p)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(p)) == True{} : Bool}

def left_len source · line 54 · raw

@-T:Data -> @+p:Nat -> @+l:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> @+pl:{perfect(T, p, l) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(p) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, slots(T, l)) : Nat}

def get_go source · line 59 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(d)) == True{} : Bool} -> @+b:Bool -> @+eb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.dec(d, j) == b : Bool} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.get_go(T, d, t, j, b) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, slots(T, t), j) : Maybe<&2, T>}

def get source · line 86 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> @+j:Nat -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(d)) == True{} : Bool} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.get(T, d, t, j) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, slots(T, t), j) : Maybe<&2, T>}

def set_go_perfect source · line 91 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> @+j:Nat -> @+v:T -> @+b:Bool -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {perfect(T, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.set_go(T, d, t, j, v, b)) == True{} : Bool}

def set_perfect source · line 104 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> @+j:Nat -> @+v:T -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {perfect(T, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.set(T, d, t, j, v)) == True{} : Bool}

def set_go_slots source · line 107 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> @+j:Nat -> @+v:T -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(d)) == True{} : Bool} -> @+b:Bool -> @+eb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.dec(d, j) == b : Bool} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {slots(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.set_go(T, d, t, j, v, b)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, slots(T, t), j, v) : List<&2, T>}

def set source · line 134 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.Vec<T> -> @+j:Nat -> @+v:T -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(d)) == True{} : Bool} -> @+pf:{perfect(T, d, t) == True{} : Bool} -> {slots(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.set(T, d, t, j, v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, slots(T, t), j, v) : List<&2, T>}

def pow2_pos source · line 139 · raw

@+d:Nat -> {Nat.is_le(1n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(d)) == True{} : Bool}

def arr source · line 147 · raw

@+p:Nat -> @+a:Nat -> @+c:Nat -> {Nat.add(p, Nat.add(Nat.add(1n, a), c)) == Nat.add(Nat.add(1n+p, c), a) : Nat}

n + 2^d <= 2^(depth_go n d room) + room, for room <= 2^d.

def le_add_cancel source · line 154 · raw

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

def depth_go_cap source · line 163 · raw

@+n:Nat -> @+d:Nat -> @+room:Nat -> @+h:{Nat.is_le(room, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(d)) == True{} : Bool} -> {Nat.is_le(Nat.add(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(d)), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.depth_go(n, d, room)), room)) == True{} : Bool}

def depth_for source · line 189 · raw

@+n:Nat -> {Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/vec.depth_for(n))) == True{} : Bool}

p + ((1 + a) + c) == ((1 + p) + c) + a a + c <= b + c implies a <= b