## Stream: Coq users

### Topic: Constructive way to build next prime function?

#### 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?

#### 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.

#### 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.

#### 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.

#### 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.

#### 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`.

#### Anthony Peterson (Mar 20 2024 at 18:42):

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

#### 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