proofs/containers/doubly_linked_list/vals.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/vals.bend as Vals

11 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32alg.bend as A
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/doubly_linked_list.bend as S
import ./state.bend as ST
import ./rel.bend as RL
import ../../lib/nat_list.bend as NL
import ../../lib/words32.bend as W32

Definitions

def val_upd_same source · line 19 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+i:Nat -> @+v:Maybe<&2, T> -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vl, i, v), i) == v : Maybe<&2, T>}

def val_upd_other source · line 28 · raw

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

def val_take source · line 41 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+i:Nat -> @+h:{Nat.is_lt(i, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Maybe<&2, T>, vl, n), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vl, i) : Maybe<&2, T>}

def val_hi source · line 52 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+i:Nat -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, vl), i) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vl, i) == None{} : Maybe<&2, T>}

def gen_nth0 source · line 63 · raw

@+gl:List<&2, U32> -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.gen_of(gl, i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(gl, i) : U32}

def nth0_take source · line 72 · raw

@+gl:List<&2, U32> -> @+n:Nat -> @+i:Nat -> @+h:{Nat.is_lt(i, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, gl, n), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(gl, i) : U32}

def gen_take source · line 83 · raw

@+gl:List<&2, U32> -> @+n:Nat -> @+i:Nat -> @+h:{Nat.is_lt(i, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.gen_of(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, gl, n), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(gl, i) : U32}

def gen_snoc source · line 86 · raw

@+gl:List<&2, U32> -> @+g:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.gen_of(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(U32, gl, g), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, gl)) == g : U32}

def take_upd_succ source · line 95 · raw

@-X:Data -> @+xs:List<&2, X> -> @+n:Nat -> @+v:X -> @+h:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(X, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(X, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(X, xs, n, v), 1n+n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(X, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(X, xs, n), v) : List<&2, X>}

def upd_snoc source · line 104 · raw

@-X:Data -> @+ys:List<&2, X> -> @+dv:X -> @+v:X -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(X, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(X, ys, dv), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(X, ys), v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(X, ys, v) : List<&2, X>}

def take_succ_u source · line 111 · raw

@+xs:List<&2, U32> -> @+n:Nat -> @+h:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, xs, 1n+n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, xs, n), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(xs, n)) : List<&2, U32>}

def or_nt source · line 122 · raw

@+b:Bool -> @+c:Bool -> @+h:{Bool.or(Bool.not(b), c) == True{} : Bool} -> @+hb:{b == True{} : Bool} -> {c == True{} : Bool}

def or_tr2 source · line 138 · raw

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

def subn source · line 165 · raw

@xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> Bool

def subn_c source · line 172 · raw

@+x:Nat -> @+y:Nat -> @+t:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(y, ys) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(y, x) == c : Bool} -> @+hm:{Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, t)) == True{} : Bool} -> @rec:(@hm2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, t) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, ys) == True{} : Bool}) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, ys) == True{} : Bool}

def subn_mem source · line 179 · raw

@+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+x:Nat -> @+h:{subn(xs, ys) == True{} : Bool} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, ys) == True{} : Bool}

def subn_wk source · line 186 · raw

@+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+y:Nat -> @+h:{subn(xs, ys) == True{} : Bool} -> {subn(xs, y <> ys) == True{} : Bool}

def subn_refl source · line 193 · raw

@+xs:List<&2, Nat> -> {subn(xs, xs) == True{} : Bool}

def mem2_c source · line 200 · raw

@+x:Nat -> @+y:Nat -> @+z:Nat -> @+ys:List<&2, Nat> -> @+c:Bool -> @+h:{Bool.or(c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, ys)) == True{} : Bool} -> {Bool.or(c, Bool.or(Nat.is_eq(z, x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(x, ys))) == True{} : Bool}

def subn_wk2 source · line 207 · raw

@+xs:List<&2, Nat> -> @+y:Nat -> @+z:Nat -> @+ys:List<&2, Nat> -> @+h:{subn(xs, y <> ys) == True{} : Bool} -> {subn(xs, y <> z <> ys) == True{} : Bool}

def subn_ins source · line 216 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+n:Nat -> {subn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, n <> b)) == True{} : Bool}

a ++ b among a ++ n :: b

def subn_rm source · line 224 · raw

@+a:List<&2, Nat> -> @+s:Nat -> @+b:List<&2, Nat> -> {subn(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, s <> b), s <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b)) == True{} : Bool}

a ++ s :: b among s :: a ++ b

def ornc source · line 231 · raw

@-T:Data -> @+m:Maybe<&2, T> -> @+c:Bool -> @+c0:Bool -> @+h:{Bool.or(Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.some_b(T, m)), c0) == True{} : Bool} -> @f:(@hc:{c0 == True{} : Bool} -> {c == True{} : Bool}) -> {Bool.or(Bool.not(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.some_b(T, m)), c) == True{} : Bool}

def gz_at source · line 293 · raw

@+gl:List<&2, U32> -> @+fr:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(gl, fr) == True{} : Bool} -> @+hl:{Nat.is_lt(fr, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, gl)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/words32.nth0(gl, fr) == 0 : U32}

def gz_succ source · line 302 · raw

@+gl:List<&2, U32> -> @+fr:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(gl, fr) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(gl, 1n+fr) == True{} : Bool}

def gz_upd source · line 311 · raw

@+gl:List<&2, U32> -> @+fr:Nat -> @+i:Nat -> @+v:U32 -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(gl, fr) == True{} : Bool} -> @+hi:{Nat.is_lt(i, fr) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, gl, i, v), fr) == True{} : Bool}

def gz_rep source · line 322 · raw

@+m:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(U32, m, 0), 0n) == True{} : Bool}

def gz_grow source · line 329 · raw

@+gl:List<&2, U32> -> @+m:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.gz(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, gl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(U32, m, 0)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, gl)) == True{} : Bool}

Templates

template lvin_elim source · line 126 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+k:Nat -> @+sl:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, vl, k, sl) == True{} : Bool} -> @+x:Nat -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.some_b(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vl, x)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(Nat.add(k, x), sl) == True{} : Bool}

every live index x (from k) is the id k + x of sl

template lvin_upd source · line 142 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+k:Nat -> @+sl:List<&2, Nat> -> @+j:Nat -> @+v:Maybe<&2, T> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, vl, k, sl) == True{} : Bool} -> @+hm:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.memn(Nat.add(k, j), sl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vl, j, v), k, sl) == True{} : Bool}

a write of a value at a listed index

template lvin_none source · line 154 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+k:Nat -> @+sl:List<&2, Nat> -> @+j:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, vl, k, sl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, vl, j, None{}), k, sl) == True{} : Bool}

a write of None

template lvin_sub source · line 239 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+k:Nat -> @+sl:List<&2, Nat> -> @+sl2:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, vl, k, sl) == True{} : Bool} -> @+hs:{subn(sl, sl2) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, vl, k, sl2) == True{} : Bool}

a larger list of ids

template lvin_low source · line 248 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+k:Nat -> @+s:Nat -> @+sl:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, vl, k, s <> sl) == True{} : Bool} -> @+hlt:{Nat.is_lt(s, k) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, vl, k, sl) == True{} : Bool}

indices from k are all above s: s can be dropped

template lvin_skip source · line 258 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+k:Nat -> @+j:Nat -> @+sl:List<&2, Nat> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, vl, k, Nat.add(k, j) <> sl) == True{} : Bool} -> @+hv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.some_b(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/doubly_linked_list.val_of(T, vl, j)) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, vl, k, sl) == True{} : Bool}

the id s = k + j with a vacant value can be dropped

template lvin_rep source · line 276 · raw

@-T:Data -> @+m:Nat -> @+k:Nat -> @+sl:List<&2, Nat> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(Maybe<&2, T>, m, None{}), k, sl) == True{} : Bool}

template lvin_grow source · line 284 · raw

@-T:Data -> @+vl:List<&2, Maybe<&2, T>> -> @+k:Nat -> @+sl:List<&2, Nat> -> @+m:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, vl, k, sl) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/doubly_linked_list/state.lvin(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, T>, vl, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(Maybe<&2, T>, m, None{})), k, sl) == True{} : Bool}

vacant slots appended