~/bend-docscommunity

euclid.bend checks

raw source on the hub · import 0xd5e9362591c1667c9894b781190e1ac9/euclid.bend as Euclid

4 imports
import Base
import ./mathlib.bend as M
import ./nat.bend as N
import ./primes.bend as P

Definitions

def eq_of_nat_eq source · line 65 · raw

@a:Nat -> @b:Nat -> @e:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.nat_eq(a, b) == True{} : Bool} -> {a == b : Nat}

nat_eq says True exactly when the two numbers are equal ...

def nat_eq_of_eq source · line 77 · raw

@a:Nat -> @b:Nat -> @e:{a == b : Nat} -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.nat_eq(a, b) == True{} : Bool}

... and it says True whenever they are.

def le_of_nat_le source · line 89 · raw

@a:Nat -> @b:Nat -> @e:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.nat_le(a, b) == True{} : Bool} -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(a, b)

nat_le is Nat.Le, in both directions, and its False answer is a strict >

def nat_le_of_le source · line 100 · raw

@a:Nat -> @b:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(a, b) -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.nat_le(a, b) == True{} : Bool}

def lt_of_nat_le_false source · line 111 · raw

@a:Nat -> @b:Nat -> @e:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.nat_le(a, b) == False{} : Bool} -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(1n+b, a)

def msub_add source · line 123 · raw

@b:Nat -> @a:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(b, a) -> {Nat.add(b, 0xd5e9362591c1667c9894b781190e1ac9/mathlib.msub(a, b)) == a : Nat}

mathlib's truncated subtraction really subtracts, when it can

def msub_lt source · line 136 · raw

@+x:Nat -> @+dp:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(1n+dp, x) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(1n+0xd5e9362591c1667c9894b781190e1ac9/mathlib.msub(x, 1n+dp), x)

subtracting a positive amount strictly shrinks: this is what makes the fuel of mod run down

def le_zero_le source · line 149 · raw

@x:Nat -> @-dp:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(x, 0n) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(x, dp)

def mgo_lt.step source · line 158 · raw

@g:Nat -> @+x:Nat -> @+dp:Nat -> @c:Bool -> @+ec:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.nat_le(1n+dp, x) == c : Bool} -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(x, 1n+g) -> @rec:(@y:Nat -> @hy:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(y, g) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(0xd5e9362591c1667c9894b781190e1ac9/mathlib.mod_go(g, y, 1n+dp), dp)) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(0xd5e9362591c1667c9894b781190e1ac9/mathlib.pick(Nat, c, 0xd5e9362591c1667c9894b781190e1ac9/mathlib.mod_go(g, 0xd5e9362591c1667c9894b781190e1ac9/mathlib.msub(x, 1n+dp), 1n+dp), x), dp)

one step of the remainder loop: the Bool c is the comparison, passed in as a parameter because a match cannot scrutinise a computed value

def mgo_lt source · line 172 · raw

@f:Nat -> @+x:Nat -> @+dp:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(x, f) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(0xd5e9362591c1667c9894b781190e1ac9/mathlib.mod_go(f, x, 1n+dp), dp)

the remainder is below the divisor

def mgo_eq.fin source · line 181 · raw

@+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}

quotient * divisor + remainder = input: the successor step

def mgo_eq.con source · line 190 · raw

@+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}

def mgo_eq.step source · line 196 · raw

@+g:Nat -> @+x:Nat -> @+dp:Nat -> @c:Bool -> @+ec:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.nat_le(1n+dp, x) == c : Bool} -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(x, 1n+g) -> @rec:(@y:Nat -> @hy:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(y, g) -> &q:Nat -> {Nat.add(Nat.mul(q, 1n+dp), 0xd5e9362591c1667c9894b781190e1ac9/mathlib.mod_go(g, y, 1n+dp)) == y : Nat}) -> &q:Nat -> {Nat.add(Nat.mul(q, 1n+dp), 0xd5e9362591c1667c9894b781190e1ac9/mathlib.pick(Nat, c, 0xd5e9362591c1667c9894b781190e1ac9/mathlib.mod_go(g, 0xd5e9362591c1667c9894b781190e1ac9/mathlib.msub(x, 1n+dp), 1n+dp), x)) == x : Nat}

def mgo_eq source · line 211 · raw

@f:Nat -> @+x:Nat -> @+dp:Nat -> @h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(x, f) -> &q:Nat -> {Nat.add(Nat.mul(q, 1n+dp), 0xd5e9362591c1667c9894b781190e1ac9/mathlib.mod_go(f, x, 1n+dp)) == x : Nat}

def mod_lt source · line 221 · raw

@+x:Nat -> @+dp:Nat -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(0xd5e9362591c1667c9894b781190e1ac9/mathlib.mod(x, 1n+dp), dp)

the two facts, at the fuel mod actually uses

def mod_eq source · line 224 · raw

@+x:Nat -> @+dp:Nat -> &q:Nat -> {Nat.add(Nat.mul(q, 1n+dp), 0xd5e9362591c1667c9894b781190e1ac9/mathlib.mod(x, 1n+dp)) == x : Nat}

def divides_elim.fin source · line 233 · raw

@+dp:Nat -> @+x:Nat -> @r:Nat -> @hr:{r == 0n : Nat} -> @+q:Nat -> @prf:{Nat.add(Nat.mul(q, 1n+dp), r) == x : Nat} -> 0xd5e9362591c1667c9894b781190e1ac9/primes.Dvd(1n+dp, x)

def divides_elim.open source · line 240 · raw

@+dp:Nat -> @+x:Nat -> @r:Nat -> @hr:{r == 0n : Nat} -> @w:(&q:Nat -> {Nat.add(Nat.mul(q, 1n+dp), r) == x : Nat}) -> 0xd5e9362591c1667c9894b781190e1ac9/primes.Dvd(1n+dp, x)

def divides_elim source · line 246 · raw

@+dp:Nat -> @+x:Nat -> @e:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(1n+dp, x) == True{} : Bool} -> 0xd5e9362591c1667c9894b781190e1ac9/primes.Dvd(1n+dp, x)

a True divisibility flag yields the quotient

def divides_intro.fin source · line 249 · raw

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

def divides_intro.open source · line 256 · raw

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

def divides_intro source · line 263 · raw

@+dp:Nat -> @+x:Nat -> @+q:Nat -> @e:{Nat.mul(q, 1n+dp) == x : Nat} -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(1n+dp, x) == True{} : Bool}

an exact quotient makes the flag True

def divides_of_dvd source · line 267 · raw

@+dp:Nat -> @+x:Nat -> @w:0xd5e9362591c1667c9894b781190e1ac9/primes.Dvd(1n+dp, x) -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(1n+dp, x) == True{} : Bool}

def divides_chain source · line 271 · raw

@+ep:Nat -> @+pp:Nat -> @+x:Nat -> @hep:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(1n+ep, 1n+pp) == True{} : Bool} -> @hpx:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(1n+pp, x) == True{} : Bool} -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(1n+ep, x) == True{} : Bool}

divisibility composes: a divisor of a divisor of x divides x

def hd_intro source · line 283 · raw

@k:Nat -> @+dp:Nat -> @+x:Nat -> @+hd:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(2n+dp, x) == True{} : Bool} -> @hle:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(2n+dp, k) -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.has_divisor(x, k) == True{} : Bool}

a divisor of x that is at least 2 and at most k makes the scan say True

def Least source · line 312 · raw

@x:Nat -> @pp:Nat -> Type

the package the scan returns: p = 2+pp divides x, and nothing below it does

def Found source · line 315 · raw

@x:Nat -> Type

def not_div_p source · line 320 · raw

@+q:Nat -> @+pp:Nat -> @+x:Nat -> @c:Bool -> @ec:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(2n+q, 2n+pp) == c : Bool} -> @hdvp:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(2n+pp, x) == True{} : Bool} -> @hnd:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.has_divisor(x, 1n+pp) == False{} : Bool} -> @hle:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(2n+q, 1n+pp) -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(2n+q, 2n+pp) == False{} : Bool}

a divisor of the least divisor would be a smaller divisor of x, so there is none: the Bool test for it is False

def least_no_divisor source · line 338 · raw

@k:Nat -> @+pp:Nat -> @+x:Nat -> @+hdvp:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(2n+pp, x) == True{} : Bool} -> @+hnd:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.has_divisor(x, 1n+pp) == False{} : Bool} -> @hle:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(k, 1n+pp) -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.has_divisor(2n+pp, k) == False{} : Bool}

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-1

def scan.step source · line 358 · raw

@+g:Nat -> @+x:Nat -> @+dp:Nat -> @c:Bool -> @ec:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(2n+dp, x) == c : Bool} -> @hnd:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.has_divisor(x, 1n+dp) == False{} : Bool} -> @hb:{Nat.add(2n+dp, 1n+g) == x : Nat} -> @rec:(@dq:Nat -> @h1:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.has_divisor(x, 1n+dq) == False{} : Bool} -> @h2:{Nat.add(2n+dq, g) == x : Nat} -> Found(x)) -> Found(x)

one step of the scan: the divisibility flag arrives as a parameter, because a match cannot scrutinise a computed value

def scan.done source · line 377 · raw

@+x:Nat -> @+dp:Nat -> @hnd:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.has_divisor(x, 1n+dp) == False{} : Bool} -> @hb:{Nat.add(2n+dp, 0n) == x : Nat} -> Found(x)

the fuel runs out exactly at d = x, and x always divides itself

def scan source · line 391 · raw

@f:Nat -> @+x:Nat -> @+dp:Nat -> @hnd:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.has_divisor(x, 1n+dp) == False{} : Bool} -> @hb:{Nat.add(2n+dp, f) == x : Nat} -> Found(x)

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 Euclid source · line 406 · raw

@n:Nat -> Type

def least_is_prime source · line 412 · raw

@+pp:Nat -> @+x:Nat -> @hdv:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(2n+pp, x) == True{} : Bool} -> @hn:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.has_divisor(x, 1n+pp) == False{} : Bool} -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.is_prime(2n+pp) == 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 euclid.fin source · line 422 · raw

@+n:Nat -> @+m:Nat -> @+hf:{0xd5e9362591c1667c9894b781190e1ac9/primes.fact(n) == 1n+m : Nat} -> @+pp:Nat -> @+hdv:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.divides(2n+pp, 2n+m) == True{} : Bool} -> @hn:{0xd5e9362591c1667c9894b781190e1ac9/mathlib.has_divisor(2n+m, 1n+pp) == False{} : Bool} -> Euclid(n)

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.found source · line 438 · raw

@+n:Nat -> @+m:Nat -> @+hf:{0xd5e9362591c1667c9894b781190e1ac9/primes.fact(n) == 1n+m : Nat} -> @+pp:Nat -> @w:Least(2n+m, pp) -> Euclid(n)

def euclid.open2 source · line 442 · raw

@+n:Nat -> @+m:Nat -> @+hf:{0xd5e9362591c1667c9894b781190e1ac9/primes.fact(n) == 1n+m : Nat} -> @w:Found(2n+m) -> Euclid(n)

def euclid.start source · line 448 · raw

@+n:Nat -> @+m:Nat -> @+hf:{0xd5e9362591c1667c9894b781190e1ac9/primes.fact(n) == 1n+m : Nat} -> Euclid(n)

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.open1 source · line 451 · raw

@+n:Nat -> @w:(&m:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/primes.fact(n) == 1n+m : Nat}) -> Euclid(n)

def no_largest_prime source · line 456 · raw

@n:Nat -> &p:Nat -> {Bool.and(0xd5e9362591c1667c9894b781190e1ac9/mathlib.nat_le(n, p), 0xd5e9362591c1667c9894b781190e1ac9/mathlib.is_prime(p)) == True{} : Bool}

THE THEOREM: for every n there is a p with n <= p and p prime.