~/bend-docscommunity

math.bend checks

raw source on the hub · import 0x4c3090ea8722081700f9d99ea7503e43/math.bend as Math

2 imports
import Base
import ./nat.bend as N

Laws

law collatz_27 provedsource · line 133 · raw

{collatz(200n, 27) == 111n : Nat}

law fib_fast_20 provedsource · line 139 · raw

{fib_fast(20) == 6765 : U32}

law pow_2_10 provedsource · line 145 · raw

{pow_u32(2, 10) == 1024 : U32}

law isqrt_16 provedsource · line 151 · raw

{isqrt(16) == 4 : U32}

law isqrt_0 provedsource · line 157 · raw

{isqrt(0) == 0 : U32}

law gcd_zero_r provedsource · line 189 · raw

@+a:U32 -> {gcd(a, 0) == a : U32}

law add_le_mono provedsource · line 199 · raw

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

add_le_mono: adding c to both sides preserves Nat order. Induction on c via N.add_zero_r (base) and N.add_succ_r (step, symmed since % rewrites RHS->LHS); 1n+_ is_le is definitional through Nat.cmp.

Definitions

def pow_go source · line 13 · raw

@fuel:Nat -> @+base:U32 -> @+exp:U32 -> @+acc:U32 -> U32

pow_u32: binary exponentiation, fixed 32 steps. pow_u32(base, exp) == base^exp (mod 2^32).

def pow_u32 source · line 25 · raw

@+base:U32 -> @+exp:U32 -> U32

def gcd_go source · line 30 · raw

@fuel:Nat -> @+a:U32 -> @+b:U32 -> U32

gcd: Euclidean algorithm, fixed 64 steps (> worst case ~47 for 32-bit). gcd(a, 0) == a, gcd(0, 0) == 0.

def gcd source · line 40 · raw

@+a:U32 -> @+b:U32 -> U32

def lcm_nonzero source · line 44 · raw

@+g:U32 -> @a:U32 -> @b:U32 -> U32

lcm: a / gcd(a,b) * b. Returns 0 when either side is 0.

def lcm source · line 47 · raw

@+a:U32 -> @+b:U32 -> U32

def isqrt_go source · line 53 · raw

@fuel:Nat -> @+n:U32 -> @+x:U32 -> U32

isqrt: floor(sqrt(n)). Integer Newton, fixed 32 steps, frozen when stable. Never divides by zero: div(n, 0) == 0 by Base, and x == 0 only when n == 0.

def isqrt source · line 61 · raw

@+n:U32 -> U32

def fib_go source · line 66 · raw

@n:Nat -> @a:U32 -> @+b:U32 -> U32

fib: nth Fibonacci (0, 1, 1, 2, 3, 5, ...). Tail loop over Nat fuel. Exact for n <= 47 (wraps mod 2^32 past that).

def fib source · line 73 · raw

@n:Nat -> U32

def fact_go source · line 77 · raw

@n:Nat -> @+i:U32 -> @acc:U32 -> U32

fact: n! . Tail loop. Exact for n <= 12 (wraps past that).

def fact source · line 84 · raw

@n:Nat -> U32

def tri source · line 89 · raw

@+n:U32 -> U32

tri: n*(n+1)/2 without overflow bias: (n/2)*((n|1)) style is overkill; plain version, wraps for huge n like everything else here.

def ff_step source · line 95 · raw

@+bit:U32 -> @+a:U32 -> @+b:U32 -> Pair(U32, U32)

fib_fast: doubling method, fixed 32 steps from bit 31 to bit 0. State (F(k), F(k+1)); bit 0 -> (F(2k), F(2k+1)); bit 1 -> (F(2k+1), F(2k+2)). 2*F(k+1) >= F(k) always, so the subtraction is exact (never wraps).

def ff_fin0 source · line 101 · raw

@q:Pair(U32, U32) -> U32

def ff_go source · line 105 · raw

@j:Nat -> @+n:U32 -> @q:Pair(U32, U32) -> U32

def fib_fast source · line 114 · raw

@+n:U32 -> U32

def collatz_go source · line 118 · raw

@fuel:Nat -> @+x:U32 -> @acc:Nat -> Nat

collatz: steps to reach 1 (fuel-capped; frozen once x == 1).

def collatz source · line 130 · raw

@fuel:Nat -> @+x:U32 -> Nat

def finv source · line 164 · raw

@x:F32 -> F32

F32 helpers (each is one cheap axiom call; F32 itself is unprovable).

def favg source · line 167 · raw

@+a:F32 -> @+b:F32 -> F32

def fclamp01 source · line 170 · raw

@x:F32 -> F32

def fdist2 source · line 173 · raw

@+x1:F32 -> @+y1:F32 -> @+x2:F32 -> @+y2:F32 -> F32

def fdist source · line 176 · raw

@+x1:F32 -> @+y1:F32 -> @+x2:F32 -> @+y2:F32 -> F32

def gcd_go_zero source · line 182 · raw

@fuel:Nat -> @+a:U32 -> U32

gcd_go_zero: frozen loop mirroring gcd_go(-, a, 0). Each gcd_go step with b == 0 has z = True, so both picks freeze (a, 0) -> (a, 0); the loop is definitionally the IH, and gcd(a, 0) normalizes to a (64n unrolls).