~/bend-docscommunity

primes.bend checks

raw source on the hub · import 0xd5e9362591c1667c9894b781190e1ac9/primes.bend as Primes

lib/primes.bend -- the structural number theory behind Euclid's theorem.

Everything here is about Base's own Nat.add / Nat.mul, on top of the semiring laws of ./nat.bend. Nothing in this file mentions a Bool test; the bridge to the trial division of demos/math/mathlib.bend lives in demos/math/euclid.bend, which imports this file.

The one convention that shapes every proof: Nat.mul recurses on its FIRST argument, so "d divides x" is written with the quotient first, Nat.mul(q, d) == x. Then mul(0n, d) and mul(1n+q, d) both reduce for a symbolic divisor d, and the divisibility inductions compute.

Reading a proof: match x refines the goal per constructor, a recursive call is the induction hypothesis, {==} closes a goal whose two sides compute to the same term, and %e : P rewrites with an equation e : {a == b}: the goal must be P with b at the _ marks, and what follows proves P with a there.

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

Definitions

def Nat.le_total source · line 28 · raw

@a:Nat -> @b:Nat -> @-P:Type -> @kl:(@_:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(a, b) -> P) -> @kr:(@_:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(1n+b, a) -> P) -> P

totality: either a <= b, or b < a. Written in continuation-passing style because the two conclusions are different propositions.

def Nat.le_split source · line 40 · raw

@a:Nat -> @b:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(a, b) -> @-P:Type -> @keq:(@_:{a == b : Nat} -> P) -> @klt:(@_:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(1n+a, b) -> P) -> P

a <= b is either a = b or a < b

def Nat.le_copy source · line 54 · raw

@a:Nat -> @b:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(a, b) -> @-Q:Type -> @k:(@_:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(a, b) -> @_:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(a, b) -> Q) -> Q

an order proof is not Data, so a hypothesis needed twice is copied in CPS

def Nat.le_cast source · line 66 · raw

@-x:Nat -> @-y:Nat -> @-c:Nat -> @e:{x == y : Nat} -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(x, c) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(y, c)

transporting an order proof along an equation of its left side

def Nat.le_absurd source · line 71 · raw

@d:Nat -> @-m:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(1n+Nat.add(d, m), d) -> Empty

nothing above d is below d: 1 + (d + m) <= d is absurd

def Dvd source · line 82 · raw

@d:Nat -> @x:Nat -> Type

def Dvd.open source · line 87 · raw

@-d:Nat -> @-x:Nat -> @w:Dvd(d, x) -> @-P:Type -> @k:(@q:Nat -> @e:{Nat.mul(q, d) == x : Nat} -> P) -> P

a sigma may only be destructured when it is a binder, so every use of a computed Dvd goes through an opener that takes it as a parameter.

def Dvd.refl source · line 92 · raw

@+d:Nat -> Dvd(d, d)

every number divides itself

def Dvd.trans.fin source · line 96 · raw

@+e:Nat -> @+d:Nat -> @+x:Nat -> @+a:Nat -> @ha:{Nat.mul(a, e) == d : Nat} -> @+b:Nat -> @hb:{Nat.mul(b, d) == x : Nat} -> Dvd(e, x)

if e divides d and d divides x then e divides x

def Dvd.trans source · line 104 · raw

@+e:Nat -> @+d:Nat -> @+x:Nat -> @hed:Dvd(e, d) -> @hdx:Dvd(d, x) -> Dvd(e, x)

def Nat.mul_rem_zero source · line 114 · raw

@q0:Nat -> @q:Nat -> @+dp:Nat -> @+r:Nat -> @e:{Nat.add(Nat.mul(q0, 1n+dp), r) == Nat.mul(q, 1n+dp) : Nat} -> @hr:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(r, dp) -> {r == 0n : Nat}

def Nat.succ_not_mul source · line 148 · raw

@a:Nat -> @b:Nat -> @+pv:Nat -> @e:{Nat.mul(b, 2n+pv) == 1n+Nat.mul(a, 2n+pv) : Nat} -> Empty

def Dvd.consecutive source · line 174 · raw

@+pv:Nat -> @+x:Nat -> @hx:Dvd(2n+pv, x) -> @hx1:Dvd(2n+pv, 1n+x) -> Empty

def fact source · line 185 · raw

@n:Nat -> Nat

def fact_pos.con source · line 194 · raw

@+p:Nat -> @+m0:Nat -> @e:{fact(p) == 1n+m0 : Nat} -> &m:Nat -> {fact(1n+p) == 1n+m : Nat}

n! is never zero, so n! + 1 is at least two

def fact_pos.step source · line 199 · raw

@+p:Nat -> @w:(&m:Nat -> {fact(p) == 1n+m : Nat}) -> &m:Nat -> {fact(1n+p) == 1n+m : Nat}

def fact_pos source · line 203 · raw

@n:Nat -> &m:Nat -> {fact(n) == 1n+m : Nat}

def fact_div.eq source · line 213 · raw

@+p:Nat -> @+dv:Nat -> @eq:{1n+dv == 1n+p : Nat} -> Dvd(1n+dv, fact(1n+p))

every d with 1 <= d <= n divides n! -- the top factor when d = n, and the induction hypothesis times (1+p) otherwise

def fact_div.con source · line 218 · raw

@+p:Nat -> @+dv:Nat -> @+q0:Nat -> @prf:{Nat.mul(q0, 1n+dv) == fact(p) : Nat} -> Dvd(1n+dv, fact(1n+p))

def fact_div.up source · line 224 · raw

@+p:Nat -> @+dv:Nat -> @w:Dvd(1n+dv, fact(p)) -> Dvd(1n+dv, fact(1n+p))

def fact_div source · line 227 · raw

@n:Nat -> @+dv:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(1n+dv, n) -> Dvd(1n+dv, fact(n))