proofs/math/typed/f64divv.bend checks

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

21 imports

import Base
import ./f64light.bend as FL
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/w64.bend as X
import ../../../src/math/u64.bend as WU
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 ./u32laws.bend as LW
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./f64round.bend as FR
import ./f64mexp.bend as EX
import ./f64divf.bend as DF
import ./f64divx.bend as DX

Definitions

def v source · line 26 · raw

@+x:U32 -> Nat

def pos52 source · line 29 · raw

@+n:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, n) == False{} : Bool} -> {Nat.is_le(1n, n) == True{} : Bool}

def hi_nz_c source · line 36 · raw

@+l:U32 -> @+h:U32 -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{l, h})) == False{} : Bool} -> @+z:Bool -> @+hz:{Nat.is_eq(v(h), 0n) == z : Bool} -> {z == False{} : Bool}

def hi_nz source · line 46 · raw

@+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b)) == False{} : Bool} -> {U32.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(b)) == False{} : Bool}

def sub_lt_of source · line 52 · raw

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

b <= a and a < 2 b give a - b < b

def sub_le0 source · line 57 · raw

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

def add_lt2 source · line 68 · raw

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

def lo52 source · line 72 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, n) == False{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(52n, one), n) == True{} : Bool}

a normalized significand is in [2^52, 2^53)

def hi53 source · line 75 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, n) == True{} : Bool} -> {Nat.is_lt(n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one)) == True{} : Bool}

def dbl53 source · line 79 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, n) == False{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(53n, one), Nat.add(n, n)) == True{} : Bool}

2^53 <= 2 n and n < 2 m for normalized n, m

def lt2x source · line 82 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+m:Nat -> @+hn:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, n) == True{} : Bool} -> @+hm:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, m) == False{} : Bool} -> {Nat.is_lt(n, Nat.add(m, m)) == True{} : Bool}

def dq_lt source · line 85 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+EA:Nat -> @+A:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+EB:Nat -> @+B:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+MX:Nat -> @+yp:Nat -> @+sx:Nat -> @+sy:Nat -> @+XX:Nat -> @+XY:Nat -> @+hA:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(sx, MX) : Nat} -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(sy, 1n+yp) : Nat} -> @+a53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A)) == True{} : Bool} -> @+a52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A)) == False{} : Bool} -> @+b53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B)) == True{} : Bool} -> @+b52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B)) == False{} : Bool} -> @+hEAx:{Nat.add(EA, sx) == Nat.add(XX, 2171n) : Nat} -> @+hEBy:{Nat.add(EB, sy) == Nat.add(XY, 2171n) : Nat} -> @+hsx:{Nat.is_le(sx, 53n) == True{} : Bool} -> @+hsy:{Nat.is_le(sy, 53n) == True{} : Bool} -> @+hXX:{Nat.is_le(1926n, XX) == True{} : Bool} -> @+hXY:{Nat.is_le(XY, 3971n) == True{} : Bool} -> @+hlt0:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_q(s, Nat.sub(Nat.add(EA, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 1021n)), EB), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(A, A), B) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 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.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def dq_ge source · line 116 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+EA:Nat -> @+A:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+EB:Nat -> @+B:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+MX:Nat -> @+yp:Nat -> @+sx:Nat -> @+sy:Nat -> @+XX:Nat -> @+XY:Nat -> @+hA:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(sx, MX) : Nat} -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(sy, 1n+yp) : Nat} -> @+a53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A)) == True{} : Bool} -> @+a52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A)) == False{} : Bool} -> @+b53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B)) == True{} : Bool} -> @+b52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B)) == False{} : Bool} -> @+hEAx:{Nat.add(EA, sx) == Nat.add(XX, 2171n) : Nat} -> @+hEBy:{Nat.add(EB, sy) == Nat.add(XY, 2171n) : Nat} -> @+hsx:{Nat.is_le(sx, 53n) == True{} : Bool} -> @+hsy:{Nat.is_le(sy, 53n) == True{} : Bool} -> @+hXX:{Nat.is_le(1926n, XX) == True{} : Bool} -> @+hXY:{Nat.is_le(XY, 3971n) == True{} : Bool} -> @+hge0:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_q(s, Nat.sub(Nat.add(EA, Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off, 1022n)), EB), A, B) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 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.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def dcore_c source · line 147 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+EA:Nat -> @+A:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+EB:Nat -> @+B:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+MX:Nat -> @+yp:Nat -> @+sx:Nat -> @+sy:Nat -> @+XX:Nat -> @+XY:Nat -> @+hA:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(sx, MX) : Nat} -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(sy, 1n+yp) : Nat} -> @+a53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A)) == True{} : Bool} -> @+a52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A)) == False{} : Bool} -> @+b53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B)) == True{} : Bool} -> @+b52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B)) == False{} : Bool} -> @+hEAx:{Nat.add(EA, sx) == Nat.add(XX, 2171n) : Nat} -> @+hEBy:{Nat.add(EB, sy) == Nat.add(XY, 2171n) : Nat} -> @+hsx:{Nat.is_le(sx, 53n) == True{} : Bool} -> @+hsy:{Nat.is_le(sy, 53n) == True{} : Bool} -> @+hXX:{Nat.is_le(1926n, XX) == True{} : Bool} -> @+hXY:{Nat.is_le(XY, 3971n) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B)) == c : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_ab(s, EA, A, EB, B, c) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 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.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def dcore source · line 154 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Bool -> @+EA:Nat -> @+A:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+EB:Nat -> @+B:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+MX:Nat -> @+yp:Nat -> @+sx:Nat -> @+sy:Nat -> @+XX:Nat -> @+XY:Nat -> @+hA:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(sx, MX) : Nat} -> @+hB:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(sy, 1n+yp) : Nat} -> @+a53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A)) == True{} : Bool} -> @+a52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(A)) == False{} : Bool} -> @+b53:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(53n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B)) == True{} : Bool} -> @+b52:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(52n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(B)) == False{} : Bool} -> @+hEAx:{Nat.add(EA, sx) == Nat.add(XX, 2171n) : Nat} -> @+hEBy:{Nat.add(EB, sy) == Nat.add(XY, 2171n) : Nat} -> @+hsx:{Nat.is_le(sx, 53n) == True{} : Bool} -> @+hsy:{Nat.is_le(sy, 53n) == True{} : Bool} -> @+hXX:{Nat.is_le(1926n, XX) == True{} : Bool} -> @+hXY:{Nat.is_le(XY, 3971n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.div_n(s, EA, A, EB, B) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(s, 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.sub(Nat.add(XX, 3000n), Nat.add(Nat.add(XY, 200n), 1n))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}