Idris - Define a primes type

Question

I am learning Idris and as a personal exercise, I would like to implement a Primes type, consisting of all the prime numbers.

Is there a way in idris to define a new type starting from a type and a property, which will select all the elements of the starting type for which the property holds true? In my case, is there a way to define Primes as the set of Nat such that n <= p and n|p => n=1 or n=p?

If this is not possible, should I define prime numbers constructing them inductively using some kind of sieve?

Answer 1

I like copumpkin's Agda definition of Prime, which looks like this in 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

Read as "if p is divisible by d, then d must be 1 or p" - a common definition for primality.

Proving this by hand for a number can be pretty tedious:

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'

It's also very involved to write a decision procedure for this. That'll be a big exercise! You'll probably find the rest of the definitions useful for that:

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