Zulip Chat Archive

Stream: general

Topic: Decidable nat.prime

Patrick Johnson (Jan 26 2022 at 19:33):

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 (Jan 26 2022 at 19:38):

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

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

Johan Commelin (Jan 26 2022 at 19:41):

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

Eric Rodriguez (Jan 26 2022 at 19:41):

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

Mario Carneiro (Jan 26 2022 at 19:52):

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 (Jan 26 2022 at 19:53):

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

Mario Carneiro (Jan 26 2022 at 19:53):

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

Patrick Johnson (Jan 26 2022 at 19:58):

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 (Jan 26 2022 at 19:59):

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

Kevin Buzzard (Jan 26 2022 at 22:54):

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

Last updated: Aug 03 2023 at 10:10 UTC