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?

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.

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.

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.

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

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`

.

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

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