Idris - Definieren Sie eine Primzahl Typ

Question

Ich lerne Idris und als eine persönliche Übung, würde ich gerne einen Primes Typ implementieren, der aus allen Primzahlen besteht.

Gibt es einen Weg in Idris, einen neuen Typ zu definieren, der von einem Typ und einer Eigenschaft ausgeht und alle Elemente des Starttyps auswählt, für die die Eigenschaft gilt? In meinem Fall gibt es eine Möglichkeit, Primes als den Satz von Nat so zu definieren, dass n <= p and n|p => n=1 or n=p?

Wenn das nicht möglich ist, sollte ich Primzahlen definieren, die sie mit einer Art Sieb induktiv aufbauen?

Answer 1

Ich mag copumpkin's Agda definition of Prime, die in Idris wie folgt aussieht:

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 

lesen wie "wenn p durch d teilbar ist, dann d 1 oder p sein muss" - eine gemeinsame Definition für primality.

dies für eine Reihe von Hand Proving kann ziemlich mühsam sein:

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' 

Es ist auch sehr engagiert ein Entscheidungsverfahren für diese zu schreiben. Das wird eine große Übung sein! Sie werden wahrscheinlich den Rest der Definitionen dafür nützlich finden:

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