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₁ : Nat.ble a 1 = false) (h₂ : Nat.ble b 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
  • One or more equations did not get rendered due to their size.
Instances For

    A predicate representing partial progress in a proof of minFac.

    Equations
    Instances For

      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 (Nat.minFac «$n») «$c»)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          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
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For