时间戳

首页 > 解决方案 > 证明自然 (n) 为零

proof - 证明自然 (n) 为零

问题描述

我正在尝试学习 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和. 我无法消除任何歧义。 absurdimpossible

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

标签： proofidris

解决方案

我正在回答，因为我认为我认为上述证明没有正确说明。我添加了 asserted 的语句n = Zero，它允许isZero n = Bool.True具有意义。继承n = Zeroasprf并允许我声明absurd prfas在某些情况下isZero n = Bool.True不成立。nSuccessorNat

  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

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

推荐阅读