proofs/math/number/prime.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/number/prime.bend as Prime

9 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/arith.bend as AR
import ../../lib/lemmas/proofs/nat_algebra.bend as A
import ../../../src/math/number.bend as NB
import ../../../spec/math/number.bend as SN
import ../natural/arith.bend as R
import ../typed/natfuel.bend as NF

Definitions

def sub_big source · line 20 · raw

@+n:Nat -> @+d:Nat -> @+h:{Nat.is_le(n, d) == True{} : Bool} -> {Nat.sub(n, d) == 0n : Nat}

def sub_split source · line 30 · raw

@+n:Nat -> @+d:Nat -> @+h:{Nat.is_lt(d, n) == True{} : Bool} -> {Nat.sub(n, d) == 1n+Nat.sub(n, 1n+d) : Nat}

d < n: n - d == 1 + (n - (d + 1))

def lt_sq source · line 41 · raw

@+dq:Nat -> {Nat.is_lt(2n+dq, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool}

2 <= d: d < d * d

def le_step source · line 46 · raw

@+d:Nat -> @+e:Nat -> @+h:{Nat.is_le(d, e) == True{} : Bool} -> {Nat.is_le(d, 1n+e) == True{} : Bool}

def at_c source · line 52 · raw

@p:Nat -> @+n:Nat -> @+d:Nat -> @+e:Nat -> @+h1:{Bool.not(Nat.is_eq(Nat.mod(n, d), 0n)) == True{} : Bool} -> @+h2:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(p, n, 1n+d) == True{} : Bool} -> @+hlo:{Nat.is_le(d, e) == True{} : Bool} -> @+hhi:{Nat.is_lt(e, Nat.add(d, 1n+p)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(d, e) == c : Bool} -> @ih:(@+e2:Nat -> @+hl:{Nat.is_le(1n+d, e2) == True{} : Bool} -> @+hh:{Nat.is_lt(e2, Nat.add(1n+d, p)) == True{} : Bool} -> {Nat.is_eq(Nat.mod(n, e2), 0n) == False{} : Bool}) -> {Nat.is_eq(Nat.mod(n, e), 0n) == False{} : Bool}

a d with lo <= e < lo + k, where nodiv(k, n, lo) holds, does not divide n

def nodiv_at source · line 62 · raw

@k:Nat -> @+n:Nat -> @+d:Nat -> @+e:Nat -> @+h:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(k, n, d) == True{} : Bool} -> @+hlo:{Nat.is_le(d, e) == True{} : Bool} -> @+hhi:{Nat.is_lt(e, Nat.add(d, k)) == True{} : Bool} -> {Nat.is_eq(Nat.mod(n, e), 0n) == False{} : Bool}

def and_true source · line 72 · raw

@+b:Bool -> {Bool.and(b, True{}) == b : Bool}

def and_assoc source · line 80 · raw

@+x:Bool -> @+y:Bool -> @+z:Bool -> {Bool.and(x, Bool.and(y, z)) == Bool.and(Bool.and(x, y), z) : Bool}

nodiv(1 + k, n, d) adds the test of d + k

def snoc source · line 87 · raw

@k:Nat -> @+n:Nat -> @+d:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(1n+k, n, d) == Bool.and(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(k, n, d), Bool.not(Nat.is_eq(Nat.mod(n, Nat.add(d, k)), 0n))) : Bool}

def mul0 source · line 99 · raw

@+x:Nat -> {Nat.mul(0n, x) == 0n : Nat}

def mul1 source · line 102 · raw

@+x:Nat -> {Nat.mul(1n, x) == x : Nat}

def c_small source · line 106 · raw

@+n:Nat -> @+dq:Nat -> @+eq:Nat -> @+qq:Nat -> @+hn:{n == Nat.mul(2n+qq, 2n+eq) : Nat} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(dq, n, 2n) == True{} : Bool} -> @+hq:{Nat.is_lt(2n+qq, 2n+dq) == True{} : Bool} -> Empty

n == q e with q >= 2 and q < d would divide n, which nodiv(dq, n, 2) rules out

def c_big source · line 113 · raw

@+n:Nat -> @+dq:Nat -> @+eq:Nat -> @+q:Nat -> @+hn:{n == Nat.mul(q, 2n+eq) : Nat} -> @+hdd:{Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool} -> @+hde:{Nat.is_le(2n+dq, 2n+eq) == True{} : Bool} -> @+hq:{Nat.is_le(2n+dq, q) == True{} : Bool} -> Empty

... and q >= d gives d * d <= q * d <= q * e == n, against n < d * d

def c_two source · line 120 · raw

@+n:Nat -> @+dq:Nat -> @+eq:Nat -> @+qq:Nat -> @+hn:{n == Nat.mul(2n+qq, 2n+eq) : Nat} -> @+hdd:{Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(dq, n, 2n) == True{} : Bool} -> @+hde:{Nat.is_le(2n+dq, 2n+eq) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(2n+qq, 2n+dq) == c : Bool} -> Empty

def contra source · line 128 · raw

@+n:Nat -> @+dq:Nat -> @+eq:Nat -> @+q:Nat -> @+hn:{n == Nat.mul(q, 2n+eq) : Nat} -> @+hen:{Nat.is_lt(2n+eq, n) == True{} : Bool} -> @+hdd:{Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(dq, n, 2n) == True{} : Bool} -> @+hde:{Nat.is_le(2n+dq, 2n+eq) == True{} : Bool} -> Empty

e divides n with d <= e < n, d * d > n and no divisor in [2, d): impossible

def lt_add1 source · line 140 · raw

@+e:Nat -> @+p:Nat -> {Nat.is_lt(e, Nat.add(e, 1n+p)) == True{} : Bool}

e < e + (1 + p)

def head_c source · line 144 · raw

@+n:Nat -> @+dq:Nat -> @+eq:Nat -> @+p:Nat -> @+hdd:{Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(dq, n, 2n) == True{} : Bool} -> @+hde:{Nat.is_le(2n+dq, 2n+eq) == True{} : Bool} -> @+hek:{Nat.is_le(Nat.add(2n+eq, 1n+p), n) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(Nat.mod(n, 2n+eq), 0n) == c : Bool} -> {Bool.not(Nat.is_eq(Nat.mod(n, 2n+eq), 0n)) == True{} : Bool}

def big source · line 157 · raw

@k:Nat -> @+n:Nat -> @+dq:Nat -> @+eq:Nat -> @+hdd:{Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(dq, n, 2n) == True{} : Bool} -> @+hde:{Nat.is_le(2n+dq, 2n+eq) == True{} : Bool} -> @+hek:{Nat.is_le(Nat.add(2n+eq, k), n) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(k, n, 2n+eq) == True{} : Bool}

every e in [2 + eq, 2 + eq + k) with d <= e, e + k <= n: none divides n

def stop source · line 168 · raw

@+n:Nat -> @+dq:Nat -> @+hdd:{Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == True{} : Bool} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(dq, n, 2n) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(2n+dq, n) == c : Bool} -> {True{} == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(Nat.sub(n, 2n+dq), n, 2n+dq) : Bool}

the stop at d * d > n: nothing in [d, n) divides n

def below source · line 178 · raw

@+n:Nat -> @+dq:Nat -> @+hdd:{Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == False{} : Bool} -> {Nat.is_lt(2n+dq, n) == True{} : Bool}

d * d <= n: d < n

def loop source · line 181 · raw

@+f:Nat -> @+n:Nat -> @+dq:Nat -> @+done:Bool -> @+hdone:{Nat.is_lt(n, Nat.mul(2n+dq, 2n+dq)) == done : Bool} -> @+dv:Bool -> @+hdv:{Nat.is_eq(Nat.mod(n, 2n+dq), 0n) == dv : Bool} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(dq, n, 2n) == True{} : Bool} -> @+hf:{Nat.add(f, 2n+dq) == Nat.add(n, 2n) : Nat} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/number.prime_go(f, n, 2n+dq, done, dv) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.nodiv(Nat.sub(n, 2n+dq), n, 2n+dq) : Bool}

def is_prime_value source · line 200 · raw

@+n:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/number.IsPrime.value(n)