Prime vs Nat.Prime and not_prime_mul

Stream: new members

[rzeta0]

One of the most basic ideas that children at primary school learn (at least 40 years ago) is that two numbers multiplied together can't give a prime.

So using a lemma that reflects this, the following is a simple proof that 12 is not prime:

example : ¬ Nat.Prime (12) := by
  have g: 12 = 3*4 := by norm_num
  rw [g]
  have h1: 3 ≠ 1 := by norm_num
  have h2: 4 ≠ 1 := by norm_num
  apply Nat.not_prime_mul h1 h2

The lemma is defined for Nat.Prime:

theorem Nat.not_prime_mul {a : ℕ}  {b : ℕ}  (a1 : a ≠ 1)  (b1 : b ≠ 1) : ¬Nat.Prime (a * b)

My question is - why isn't there a similar lemma for Prime (not just Nat.Prime) that reflects the idea that a*b is not prime?

Something like the following:

theorem Nat.not_prime_mul {a : ℕ}  {b : ℕ}  (a1 : a ≠ 1)  (b1 : b ≠ 1) : ¬ Prime (a * b) -- made up lemma

[Adam Topaz]

docs#Nat.not_prime_mul

[Eric Wieser]

I think the question is kind of "why not pull every theorem about Nat.Prime across docs#Nat.prime_iff to translate it to docs#Prime"

[rzeta0]

yes - that's the question.

For example IsSquare.not_prime is about Prime not Nat.Prime

[Eric Wieser]

I had hoped the answer would be "Nat.Prime is the simp-normal form for Prime (n : Nat) so there is no need", but unfortunately that's not true...

[Eric Wieser]

rzeta0 said:

For example IsSquare.not_prime is about Prime not Nat.Prime

Anything that is not about Nat will use Prime not Nat.Prime

[Adam Topaz]

It's not completely clear that Nat.Prime should be the simp normal form.

[Eric Wieser]

Arguably Nat.Prime shouldn't exist at all, and we should only have Prime

[rzeta0]

something to look forward to in Lean 5? :)

[Eric Wieser]

Eric Wieser said:

Arguably Nat.Prime shouldn't exist at all, and we should only have Prime

But in fact, Nat.Prime is defined as Irreducible, so I think there's no free lunch here

[Eric Wieser]

I guess we could go down from having 3 spellings (Prime n, Nat.Prime n, Irreducible n) to having two

[Eric Wieser]

Back to your original question, perhaps

theorem not_prime_mul [CancelCommMonoidWithZero M] {a b : M} (ha : ¬IsUnit a) (hb : ¬IsUnit b) : ¬Prime (a * b) :=
  prime_mul_iff.not.mpr <| Or.rec (hb ·.2) (ha ·.1)

should be in mathlib

[Kyle Miller]

By the way, norm_num knows how to compute whether numbers are prime, so this works:

example : ¬ Nat.Prime 12 := by norm_num

I know that's not the point of your exercise, but I thought I'd mention it.

[Kevin Buzzard]

rzeta0 said:

something to look forward to in Lean 5? :)

This is a mathlib issue, not a lean issue. Lean has all the basic machinery to make the concept of mathlib work, but very little mathematics (eg I doubt it has anything to do with prime numbers)

[Kevin Buzzard]

docs#Nat.Prime yeah this is all mathlib

[Edward van de Meent]

Eric Wieser said:

I guess we could go down from having 3 spellings (Prime n, Nat.Prime n, Irreducible n) to having two

do note that Irreducible n and Prime n mean different things...

[Ruben Van de Velde]

Not for n : Nat

[Kevin Buzzard]

Yes but Edward's point is that we'll never be able to get down to one.

[Ruben Van de Velde]

Oh sure, but two should be relatively easy

[Ruben Van de Velde]

Though the question is if we should replace Nat.Prime by Prime or Irreducible

[Johan Commelin]

I think this was discussed in the past. We wanted to keep Nat.Prime because of the recognizable name. But it's defined in terms of Irreducible because that is the definition in the literature for natural prime numbers.

[Johan Commelin]

It could certainly become an abbrev, if it isn't already.

[Ruben Van de Velde]

Pretty sure it isn't an abbrev right now