Nat.primeFactors

Stream: mathlib4

[Martin Dvořák]

Following on the recent project mentioned here
#Machine Learning for Theorem Proving > Autoformalization of the probabilistic abc-conjecture
in order to check what the repo proves, I had to review the following stack of definitions:

def Nat.minFacAux (n : ℕ) : ℕ → ℕ
  | k =>
    if n < k * k then n
    else
      if k ∣ n then k
      else
        minFacAux n (k + 2)

def Nat.minFac (n : ℕ) : ℕ :=
  if 2 ∣ n then 2 else minFacAux n 3

def Nat.primeFactorsList : ℕ → List ℕ
  | 0 => []
  | 1 => []
  | k + 2 =>
    let m := minFac (k + 2)
    m :: primeFactorsList ((k + 2) / m)

def Nat.primeFactors (n : ℕ) : Finset ℕ := n.primeFactorsList.toFinset

It took me about 10 minutes to check that it indeed defines the set of all prime factors.

Only afterwards I noticed that Mathlib contains:

@[simp] lemma mem_primeFactors : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
  simp_rw [← toFinset_factors, List.mem_toFinset, mem_primeFactorsList']

Shouldn't we exchange what is the official definition (the one we get to via clicking "Go to Definition") and what is the efficiently computable definition? Noticing that Nat.mem_primeFactors exists is kinda random.

My point is that, in order to check which version of the abc conjecture has been formally verified, I shouldn't need to study how to efficiently generate a list of prime factors; the mathematical definition should suffice (and, indeed, it would be much easier to read).

PS: On the other hand, checking what Nat.Prime means is not entirely trivial either...

[Joachim Breitner]

I don't think you can do that for definitions without affecting by decide, unfortunately.

[Martin Dvořák]

Don't we have a mechanism that signifies that a certain definition gets computed by a certain instance?

[Joachim Breitner]

For propositions there is the Decidable type class. And for compiled computation (not kernel reduction) there is csimp. I don't know of anything else?

[Eric Wieser]

I don't understand what you are proposing the definition be replaced with

[Kenny Lau]

isn't there this mechanism where some c++ or python code replaces certain calculations with Nat?

[Eric Wieser]

Perhaps, but I don't see how that would help with Martin's complaint that the function is hard to understand