Jannik Mähn (May 31 2024 at 10:49): 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.
Jannik Mähn has marked this topic as resolved.
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).
Jannik Mähn (Jun 05 2024 at 14:23):Thanks Bas, I'll have a look there as well!
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: Oct 13 2024 at 01:02 UTC