Proving a constant is prime

Stream: new members

[Newell Jensen]

Forgive me for the simple question but, how do you simply prove that a constant nat is prime? I have tried the below but stuck at the next step...

let p := 5,
have h : prime p :=
begin
   refine tactic.norm_num.is_prime_helper p _ _,
   linarith,
end

Seems like there should be a better way of doing this?

[Yaël Dillies]

Use norm_num. It knows about primes.

[Newell Jensen]

Thansk for the reply Yaël. From test/norm_num_ext.lean I found example : nat.prime 5 := by norm_num, which works for me but when I go to do

let p := 5,
have h : prime p := by norm_num,

it errors out saying that norm_num failed to simplify. Ultimately what I am trying to do is prove that prime p ^ p < stuff .... Any ideas why the example would work and why the above wouldn't?

[Alex J. Best]

Does h : nat.prime p work instead? docs#nat.prime is different from docs#prime i believe, and perhaps norm_num only deals with the former.

[Eric Rodriguez]

if you want to convert between both there is docs#nat.prime_iff

[Mario Carneiro]

The issue here is not nat.prime vs prime but the fact that you have a let in the way. Unfold that first

[Mario Carneiro]

also, #mwe

[Newell Jensen]

Here should be an mwe:

import data.nat.prime

namespace nat

example : prime 5 := by norm_num

example (p : ℕ): prime p :=
begin
  let p₀ := 5,
  have h : prime p₀ := by { unfold p₀, norm_num }
end

Thanks for all the replies, I truly appreciate it.

[Mario Carneiro]

norm_num [p₀] works

[Tyler Josephson]

This is neat! Is there a limit to this? Could it prove a 10-digit prime, like 6570237887, or will it time out before finishing?

[Jason Rute]

import data.nat.prime

namespace nat

example : prime 6570237887 := by norm_num - -deterministic timeout

end nat

[Mario Carneiro]

It uses trial division, so it's order sqrt n. There hasn't really been demand / applications for larger primes, because usually something else goes wrong first

[Junyan Xu]

There is https://github.com/leanprover-community/mathlib/pull/12254/files#diff-0f95a1dfea2490459388549f1aa3b3e8bf2da091c83cf579e01d092c378f9b44