伊德里斯 - 定義素數類型

Question

我正在學習伊德里斯，作爲一項個人練習，我想實現一個由所有素數組成的Primes類型。

idris中有一種方法來定義一個從類型和屬性開始的新類型，它將選擇屬性爲true的所有啓動類型的元素？在我的情況下，有沒有辦法將Primes定義爲Nat這樣的集合，使得n <= p and n|p => n=1 or n=p？

如果這是不可能的，我應該使用某種篩子定義素數來構建它們嗎？

Answer 1

我喜歡copumpkin's Agda definition of Prime，它看起來像這樣在伊德里斯：

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 

讀爲「如果p是由d整除，則d必須是1或P」 - 爲素性的共同定義。

用手一些證明這一點也相當單調乏味：

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' 

這也是非常複雜的撰寫對這一決定的過程。這將是一個很大的練習！您可能會發現其餘定義對此很有用：

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