~/bend-docscommunity

proofs/math/typed/f64rtools.bend checks

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

14 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../spec/math/w64.bend as SW
import ../../../src/math/f64.bend as F
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/bits.bend as BT
import ./width.bend as WW
import ./natcmp.bend as NC
import ./f64round.bend as FR
import ./f64bl.bend as FO

Definitions

def lt0f source · line 26 · raw

@+h:Nat -> {Nat.is_lt(h, 0n) == False{} : Bool}

def rne_exact source · line 29 · raw

@+k:Nat -> @+m:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), k) == m : Nat}

def rne_shift source · line 47 · raw

@+k:Nat -> @+m:Nat -> @+j:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), Nat.add(j, k)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, j) : Nat}

rounding m * 2^k by j + k bits is rounding m by j bits

def bl_fit source · line 66 · raw

@+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), n) == True{} : Bool}

def bl_nfit source · line 69 · raw

@+n:Nat -> @+hz:{Nat.is_eq(n, 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(n), 1n), n) == False{} : Bool}

def fits_sh source · line 74 · raw

@+k:Nat -> @+a:Nat -> @+m:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(k, a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(a, m) : Bool}

def bl_shift source · line 77 · raw

@+k:Nat -> @+m:Nat -> @+hz:{Nat.is_eq(m, 0n) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m)) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(m), k) : Nat}

def a1 source · line 91 · raw

@+x:Nat -> @+k:Nat -> @+u:Nat -> @+h:{Nat.is_le(Nat.add(x, k), u) == True{} : Bool} -> {Nat.sub(u, x) == Nat.add(Nat.sub(u, Nat.add(x, k)), k) : Nat}

def qeq_f source · line 96 · raw

@+k:Nat -> @+m:Nat -> @+x:Nat -> @+u:Nat -> @+c1:Bool -> @+hc1:{Nat.is_le(x, u) == c1 : Bool} -> @+hc2:{Nat.is_le(Nat.add(x, k), u) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, c1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), Nat.sub(u, x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(x, u), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(Nat.add(x, k), u), m) : Nat}

def qeq_c source · line 113 · raw

@+k:Nat -> @+m:Nat -> @+x:Nat -> @+u:Nat -> @+c1:Bool -> @+hc1:{Nat.is_le(x, u) == c1 : Bool} -> @+c2:Bool -> @+hc2:{Nat.is_le(Nat.add(x, k), u) == c2 : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, c1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), Nat.sub(u, x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(x, u), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, c2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, Nat.sub(u, Nat.add(x, k))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(Nat.add(x, k), u), m)) : Nat}

def rd source · line 128 · raw

@+s:Bool -> @+m:Nat -> @+x:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Nat.is_eq(m, 0n), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zero(s), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round_u(s, m, x, Nat.max(Nat.sub(Nat.add(x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(m)), 53n), Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.zb, 1074n)))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

SF.round, SF.round_u and SF.pick unfolded once, over variables: proofs rewrite with these instead of letting a conversion unfold (and normalize) the rounding on both sides

def rud source · line 131 · raw

@+s:Bool -> @+m:Nat -> @+x:Nat -> @+u:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round_u(s, m, x, u) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pack(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(Nat, Nat.is_le(x, u), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.rne(m, Nat.sub(u, x)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(Nat.sub(x, u), m)), u) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def rs_c source · line 134 · raw

@+s:Bool -> @+k:Nat -> @+m:Nat -> @+x:Nat -> @+z:Bool -> @+hz:{Nat.is_eq(m, 0n) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, Nat.add(x, k)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def round_shift source · line 151 · raw

@+s:Bool -> @+k:Nat -> @+m:Nat -> @+x:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, Nat.add(x, k)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

round(s, m * 2^k, x) = round(s, m, x + k)

def round_shift_to source · line 156 · raw

@+s:Bool -> @+k:Nat -> @+m:Nat -> @+x:Nat -> @+y:Nat -> @+hy:{Nat.add(x, k) == y : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, m), x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, y) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

round_shift with the new exponent y == x + k given (a literal at the use), so the result needs no conversion of Nat.add(x, k) inside SF.round

def max_ge_l source · line 161 · raw

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

def le_sub source · line 170 · raw

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

def fit_td source · line 177 · raw

@+a:Nat -> @+t:Nat -> @+y:Nat -> @+ht:{Nat.is_le(t, 1n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+a, Nat.add(t, Nat.double(y))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(a, y) : Bool}

a bit t <= 1 below 2 y leaves the width of y

def jam_fits source · line 180 · raw

@+a:Nat -> @+h:Nat -> @+l:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+a, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(h, l)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+a, h) : Bool}

def nz_bl source · line 188 · raw

@+m:Nat -> @+K:Nat -> @+hb:{Nat.is_le(1n+K, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(m)) == True{} : Bool} -> @+z:Bool -> @+hz:{Nat.is_eq(m, 0n) == z : Bool} -> {z == False{} : Bool}

def rj2 source · line 198 · raw

@+s:Bool -> @+d:Nat -> @+m:Nat -> @+x:Nat -> @+hb:{Nat.is_le(Nat.add(d, 55n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(m)) == True{} : Bool} -> @+hz:{Nat.is_eq(m, 0n) == False{} : Bool} -> @+e:Nat -> @+fh0:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(e, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, m)) == False{} : Bool} -> @+fh1:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+e, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, m)) == True{} : Bool} -> @+eB:{Nat.add(d, 1n+e) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(m) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, m)), Nat.add(x, d)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def round_jam source · line 230 · raw

@+s:Bool -> @+d:Nat -> @+m:Nat -> @+x:Nat -> @+hb:{Nat.is_le(Nat.add(d, 55n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.bit_length(m)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, m, x) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.jam(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(d, m), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(d, m)), Nat.add(x, d)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

round(s, m, x) = round(s, jam(m >> d, m mod 2^d), x + d) when m has d + 55 bits