我正在学习Idris,作为个人练习,我想实现一个Primes
类型,包含所有素数。
在Idris中,是否有一种定义新类型的方式,可以从一个类型和一个属性开始,选择所有满足该属性的起始类型的元素?在我的情况下,是否有一种方式可以将Primes
定义为Nat
集合,使得n <= p and n|p => n=1 or n=p
?
如果这不可能,那么我应该通过某种筛法递归地定义素数吗?
我喜欢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'
为此编写一个决策过程也是非常复杂的。那将是一项重大的练习!您可能会发现其余定义在这方面非常有用: