The Lucas test for primes.

This file implements the Lucas test for primes (not to be confused with the Lucas-Lehmer test for Mersenne primes). A number a witnesses that n is prime if a has order n-1 in the multiplicative group of integers mod n. This is checked by verifying that a^(n-1) = 1 (mod n) and a^d ≠ 1 (mod n) for any divisor d | n - 1. This test is the basis of the Pratt primality certificate.

TODO

• Bonus: Show the reverse implication i.e. if a number is prime then it has a Lucas witness. Use Units.IsCyclic from RingTheory/IntegralDomain to show the group is cyclic.
• Write a tactic that uses this theorem to generate Pratt primality certificates
• Integrate Pratt primality certificates into the norm_num primality verifier

Implementation notes

Note that the proof for lucas_primality relies on analyzing the multiplicative group modulo p. Despite this, the theorem still holds vacuously for p = 0 and p = 1: In these cases, we can take q to be any prime and see that hd does not hold, since a^((p-1)/q) reduces to 1.

theorem Nat.Prime.dvd_mul_list {p : ℕ} {l : List ℕ} (h : Prime p) : p ∣ l.prod ↔ ∃ r ∈ l, p ∣ r

inductive PrattPartList (p : ℕ) (a : ZMod p) : ℕ → Prop

Recursive form of a Pratt certificate for p, which may take in Pratt certificates for a list of prime powers r less than p whose product is equal to p - 1.

• prime {p : ℕ} {a : ZMod p} (n k nk : ℕ) : Nat.Prime n → a ^ ((p - 1) / n) ≠ 1 → n ^ k = nk → PrattPartList p a nk
• split {p : ℕ} {a : ZMod p} {n : ℕ} (list : List ℕ) : (∀ r ∈ list, PrattPartList p a r) → list.prod = n → PrattPartList p a n

structure PrattCertificate' (p : ℕ) : Type

Alternative form of a Pratt certificate for p, which may take in Pratt certificates for a list of prime powers r less than p whose product is equal to p - 1.

• a : ZMod p
• pow_eq_one : self.a ^ (p - 1) = 1
• part : PrattPartList p self.a (p - 1)

theorem PrattPartList.out {p : ℕ} {a : ZMod p} {n : ℕ} (h : PrattPartList p a n) (q : ℕ) : Nat.Prime q → q ∣ n → a ^ ((p - 1) / q) ≠ 1

theorem PrattCertificate'.out {p : ℕ} (c : PrattCertificate' p) : Nat.Prime p

inductive PrattPart (p : ℕ) (a : ZMod p) : ℕ → Prop

The binary version of PrattPartList. This is the one in the original file.

• prime {p : ℕ} {a : ZMod p} (n k nk : ℕ) : Nat.Prime n → a ^ ((p - 1) / n) ≠ 1 → n ^ k = nk → PrattPart p a nk
• split {p : ℕ} {a : ZMod p} {n : ℕ} (l r : ℕ) : PrattPart p a l → PrattPart p a r → l * r = n → PrattPart p a n

structure PrattCertificate (p : ℕ) : Type

• a : ZMod p
• pow_eq_one : self.a ^ (p - 1) = 1
• part : PrattPart p self.a (p - 1)

theorem PrattPart.out {p : ℕ} {a : ZMod p} {n : ℕ} (h : PrattPart p a n) (q : ℕ) : Nat.Prime q → q ∣ n → a ^ ((p - 1) / q) ≠ 1

theorem PrattCertificate.out {p : ℕ} (c : PrattCertificate p) : Nat.Prime p

theorem prime_2 : Nat.Prime 2

theorem prime_3 : Nat.Prime 3

theorem prime_5 : Nat.Prime 5

theorem prime_7 : Nat.Prime 7

theorem prime_11 : Nat.Prime 11

theorem prime_13 : Nat.Prime 13

theorem prime_17 : Nat.Prime 17

theorem prime_19 : Nat.Prime 19

theorem prime_23 : Nat.Prime 23

theorem prime_29 : Nat.Prime 29

theorem prime_31 : Nat.Prime 31

theorem prime_37 : Nat.Prime 37

theorem prime_41 : Nat.Prime 41

theorem prime_43 : Nat.Prime 43

theorem prime_47 : Nat.Prime 47

theorem prime_101 : Nat.Prime 101

def powMod (a b m : ℕ) : ℕ

structure PowTwoRepr : Type

• two_exp : ℕ
• odd_part : ℕ

def factorOutTwos (n : ℕ) : PowTwoRepr

def millerRabinBases : List ℕ

def deterministicMillerRabin (n : ℕ) : Bool

def g (n c x : ℕ) : ℕ

def rho' (n start c : ℕ) : Option ℕ

Auxiliary function for rho that tries to find a factor of n

def rho (n : ℕ) : Option ℕ

partial def factor (n : ℕ) : Option (List ℕ)

structure PrimeWithMultiplicity : Type

• prime : ℕ
• multiplicity : ℕ

def instReprPrimeWithMultiplicity.repr : PrimeWithMultiplicity → ℕ → Std.Format

@[implicit_reducible]

instance instReprPrimeWithMultiplicity : Repr PrimeWithMultiplicity

def factor' (n : ℕ) : Option (List PrimeWithMultiplicity)

Factor n into a list of prime numbers with their multiplicities

inductive UnverifiedPrattPart : Type

• prime (p k : ℕ) (hp : UnverifiedPrattCertificate p) : UnverifiedPrattPart
• split : UnverifiedPrattPart → UnverifiedPrattPart → UnverifiedPrattPart

@[implicit_reducible]

instance instReprUnverifiedPrattPart : Repr UnverifiedPrattPart

partial def instReprUnverifiedPrattCertificate.repr_1 : UnverifiedPrattPart → ℕ → Std.Format

@[implicit_reducible]

instance instReprUnverifiedPrattCertificate {a✝ : ℕ} : Repr (UnverifiedPrattCertificate a✝)

partial def instReprUnverifiedPrattCertificate.repr_2 {a✝ : ℕ} : UnverifiedPrattCertificate a✝ → ℕ → Std.Format

partial def instReprUnverifiedPrattPart.repr_2 {a✝ : ℕ} : UnverifiedPrattCertificate a✝ → ℕ → Std.Format

partial def instReprUnverifiedPrattPart.repr_1 : UnverifiedPrattPart → ℕ → Std.Format

inductive UnverifiedPrattCertificate : ℕ → Type

• knownPrime (n : ℕ) : UnverifiedPrattCertificate n
• of (n a : ℕ) (part : UnverifiedPrattPart) : UnverifiedPrattCertificate n

@[implicit_reducible]

instance instToStringUnverifiedPrattCertificate {n : ℕ} : ToString (UnverifiedPrattCertificate n)

partial def computePrattPart (l : List PrimeWithMultiplicity) : Option UnverifiedPrattPart

partial def computePrattCertificate (n : ℕ) : Option (UnverifiedPrattCertificate n)

def computePrattCertificate.findWitness (n : ℕ) (fs : List PrimeWithMultiplicity) : Option ℕ

def Tactic.verifySmallPrime (n' : Q(ℕ)) : Lean.MetaM Q(Nat.Prime «$n'»)

theorem Tactic.ZMod.powEqOfPowMod {n a' c : ℕ} (a : ZMod n) : ↑a' = a → (a'.pow (n - 1)).mod n = c → c = 1 → a ^ (n - 1) = 1

theorem Tactic.ZMod.bla {n c : ℕ} (a : ZMod n) : c = 1 → Mathlib.Meta.NormNum.IsNat (a ^ (n - 1)) c → a ^ (n - 1) = 1

def Tactic.verifyEqOne (n a' : Q(ℕ)) (a : Q(ZMod «$n»)) : Q(↑«$a'» = «$a») → Lean.MetaM Q(«$a» ^ («$n» - 1) = 1)

theorem Tactic.ZMod.powNeOfPowMod {n a' q c : ℕ} (a : ZMod n) : ↑a' = a → decide (n ≥ 2) = true → (a'.pow ((n - 1) / q)).mod n = c → decide (c ≠ 1) = true → a ^ ((n - 1) / q) ≠ 1

theorem Tactic.ZMod.blub {n q c : ℕ} (a : ZMod n) : decide (n ≥ 2) = true → decide (c < n) = true → decide (c ≠ 1) = true → Mathlib.Meta.NormNum.IsNat (a ^ ((n - 1) / q)) c → a ^ ((n - 1) / q) ≠ 1

def Tactic.verifyNeOne (n a' q : Q(ℕ)) (a : Q(ZMod «$n»)) : Q(↑«$a'» = «$a») → Lean.MetaM Q(«$a» ^ ((«$n» - 1) / «$q») ≠ 1)

partial def Tactic.verifyCertificate (n' : Q(ℕ)) (n : ℕ) : UnverifiedPrattCertificate n → Lean.MetaM Q(Nat.Prime «$n'»)

partial def Tactic.verifyCertificate.generateCertificate (n' : Q(ℕ)) : ℕ → (a : ℕ) → (part : UnverifiedPrattPart) → Lean.MetaM Q(PrattCertificate «$n'»)

partial def Tactic.verifyCertificate.generatePart (n' : Q(ℕ)) (a : Q(ZMod «$n'»)) (a' : Q(ℕ)) (pa' : Q(↑«$a'» = «$a»)) : UnverifiedPrattPart → Lean.MetaM ((nn : Q(ℕ)) × Q(PrattPart «$n'» «$a» «$nn»))

theorem Tactic.Nat.Prime_of_isNat {n n' : ℕ} : Mathlib.Meta.NormNum.IsNat n n' → Nat.Prime n' → Nat.Prime n

def Tactic.tacticPratt : Lean.ParserDescr