~/bend-docscommunity

proofs/math/natural/roots.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/math/natural/roots.bend as Roots

13 imports
import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../../spec/lib/common.bend as SC
import ../../lib/lemmas/proofs/nat_algebra.bend as A
import ../../lib/lemmas/proofs/natural_products.bend as PR
import ../../../src/math/natural.bend as M
import ../../../src/math/pow2.bend as P2
import ../pow2/pow2.bend as PP
import ./arith.bend as R
import ./lcm.bend as LC
import ./fact.bend as F
import ./bits.bend as B

Definitions

def pow_pos source · line 23 · raw

@+rp:Nat -> @+j:Nat -> {Nat.is_lt(0n, Nat.pow(1n+rp, j)) == True{} : Bool}

def le_mul_pos source · line 31 · raw

@+x:Nat -> @+y:Nat -> @+hy:{Nat.is_lt(0n, y) == True{} : Bool} -> {Nat.is_le(x, Nat.mul(x, y)) == True{} : Bool}

x <= x y for y > 0

def pow_le_case source · line 40 · raw

@+j:Nat -> @+rp:Nat -> @+acc:Nat -> @+n:Nat -> @+ok:Bool -> @+hk:{ok == Nat.is_le(Nat.mul(acc, 1n+rp), n) : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.pow_le_go(1n+j, 1n+rp, acc, n, ok) == Nat.is_le(Nat.mul(Nat.mul(acc, 1n+rp), Nat.pow(1n+rp, j)), n) : Bool}

the division-guarded loop computes (acc r) r^j <= n

def root_le_ok source · line 55 · raw

@+n:Nat -> @+k:Nat -> @+r:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.root_le(n, k, r) == Nat.is_le(Nat.pow(r, k), n) : Bool}

root_le(n, k, r) is r^k <= n

def two_mul source · line 69 · raw

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

x 2 == x + x

def lo_lt_mid source · line 73 · raw

@+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_lt(1n+lo, hi) == True{} : Bool} -> {Nat.is_lt(lo, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.mid(lo, hi)) == True{} : Bool}

lo + 1 < hi gives lo < (lo + hi) / 2

def mid_lt_hi source · line 81 · raw

@+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_lt(lo, hi) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.mid(lo, hi), hi) == True{} : Bool}

lo < hi gives (lo + hi) / 2 < hi

def lt_sub source · line 89 · raw

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

b < c <= a gives a - c < a - b

def lt_sub2 source · line 109 · raw

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

a < b and c <= a give a - c < b - c

def sub_pos source · line 125 · raw

@+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_lt(lo, hi) == True{} : Bool} -> {Nat.is_lt(0n, Nat.sub(hi, lo)) == True{} : Bool}

lo < hi gives 0 < hi - lo

def root_ok source · line 137 · raw

@+n:Nat -> @+k:Nat -> @+r:Nat -> Type

the answer r: r^k <= n < (r + 1)^k, through root_le

def no_fuel source · line 140 · raw

@+lo:Nat -> @+hi:Nat -> @+hlt:{Nat.is_lt(lo, hi) == True{} : Bool} -> @+hf:{Nat.is_le(Nat.sub(hi, lo), 0n) == True{} : Bool} -> Empty

def done_ok source · line 144 · raw

@+n:Nat -> @+k:Nat -> @+lo:Nat -> @+hi:Nat -> @+hlo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.root_le(n, k, lo) == True{} : Bool} -> @+hhi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.root_le(n, k, hi) == False{} : Bool} -> @+hlt:{Nat.is_lt(lo, hi) == True{} : Bool} -> @+hm:{False{} == Nat.is_lt(1n+lo, hi) : Bool} -> root_ok(n, k, lo)

lo + 1 >= hi with lo < hi: the interval is [lo, lo + 1)

def shrink source · line 149 · raw

@+x:Nat -> @+y:Nat -> @+f:Nat -> @+h:{Nat.is_lt(x, y) == True{} : Bool} -> @+hf:{Nat.is_le(y, 1n+f) == True{} : Bool} -> {Nat.is_le(x, f) == True{} : Bool}

the interval shrinks: a step fits in the remaining fuel

def search_ok source · line 152 · raw

@fuel:Nat -> @+n:Nat -> @+k:Nat -> @+lo:Nat -> @+hi:Nat -> @+more:Bool -> @+ok:Bool -> @+hlo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.root_le(n, k, lo) == True{} : Bool} -> @+hhi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.root_le(n, k, hi) == False{} : Bool} -> @+hlt:{Nat.is_lt(lo, hi) == True{} : Bool} -> @+hf:{Nat.is_le(Nat.sub(hi, lo), fuel) == True{} : Bool} -> @+hm:{more == Nat.is_lt(1n+lo, hi) : Bool} -> @+hok:{ok == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.root_le(n, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.mid(lo, hi)) : Bool} -> root_ok(n, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.search_go(fuel, n, k, lo, hi, more, ok))

def search_top source · line 177 · raw

@+n:Nat -> @+k:Nat -> @+lo:Nat -> @+hi:Nat -> @+hlo:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.root_le(n, k, lo) == True{} : Bool} -> @+hhi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.root_le(n, k, hi) == False{} : Bool} -> @+hlt:{Nat.is_lt(lo, hi) == True{} : Bool} -> root_ok(n, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.search(n, k, lo, hi))

def pow2_add source · line 183 · raw

@+x:Nat -> @+y:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(Nat.add(x, y)) == Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(x), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(y)) : Nat}

2^(x + y) == 2^x 2^y

def pow_pow2 source · line 193 · raw

@+a:Nat -> @+k:Nat -> {Nat.pow(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(a), k) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(Nat.mul(k, a)) : Nat}

(2^a)^k == 2^(k a)

def bl_le source · line 203 · raw

@+kp:Nat -> @+bl:Nat -> {Nat.is_le(bl, Nat.mul(1n+kp, 1n+Nat.div(bl, 1n+kp))) == True{} : Bool}

L <= k (1 + L / k)

def hi_bound source · line 213 · raw

@+n:Nat -> @+kp:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.root_le(n, 1n+kp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/pow2.pow2t(1n+Nat.div(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.bit_length(n), 1n+kp))) == False{} : Bool}

n < (2^(1 + L/k))^k

def hi_pos source · line 222 · raw

@+a:Nat -> {Nat.is_lt(0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/pow2.pow2t(a)) == True{} : Bool}

def root_top source · line 226 · raw

@+n:Nat -> @+kp:Nat -> root_ok(n, 1n+kp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.search(n, 1n+kp, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/pow2.pow2t(1n+Nat.div(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.bit_length(n), 1n+kp))))

def ok_le source · line 231 · raw

@+n:Nat -> @+k:Nat -> @+r:Nat -> @p:root_ok(n, k, r) -> {Nat.is_le(Nat.pow(r, k), n) == True{} : Bool}

def ok_lt source · line 235 · raw

@+n:Nat -> @+k:Nat -> @+r:Nat -> @p:root_ok(n, k, r) -> {Nat.is_lt(n, Nat.pow(1n+r, k)) == True{} : Bool}

def iroot_k_ok source · line 239 · raw

@+n:Nat -> @+kp:Nat -> root_ok(n, 1n+kp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.iroot_k(n, 1n+kp))

def iroot_done source · line 248 · raw

@+n:Nat -> @+kp:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.iroot(n, 1n+kp) == Done{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.iroot_k(n, 1n+kp)} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>}

iroot(n, k) == Done{r} with r^k <= n < (r + 1)^k for k >= 1, Domain for k == 0

def iroot_zero source · line 251 · raw

@+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.iroot(n, 0n) == Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.Domain{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>}

def iroot_le source · line 254 · raw

@+n:Nat -> @+kp:Nat -> {Nat.is_le(Nat.pow(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.iroot_k(n, 1n+kp), 1n+kp), n) == True{} : Bool}

def lt_succ_iroot source · line 257 · raw

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