proofs/lib/u32seq.bend checks

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

8 imports

import Base
import ./logic.bend as L
import ./nat.bend as N
import ./list.bend as LL
import ./u32.bend as U
import ./u32alg.bend as UA
import ../../spec/lib/common.bend as SC
import ../../spec/lib/u32seq.bend as Q

Definitions

def addat source · line 12 · raw

@xs:List<&2, U32> -> @+i:Nat -> @+v:U32 -> List<&2, U32>

def sum_append source · line 21 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.sum(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, xs, ys)) == U32.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.sum(xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.sum(ys)) : U32}

def sum_zeros source · line 29 · raw

@+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.sum(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.zeros(n)) == 0 : U32}

def length_addat source · line 37 · raw

@+xs:List<&2, U32> -> @+i:Nat -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, addat(xs, i, v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs) : Nat}

def sum_addat source · line 47 · raw

@+xs:List<&2, U32> -> @+i:Nat -> @+v:U32 -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.sum(addat(xs, i, v)) == U32.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.sum(xs), v) : U32}

Adding v at an index below the length adds v to the sum.

def addat_left source · line 60 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+i:Nat -> @+v:U32 -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)) == True{} : Bool} -> {addat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, xs, ys), i, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, addat(xs, i, v), ys) : List<&2, U32>}

def addat_right source · line 69 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+i:Nat -> @+v:U32 -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs), i) == True{} : Bool} -> {addat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, xs, ys), i, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(U32, xs, addat(ys, Nat.sub(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)), v)) : List<&2, U32>}

def take_addat source · line 80 · raw

@+xs:List<&2, U32> -> @+i:Nat -> @+v:U32 -> @+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, addat(xs, i, v), n) == addat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, xs, n), i, v) : List<&2, U32>}

def update_addat source · line 94 · raw

@+xs:List<&2, U32> -> @+i:Nat -> @+y:U32 -> @+v:U32 -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, xs, i) == Some{y} : Maybe<&2, U32>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, xs, i, U32.add(y, v)) == addat(xs, i, v) : List<&2, U32>}

The spec's "update index i with (old + v)" is addat.

def sum_slice source · line 105 · raw

@+xs:List<&2, U32> -> @+l:Nat -> @+r:Nat -> @+h:{Nat.is_le(l, r) == True{} : Bool} -> {U32.sub(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.sum(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, xs, r)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.sum(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, xs, l))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.sum(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.slice(xs, l, r)) : U32}

sum of the slice [l, r) is the difference of prefix sums

def sub_le_mono source · line 111 · raw

@+l:Nat -> @+r:Nat -> @+n:Nat -> @+h:{Nat.is_le(r, n) == True{} : Bool} -> {Nat.is_le(Nat.sub(r, l), Nat.sub(n, l)) == True{} : Bool}

slicing the first n values equals slicing the whole list when r <= n

def slice_take source · line 124 · raw

@+xs:List<&2, U32> -> @+n:Nat -> @+l:Nat -> @+r:Nat -> @+h:{Nat.is_le(r, n) == True{} : Bool} -> @+hl:{Nat.is_le(l, r) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.slice(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(U32, xs, n), l, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/u32seq.slice(xs, l, r) : List<&2, U32>}