Stream: math-comp users

Topic: ✔ Definition of the set of Prime numbers.


view this post on Zulip Jannik Mähn (May 31 2024 at 10:49):

Thanks you two for you help! The final solution looks like this:

From mathcomp Require Import all_ssreflect prime zmodp reals.

Module Type Primes.

  Variable n : nat.

  Definition P := [set x : 'I_n.+1 | prime x].

  Lemma four_notin_P : inZp 4 \notin P.
  Proof.
  Admitted.

End Primes.

view this post on Zulip Notification Bot (May 31 2024 at 10:49):

Jannik Mähn has marked this topic as resolved.

view this post on Zulip Bas Spitters (May 31 2024 at 14:01):

@Jannik Mähn I was going to point to the coq-prima package, but now I see there are actually a number of packages defining them: https://github.com/thery/coqprime
https://coq.inria.fr/coq-package-index (search prime-numbers).

view this post on Zulip Jannik Mähn (Jun 05 2024 at 14:23):

Thanks Bas, I'll have a look there as well!

view this post on Zulip Jannik Mähn (Jun 13 2024 at 09:52):

Dear math-comp users, I have to reopen the topic.

How can we define a type for the set of primes that we have defined above?

So, given this definition:

From mathcomp Require Import all_ssreflect prime zmodp reals.

Module Type Primes.

  Variable n : nat.
  Definition P := [set x : 'I_n.+1 | prime x].

End Primes.

We need to write something like this:

From mathcomp Require Import all_ssreflect prime zmodp reals.

Module Type Primes.

  Variable n : nat.
 Definition P' : {set x : 'I_n.+1 | prime x} := [set x : 'I_n.+1 | prime x].


End Primes.

Where I get a syntax error right now.

There might also be another approach, where we define things like this:

From mathcomp Require Import all_ssreflect prime zmodp reals.

Module Type Primes.

  Variable n : nat.

  Definition P : {set 'I_n.+1} := [set : 'I_n.+1].
  Parameter all_prime : forall x, x \in P -> prime x.
  Definition Z_n_prod := [finType of P].

End Primes.

I want to define it in this
finType
notation becauce of the setting we're working in. Here I get the following error:

**Error:** `The term "P" has type "{set 'I_n.+1}" while it is expected to have type "Type".`

Thanks a lot in advance!


Last updated: Jul 15 2024 at 20:02 UTC