Decidable nat.prime

Stream: general

[Patrick Johnson]

I implemented a decidable instance for nat.prime. Do we already have such instance that I'm not aware of? If not, should I open a PR?

[Patrick Johnson]

By decidable, I mean solvable using dec_trivial, like this:

example : nat.prime 7 ∧ ¬nat.prime 8 := dec_trivial

[Johan Commelin]

I'm pretty sure it's there already. There's also a norm_num extension for proving primality

[Eric Rodriguez]

there's actually two: docs#nat.decidable_prime and docs#nat.decidable_prime1

[Mario Carneiro]

The reason why decidable_prime_1 is not the default instance (and similar for other decidability instances like it) is because it is slower to perform computations like this than norm_num style proofs. You will very quickly run into the problem that direct computation on nat using this method works on unary numerals and so inevitably hits a wall at not-very-large numbers. decidable_prime is a more useful instance because it computes in #eval quickly (and in fact it is used in norm_num internally)

[Mario Carneiro]

If you really want to do computation in the kernel you should use docs#num instead of nat

[Mario Carneiro]

There is in fact an instance for primality over num as well: docs#num.decidable_prime

[Patrick Johnson]

Oh, I didn't look at the docs for nat.prime :face_palm:. I just tried dec_trivial and since it failed, I thought we don't even have a decidability instance, so I wrote one. But it was a fun excercise anyway. My instance timeouts for numbers >100, so it's pretty much useless.

[Patrick Johnson]

TIL that norm_num can also prove primality. That's interesting.

[Kevin Buzzard]

Here's how it happened: https://xenaproject.wordpress.com/2018/07/26/617-is-prime/