primality

Defines the frontend of the primality tactic, which closes goals Nat.Prime n using a certificate constructed from witnesses it takes from the user.

structure Mathlib.Tactic.Primality.Config : Type

Configuration for primality.

• cert : CertMode

  The certificate configuration to use.

def Mathlib.Tactic.Primality.elabPrimalityConfig (cfg : Lean.Syntax) (init : Config := { }) (logExceptions : Bool := true) : Lean.Elab.Tactic.TacticM Config

Function elaborating Config.

Equations

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

def Mathlib.Tactic.Primality.evalNumeral? (e : Q(ℕ)) : Lean.MetaM (Option (ℕ × (nQ : Q(ℕ)) × Q(Meta.NormNum.IsNat «$e» «$nQ»)))

Evaluates e to a numeral with norm_num, if it can.

Equations

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

def Mathlib.Tactic.Primality.elabKnownPrimes (hs : Array Lean.Term) : Lean.Elab.Tactic.TacticM (Std.HashMap ℕ Lean.Expr)

Store the proofs hs of Nat.Prime n in a hashmap.

Equations

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

def Mathlib.Tactic.Primality.primality : Lean.ParserDescr

primality proves a goal Nat.Prime n, where norm_num evaluates n to a numeral, from a Lucas certificate given as a list of witnesses.

A Lucas certificate proves p prime by a primitive root a of p, a number with a ^ (p - 1) % p = 1 and a ^ ((p - 1) / q) % p ≠ 1 for each prime factor q of p - 1. Each such q needs a certificate too, except for primes below 2 ^ 10 which are left to norm_num.

example : Nat.Prime 1000003 := by
  primality (cert := .witnesses [
    -- Proves `1000003` prime, since `1000003 - 1 = 2 * 3 * 166667` and `2` is a primitive root.
    .lucas { root := 2, primeFactors := [2, 3, 166667] },
    -- Proves `166667` prime, since `166667 - 1 = 2 * 167 * 499` and `2` is a primitive root.
    .lucas { root := 2, primeFactors := [2, 167, 499] }])

primality (cert := …) [h₁, …] takes proofs hᵢ : Nat.Prime m instead of a certificate. See MathlibTest/Tactic/Primality.lean for more examples.

Equations

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