代码之家 › 专栏 › 技术社区 › marcosh

Idris-定义素数类型

idris primes

marcosh · 技术社区 · 7 年前

我正在学习Idris,作为个人练习,我想实施一个 Primes

idris中是否有方法定义从类型和属性开始的新类型,该类型和属性将选择属性为true的起始类型的所有元素?就我而言,有没有办法定义 素数 作为 Nat 因此 n <= p and n|p => n=1 or n=p

1 回复 | 直到 7 年前

Brian McKenna 7 年前

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

推荐文章

Donovan · (提炼?是吗?)Idris中具体类型的类型变量?对于独立键入的HOAS拉链

6 年前

LogicChains · 是否有一种类型理论可以表示形状相同的归纳数据类型的等价性?

6 年前

BlenderBender · Idris中非零整数的类型?

6 年前

ice1000 · 当Agda/Idris无法做到时,Coq可以做什么?

7 年前

Roasted Yam · 查找归纳定义类型的实现(show)

7 年前

luochen1990 · 如何在Idris/Agda/Coq中模式匹配多个值?

7 年前

michaelmesser · Idris重写未发生

7 年前

marcosh · Idris-定义素数类型

7 年前

rfliam · 整数LTE(ZZ)

7 年前

lodo · 依赖类型:在归纳类型中强制全局属性

7 年前