证明自然 (n) 为零答案

【问题标题】：Proof a Natural (n) is Zero证明自然 (n) 为零
【发布时间】：2019-10-06 21:37:03
【问题描述】：

我正在努力学习 idris 范式，但仍在苦苦挣扎。这里我有一个函数 isZero，它接受一些自然的 Nat 并返回 True 或 False。

我的问题在于非自反案例。

namespace Numbers

  data Nat : Type where
    Zero : Numbers.Nat
    Successor : Numbers.Nat -> Numbers.Nat

  isZero: Numbers.Nat -> Prelude.Bool.Bool
  isZero Zero = True
  isZero _ = False

  isNotZero: Numbers.Nat -> Prelude.Bool.Bool
  isNotZero Zero = False
  isNotZero _ = True

  proofNIsZero : (n : Numbers.Nat) -> isZero n = Bool.True
  proofNIsZero Zero = Refl
  proofNIsZero (Successor _) = ?rhs

很明显，任何 Nat 的某些继任者不可能是零。但我的斗争是在证明。 ?rhs 孔的类型是

--------------------------------------
rhs : False = True

试图导航我认为应该（并且有一天会）简单的东西导致uninhabited、Void、absurd 和impossible。我无法消除任何歧义。

也许这些就是钥匙——但我无法破译！

【问题讨论】：

标签： proof idris

【解决方案1】：

我正在回答，因为我想我已经意识到，也许上面的证明没有正确陈述。我添加了断言n = Zero 的语句，它允许isZero n = Bool.True 有意义。 n = Zero 继承为 prf 并允许我将 absurd prf 声明为 isZero n = Bool.True 如果 n 是 Successor 到某些 Nat，则不能成立。

  Uninhabited (Successor _ = Zero) where
    uninhabited Refl impossible

  proofNIsZero : (n : Numbers.Nat) -> n = Zero -> isZero n = Bool.True
  proofNIsZero Zero prf = Refl
  proofNIsZero (Successor _) prf = absurd prf

是否有另一种方法或方式来定义这些以不陷入陷阱？

【讨论】：