primes.bend source
primes.bend on the hub · documented module
# 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.import Baseimport ./nat.bend as N# ---------------------------------------------------------------------# two decisions about <=, both by plain induction (no Bool reflection)# ---------------------------------------------------------------------# totality: either a <= b, or b < a. Written in continuation-passing# style because the two conclusions are different propositions.def Nat.le_total(a: Nat, b: Nat, -P: Type, kl: N.Nat.Le(a, b) -> P, kr: N.Nat.Le(1n+b, a) -> P) -> P: match a b: case 0n 0n: kl(Unit{}) case 0n 1n+q: kl(Unit{}) case 1n+p 0n: kr(Unit{}) case 1n+p 1n+q: Nat.le_total(p, q, P, kl, kr)# a <= b is either a = b or a < bdef Nat.le_split(a: Nat, b: Nat, h: N.Nat.Le(a, b), -P: Type, keq: {a == b : Nat} -> P, klt: N.Nat.Le(1n+a, b) -> P) -> P: match a b: case 0n 0n: keq({==}) case 0n 1n+q: klt(Unit{}) case 1n+p 0n: match h: case 1n+p 1n+q: +p2 = p +q2 = q Nat.le_split(p2, q2, h, P, e => keq(Equal.cong(Nat, Nat, x => 1n+x, p2, q2, e)), klt)# an order proof is not Data, so a hypothesis needed twice is copied in CPSdef Nat.le_copy(a: Nat, b: Nat, h: N.Nat.Le(a, b), -Q: Type, k: N.Nat.Le(a, b) -> N.Nat.Le(a, b) -> Q) -> Q: match a b: case 0n 0n: k(Unit{}, Unit{}) case 0n 1n+q: k(Unit{}, Unit{}) case 1n+p 0n: match h: case 1n+p 1n+q: Nat.le_copy(p, q, h, Q, k)# transporting an order proof along an equation of its left sidedef Nat.le_cast(-x: Nat, -y: Nat, -c: Nat, e: {x == y : Nat}, h: N.Nat.Le(x, c)) -> N.Nat.Le(y, c): %e : N.Nat.Le(_, c) h# nothing above d is below d: 1 + (d + m) <= d is absurddef Nat.le_absurd(d: Nat, -m: Nat, h: N.Nat.Le(1n+Nat.add(d, m), d)) -> Empty: match d: case 0n: match h: case 1n+dp: Nat.le_absurd(dp, m, h)# ---------------------------------------------------------------------# divisibility, as an existential: some quotient makes the product exact# ---------------------------------------------------------------------def Dvd(d: Nat, x: Nat) -> Type: &q: Nat -> {Nat.mul(q, d) == x : Nat}# 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.open(-d: Nat, -x: Nat, w: Dvd(d, x), -P: Type, k: @q: Nat -> @e: {Nat.mul(q, d) == x : Nat} -> P) -> P: (q, prf) = w k(q, prf)# every number divides itselfdef Dvd.refl(+d: Nat) -> Dvd(d, d): (1n, N.Nat.one_mul(d))# if e divides d and d divides x then e divides xdef Dvd.trans.fin(+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): (Nat.mul(b, a), Equal.trans(Nat, Nat.mul(Nat.mul(b, a), e), Nat.mul(b, d), x, Equal.trans(Nat, Nat.mul(Nat.mul(b, a), e), Nat.mul(b, Nat.mul(a, e)), Nat.mul(b, d), Equal.sym(Nat, Nat.mul(b, Nat.mul(a, e)), Nat.mul(Nat.mul(b, a), e), N.Nat.mul_assoc(b, a, e)), Equal.cong(Nat, Nat, z => Nat.mul(b, z), Nat.mul(a, e), d, ha)), hb))def Dvd.trans(+e: Nat, +d: Nat, +x: Nat, hed: Dvd(e, d), hdx: Dvd(d, x)) -> Dvd(e, x): Dvd.open(e, d, hed, Dvd(e, x), a => ha => Dvd.open(d, x, hdx, Dvd(e, x), b => hb => Dvd.trans.fin(e, d, x, a, ha, b, hb)))# ---------------------------------------------------------------------# uniqueness of the remainder, in the only form the mod proof needs:# if q0*d + r = q*d and r < d then r is zero.# ---------------------------------------------------------------------def Nat.mul_rem_zero(q0: Nat, q: Nat, +dp: Nat, +r: Nat, e: {Nat.add(Nat.mul(q0, 1n+dp), r) == Nat.mul(q, 1n+dp) : Nat}, hr: N.Nat.Le(r, dp)) -> {r == 0n : Nat}: match q0 q: case 0n 0n: e case 0n 1n+qq: +qq2 = qq Empty.absurd({r == 0n : Nat}, Nat.le_absurd(dp, Nat.mul(qq2, 1n+dp), Nat.le_cast(r, 1n+Nat.add(dp, Nat.mul(qq2, 1n+dp)), dp, e, hr))) case 1n+q0p 0n: +q0p2 = q0p Empty.absurd({r == 0n : Nat}, N.Nat.succ_neq_zero(Nat.add(Nat.add(dp, Nat.mul(q0p2, 1n+dp)), r), e)) case 1n+q0p 1n+qq: +q0p2 = q0p +qq2 = qq Nat.mul_rem_zero(q0p2, qq2, dp, r, N.Nat.add_cancel_l(dp, Nat.add(Nat.mul(q0p2, 1n+dp), r), Nat.mul(qq2, 1n+dp), Equal.trans(Nat, Nat.add(dp, Nat.add(Nat.mul(q0p2, 1n+dp), r)), Nat.add(Nat.add(dp, Nat.mul(q0p2, 1n+dp)), r), Nat.add(dp, Nat.mul(qq2, 1n+dp)), N.Nat.add_assoc(dp, Nat.mul(q0p2, 1n+dp), r), N.Nat.succ_inj(Nat.add(Nat.add(dp, Nat.mul(q0p2, 1n+dp)), r), Nat.add(dp, Nat.mul(qq2, 1n+dp)), e))), hr)# ---------------------------------------------------------------------# a divisor of 2 or more cannot divide two consecutive numbers: b*d is# never 1 + a*d when d >= 2. (This is "p | N and p | N+1 gives p | 1",# in the only instance Euclid needs.)# ---------------------------------------------------------------------def Nat.succ_not_mul(a: Nat, b: Nat, +pv: Nat, e: {Nat.mul(b, 2n+pv) == 1n+Nat.mul(a, 2n+pv) : Nat}) -> Empty: match a b: case 0n 0n: N.Nat.zero_neq_succ(0n, e) case 0n 1n+bp: +bp2 = bp N.Nat.succ_neq_zero(Nat.add(pv, Nat.mul(bp2, 2n+pv)), N.Nat.succ_inj(1n+Nat.add(pv, Nat.mul(bp2, 2n+pv)), 0n, e)) case 1n+ap 0n: +ap2 = ap N.Nat.zero_neq_succ(2n+Nat.add(pv, Nat.mul(ap2, 2n+pv)), e) case 1n+ap 1n+bp: +ap2 = ap +bp2 = bp Nat.succ_not_mul(ap2, bp2, pv, N.Nat.add_cancel_l(pv, Nat.mul(bp2, 2n+pv), 1n+Nat.mul(ap2, 2n+pv), Equal.trans(Nat, Nat.add(pv, Nat.mul(bp2, 2n+pv)), 1n+Nat.add(pv, Nat.mul(ap2, 2n+pv)), Nat.add(pv, 1n+Nat.mul(ap2, 2n+pv)), N.Nat.succ_inj(Nat.add(pv, Nat.mul(bp2, 2n+pv)), 1n+Nat.add(pv, Nat.mul(ap2, 2n+pv)), N.Nat.succ_inj(1n+Nat.add(pv, Nat.mul(bp2, 2n+pv)), 2n+Nat.add(pv, Nat.mul(ap2, 2n+pv)), e)), Equal.sym(Nat, Nat.add(pv, 1n+Nat.mul(ap2, 2n+pv)), 1n+Nat.add(pv, Nat.mul(ap2, 2n+pv)), N.Nat.add_succ(pv, Nat.mul(ap2, 2n+pv))))))def Dvd.consecutive(+pv: Nat, +x: Nat, hx: Dvd(2n+pv, x), hx1: Dvd(2n+pv, 1n+x)) -> Empty: Dvd.open(2n+pv, x, hx, Empty, a => ha => Dvd.open(2n+pv, 1n+x, hx1, Empty, b => hb => Nat.succ_not_mul(a, b, pv, Equal.trans(Nat, Nat.mul(b, 2n+pv), 1n+x, 1n+Nat.mul(a, 2n+pv), hb, Equal.cong(Nat, Nat, z => 1n+z, x, Nat.mul(a, 2n+pv), Equal.sym(Nat, Nat.mul(a, 2n+pv), x, ha))))))# ---------------------------------------------------------------------# the factorial, and the two facts Euclid asks of it# ---------------------------------------------------------------------def fact(n: Nat) -> Nat: match n: case 0n: 1n case 1n+p: +p2 = p Nat.mul(1n+p2, fact(p2))# n! is never zero, so n! + 1 is at least twodef fact_pos.con(+p: Nat, +m0: Nat, e: {fact(p) == 1n+m0 : Nat}) -> (&m: Nat -> {fact(1n+p) == 1n+m : Nat}): (Nat.add(m0, Nat.mul(p, 1n+m0)), %Equal.sym(Nat, fact(p), 1n+m0, e) : {Nat.mul(1n+p, _) == 1n+Nat.add(m0, Nat.mul(p, 1n+m0)) : Nat} {==})def fact_pos.step(+p: Nat, w: (&m: Nat -> {fact(p) == 1n+m : Nat})) -> (&m: Nat -> {fact(1n+p) == 1n+m : Nat}): (m0, e) = w fact_pos.con(p, m0, e)def fact_pos(n: Nat) -> (&m: Nat -> {fact(n) == 1n+m : Nat}): match n: case 0n: (0n, {==}) case 1n+p: +p2 = p fact_pos.step(p2, fact_pos(p2))# every d with 1 <= d <= n divides n! -- the top factor when d = n,# and the induction hypothesis times (1+p) otherwisedef fact_div.eq(+p: Nat, +dv: Nat, eq: {1n+dv == 1n+p : Nat}) -> Dvd(1n+dv, fact(1n+p)): (fact(p), %Equal.sym(Nat, 1n+dv, 1n+p, eq) : {Nat.mul(fact(p), _) == fact(1n+p) : Nat} N.Nat.mul_comm(fact(p), 1n+p))def fact_div.con(+p: Nat, +dv: Nat, +q0: Nat, prf: {Nat.mul(q0, 1n+dv) == fact(p) : Nat}) -> Dvd(1n+dv, fact(1n+p)): (Nat.mul(1n+p, q0), Equal.trans(Nat, Nat.mul(Nat.mul(1n+p, q0), 1n+dv), Nat.mul(1n+p, Nat.mul(q0, 1n+dv)), fact(1n+p), Equal.sym(Nat, Nat.mul(1n+p, Nat.mul(q0, 1n+dv)), Nat.mul(Nat.mul(1n+p, q0), 1n+dv), N.Nat.mul_assoc(1n+p, q0, 1n+dv)), Equal.cong(Nat, Nat, z => Nat.mul(1n+p, z), Nat.mul(q0, 1n+dv), fact(p), prf)))def fact_div.up(+p: Nat, +dv: Nat, w: Dvd(1n+dv, fact(p))) -> Dvd(1n+dv, fact(1n+p)): Dvd.open(1n+dv, fact(p), w, Dvd(1n+dv, fact(1n+p)), q0 => prf => fact_div.con(p, dv, q0, prf))def fact_div(n: Nat, +dv: Nat, h: N.Nat.Le(1n+dv, n)) -> Dvd(1n+dv, fact(n)): match n: case 0n: match h: case 1n+p: +p2 = p Nat.le_split(1n+dv, 1n+p2, h, Dvd(1n+dv, fact(1n+p2)), eq => fact_div.eq(p2, dv, eq), lt => fact_div.up(p2, dv, fact_div(p2, dv, lt)))