euclid.bend source
euclid.bend on the hub · documented module
import Baseimport ./mathlib.bend as Mimport ./nat.bend as Nimport ./primes.bend as P# ===========================================================================# euclid.bend -- THERE IS NO LARGEST PRIME, checked.## The theorem at the bottom of the file reads## for every n there is a p with n <= p and p is prime## and it is stated in the vocabulary of mathlib.bend, the tiny arithmetic# library the website's math card runs: `M.nat_le` is the Bool comparison# and `M.is_prime` is Bool trial division -- p is prime when 2 <= p and no# d with 2 <= d <= p-1 divides it, divisibility being "the remainder of# repeated subtraction is zero".## THE ARGUMENT, in plain words.## Let N = n! + 1. It is at least 2, so it has divisors above 1; let p be# the SMALLEST of them. Then## * p is prime, because a divisor of p is a divisor of N, and p was# the smallest one above 1: nothing between 2 and p-1 divides p.# * p > n, because every d between 2 and n divides n!, and no such d# can also divide n! + 1 -- it would have to divide 1.## So for every n there is a prime at least as large as n: no prime is# the largest.## THE PROOF, in the shape the checker wants. Three layers.## 1. Reflection (this file, first half). mathlib decides things with# Bools; the argument needs propositions. `M.nat_le`, `M.nat_eq` and# `M.msub` are reflected in both directions, and then the interesting# one: `M.mod` really is the remainder. mathlib computes it by# repeated subtraction under a fuel, so `mgo_lt` and `mgo_eq` prove,# by induction on that fuel, that the answer is below the divisor and# that quotient*divisor + answer is the input. Those two# turn `M.divides(d, x) == True{}` into "some q has q*d = x" and back# (`divides_elim`, `divides_intro`).## 2. Structure (../../lib/primes.bend). Divisibility as an existential,# its transitivity, the factorial, "every 1 <= d <= n divides n!",# and "a divisor of 2 or more never divides two consecutive numbers".## 3. The scan (this file, second half). `scan` walks d = 2, 3, 4, ...# through N carrying the invariant `M.has_divisor(N, d-1) == False{}`# -- which is literally mathlib's own trial division, so when the# scan stops at the first divisor p it hands back exactly the Bool# fact that nothing below p divides N. `least_is_prime` turns that# into `M.has_divisor(p, p-1) == False{}`, i.e. `M.is_prime(p)`, and# `no_largest_prime` puts p above n.## Nothing here is a decision procedure run on a literal: every proof is an# induction over a variable, so the checker never builds a large Nat.# ===========================================================================# ---------------------------------------------------------------------# 1a. mathlib's Bool tests, reflected into lib/nat.bend's propositions# ---------------------------------------------------------------------# nat_eq says True exactly when the two numbers are equal ...def eq_of_nat_eq(a: Nat, b: Nat, e: {M.nat_eq(a, b) == True{} : Bool}) -> {a == b : Nat}: match a b: case 0n 0n: {==} case 0n 1n+q: Empty.absurd({0n == 1n+q : Nat}, N.Bool.false_ne_true(e)) case 1n+p 0n: Empty.absurd({1n+p == 0n : Nat}, N.Bool.false_ne_true(e)) case 1n+p 1n+q: Equal.cong(Nat, Nat, x => 1n+x, p, q, eq_of_nat_eq(p, q, e))# ... and it says True whenever they are.def nat_eq_of_eq(a: Nat, b: Nat, e: {a == b : Nat}) -> {M.nat_eq(a, b) == True{} : Bool}: match a b: case 0n 0n: {==} case 0n 1n+q: Empty.absurd({M.nat_eq(0n, 1n+q) == True{} : Bool}, N.Nat.zero_neq_succ(q, e)) case 1n+p 0n: Empty.absurd({M.nat_eq(1n+p, 0n) == True{} : Bool}, N.Nat.succ_neq_zero(p, e)) case 1n+p 1n+q: nat_eq_of_eq(p, q, N.Nat.succ_inj(p, q, e))# nat_le is Nat.Le, in both directions, and its False answer is a strict >def le_of_nat_le(a: Nat, b: Nat, e: {M.nat_le(a, b) == True{} : Bool}) -> N.Nat.Le(a, b): match a b: case 0n 0n: Unit{} case 0n 1n+q: Unit{} case 1n+p 0n: Empty.absurd(N.Nat.Le(1n+p, 0n), N.Bool.false_ne_true(e)) case 1n+p 1n+q: le_of_nat_le(p, q, e)def nat_le_of_le(a: Nat, b: Nat, h: N.Nat.Le(a, b)) -> {M.nat_le(a, b) == True{} : Bool}: match a b: case 0n 0n: {==} case 0n 1n+q: {==} case 1n+p 0n: match h: case 1n+p 1n+q: nat_le_of_le(p, q, h)def lt_of_nat_le_false(a: Nat, b: Nat, e: {M.nat_le(a, b) == False{} : Bool}) -> N.Nat.Le(1n+b, a): match a b: case 0n 0n: Empty.absurd(N.Nat.Le(1n, 0n), N.Bool.true_ne_false(e)) case 0n 1n+q: Empty.absurd(N.Nat.Le(2n+q, 0n), N.Bool.true_ne_false(e)) case 1n+p 0n: Unit{} case 1n+p 1n+q: lt_of_nat_le_false(p, q, e)# mathlib's truncated subtraction really subtracts, when it candef msub_add(b: Nat, a: Nat, h: N.Nat.Le(b, a)) -> {Nat.add(b, M.msub(a, b)) == a : Nat}: match b a: case 0n 0n: {==} case 0n 1n+p: {==} case 1n+q 0n: match h: case 1n+q 1n+p: Equal.cong(Nat, Nat, x => 1n+x, Nat.add(q, M.msub(p, q)), p, msub_add(q, p, h))# subtracting a positive amount strictly shrinks: this is what makes the# fuel of `mod` run downdef msub_lt(+x: Nat, +dp: Nat, h: N.Nat.Le(1n+dp, x)) -> N.Nat.Le(1n+M.msub(x, 1n+dp), x): %msub_add(1n+dp, x, h) : N.Nat.Le(1n+M.msub(x, 1n+dp), _) N.Nat.le_add_l(dp, M.msub(x, 1n+dp))# ---------------------------------------------------------------------# 1b. mathlib's `mod` really is the remainder.## `M.mod(x, d)` is `M.mod_go(x, x, d)`: subtract d while d <= x, with a# fuel to keep the recursion structural. Two inductions on that fuel say# what the answer means -- it is below d, and it completes a multiple of d# to x. Everything about divisibility below is a corollary of these two.# ---------------------------------------------------------------------def le_zero_le(x: Nat, -dp: Nat, h: N.Nat.Le(x, 0n)) -> N.Nat.Le(x, dp): match x: case 0n: Unit{} case 1n+p: match h:# one step of the remainder loop: the Bool `c` is the comparison, passed in# as a parameter because a match cannot scrutinise a computed valuedef mgo_lt.step(g: Nat, +x: Nat, +dp: Nat, c: Bool, +ec: {M.nat_le(1n+dp, x) == c : Bool}, h: N.Nat.Le(x, 1n+g), rec: @y: Nat -> @hy: N.Nat.Le(y, g) -> N.Nat.Le(M.mod_go(g, y, 1n+dp), dp)) -> N.Nat.Le(M.pick(Nat, c, M.mod_go(g, M.msub(x, 1n+dp), 1n+dp), x), dp): match c: case True{}: rec(M.msub(x, 1n+dp), N.Nat.le_trans(1n+M.msub(x, 1n+dp), x, 1n+g, msub_lt(x, dp, le_of_nat_le(1n+dp, x, ec)), h)) case False{}: lt_of_nat_le_false(1n+dp, x, ec)# the remainder is below the divisordef mgo_lt(f: Nat, +x: Nat, +dp: Nat, h: N.Nat.Le(x, f)) -> N.Nat.Le(M.mod_go(f, x, 1n+dp), dp): match f: case 0n: le_zero_le(x, dp, h) case 1n+g: +g2 = g mgo_lt.step(g2, x, dp, M.nat_le(1n+dp, x), {==}, h, y => hy => mgo_lt(g2, y, dp, hy))# quotient * divisor + remainder = input: the successor stepdef mgo_eq.fin(+x: Nat, +dp: Nat, +s: Nat, +r: Nat, es: {Nat.add(1n+dp, s) == x : Nat}, +q0: Nat, prf: {Nat.add(Nat.mul(q0, 1n+dp), r) == s : Nat}) -> (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), r) == x : Nat}): (1n+q0, %es : {Nat.add(Nat.mul(1n+q0, 1n+dp), r) == _ : Nat} %prf : {Nat.add(Nat.mul(1n+q0, 1n+dp), r) == Nat.add(1n+dp, _) : Nat} Equal.sym(Nat, Nat.add(1n+dp, Nat.add(Nat.mul(q0, 1n+dp), r)), Nat.add(Nat.add(1n+dp, Nat.mul(q0, 1n+dp)), r), N.Nat.add_assoc(1n+dp, Nat.mul(q0, 1n+dp), r)))def mgo_eq.con(+x: Nat, +dp: Nat, +s: Nat, +r: Nat, es: {Nat.add(1n+dp, s) == x : Nat}, w: (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), r) == s : Nat})) -> (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), r) == x : Nat}): (q0, prf) = w mgo_eq.fin(x, dp, s, r, es, q0, prf)def mgo_eq.step(+g: Nat, +x: Nat, +dp: Nat, c: Bool, +ec: {M.nat_le(1n+dp, x) == c : Bool}, h: N.Nat.Le(x, 1n+g), rec: @y: Nat -> @hy: N.Nat.Le(y, g) -> (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), M.mod_go(g, y, 1n+dp)) == y : Nat})) -> (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), M.pick(Nat, c, M.mod_go(g, M.msub(x, 1n+dp), 1n+dp), x)) == x : Nat}): match c: case True{}: mgo_eq.con(x, dp, M.msub(x, 1n+dp), M.mod_go(g, M.msub(x, 1n+dp), 1n+dp), msub_add(1n+dp, x, le_of_nat_le(1n+dp, x, ec)), rec(M.msub(x, 1n+dp), N.Nat.le_trans(1n+M.msub(x, 1n+dp), x, 1n+g, msub_lt(x, dp, le_of_nat_le(1n+dp, x, ec)), h))) case False{}: (0n, {==})def mgo_eq(f: Nat, +x: Nat, +dp: Nat, h: N.Nat.Le(x, f)) -> (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), M.mod_go(f, x, 1n+dp)) == x : Nat}): match f: case 0n: (0n, {==}) case 1n+g: +g2 = g mgo_eq.step(g2, x, dp, M.nat_le(1n+dp, x), {==}, h, y => hy => mgo_eq(g2, y, dp, hy))# the two facts, at the fuel `mod` actually usesdef mod_lt(+x: Nat, +dp: Nat) -> N.Nat.Le(M.mod(x, 1n+dp), dp): mgo_lt(x, x, dp, N.Nat.le_refl(x))def mod_eq(+x: Nat, +dp: Nat) -> (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), M.mod(x, 1n+dp)) == x : Nat}): mgo_eq(x, x, dp, N.Nat.le_refl(x))# ---------------------------------------------------------------------# 1c. `M.divides(d, x) == True{}` and "some q has q*d = x" are the same# thing, for every d >= 1. This is the hinge of the whole file: above it# everything is Bools, below it everything is arithmetic.# ---------------------------------------------------------------------def divides_elim.fin(+dp: Nat, +x: Nat, r: Nat, hr: {r == 0n : Nat}, +q: Nat, prf: {Nat.add(Nat.mul(q, 1n+dp), r) == x : Nat}) -> P.Dvd(1n+dp, x): (q, %N.Nat.add_zero(Nat.mul(q, 1n+dp)) : {_ == x : Nat} %hr : {Nat.add(Nat.mul(q, 1n+dp), _) == x : Nat} prf)def divides_elim.open(+dp: Nat, +x: Nat, r: Nat, hr: {r == 0n : Nat}, w: (&q: Nat -> {Nat.add(Nat.mul(q, 1n+dp), r) == x : Nat})) -> P.Dvd(1n+dp, x): (q, prf) = w divides_elim.fin(dp, x, r, hr, q, prf)# a True divisibility flag yields the quotientdef divides_elim(+dp: Nat, +x: Nat, e: {M.divides(1n+dp, x) == True{} : Bool}) -> P.Dvd(1n+dp, x): divides_elim.open(dp, x, M.mod(x, 1n+dp), eq_of_nat_eq(M.mod(x, 1n+dp), 0n, e), mod_eq(x, dp))def divides_intro.fin(+dp: Nat, +x: Nat, +q: Nat, e: {Nat.mul(q, 1n+dp) == x : Nat}, +r: Nat, hr: N.Nat.Le(r, dp), +q0: Nat, prf: {Nat.add(Nat.mul(q0, 1n+dp), r) == x : Nat}) -> {r == 0n : Nat}: P.Nat.mul_rem_zero(q0, q, dp, r, Equal.trans(Nat, Nat.add(Nat.mul(q0, 1n+dp), r), x, Nat.mul(q, 1n+dp), prf, Equal.sym(Nat, Nat.mul(q, 1n+dp), x, e)), hr)def divides_intro.open(+dp: Nat, +x: Nat, +q: Nat, e: {Nat.mul(q, 1n+dp) == x : Nat}, +r: Nat, hr: N.Nat.Le(r, dp), w: (&q0: Nat -> {Nat.add(Nat.mul(q0, 1n+dp), r) == x : Nat})) -> {r == 0n : Nat}: (q0, prf) = w divides_intro.fin(dp, x, q, e, r, hr, q0, prf)# an exact quotient makes the flag Truedef divides_intro(+dp: Nat, +x: Nat, +q: Nat, e: {Nat.mul(q, 1n+dp) == x : Nat}) -> {M.divides(1n+dp, x) == True{} : Bool}: nat_eq_of_eq(M.mod(x, 1n+dp), 0n, divides_intro.open(dp, x, q, e, M.mod(x, 1n+dp), mod_lt(x, dp), mod_eq(x, dp)))def divides_of_dvd(+dp: Nat, +x: Nat, w: P.Dvd(1n+dp, x)) -> {M.divides(1n+dp, x) == True{} : Bool}: P.Dvd.open(1n+dp, x, w, {M.divides(1n+dp, x) == True{} : Bool}, q => e => divides_intro(dp, x, q, e))# divisibility composes: a divisor of a divisor of x divides xdef divides_chain(+ep: Nat, +pp: Nat, +x: Nat, hep: {M.divides(1n+ep, 1n+pp) == True{} : Bool}, hpx: {M.divides(1n+pp, x) == True{} : Bool}) -> {M.divides(1n+ep, x) == True{} : Bool}: divides_of_dvd(ep, x, P.Dvd.trans(1n+ep, 1n+pp, x, divides_elim(ep, 1n+pp, hep), divides_elim(pp, x, hpx)))# ---------------------------------------------------------------------# 2. mathlib's trial division `has_divisor(x, k)` = "some d with# 2 <= d <= k divides x", in the direction the argument needs.# ---------------------------------------------------------------------# a divisor of x that is at least 2 and at most k makes the scan say Truedef hd_intro(k: Nat, +dp: Nat, +x: Nat, +hd: {M.divides(2n+dp, x) == True{} : Bool}, hle: N.Nat.Le(2n+dp, k)) -> {M.has_divisor(x, k) == True{} : Bool}: match k: case 0n: match hle: case 1n: match hle: case 2n+q: +q2 = q P.Nat.le_split(dp, q2, hle, {M.has_divisor(x, 2n+q2) == True{} : Bool}, eqd => %eqd : {Bool.or(M.divides(2n+_, x), M.has_divisor(x, 1n+_)) == True{} : Bool} %Equal.sym(Bool, M.divides(2n+dp, x), True{}, hd) : {Bool.or(_, M.has_divisor(x, 1n+dp)) == True{} : Bool} {==}, ltd => %Equal.sym(Bool, M.has_divisor(x, 1n+q2), True{}, hd_intro(1n+q2, dp, x, hd, ltd)) : {Bool.or(M.divides(2n+q2, x), _) == True{} : Bool} M.or_true(M.divides(2n+q2, x)))# ---------------------------------------------------------------------# 3. the scan, and why its answer is prime.## `scan` walks d = 2, 3, ... upward through x carrying mathlib's own# "nothing from 2 to d-1 divides x" as a Bool equation, and stops at the# first d that divides x. The invariant is the whole point: what comes out# is not just a divisor but the LEAST one, in exactly the form# `M.is_prime` will need.# ---------------------------------------------------------------------# the package the scan returns: p = 2+pp divides x, and nothing below it doesdef Least(x: Nat, pp: Nat) -> Type: {M.divides(2n+pp, x) == True{} : Bool} & {M.has_divisor(x, 1n+pp) == False{} : Bool}def Found(x: Nat) -> Type: &pp: Nat -> Least(x, pp)# a divisor of the least divisor would be a smaller divisor of x, so there# is none: the Bool test for it is Falsedef not_div_p(+q: Nat, +pp: Nat, +x: Nat, c: Bool, ec: {M.divides(2n+q, 2n+pp) == c : Bool}, hdvp: {M.divides(2n+pp, x) == True{} : Bool}, hnd: {M.has_divisor(x, 1n+pp) == False{} : Bool}, hle: N.Nat.Le(2n+q, 1n+pp)) -> {M.divides(2n+q, 2n+pp) == False{} : Bool}: match c: case True{}: Empty.absurd({M.divides(2n+q, 2n+pp) == False{} : Bool}, N.Bool.true_ne_false( Equal.trans(Bool, True{}, M.has_divisor(x, 1n+pp), False{}, Equal.sym(Bool, M.has_divisor(x, 1n+pp), True{}, hd_intro(1n+pp, q, x, divides_chain(1n+q, 1n+pp, x, ec, hdvp), hle)), hnd))) case False{}: ec# so trial division on the least divisor itself finds nothing, at every k# up to p-1 -- which is `M.is_prime(p)` once k reaches p-1def least_no_divisor(k: Nat, +pp: Nat, +x: Nat, +hdvp: {M.divides(2n+pp, x) == True{} : Bool}, +hnd: {M.has_divisor(x, 1n+pp) == False{} : Bool}, hle: N.Nat.Le(k, 1n+pp)) -> {M.has_divisor(2n+pp, k) == False{} : Bool}: match k: case 0n: {==} case 1n: {==} case 2n+q: +q2 = q P.Nat.le_copy(2n+q2, 1n+pp, hle, {M.has_divisor(2n+pp, 2n+q2) == False{} : Bool}, h1 => h2 => %Equal.sym(Bool, M.has_divisor(2n+pp, 1n+q2), False{}, least_no_divisor(1n+q2, pp, x, hdvp, hnd, N.Nat.lt_le(q2, pp, h1))) : {Bool.or(M.divides(2n+q2, 2n+pp), _) == False{} : Bool} %Equal.sym(Bool, M.divides(2n+q2, 2n+pp), False{}, not_div_p(q2, pp, x, M.divides(2n+q2, 2n+pp), {==}, hdvp, hnd, h2)) : {Bool.or(_, False{}) == False{} : Bool} {==})# one step of the scan: the divisibility flag arrives as a parameter,# because a match cannot scrutinise a computed valuedef scan.step(+g: Nat, +x: Nat, +dp: Nat, c: Bool, ec: {M.divides(2n+dp, x) == c : Bool}, hnd: {M.has_divisor(x, 1n+dp) == False{} : Bool}, hb: {Nat.add(2n+dp, 1n+g) == x : Nat}, rec: @dq: Nat -> @h1: {M.has_divisor(x, 1n+dq) == False{} : Bool} -> @h2: {Nat.add(2n+dq, g) == x : Nat} -> Found(x)) -> Found(x): match c: case True{}: (dp, (ec, hnd)) case False{}: rec(1n+dp, %Equal.sym(Bool, M.has_divisor(x, 1n+dp), False{}, hnd) : {Bool.or(M.divides(2n+dp, x), _) == False{} : Bool} %Equal.sym(Bool, M.divides(2n+dp, x), False{}, ec) : {Bool.or(_, False{}) == False{} : Bool} {==}, Equal.trans(Nat, 3n+Nat.add(dp, g), Nat.add(2n+dp, 1n+g), x, Equal.cong(Nat, Nat, z => 2n+z, 1n+Nat.add(dp, g), Nat.add(dp, 1n+g), Equal.sym(Nat, Nat.add(dp, 1n+g), 1n+Nat.add(dp, g), N.Nat.add_succ(dp, g))), hb))# the fuel runs out exactly at d = x, and x always divides itselfdef scan.done(+x: Nat, +dp: Nat, hnd: {M.has_divisor(x, 1n+dp) == False{} : Bool}, hb: {Nat.add(2n+dp, 0n) == x : Nat}) -> Found(x): (dp, (divides_intro(1n+dp, x, 1n, Equal.trans(Nat, Nat.mul(1n, 2n+dp), 2n+dp, x, N.Nat.one_mul(2n+dp), Equal.trans(Nat, 2n+dp, Nat.add(2n+dp, 0n), x, Equal.sym(Nat, Nat.add(2n+dp, 0n), 2n+dp, N.Nat.add_zero(2n+dp)), hb))), hnd))# the least divisor above 1 of x, found by walking up from 2. The fuel is# tied to the value by `2 + dp + f = x`, so it cannot run out early.def scan(f: Nat, +x: Nat, +dp: Nat, hnd: {M.has_divisor(x, 1n+dp) == False{} : Bool}, hb: {Nat.add(2n+dp, f) == x : Nat}) -> Found(x): match f: case 0n: scan.done(x, dp, hnd, hb) case 1n+g: +g2 = g scan.step(g2, x, dp, M.divides(2n+dp, x), {==}, hnd, hb, dq => h1 => h2 => scan(g2, x, dq, h1, h2))# ---------------------------------------------------------------------# 4. Euclid's theorem# ---------------------------------------------------------------------def Euclid(n: Nat) -> Type: &p: Nat -> {Bool.and(M.nat_le(n, p), M.is_prime(p)) == True{} : Bool}# `M.is_prime(2+pp)` unfolds to "2 <= 2+pp" (immediate) and "trial# division up to (2+pp)-1 = 1+pp finds nothing", which is# `least_no_divisor` at k = 1+pp.def least_is_prime(+pp: Nat, +x: Nat, hdv: {M.divides(2n+pp, x) == True{} : Bool}, hn: {M.has_divisor(x, 1n+pp) == False{} : Bool}) -> {M.is_prime(2n+pp) == True{} : Bool}: %Equal.sym(Bool, M.has_divisor(2n+pp, 1n+pp), False{}, least_no_divisor(1n+pp, pp, x, hdv, hn, N.Nat.le_refl(1n+pp))) : {Bool.not(_) == True{} : Bool} {==}# with p = 2+pp the least divisor of n!+1 in hand: either n <= p, and we# are done, or p < n -- and then p divides n! as well as n!+1, which no# number above 1 can do.def euclid.fin(+n: Nat, +m: Nat, +hf: {P.fact(n) == 1n+m : Nat}, +pp: Nat, +hdv: {M.divides(2n+pp, 2n+m) == True{} : Bool}, hn: {M.has_divisor(2n+m, 1n+pp) == False{} : Bool}) -> Euclid(n): P.Nat.le_total(n, 2n+pp, Euclid(n), hle => (2n+pp, %Equal.sym(Bool, M.nat_le(n, 2n+pp), True{}, nat_le_of_le(n, 2n+pp, hle)) : {Bool.and(_, M.is_prime(2n+pp)) == True{} : Bool} %Equal.sym(Bool, M.is_prime(2n+pp), True{}, least_is_prime(pp, 2n+m, hdv, hn)) : {Bool.and(True{}, _) == True{} : Bool} {==}), hgt => Empty.absurd(Euclid(n), P.Dvd.consecutive(pp, P.fact(n), P.fact_div(n, 1n+pp, N.Nat.lt_le(2n+pp, n, hgt)), %Equal.sym(Nat, P.fact(n), 1n+m, hf) : P.Dvd(2n+pp, 1n+_) divides_elim(1n+pp, 2n+m, hdv))))def euclid.found(+n: Nat, +m: Nat, +hf: {P.fact(n) == 1n+m : Nat}, +pp: Nat, w: Least(2n+m, pp)) -> Euclid(n): (hdv, hn) = w euclid.fin(n, m, hf, pp, hdv, hn)def euclid.open2(+n: Nat, +m: Nat, +hf: {P.fact(n) == 1n+m : Nat}, w: Found(2n+m)) -> Euclid(n): (pp, w2) = w euclid.found(n, m, hf, pp, w2)# n! + 1 is 2 + m, so the scan starts at d = 2 with fuel m and the# invariant "nothing up to 1 divides it", which is True by definition.def euclid.start(+n: Nat, +m: Nat, +hf: {P.fact(n) == 1n+m : Nat}) -> Euclid(n): euclid.open2(n, m, hf, scan(m, 2n+m, 0n, {==}, {==}))def euclid.open1(+n: Nat, w: (&m: Nat -> {P.fact(n) == 1n+m : Nat})) -> Euclid(n): (m, hf) = w euclid.start(n, m, hf)# THE THEOREM: for every n there is a p with n <= p and p prime.def no_largest_prime(n: Nat) -> (&p: Nat -> {Bool.and(M.nat_le(n, p), M.is_prime(p)) == True{} : Bool}): +n2 = n euclid.open1(n2, P.fact_pos(n2))