## Stream: math-comp users

### Topic: Definition of the set of Prime numbers.

#### Jannik Mähn (May 30 2024 at 12:58):

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?

#### Quentin VERMANDE (May 30 2024 at 13:17):

Here, `P` would be a copy of `'I_n`, you probably want something like `Definition P := [set x : 'I_n | prime x]`.

#### Jannik Mähn (May 30 2024 at 13:29):

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

#### Quentin VERMANDE (May 30 2024 at 13:33):

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.

#### Cyril Cohen (May 30 2024 at 15:49):

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