~/bend-docscommunity

proofs/math/natural/proof.bend checks

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

16 imports
import Base
import ../../../src/math/natural.bend as M
import ../../../spec/lib/common.bend as SC
import ../../../spec/math/natural.bend as S
import ./arith.bend as R
import ./gcd.bend as G
import ./lcm.bend as LC
import ./fact.bend as F
import ./bits.bend as B
import ./roots.bend as RT
import ./sqrtn.bend as SQ
import ./logs.bend as LG
import ./modpow.bend as MP
import ./inverse.bend as IV
import ./lists.bend as LS
import ./misc.bend as MS

Definitions

def res_val source · line 26 · raw

@r:Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat> -> Nat

the value of a successful result, 0 on an error

def done_eq source · line 34 · raw

@+t:Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat> -> @+a:Nat -> @+b:Nat -> @+ha:{t == Done{a} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>} -> @+hb:{t == Done{b} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>} -> {a == b : Nat}

a result that is Done twice holds one value

def divides_left source · line 39 · raw

@+a:Nat -> @+b:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Gcd.divides_left(a, b)

def divides_right source · line 42 · raw

@+a:Nat -> @+b:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Gcd.divides_right(a, b)

def greatest source · line 45 · raw

@+a:Nat -> @+b:Nat -> @+d:Nat -> @+ka:Nat -> @+kb:Nat -> @+ea:{a == Nat.mul(ka, d) : Nat} -> @+eb:{b == Nat.mul(kb, d) : Nat} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Gcd.greatest(a, b, d, ka, kb, ea, eb)

def mul_left source · line 48 · raw

@+c:Nat -> @+a:Nat -> @+b:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Gcd.mul_left(c, a, b)

def lcm_divides_left source · line 51 · raw

@+a:Nat -> @+b:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Lcm.divides_left(a, b)

def lcm_divides_right source · line 54 · raw

@+a:Nat -> @+b:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Lcm.divides_right(a, b)

def least source · line 57 · raw

@+a:Nat -> @+b:Nat -> @+m:Nat -> @+x:Nat -> @+y:Nat -> @+ex:{m == Nat.mul(x, a) : Nat} -> @+ey:{m == Nat.mul(y, b) : Nat} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Lcm.least(a, b, m, x, y, ex, ey)

def gcd_mul_lcm source · line 60 · raw

@+a:Nat -> @+b:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Lcm.gcd_mul_lcm(a, b)

def gcd_all_divides source · line 65 · raw

@+xs:List<&2, Nat> -> @+i:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.GcdAll.divides(xs, i)

def gcd_all_greatest source · line 68 · raw

@+d:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.dvd_with(d, xs, ks) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.GcdAll.greatest(d, xs, ks, h)

def lcm_all_divides source · line 71 · raw

@+xs:List<&2, Nat> -> @+i:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.LcmAll.divides(xs, i)

def lcm_all_least source · line 74 · raw

@+m:Nat -> @+xs:List<&2, Nat> -> @+ks:List<&2, Nat> -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.mul_with(m, xs, ks) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.LcmAll.least(m, xs, ks, h)

def sum_value source · line 77 · raw

@+xs:List<&2, Nat> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Sum.value(xs)

def prod_value source · line 80 · raw

@+xs:List<&2, Nat> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Prod.value(xs)

def factorial_value source · line 85 · raw

@+n:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Factorial.value(n)

def perm_value source · line 88 · raw

@+n:Nat -> @+k:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Perm.value(n, k)

def perm_self source · line 91 · raw

@+n:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Perm.self(n)

def comb_value source · line 94 · raw

@+n:Nat -> @+k:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Comb.value(n, k)

def pascal source · line 97 · raw

@+m:Nat -> @+j:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Comb.pascal(m, j)

def factorials source · line 102 · raw

@+n:Nat -> @+k:Nat -> @+h:{Nat.is_le(k, n) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Comb.factorials(n, k, h)

def comb_zero source · line 106 · raw

@+n:Nat -> @+k:Nat -> @+h:{Nat.is_lt(n, k) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Comb.zero(n, k, h)

def isqrt_le source · line 111 · raw

@+n:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Isqrt.le(n)

def isqrt_lt_succ source · line 114 · raw

@+n:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Isqrt.lt_succ(n)

def iroot_done source · line 117 · raw

@+n:Nat -> @+kp:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Iroot.done(n, kp)

def iroot_value source · line 120 · raw

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

def iroot_le source · line 123 · raw

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

def iroot_lt_succ source · line 127 · raw

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

def zero_degree source · line 131 · raw

@+n:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Iroot.zero_degree(n)

def ilog_done source · line 134 · raw

@+np:Nat -> @+bq:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Ilog.done(np, bq)

def ilog_value source · line 137 · raw

@+np:Nat -> @+bq:Nat -> @+r:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.ilog(1n+np, 2n+bq) == Done{r} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/math/natural/logs.ilog_value(np, bq) == r : Nat}

def pow_le source · line 140 · raw

@+np:Nat -> @+bq:Nat -> @+r:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.ilog(1n+np, 2n+bq) == Done{r} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Ilog.pow_le(np, bq, r, h)

def lt_pow_succ source · line 144 · raw

@+np:Nat -> @+bq:Nat -> @+r:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.ilog(1n+np, 2n+bq) == Done{r} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Ilog.lt_pow_succ(np, bq, r, h)

def ilog_zero source · line 148 · raw

@+b:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Ilog.zero(b)

def small_base source · line 151 · raw

@+n:Nat -> @+b:Nat -> @+hb:{Nat.is_lt(b, 2n) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Ilog.small_base(n, b, hb)

def bit_length_lt source · line 154 · raw

@+n:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.BitLength.lt(n)

def bit_length_le source · line 157 · raw

@+np:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.BitLength.le(np)

def pow_mod_value source · line 162 · raw

@+b:Nat -> @+e:Nat -> @+mp:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.PowMod.value(b, e, mp)

def pow_mod_zero_modulus source · line 165 · raw

@+b:Nat -> @+e:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.PowMod.zero_modulus(b, e)

def inverse source · line 168 · raw

@+a:Nat -> @+mp:Nat -> @+x:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.mod_inverse(a, 1n+mp) == Done{x} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.ModInverse.inverse(a, mp, x, h)

def reduced source · line 171 · raw

@+a:Nat -> @+mp:Nat -> @+x:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.mod_inverse(a, 1n+mp) == Done{x} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.ModInverse.reduced(a, mp, x, h)

def factor_parts source · line 175 · raw

@+a:Nat -> @+mp:Nat -> @+g:Nat -> @+ka:Nat -> @+km:Nat -> @p:Pair({Nat.is_le(2n, g) == True{} : Bool}, Pair({a == Nat.mul(ka, g) : Nat}, {1n+mp == Nat.mul(km, g) : Nat})) -> Pair({Nat.is_le(2n, g) == True{} : Bool}, Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.dvd(g, a), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.dvd(g, 1n+mp)))

the shared factor g >= 2 and its two quotients, as dvd pairs

def not_coprime source · line 180 · raw

@+a:Nat -> @+mp:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.mod_inverse(a, 1n+mp) == Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.NotInvertible{}} : Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/natural.MathError, Nat>} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.ModInverse.not_coprime(a, mp, h)

def inverse_zero_modulus source · line 183 · raw

@+a:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.ModInverse.zero_modulus(a)

def divmod_value source · line 188 · raw

@+a:Nat -> @+bp:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.DivMod.value(a, bp)

def euclid source · line 191 · raw

@+a:Nat -> @+bp:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.DivMod.euclid(a, bp)

def rem_lt source · line 194 · raw

@+a:Nat -> @+bp:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.DivMod.rem_lt(a, bp)

def zero_divisor source · line 197 · raw

@+a:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.DivMod.zero_divisor(a)

def clamp_value source · line 200 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_le(lo, hi) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Clamp.value(x, lo, hi, h)

def clamp_ge source · line 203 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> @+h:{Nat.is_le(lo, hi) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Clamp.ge(x, lo, hi, h)

def clamp_le source · line 206 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Clamp.le(x, lo, hi)

def clamp_id source · line 209 · raw

@+x:Nat -> @+lo:Nat -> @+hi:Nat -> @+h1:{Nat.is_le(lo, x) == True{} : Bool} -> @+h2:{Nat.is_le(x, hi) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/math/natural.Clamp.id(x, lo, hi, h1, h2)

def domain source · line 212 · raw

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