Stream: Coq users

Topic: Constructive way to build next prime function?


view this post on Zulip Anthony Peterson (Mar 15 2024 at 12:41):

I would like to write a definition in Coq that, given a natural number n, would find the next prime number greater than n. I know there must be a prime before 2n, but I don't know how to formalize that.

If I just search for the next prime, Coq will complain about non-termination, but if I explicit tell it to stop at 2n, proving that it actually found a prime and dealing with the option type result might be tricky? What do you think the best approach is?

view this post on Zulip Rígille S. B. Menezes (Mar 15 2024 at 12:52):

You could define a function using Function like in Recursive Functions That are Not Structurally Recursive. Instead of using the 2n bound which would take a lot of work to formalize, try using Euclid's bound as the measure. Namely (the product of all primes up to n) + 1.

view this post on Zulip Anthony Peterson (Mar 15 2024 at 13:05):

Rígille S. B. Menezes said:

Instead of using the 2n bound which would take a lot of work to formalize, try using Euclid's bound as the measure. Namely (the product of all primes up to n) + 1.

OK, sounds like something easier to try. Thanks.

view this post on Zulip Dominique Larchey-Wendling (Mar 15 2024 at 21:32):

There is such a function defined in the Coq Library of Undecidability proofs that is used for the Gödel coding of Minsky machines into FRACTRAN.

view this post on Zulip Dominique Larchey-Wendling (Mar 15 2024 at 21:35):

Actually there is a whole library for prime numbers incl. theorems such as Wilson's theorem or Lucas's theorem.

view this post on Zulip Dominique Larchey-Wendling (Mar 15 2024 at 21:51):

The function is based on the following bound: any prime divisor of n!+1 must be greater than n. Also any number has a prime divisor. So there is a prime above n which is also smaller than n!+1. That is not a great bound but you do not need to compute it if you are concerned with efficiency. It can just serves as a termination certificate in Prop.

view this post on Zulip Anthony Peterson (Mar 20 2024 at 18:42):

Actually, that's funny. I was trying to implement this for something Godel related.

view this post on Zulip Dominique Larchey-Wendling (Mar 21 2024 at 09:03):

Anthony Peterson said:

Actually, that's funny. I was trying to implement this for something Godel related.

Could you be more specific ?


Last updated: Jun 18 2024 at 21:01 UTC