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.

Equations

• Mathlib.Meta.NormNum.deriveNotPrime n d en = (let d' := n / d; let prf := q(⋯); let r := q(⋯); let r' := q(⋯); pure q(⋯)).run

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

A predicate representing partial progress in a proof of minFac.

Equations

• Mathlib.Meta.NormNum.MinFacHelper n k = (2 < k ∧ k % 2 = 1 ∧ k ≤ n.minFac)

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

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

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

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

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

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

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

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

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

def Mathlib.Meta.NormNum.evalMinFac : Mathlib.Meta.NormNum.NormNumExt

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

def Mathlib.Meta.NormNum.evalNatPrime : Mathlib.Meta.NormNum.NormNumExt

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.NormNum.evalNatPrime.core n nn pn 0 = pure (Mathlib.Meta.NormNum.Result.isFalse q(⋯))
• Mathlib.Meta.NormNum.evalNatPrime.core n nn pn 1 = pure (Mathlib.Meta.NormNum.Result.isFalse q(⋯))