# 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) :
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 • = (let d' := n / d; let prf := q(); let r := q(); let r' := q(); pure q()).run Instances For A predicate representing partial progress in a proof of minFac. Equations Instances For theorem Mathlib.Meta.NormNum.minFacHelper_0 (n : ) (h1 : Nat.ble 2 n = true) (h2 : 1 = n % 2) : theorem Mathlib.Meta.NormNum.minFacHelper_1 {n : } {k : } {k' : } (e : k + 2 = k') (h : ) (np : n.minFac k) : theorem Mathlib.Meta.NormNum.minFacHelper_2 {n : } {k : } {k' : } (e : k + 2 = k') (nk : ) (h : ) : theorem Mathlib.Meta.NormNum.minFacHelper_3 {n : } {k : } {k' : } (e : k + 2 = k') (nk : (n % k).beq 0 = false) (h : ) : theorem Mathlib.Meta.NormNum.isNat_minFac_2 {a : } {a' : } : a' % 2 = 0Mathlib.Meta.NormNum.IsNat a.minFac 2 theorem Mathlib.Meta.NormNum.isNat_minFac_3 {n : } {n' : } (k : ) : 0 = n' % kMathlib.Meta.NormNum.IsNat n.minFac k theorem Mathlib.Meta.NormNum.isNat_minFac_4 {n : } {n' : } {k : } : (k * k).ble n' = falseMathlib.Meta.NormNum.IsNat n.minFac n' 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. Instances For partial def Mathlib.Meta.NormNum.evalMinFac.aux (n : Q()) (sℕ : ) (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ℕ : ) (nn : Q()) (pn : Q(Mathlib.Meta.NormNum.IsNat «$n» «$nn»)) (n' : ) : Equations • One or more equations did not get rendered due to their size. Instances For theorem Mathlib.Meta.NormNum.isNat_prime_2 {n : } {n' : } : Nat.ble 2 n' = trueMathlib.Meta.NormNum.IsNat n'.minFac n' theorem Mathlib.Meta.NormNum.isNat_not_prime {n : } {n' : } (h : ) : ¬ 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. Instances For def Mathlib.Meta.NormNum.evalNatPrime.core (n : Q()) (nn : Q()) (pn : Q(Mathlib.Meta.NormNum.IsNat «$n» «\$nn»)) (n' : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For