Documentation

Mathlib.Tactic.NormNum.Prime

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) :
¬n.Prime
def Mathlib.Meta.NormNum.deriveNotPrime (n : ) (d : ) (en : Q()) :
Q(¬«$en».Prime)

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
Instances For

    A predicate representing partial progress in a proof of minFac.

    Equations
    Instances For
      theorem Mathlib.Meta.NormNum.minFacHelper_1 {n : } {k : } {k' : } (e : k + 2 = k') (h : Mathlib.Meta.NormNum.MinFacHelper n k) (np : n.minFac 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) :

      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ℕ : 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' : ) :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem Mathlib.Meta.NormNum.isNat_not_prime {n : } {n' : } (h : Mathlib.Meta.NormNum.IsNat n n') :
          ¬n'.Prime¬n.Prime

          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