Dear math-comp users,

what is the best way to define the set of prime numbers in Coq?

I have tried the following:

```
From mathcomp Require Import all_ssreflect.
Module Type Primes.
Variable n : nat.
Hypothesis n_pos : 0 < n.
Definition P := [finType of 'I_n].
Parameter primes : forall p : P, prime p.
Lemma four_notin_P : 4 \notin P.
End Primes.
```

However, Coq doesn't understand the Lemma and throughs the error:

```
Error: The term "mem P" has type "mem_pred P" while it is expected to have type
"mem_pred nat".
```

Do you know how I can fix this?

Thanks in advance!

Here, `P`

would be a copy of `'I_n`

, you probably want something like `Definition P := [set x : 'I_n | prime x]`

.

Then the Lemma throws this error:

```
Error: The term "mem P" has type
"mem_pred (fintype_ordinal__canonical__fintype_Finite n)"
while it is expected to have type "mem_pred nat".
```

Yes, because Coq does not know that `4`

is in `I_n`

(which is the type of integers less than `n`

). I am not sure there is good support for sets with arbitrary support, unless you have mathcomp-classical.

If you write `'I_n.+1`

instead of having a side condition for `n`

, if you import `zmodp`

and if you write `4%R`

instead of `4`

, it should recognize `4%R`

as `1 + 1 + 1 + 1`

in the ring `'I_n.+1`

.

Last updated: Jul 15 2024 at 20:02 UTC