Idris -定义素数类型

Question

我正在学习Idris，作为个人练习，我想实现一个由所有素数组成的Primes类型。

在idris中是否有一种方法可以从类型和属性开始定义一个新类型，它将选择属性为真的起始类型的所有元素？在我的例子中，是否有一种方法可以将Primes定义为Nat的集合，以便使n <= p and n|p => n=1 or n=p

如果这是不可能的，我应该用某种筛子来定义质数来构造它们吗？

Answer 1

我喜欢copumpkin的Agda素数定义，它在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

读为“如果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