如何证明 2 是 Idris 中的素数？答案

【问题标题】：How to prove that 2 is Prime in Idris?如何证明 2 是 Idris 中的素数？
【发布时间】：2020-03-28 10:22:34
【问题描述】：

我现在是 Idris 的初学者，所以我想寻求帮助。我有划分的定义：

data DividesNat : (a : Nat) -> (b : Nat) -> Type where
    Div : (k ** (k * x = y)) -> DividesNat y x

以及基于 DividesNat 的素数定义：

data Prime : (p : Nat) -> Type where
    ConsPrime : LTE 2 p ->
        ((d : Nat) -> DividesNat p d -> Either (d = 1) (d = p)) ->
        Prime p

现在我要证明 2 是素数：

prf2IsPrime : Prime (S (S Z))
prf2IsPrime = ConsPrime (LTESucc (LTESucc LTEZero)) prf
    where
        prf : (d : Nat) -> DividesNat (S (S Z)) d ->
            Either (d = 1) (d = (S (S Z)))
        prf d x = ?prf_rhs

d = (S Z) 或 d = (S (S Z)) 的情况非常简单：

prf : (d : Nat) -> DividesNat (S (S Z)) d ->
            Either (d = 1) (d = (S (S Z)))
        prf Z (Div (x ** pf)) = ?prf_rhs2_3
        prf (S Z) (Div (x ** pf)) = Left Refl
        prf (S (S Z)) (Div (x ** pf)) = Right Refl
        prf (S (S (S _))) (Div (x ** pf)) = ?rr_2

但我不知道如何证明 d = Z 或 d = (S (S (S _)))。我如何证明这些情况是不可能的？

【问题讨论】：

主要的做法是使用views：docs.idris-lang.org/en/latest/tutorial/views.html

标签： proof idris

【解决方案1】：

终于找到了解决办法：

prf2IsPrime : Prime (S (S Z))
prf2IsPrime = ConsPrime (LTESucc (LTESucc LTEZero)) prf
    where
        prfGT32 : (S (S (S a))) `GT` (S (S Z))
        prfGT32 = LTESucc (LTESucc (LTESucc LTEZero))

        prf : (d : Nat) -> DividesNat (S (S Z)) d -> Either (d = 1) (d = (S (S Z)))
        prf Z (Div (x ** pf)) = absurd (zeroIsNotDiv (x ** pf))
        prf (S Z) (Div (x ** pf)) = Left Refl
        prf (S (S Z)) (Div (x ** pf)) = Right Refl
        prf (S (S (S _))) (Div (k ** pf)) =
            absurd (gtIsNotDiv prfGT32 (k ** pf))

【讨论】：