Idris - Définir un type de nombres premiers

Question

J'apprends l'Idris et comme exercice personnel, je voudrais implémenter un type Primes, composé de tous les nombres premiers.

Est-il possible de définir un nouveau type dans idris à partir d'un type et d'une propriété, qui sélectionnera tous les éléments du type de départ pour lesquels la propriété est vraie? Dans mon cas, existe-t-il un moyen de définir Primes comme l'ensemble de Nat tel que n <= p and n|p => n=1 or n=p?

Si cela n'est pas possible, devrais-je définir les nombres premiers en les construisant de manière inductive en utilisant une sorte de tamis?

Answer 1

J'aime copumpkin's Agda definition of Prime, qui ressemble à ceci à Idris:

data Divides : Nat -> Nat -> Type where 
    MkDivides : (q : Nat) -> 
       n = q * S m -> 
       Divides (S m) n 

data Prime : Nat -> Type where 
    MkPrime : GT p 1 -> 
      ((d : Nat) -> Divides d p -> Either (d = 1) (d = p)) 
      -> Prime p 

Lire comme "si p est divisible par d, alors d doit être 1 ou p" - une définition commune pour primalité.

prouvons à la main pour un certain nombre peut être assez fastidieux:

p2' : (d : Nat) -> Divides d 2 -> Either (d = 1) (d = 2) 
p2' Z (MkDivides _ _) impossible 
p2' (S Z) (MkDivides Z Refl) impossible 
p2' (S Z) (MkDivides (S Z) Refl) impossible 
p2' (S Z) (MkDivides (S (S Z)) Refl) = Left Refl 
p2' (S Z) (MkDivides (S (S (S _))) Refl) impossible 
p2' (S (S Z)) (MkDivides Z Refl) impossible 
p2' (S (S Z)) (MkDivides (S Z) Refl) = Right Refl 
p2' (S (S Z)) (MkDivides (S (S _)) Refl) impossible 
p2' (S (S (S _))) (MkDivides Z Refl) impossible 
p2' (S (S (S _))) (MkDivides (S _) Refl) impossible 

p2 : Prime 2 
p2 = MkPrime (LTESucc (LTESucc LTEZero)) p2' 

Il est également très impliqué d'écrire une procédure de décision à cet effet. Ce sera un gros exercice! Vous trouverez probablement le reste des définitions utiles pour cela:

https://gist.github.com/copumpkin/1286093