norm_num extensions on natural numbers

This file provides a norm_num extension to prove that natural numbers are prime and compute its minimal factor. Todo: compute the list of all factors.

Implementation Notes

For numbers larger than 25 bits, the primality proof produced by norm_num is an expression that is thousands of levels deep, and the Lean kernel seems to raise a stack overflow when type-checking that proof. If we want an implementation that works for larger primes, we should generate a proof that has a smaller depth.

Note: evalMinFac.aux does not raise a stack overflow, which can be checked by replacing the prf' in the recursive call by something like (.sort .zero)

theorem Mathlib.Meta.NormNum.not_prime_mul_of_ble (a b n : ℕ) (h : a * b = n) (h₁ : a.ble 1 = false) (h₂ : b.ble 1 = false) : ¬Nat.Prime n

def Mathlib.Meta.NormNum.deriveNotPrime (n d : ℕ) (en : Q(ℕ)) : Q(¬Nat.Prime «$en»)

Produce a proof that n is not prime from a factor 1 < d < n. en should be the expression that is the natural number literal n.

def Mathlib.Meta.NormNum.MinFacHelper (n k : ℕ) : Prop

A predicate representing partial progress in a proof of minFac.

theorem Mathlib.Meta.NormNum.MinFacHelper.one_lt {n k : ℕ} (h : MinFacHelper n k) : 1 < n

theorem Mathlib.Meta.NormNum.minFacHelper_0 (n : ℕ) (h1 : Nat.ble 2 n = true) (h2 : 1 = n % 2) : MinFacHelper n 3

theorem Mathlib.Meta.NormNum.minFacHelper_1 {n k k' : ℕ} (e : k + 2 = k') (h : MinFacHelper n k) (np : n.minFac ≠ k) : MinFacHelper n k'

theorem Mathlib.Meta.NormNum.minFacHelper_2 {n k k' : ℕ} (e : k + 2 = k') (nk : ¬Nat.Prime k) (h : MinFacHelper n k) : MinFacHelper n k'

theorem Mathlib.Meta.NormNum.minFacHelper_3 {n k k' : ℕ} (e : k + 2 = k') (nk : (n % k).beq 0 = false) (h : MinFacHelper n k) : MinFacHelper n k'

theorem Mathlib.Meta.NormNum.isNat_minFac_1 {a : ℕ} : IsNat a 1 → IsNat a.minFac 1

theorem Mathlib.Meta.NormNum.isNat_minFac_2 {a a' : ℕ} : IsNat a a' → a' % 2 = 0 → IsNat a.minFac 2

theorem Mathlib.Meta.NormNum.isNat_minFac_3 {n n' : ℕ} (k : ℕ) : IsNat n n' → MinFacHelper n' k → 0 = n' % k → IsNat n.minFac k

theorem Mathlib.Meta.NormNum.isNat_minFac_4 {n n' k : ℕ} : IsNat n n' → MinFacHelper n' k → (k * k).ble n' = false → IsNat n.minFac n'

def Mathlib.Meta.NormNum.evalMinFac : NormNumExt

The norm_num extension which identifies expressions of the form minFac n.

partial def Mathlib.Meta.NormNum.evalMinFac.aux (n : Q(ℕ)) (sℕ : Q(AddMonoidWithOne ℕ)) (nn : Q(ℕ)) (pn : Q(IsNat «$n» «$nn»)) (n' : ℕ) (ek : Q(ℕ)) (prf : Q(MinFacHelper «$nn» «$ek»)) : (c : Q(ℕ)) × Q(IsNat «$n».minFac «$c»)

def Mathlib.Meta.NormNum.evalMinFac.core (n : Q(ℕ)) (sℕ : Q(AddMonoidWithOne ℕ)) (nn : Q(ℕ)) (pn : Q(IsNat «$n» «$nn»)) (n' : ℕ) : Lean.MetaM (Result q(«$n».minFac))

theorem Mathlib.Meta.NormNum.isNat_prime_0 {n : ℕ} : IsNat n 0 → ¬Nat.Prime n

theorem Mathlib.Meta.NormNum.isNat_prime_1 {n : ℕ} : IsNat n 1 → ¬Nat.Prime n

theorem Mathlib.Meta.NormNum.isNat_prime_2 {n n' : ℕ} : IsNat n n' → Nat.ble 2 n' = true → IsNat n'.minFac n' → Nat.Prime n

theorem Mathlib.Meta.NormNum.isNat_not_prime {n n' : ℕ} (h : IsNat n n') : ¬Nat.Prime n' → ¬Nat.Prime n

def Mathlib.Meta.NormNum.evalNatPrime : NormNumExt

The norm_num extension which identifies expressions of the form Nat.Prime n.

def Mathlib.Meta.NormNum.evalNatPrime.core (n nn : Q(ℕ)) (pn : Q(IsNat «$n» «$nn»)) (n' : ℕ) : Lean.MetaM (Result q(Nat.Prime «$n»))