Idris - 定义素数类型答案

【问题标题】：Idris - Define a primes typeIdris - 定义素数类型
【发布时间】：2017-09-09 16:54:17
【问题描述】：

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

idris 中是否有一种方法可以从一个类型和一个属性开始定义一个新类型，它将选择该属性成立的所有起始类型的元素？就我而言，有没有办法将Primes 定义为Nat 的集合，这样n <= p and n|p => n=1 or n=p？

如果这不可能，我是否应该定义质数，使用某种筛子归纳构造它们？

【问题讨论】：

标签： primes idris

【解决方案1】：

我喜欢 copumpkin's Agda definition of Prime，它在 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

【讨论】：