Extensible framework for primality certificates

The prime_cert% elaborator processes a sequence of step groups (e.g. small, pock, pock3), each registered via the @[prime_cert] attribute. A PrimeDict threads proof terms for already-certified primes through the ladder so later steps can reference earlier ones.

@[reducible, inline]

abbrev PrimeCert.Meta.PrimeDict : Type

We store the metavariable assigned to each certified prime.

Equations

• PrimeCert.Meta.PrimeDict = Std.HashMap ℕ Lean.Expr

def PrimeCert.Meta.PrimeDict.getM (dict : PrimeDict) (n : ℕ) : Lean.MetaM Lean.Expr

Equations

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

@[reducible, inline]

abbrev PrimeCert.Meta.PrimeCertMethod (syntaxName : Lean.Name) : Type

Equations

• PrimeCert.Meta.PrimeCertMethod syntaxName = (Lean.TSyntax syntaxName → PrimeCert.Meta.PrimeDict → Lean.MetaM (ℕ × (N : Q(ℕ)) × Q(Nat.Prime «$N»)))

structure PrimeCert.Meta.PrimeCertExt : Type

A method to climb one step in the ladder, given the dictionary of previously proved primes.

• syntaxName : Lean.Name

  The syntax specific to the certification method

• methodName : Lean.Name

  The function to build the prime proof in the step

def PrimeCert.Meta.instInhabitedPrimeCertExt.default : PrimeCertExt

Equations

• PrimeCert.Meta.instInhabitedPrimeCertExt.default = { syntaxName := default, methodName := default }

instance PrimeCert.Meta.instInhabitedPrimeCertExt : Inhabited PrimeCertExt

Equations

• PrimeCert.Meta.instInhabitedPrimeCertExt = { default := PrimeCert.Meta.instInhabitedPrimeCertExt.default }

opaque PrimeCert.Meta.primeCertExt : Lean.SimpleScopedEnvExtension (String × PrimeCertExt) (Std.HashMap String PrimeCertExt)

def PrimeCert.Meta.prime_cert : Lean.ParserDescr

Attribute to register a new certification method for use in prime_cert%.

Usage: @[prime_cert key] def myExt : PrimeCertExt where ...

This registers the method under key, generating syntax rules so it can be used as key spec or key {spec₁; spec₂; ...} inside prime_cert%.

Equations

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

def PrimeCert.Meta.mkPrimeCertExt (n : Lean.Name) : Lean.ImportM PrimeCertExt

Read a prime_cert extension from a declaration of the right type.

Equations

• PrimeCert.Meta.mkPrimeCertExt n = do let __discr ← read match __discr with | { env := env, opts := opts } => liftM (IO.ofExcept (PrimeCert.Meta.mkPrimeCertExt.unsafe_impl_3 n env opts))

def PrimeCert.Meta.PrimeCertExt.mkMethod (ext : PrimeCertExt) : Lean.ImportM (PrimeCertMethod ext.syntaxName)

Read a prime certifying method from a declaration of the right type.

Equations

• ext.mkMethod = do let __discr ← read match __discr with | { env := env, opts := opts } => liftM (IO.ofExcept (PrimeCert.Meta.PrimeCertExt.mkMethod.unsafe_impl_3 ext env opts))

def PrimeCert.Meta.step_group.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.step_group : Category

Equations

• Lean.Parser.Category.step_group = { }

def Lean.Name.toSyntaxCat (cat : Name) : TSyntax `stx

Convert a syntax category name to a TSyntax `stx dynamically.

Equations

• cat.toSyntaxCat = { raw := (Lean.mkNode `Lean.Parser.Syntax.cat #[(Lean.mkIdent cat).raw, Lean.mkNullNode]).raw }

def PrimeCert.Meta.mkSyntax (key : String) (spec : Lean.Name) : Lean.Elab.Command.CommandElabM Unit

If we're given a syntax pock_spec for a step in pock, we do the following:

syntax "pock" pock_spec : step_spec
syntax "pock" "{" pock_spec;+ "}" : step_spec

Equations

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

def PrimeCert.Meta.parseStepGroup (stx : Lean.TSyntax `step_group) : Lean.CoreM ((e : PrimeCertExt) × Array (Lean.TSyntax e.syntaxName))

Equations

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

def PrimeCert.Meta.«termPrime_cert%[_,,]» : Lean.ParserDescr

The main primality certificate elaborator.

Syntax: prime_cert% [group₁, group₂, ...]

Each group is a registered method name followed by one or more steps:

• small {p₁; p₂; ...} — look up pre-proved small primes
• pock (N, root, F₁) or pock {step₁; step₂; ...} — Pocklington certificates
• pock3 (N, root, m, mode, F) — cube-root Pocklington certificates

Groups are processed left-to-right. Within each group, steps are processed in order. Every certified prime is added to an internal PrimeDict so later steps can reference it. The last prime certified becomes the result.

theorem prime_60digit :
    Nat.Prime 236684654874665389773181956283167565443541280517430278333971 := prime_cert%
  [small {2; 3; 7; 11; 29; 31},
   pock3 (73471, 3, 1, 7, 2 * 31),
   pock3 (32560621, 2, 1, 7, 2 ^ 2 * 3 * 29),
   pock3 (3586530508831189, 2, 1, 11, 2 ^ 2 * 73471),
   pock3 (236684654874665389773181956283167565443541280517430278333971,
     2, 1, 3, 2 * 32560621 * 3586530508831189)]

Equations

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