~/bend-docscommunity

proofs/math/typed/f64close.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend as F64close

8 imports
import Base
import ../../../spec/math/f64.bend as SF
import ../../../src/math/f64.bend as F
import ../../../src/math/num.bend as NE
import ./f64bits.bend as FB
import ./f64cmp.bend as FC
import ./f64addv.bend as AV
import ./f64mulv.bend as MV

Definitions

def fabs_v source · line 16 · raw

@+z:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+z2:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+h:{z == z2 : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.abs(z) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.fabs(z2) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def D source · line 19 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def or3 source · line 24 · raw

@+x1:Bool -> @+x2:Bool -> @+x3:Bool -> @+y1:Bool -> @+y2:Bool -> @+y3:Bool -> @+h1:{x1 == y1 : Bool} -> @+h2:{x2 == y2 : Bool} -> @+h3:{x3 == y3 : Bool} -> {Bool.or(Bool.or(x1, x2), x3) == Bool.or(Bool.or(y1, y2), y3) : Bool}

three-way disjunction congruence over abstract Booleans (book-less: the checker never unfolds the comparisons it is applied to)

def lek source · line 31 · raw

@+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.le(d, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.abs(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.mul(r, x))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.le_s(d, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.fabs(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mul(r, x))) : Bool}

d <= |r * x| on the implementation is le_s against the spec's |r * x|

def icd_t source · line 35 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+rel:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+at:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ic_d(a, b, rel, at, d) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ic_near(a, b, rel, at, d) : Bool}

def icd source · line 38 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+rel:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+at:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ic_d(a, b, rel, at, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.abs(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sub(b, a))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ic_near(a, b, rel, at, D(a, b)) : Bool}

def ii_f source · line 44 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+rel:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+at:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ic_inf(a, b, rel, at, False{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ic_d(a, b, rel, at, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.abs(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sub(b, a))) : Bool}

one unfolding step each, stated so the checker compares syntactically

def pk_f source · line 47 · raw

@+x:Bool -> @+y:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Bool, False{}, x, y) == y : Bool}

def iinf source · line 50 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+rel:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+at:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+big:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ic_inf(a, b, rel, at, big) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Bool, big, False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ic_near(a, b, rel, at, D(a, b))) : Bool}

def ie_f source · line 59 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+rel:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+at:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ic_eq(a, b, rel, at, False{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ic_inf(a, b, rel, at, Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.is_inf(a), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.is_inf(b))) : Bool}

def ieq source · line 62 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+rel:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+at:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+e:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ic_eq(a, b, rel, at, e) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Bool, e, True{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Bool, Bool.or(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_inf(a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.is_inf(b)), False{}, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.ic_near(a, b, rel, at, D(a, b)))) : Bool}

def NEAR source · line 76 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+rel:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+at:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Bool

def itol source · line 79 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+rel:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+at:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+bad:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ic_tol(a, b, rel, at, bad) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Bool>, bad, Fail{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.BadDomain{}}, Done{NEAR(a, b, rel, at)}) : Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Bool>}

def isclose_value source · line 88 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+rel:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+at:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.IsClose.value(a, b, rel, at)