~/bend-docscommunity

proofs/math/typed/f64sqa.bend checks

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

11 imports
import Base
import ./natlight.bend as NL
import ../../../spec/lib/common.bend as C
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/sqrtn.bend as SQ
import ./width.bend as WW
import ./natcmp.bend as NC
import ./natfuel.bend as NF

Definitions

def sqm source · line 16 · raw

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

def isl source · line 19 · raw

@+n:Nat -> {Nat.is_le(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n)), n) == True{} : Bool}

def ilt source · line 22 · raw

@+n:Nat -> {Nat.is_lt(n, Nat.mul(1n+0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n), 1n+0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n))) == True{} : Bool}

def mle2 source · line 25 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+hab:{Nat.is_le(a, b) == True{} : Bool} -> @+hcd:{Nat.is_le(c, d) == True{} : Bool} -> {Nat.is_le(Nat.mul(a, c), Nat.mul(b, d)) == True{} : Bool}

def sqmono source · line 28 · raw

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

def ige_c source · line 31 · raw

@+n:Nat -> @+s:Nat -> @+h:{Nat.is_le(Nat.mul(s, s), n) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n)) == c : Bool} -> {c == True{} : Bool}

def isqrt_ge source · line 40 · raw

@+n:Nat -> @+s:Nat -> @+h:{Nat.is_le(Nat.mul(s, s), n) == True{} : Bool} -> {Nat.is_le(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n)) == True{} : Bool}

def ilt_c source · line 43 · raw

@+n:Nat -> @+s:Nat -> @+h:{Nat.is_lt(n, Nat.mul(s, s)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n), s) == c : Bool} -> {c == True{} : Bool}

def isqrt_lt source · line 52 · raw

@+n:Nat -> @+s:Nat -> @+h:{Nat.is_lt(n, Nat.mul(s, s)) == True{} : Bool} -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n), s) == True{} : Bool}

def isqrt_char source · line 55 · raw

@+n:Nat -> @+s:Nat -> @+h1:{Nat.is_le(Nat.mul(s, s), n) == True{} : Bool} -> @+h2:{Nat.is_lt(n, Nat.mul(1n+s, 1n+s)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n) == s : Nat}

def sh_sq source · line 59 · raw

@+j:Nat -> @+a:Nat -> {Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, a), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, a)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, Nat.mul(a, a))) : Nat}

shifting a square by j on both factors

def le_sh2 source · line 62 · raw

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

def lt_sh2 source · line 65 · raw

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

def sc_lo source · line 69 · raw

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

isqrt(n * 4^j) lies in [isqrt(n) * 2^j, (isqrt(n) + 1) * 2^j)

def sc_hi source · line 72 · raw

@+n:Nat -> @+j:Nat -> {Nat.is_lt(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 1n+0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n))) == True{} : Bool}

def sc_eq source · line 75 · raw

@+n:Nat -> @+j:Nat -> {Nat.add(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))) : Nat}

def sc_fit source · line 78 · raw

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

def sc_high source · line 84 · raw

@+n:Nat -> @+j:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.high(j, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n) : Nat}

def sc_low source · line 87 · raw

@+n:Nat -> @+j:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.low(j, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))) == Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n))) : Nat}

def eq_sh source · line 90 · raw

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

def eq_sh2 source · line 93 · raw

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

def sqlt source · line 96 · raw

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

def FR_or_t source · line 101 · raw

@+b:Bool -> {Bool.or(b, True{}) == True{} : Bool}

def sub_z source · line 108 · raw

@+a:Nat -> @+b:Nat -> @+h:{a == b : Nat} -> {Nat.sub(a, b) == 0n : Nat}

def sc_x_f source · line 112 · raw

@+n:Nat -> @+j:Nat -> @+hc:{Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n)), n) == False{} : Bool} -> @+d:Bool -> @+hd:{Nat.is_eq(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n))), 0n) == d : Bool} -> {Bool.or(Bool.not(Nat.is_eq(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n))), 0n)), Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))))) == True{} : Bool}

def sc_x_c source · line 124 · raw

@+n:Nat -> @+j:Nat -> @+c:Bool -> @+hc:{Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n)), n) == c : Bool} -> {Bool.or(Bool.not(Nat.is_eq(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n))), 0n)), Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))))) == Bool.not(c) : Bool}

def sc_x source · line 140 · raw

@+n:Nat -> @+j:Nat -> {Bool.or(Bool.not(Nat.is_eq(Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n))), 0n)), Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n)))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(j, n))))) == Bool.not(Nat.is_eq(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.isqrt(n)), n)) : Bool}