Stream: math-comp users

Topic: Definition of the set of Prime numbers.


view this post on Zulip 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?

Thanks in advance!

view this post on Zulip 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].

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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