~/bend-docscommunity

proofs/math/typed/f64divn.bend checks

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

11 imports
import Base
import ./f64light.bend as FL
import ../../../spec/lib/common.bend as C
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ./width.bend as WW
import ./natcmp.bend as NC
import ./f64rtools.bend as RT
import ./natfuel.bend as NF

Definitions

def add_eq0 source · line 19 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}

def mul_eq0 source · line 22 · raw

@+a:Nat -> @+yp:Nat -> {Nat.is_eq(Nat.mul(a, 1n+yp), 0n) == Nat.is_eq(a, 0n) : Bool}

def min1_eq0 source · line 29 · raw

@+b:Nat -> {Nat.is_eq(Nat.min(b, 1n), 0n) == Nat.is_eq(b, 0n) : Bool}

def min1_le source · line 36 · raw

@+b:Nat -> {Nat.is_le(Nat.min(b, 1n), 1n) == True{} : Bool}

def and_comm source · line 47 · raw

@+a:Bool -> @+b:Bool -> {Bool.and(a, b) == Bool.and(b, a) : Bool}

def mul1 source · line 58 · raw

@+y:Nat -> {Nat.mul(1n, y) == y : Nat}

def sh_y source · line 62 · raw

@+k:Nat -> @+y:Nat -> {Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 1n), y) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y) : Nat}

2^k * y as a product

def le_sh source · line 66 · raw

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

le/lt under a common shift

def lt_sh source · line 69 · raw

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

def specA source · line 73 · raw

@+MX:Nat -> @+yp:Nat -> @+P:Nat -> @+dp:Nat -> @+hP:{Nat.add(dp, P) == 200n : Nat} -> {Nat.add(Nat.add(Nat.min(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(dp, Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(dp, Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp)), 1n+yp))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(1n+dp, Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp))) == Nat.add(Nat.mul(2n, Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(200n, MX), 1n+yp), 1n)) : Nat}

the spec's significand cut at bit 1+dp, where P + dp = 200

def specA_fit source · line 97 · raw

@+MX:Nat -> @+yp:Nat -> @+P:Nat -> @+dp:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(1n+dp, Nat.add(Nat.min(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(dp, Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(dp, Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp)), 1n+yp)))) == True{} : Bool}

the low part fits 1+dp bits

def specA_z source · line 104 · raw

@+MX:Nat -> @+yp:Nat -> @+P:Nat -> @+dp:Nat -> {Nat.is_eq(Nat.add(Nat.min(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(dp, Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(dp, Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp)), 1n+yp))), 0n) == Nat.is_eq(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp), 0n) : Bool}

the low part is zero exactly when MX * 2^P is a multiple of MY

def iq_parts source · line 119 · raw

@+B:Nat -> @+R:Nat -> @+Q:Nat -> @+r2:Nat -> @+hQ:{Nat.add(Nat.mul(Q, B), r2) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, R) : Nat} -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(2n, Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, Q), B)), Nat.add(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(2n, Q), B), r2)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, R)) : Nat}

SoftFloat's quotient: (a - b) * 2^64 = Q * b + r2 with r2 < b gives a * 2^62 = T * b + e with T = 2^62 + floor(Q / 4) and e < b

def iq_le source · line 130 · raw

@+B:Nat -> @+R:Nat -> @+Q:Nat -> @+r2:Nat -> @+hQ:{Nat.add(Nat.mul(Q, B), r2) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, R) : Nat} -> {Nat.is_le(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, Q), B), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, R)) == True{} : Bool}

h * b <= (a - b) * 2^62

def iq_eps source · line 136 · raw

@+B:Nat -> @+R:Nat -> @+Q:Nat -> @+r2:Nat -> @+hQ:{Nat.add(Nat.mul(Q, B), r2) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, R) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(2n, Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, R), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, Q), B))) == Nat.add(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(2n, Q), B), r2) : Nat}

the remainder e = (a - b) * 2^62 - h * b, and 4 e = low2(Q) * b + r2

def low2_le source · line 142 · raw

@+Q:Nat -> @+bp:Nat -> {Nat.is_le(Nat.mul(1n+0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(2n, Q), 1n+bp), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(2n, 1n+bp)) == True{} : Bool}

def iq_lt source · line 149 · raw

@+bp:Nat -> @+R:Nat -> @+Q:Nat -> @+r2:Nat -> @+hQ:{Nat.add(Nat.mul(Q, 1n+bp), r2) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, R) : Nat} -> @+hr2:{Nat.is_lt(r2, 1n+bp) == True{} : Bool} -> {Nat.is_lt(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, R), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, Q), 1n+bp)), 1n+bp) == True{} : Bool}

e < b

def iq_z source · line 158 · raw

@+bp:Nat -> @+R:Nat -> @+Q:Nat -> @+r2:Nat -> @+hQ:{Nat.add(Nat.mul(Q, 1n+bp), r2) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, R) : Nat} -> {Nat.is_eq(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, R), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(2n, Q), 1n+bp)), 0n) == Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(2n, Q), 0n), Nat.is_eq(r2, 0n)) : Bool}

e is zero exactly when the low two quotient bits and r2 are

def jn_eq source · line 168 · raw

@+MX:Nat -> @+yp:Nat -> @+u:Nat -> @+w:Nat -> @+P:Nat -> @+hP:{Nat.add(62n, u) == Nat.add(w, P) : Nat} -> @+bp:Nat -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(w, 1n+yp) == 1n+bp : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(u, MX)) == Nat.add(Nat.mul(Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp), 1n+bp), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(w, Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp))) : Nat}

the two scales agree: a * 2^62 = T * b + e with e < b, a = MX * 2^u and b = MY * 2^w give T = floor(MX * 2^P / MY) and e = 0 iff MY | MX * 2^P

def jn_lt source · line 178 · raw

@+MX:Nat -> @+yp:Nat -> @+w:Nat -> @+P:Nat -> @+bp:Nat -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(w, 1n+yp) == 1n+bp : Nat} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(w, Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp)), 1n+bp) == True{} : Bool}

def jn_q source · line 181 · raw

@+MX:Nat -> @+yp:Nat -> @+u:Nat -> @+w:Nat -> @+P:Nat -> @+hP:{Nat.add(62n, u) == Nat.add(w, P) : Nat} -> @+bp:Nat -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(w, 1n+yp) == 1n+bp : Nat} -> @+T:Nat -> @+e:Nat -> @+hE:{Nat.add(Nat.mul(T, 1n+bp), e) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(u, MX)) : Nat} -> @+he:{Nat.is_lt(e, 1n+bp) == True{} : Bool} -> {T == Nat.div(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp) : Nat}

def jn_z source · line 187 · raw

@+MX:Nat -> @+yp:Nat -> @+u:Nat -> @+w:Nat -> @+P:Nat -> @+hP:{Nat.add(62n, u) == Nat.add(w, P) : Nat} -> @+bp:Nat -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(w, 1n+yp) == 1n+bp : Nat} -> @+T:Nat -> @+e:Nat -> @+hE:{Nat.add(Nat.mul(T, 1n+bp), e) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(62n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(u, MX)) : Nat} -> @+he:{Nat.is_lt(e, 1n+bp) == True{} : Bool} -> {Nat.is_eq(e, 0n) == Nat.is_eq(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(P, MX), 1n+yp), 0n) : Bool}