proofs/math/natural/sqrtn.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/natural/sqrtn.bend as Sqrtn

10 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as A
import ../../../src/math/natural.bend as M
import ../../../src/math/pow2.bend as P2
import ./arith.bend as R
import ./bits.bend as B
import ./roots.bend as RT
import ./logs.bend as LG

Definitions

def succ_mul_succ source · line 23 · raw

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

(1 + u)(1 + v) == 1 + ((u + v) + u v)

def le_add2 source · line 28 · raw

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

a <= b and c <= d give a + c <= b + d

def add_two source · line 32 · raw

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

(1 + x) + (1 + y) == 2 + (x + y)

def prod_le source · line 36 · raw

@+u:Nat -> @+v:Nat -> @+w:Nat -> @+h:{Nat.is_le(Nat.add(u, v), Nat.add(w, w)) == True{} : Bool} -> {Nat.is_le(Nat.mul(u, v), Nat.mul(w, w)) == True{} : Bool}

u + v <= 2 w gives u v <= w w

def stop_sq source · line 55 · raw

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

def le_zero source · line 67 · raw

@+g:Nat -> @+h:{Nat.is_le(g, 0n) == True{} : Bool} -> {g == 0n : Nat}

def iter_sq source · line 74 · raw

@fuel:Nat -> @+n:Nat -> @+g:Nat -> @+m:Nat -> @+down:Bool -> @+hm:{m == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.sqrt_next(n, g) : Nat} -> @+hd:{down == Nat.is_lt(m, g) : Bool} -> @+hf:{Nat.is_le(g, fuel) == True{} : Bool} -> {Nat.is_le(Nat.mul(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.sqrt_iter(fuel, n, g, m, down), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.sqrt_iter(fuel, n, g, m, down)), n) == True{} : Bool}

def step_lt source · line 89 · raw

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

def step_any source · line 116 · raw

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

def iter_lt source · line 123 · raw

@fuel:Nat -> @+n:Nat -> @+g:Nat -> @+m:Nat -> @+down:Bool -> @+hm:{m == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.sqrt_next(n, g) : Nat} -> @+hd:{down == Nat.is_lt(m, g) : Bool} -> @+hn:{Nat.is_lt(n, Nat.mul(1n+g, 1n+g)) == True{} : Bool} -> {Nat.is_lt(n, Nat.mul(1n+0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.sqrt_iter(fuel, n, g, m, down), 1n+0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.sqrt_iter(fuel, n, g, m, down))) == True{} : Bool}

def g0_bound source · line 136 · raw

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

def isqrt_le source · line 143 · raw

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

isqrt(n)^2 <= n (Mathlib Nat.sqrt_le')

def lt_succ_isqrt source · line 149 · raw

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

n < (isqrt(n) + 1)^2 (Mathlib Nat.lt_succ_sqrt')