proofs/math/typed/f64sqk.bend checks

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

11 imports

import Base
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/sqrtn.bend as SQ
import ./width.bend as WW
import ./f64sqa.bend as AQ
import ./f64sqn.bend as QN
import ./w64dm.bend as DM
import ./w64div.bend as W64D

Definitions

def sqa source · line 18 · raw

@+a:Nat -> @+b:Nat -> {Nat.mul(Nat.add(a, b), Nat.add(a, b)) == Nat.add(Nat.add(Nat.mul(a, a), Nat.add(Nat.mul(a, b), Nat.mul(a, b))), Nat.mul(b, b)) : Nat}

(a + b)^2 expanded

def uw2 source · line 22 · raw

@+s:Nat -> @+w:Nat -> @+D:Nat -> @+hD:{Nat.add(s, s) == D : Nat} -> {Nat.add(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s), w), Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s), w)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.mul(w, D)) : Nat}

2 (s 2^32) w == (w D) 2^32 for D = 2 s

def usq source · line 26 · raw

@+s:Nat -> @+r:Nat -> @+n:Nat -> @+hn:{Nat.add(Nat.mul(s, s), r) == n : Nat} -> {Nat.add(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, s)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, r))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, n)) : Nat}

(s 2^32)^2 + r 2^64 == n 2^64 for s^2 + r == n

def qb source · line 32 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:Nat -> @+q:Nat -> @+D:Nat -> @+hq:{Nat.is_le(Nat.mul(q, D), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, r)) == True{} : Bool} -> @+hr:{Nat.is_le(r, D) == True{} : Bool} -> @+hD:{Nat.is_lt(0n, D) == True{} : Bool} -> {Nat.is_le(q, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one)) == True{} : Bool}

from below: n 2^64 < (S0 + 1)^2, so isqrt(n 2^64) <= S0 from above: S0^2 <= n 2^64 + q^2 q <= 2^32: q D <= r 2^32 <= D 2^32 < (2^32 + 1) D

def four source · line 40 · raw

@+x:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(2n, x) == Nat.add(Nat.add(x, x), Nat.add(x, x)) : Nat}

def two_mul source · line 43 · raw

@+x:Nat -> {Nat.mul(x, 2n) == Nat.add(x, x) : Nat}

def t3 source · line 47 · raw

@+T:Nat -> {Nat.is_lt(Nat.add(Nat.mul(1n+T, 1n+T), Nat.add(Nat.add(T, T), Nat.add(T, T))), Nat.mul(Nat.add(1n+T, 2n), Nat.add(1n+T, 2n))) == True{} : Bool}

(T + 3)^2 exceeds (T + 1)^2 + 4 T

def k_hi_c source · line 58 · raw

@+X:Nat -> @+T:Nat -> @+S:Nat -> @+hlt:{Nat.is_lt(Nat.mul(S, S), Nat.add(Nat.mul(1n+T, 1n+T), Nat.add(Nat.add(T, T), Nat.add(T, T)))) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(S, Nat.add(T, 2n)) == c : Bool} -> {c == True{} : Bool}