proofs/math/typed/f64sqn.bend checks

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

10 imports

import Base
import ./natlight.bend as NL
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/arith.bend as NR
import ./width.bend as WW
import ./f64round.bend as FR
import ./f64sqa.bend as AQ

Definitions

def mul1 source · line 16 · raw

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

def two_mul source · line 19 · raw

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

def c14 source · line 22 · raw

@+S:Nat -> {Nat.mul(S, 14n) == Nat.add(Nat.add(S, S), Nat.mul(S, 12n)) : Nat}

def le_cancel_true source · line 25 · raw

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

def nw_lo source · line 29 · raw

@+N:Nat -> @+S:Nat -> @+c:Nat -> @+d:Nat -> @+rp:Nat -> @+hS:{S == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(N) : Nat} -> @+hc:{Nat.add(c, d) == S : Nat} -> @+hr:{Nat.add(S, d) == 1n+rp : Nat} -> {Nat.is_le(Nat.add(S, S), Nat.add(Nat.add(S, d), Nat.div(N, 1n+rp))) == True{} : Bool}

the lower bound: 2 S <= r0 + Q, with S = c + d and r0 = S + d

def nw_prod source · line 41 · raw

@+S:Nat -> @+d:Nat -> @+c3:Nat -> @+hc3:{Nat.add(c3, d) == Nat.add(S, 14n) : Nat} -> @+hdd:{Nat.is_le(Nat.add(Nat.mul(d, d), 1n), Nat.mul(S, 12n)) == True{} : Bool} -> {Nat.is_le(Nat.mul(1n+S, 1n+S), Nat.mul(c3, Nat.add(S, d))) == True{} : Bool}

the product bound: (1 + S)^2 <= c3 * r0 when c3 + d = S + 14 and d^2 + 1 <= 12 S

def nw_hi source · line 56 · raw

@+N:Nat -> @+S:Nat -> @+d:Nat -> @+rp:Nat -> @+c3:Nat -> @+hS:{S == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(N) : Nat} -> @+hr:{Nat.add(S, d) == 1n+rp : Nat} -> @+hc3:{Nat.add(c3, d) == Nat.add(S, 14n) : Nat} -> @+hdd:{Nat.is_le(Nat.add(Nat.mul(d, d), 1n), Nat.mul(S, 12n)) == True{} : Bool} -> {Nat.is_le(Nat.add(Nat.add(S, d), Nat.div(N, 1n+rp)), Nat.add(13n, Nat.add(S, S))) == True{} : Bool}

the upper bound: r0 + Q <= 2 S + 13

def half_lo source · line 66 · raw

@+S:Nat -> @+n:Nat -> @+h:{Nat.is_le(Nat.add(S, S), n) == True{} : Bool} -> {Nat.is_le(S, Nat.div(n, 2n)) == True{} : Bool}

halving: S <= (r0 + Q) / 2 <= S + 6

def half_hi source · line 69 · raw

@+S:Nat -> @+n:Nat -> @+h:{Nat.is_le(n, Nat.add(13n, Nat.add(S, S))) == True{} : Bool} -> {Nat.is_le(Nat.div(n, 2n), Nat.add(6n, S)) == True{} : Bool}