证明自然（n）为零

Question

我正在尝试学习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 : False = True

[尝试导航我认为应该（并且有一天将会是）简单的事物导致uninhabited，Void，absurd和impossible。我没有什么可以消除歧义的。

也许这些是关键-但我无法解密！

Answer 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
还有另一种方法或方法可以将这些定义为不会陷入陷阱吗？