Benchmark / PrimeCert

PrimeCert: Mathlib v4.31.0 → v4.35.0

lake build passes after repair. The bump spans 4 Mathlib releases and produced 8 raw build errors in 2 files; an alias rewrite resolves 0 of them.

Project: b-mehta/PrimeCert. First build after the bump: 45.8 s, 1 deprecation warnings (0 with a replacement an alias rewrite would apply).

Changed what it proves. The repair that made lake build pass also changed the project itself:

PrimeCert/Pocklington.lean::Nat.modEq_iff_forall_prime_dvd: statement weakened

Review these before you treat the build as a proof of the original statement.

Local copies removed. 1 declaration the project defined itself, now provided by Mathlib at v4.35.0 (each checked there):

PrimeCert/Pocklington.lean::multiplicity_zero_right

Repairs

Arm	lake build	Rebuilds	Agent min	Labelled changes
Arm A (diagnosing session, not blind)	green	2	12	3 signature change, 1 rename, 1 reproof
Arm A2 (fresh agent, compiler output only: blind)	green	2	2	2 signature change, 1 rename
Arm B (fresh agent, compiler output plus enclosing declarations: blind)	green	2	2.8	2 signature change, 1 rename

What changed, labelled

Label	File	What changed in Mathlib, and the repair
signature change	PrimeCert/PowMod.lean	upstream added Nat.powMod; local powMod became ambiguous under `open Nat`. Fixed with `open Nat hiding powMod`.
rename	PrimeCert/Interval.lean	Bool.and' deprecated -> Bool.and (&&); the simp lemma Bool.and'_eq_and was deleted, so the simp line was dropped.
signature change	PrimeCert/Pocklington.lean	Mathlib's multiplicity a 0 is now 0 (was junk 1) and multiplicity_zero_right exists upstream: local copy deleted; Nat.modEq_iff_forall_prime_dvd no longer true for n=0, so hypothesis n ≠ 0 added and its caller updated.
signature change	PrimeCert/Pocklington.lean	Nat.multiplicity_eq_factorization lost its nonzero hypothesis argument (3 call sites).
reproof	PrimeCert/Pocklington.lean	`multiplicity_eq_zero.mpr hqn` replaced by `multiplicity_eq_zero_of_not_dvd hqn`.

The diff

diff --git a/PrimeCert/Interval.lean b/PrimeCert/Interval.lean

index 2ab97df..0ff658d 100644

--- a/PrimeCert/Interval.lean

+++ b/PrimeCert/Interval.lean

@@ -18,12 +18,11 @@ section forallB

noncomputable def forallB (f : ℕ → Bool) (start len : ℕ) (step : ℕ := 1) : Bool :=

(Nat.rec (motive := fun _ ↦ ℕ × Bool) (start, true)

- (fun _ ih ↦ ih.rec fun i b ↦ (i.add step, (f i).and' b)) len).2

+ (fun _ ih ↦ ih.rec fun i b ↦ (i.add step, (f i && b))) len).2

theorem forallB_iff_range' (f : ℕ → Bool) (start len step : ℕ) :

forallB f start len step ↔ ∀ n ∈ List.range' start len step, f n := by

unfold forallB

- simp only [Bool.and'_eq_and]

induction len with

| zero => simp

| succ len ih =>

diff --git a/PrimeCert/Pocklington.lean b/PrimeCert/Pocklington.lean

index c801581..5173157 100644

--- a/PrimeCert/Pocklington.lean

+++ b/PrimeCert/Pocklington.lean

@@ -36,27 +36,14 @@ theorem Nat.modEq_finset_prod_iff {a b : ℕ} {ι : Type*} (s : Finset ι) (e :

· simp_rw [List.mem_toFinset]

· rwa [← List.pairwise_iff_coe_toFinset_pairwise hl]

-theorem multiplicity_zero_right {α : Type*} [MonoidWithZero α] (x : α) : multiplicity x 0 = 1 :=

- multiplicity_eq_one_of_not_finiteMultiplicity fun h ↦ h.ne_zero rfl

-theorem Nat.modEq_iff_forall_prime_dvd {a b n : ℕ} :

+theorem Nat.modEq_iff_forall_prime_dvd {a b n : ℕ} (hn₀ : n ≠ 0) :

a ≡ b [MOD n] ↔ ∀ p : ℕ, p ∣ n → p.Prime → a ≡ b [MOD p ^ multiplicity p n] := by

- by_cases hn₀ : n = 0

- · subst hn₀

- simp_rw [modEq_zero_iff, dvd_zero, true_imp_iff]

- constructor

- · rintro rfl; exact fun _ _ ↦ by rfl

- · intro h

- obtain ⟨p, hbp, hp⟩ := exists_infinite_primes (a + b + 1)

- specialize h p hp

- rw [multiplicity_zero_right, pow_one] at h

- exact h.eq_of_lt_of_lt (by linarith) (by linarith)

- · conv_lhs => rw [← prod_factorization_pow_eq_self hn₀]

- rw [Finsupp.prod, modEq_finset_prod_iff]

- · simp_rw [support_factorization, mem_primeFactors_of_ne_zero hn₀, and_comm, and_imp]

- refine forall_congr' fun p ↦ imp_congr_right fun hpn ↦ imp_congr_right fun hp ↦ ?_

- rw [multiplicity_eq_factorization hp hn₀]

- · grind [support_factorization, coprime_pow_primes, Set.Pairwise]

+ conv_lhs => rw [← prod_factorization_pow_eq_self hn₀]

+ rw [Finsupp.prod, modEq_finset_prod_iff]

+ · simp_rw [support_factorization, mem_primeFactors_of_ne_zero hn₀, and_comm, and_imp]

+ refine forall_congr' fun p ↦ imp_congr_right fun hpn ↦ imp_congr_right fun hp ↦ ?_

+ rw [multiplicity_eq_factorization hp]

+ · grind [support_factorization, coprime_pow_primes, Set.Pairwise]

theorem Nat.pow_multiplicity_dvd_of_dvd_of_not_dvd_div

{q n x : ℕ} (hq : q.Prime) (hxn : x ∣ n) (hxnq : ¬ x ∣ n / q) :

@@ -72,7 +59,7 @@ theorem Nat.pow_multiplicity_dvd_of_dvd_of_not_dvd_div

rw [← Nat.factorization_le_iff_dvd hx₀ hqn₀] at hxn

rw [Nat.factorization_mul hq.ne_zero hn₀, hq.factorization, add_comm] at hxn

refine pow_dvd_of_le_multiplicity ?_

- rw [multiplicity_eq_factorization hq hqn₀, multiplicity_eq_factorization hq hx₀,

+ rw [multiplicity_eq_factorization hq, multiplicity_eq_factorization hq,

Nat.factorization_mul hq.ne_zero hn₀, Finsupp.add_apply, hq.factorization,

Finsupp.single_apply, if_pos rfl, add_comm]

refine le_of_not_gt fun h ↦ hxnq fun p ↦ ?_

@@ -80,7 +67,7 @@ theorem Nat.pow_multiplicity_dvd_of_dvd_of_not_dvd_div

· subst hpq; exact Nat.lt_succ_iff.mp h

convert hxn p using 1

rw [Finsupp.add_apply, Finsupp.single_apply, if_neg (Ne.symm hpq), add_zero]

- · rw [multiplicity_eq_zero.mpr hqn, pow_zero]

+ · rw [multiplicity_eq_zero_of_not_dvd hqn, pow_zero]

exact one_dvd _

/-- Let `N` be a natural number whose primality we want to certify.

@@ -102,7 +89,7 @@ theorem pocklington_test (N F₁ : ℕ) (hn₀ : 0 < N) (hf₁ : F₁ ∣ N - 1)

rintro rfl

rw [zero_dvd_iff] at hf₁

omega

- rw [Nat.modEq_iff_forall_prime_dvd]

+ rw [Nat.modEq_iff_forall_prime_dvd hf₀]

intro q hqf hq

have := Fact.mk hp

have := (Nat.prime_iff_card_units _).mp hp

@@ -113,7 +100,7 @@ theorem pocklington_test (N F₁ : ℕ) (hn₀ : 0 < N) (hf₁ : F₁ ∣ N - 1)

let a' : (ZMod p)ˣ := Units.ofPowEqOne _ _ hanp (by grind)

refine dvd_trans ?_ (orderOf_dvd_card (x := a'))

have : multiplicity q F₁ ≤ multiplicity q (N - 1) := by

- rw [Nat.multiplicity_eq_factorization hq hf₀, Nat.multiplicity_eq_factorization hq (by grind)]

+ rw [Nat.multiplicity_eq_factorization hq, Nat.multiplicity_eq_factorization hq]

exact (Nat.factorization_le_iff_dvd hf₀ (by grind)).mpr hf₁ _

refine dvd_trans (pow_dvd_pow _ this) ?_

refine Nat.pow_multiplicity_dvd_of_dvd_of_not_dvd_div hq ?_ ?_

diff --git a/PrimeCert/PowMod.lean b/PrimeCert/PowMod.lean

index 6f8a8e4..6ee5759 100644

--- a/PrimeCert/PowMod.lean

+++ b/PrimeCert/PowMod.lean

@@ -15,7 +15,7 @@ Note that `Mathlib.Tactic.NormNum.PowMod` contains a similar tactic, but that ru

slower and less efficiently than the one here.

-open Nat

+open Nat hiding powMod

/-- The pow-mod function, named explicitly to allow more precise control of reduction. -/

def powMod (a b n : ℕ) : ℕ := a ^ b % n

Re-run it

source bench/env.sh
python3 bench/lbbench.py setup primecert      # clone b-mehta/PrimeCert at v4.31.0, bump the Mathlib pin to v4.35.0
python3 bench/lbbench.py build primecert      # cache get + lake build; writes the raw errors to bench/runs/primecert/v4.35.0/errors.json
git -C bench/work/primecert/proj apply ../../../runs/primecert/v4.35.0/armA.diff   # replay the recorded repair
python3 bench/lbbench.py build primecert --pass replay        # a green replay prints "build rc=0"

Files

Correct this page

Something wrong on this row, or you maintain this project and want it off the benchmark? Correct this row or remove my project.