我无法用 Idris 证明 (n - 0) = n答案

【问题标题】：I can't prove (n - 0) = n with Idris我无法用 Idris 证明 (n - 0) = n
【发布时间】：2014-05-07 13:21:28
【问题描述】：

我试图证明，在我看来什么是合理的定理：

theorem1 : (n : Nat) -> (m : Nat) -> (n + (m - n)) = m

归纳证明到了我需要证明这一点的地步：

lemma1 : (n : Nat) -> (n - 0) = n

当我尝试使用交互式证明者来证明它（为了简单起见，引理）时会发生这种情况：

----------                 Goal:                  ----------
{hole0} : (n : Nat) -> minus n 0 = n

> intros
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
{hole1} : minus n 0 = n

> trivial
Can't unify
        n = n
with
        minus n 0 = n

Specifically:
        Can't unify
                n
        with
                minus n 0

我觉得我一定错过了关于减号的定义，所以我在源代码中查找了它：

||| Subtract natural numbers. If the second number is larger than the first, return 0.
total minus : Nat -> Nat -> Nat
minus Z        right     = Z
minus left     Z         = left
minus (S left) (S right) = minus left right

我需要的定义就在那里！ minus left Z = left。我的理解是，Idris 应该在这里用m 替换minus m 0，然后这是反身成立的。我错过了什么？

【问题讨论】：

Idris 是一种依赖类型的编程语言，由于 Curry-Howard 同构，它使证明和程序成为同义词。我需要在代码中证明这个定理，以便我的函数可以很好地键入（我把函数省略了，因为解释它会占用不必要的空间）。出于这个原因，Idris 附带了一个交互式证明器。所以问题是关于如何使用编程语言 Idris 的问题，而不是关于数学本身的问题。
对不起，如果这很明显，不熟悉该语言，但查看该语言的一些示例 - 这远不清楚。 0 和 Z 是否总是被视为同义词，还是需要一些东西才能使其工作？
数字字面量是多态重载的，就像在 Haskell 中一样。 Nat 是Num 类的成员，其中一个函数是fromInteger。和fromInteger 0 = Z。（我认为在语言本身和终端中还有一些 Nat 的特殊外壳。）简而言之，我认为这不是问题，尽管我还不能完全确定。
顺便说一句：我不认为这是可以证明的。当然，这在数学上是有道理的，但减号在 Naturals 上的总体定义并不明确。一个失败的情况：如果 m 为零，并且 n 不为零 - 零减去任何东西都被定义为零。这样一来，您就只能尝试证明 (S k) + 0 = 0。也许我们需要更好地定义对 Nats 的“减”运算，否则请停止尝试将它们用于数学证明。

标签： proof idris

【解决方案1】：

不幸的是，您想在这里证明的定理实际上并不正确，因为 Idris naturals 在 0 处截断减法。theorem1 的反例是 n=3, m=0。让我们逐步进行评估：

首先，我们替换：

3 + (0 - 3) = 0

接下来，我们将语法脱糖到底层 Num 实例，并放入被调用的实际函数：

plus (S (S (S Z))) (minus Z (S (S (S Z))))) = Z

Idris 是一种严格的按值调用的语言，因此我们首先评估函数的参数。因此，我们减少了表达式minus Z (S (S (S Z))))。查看the definition of minus，第一个模式适用，因为第一个参数是Z。所以我们有：

plus (S (S (S Z))) Z = Z

plus 在其第一个参数上是递归的，因此下一步的求值产生：

S (plus (S (S Z)) Z) = Z

我们继续这种方式，直到plus 获得Z 作为它的第一个参数，此时它返回它的第二个参数Z，产生类型：

S (S (S Z)) = Z

我们无法为其建造居民。

很抱歉，如果上述内容看起来有点迂腐和低级，但在使用依赖类型时考虑特定的缩减步骤非常重要。这是您在类型内部“免费”获得的计算，因此最好安排它以产生方便的结果。

pdxleif 的上述解决方案非常适合您的引理。要使minus 中的模式匹配起作用，必须对第一个参数进行大小写拆分。请记住，它在模式匹配中从上到下进行，并且第一个模式在第一个参数上有一个具体的构造函数，这意味着在知道该构造函数是否匹配之前，归约不能继续。

【讨论】：

【解决方案2】：

只是玩弄交互式编辑，进行案例拆分和证明搜索，结果：

lemma1 : (n : Nat) -> (n - 0) = n
lemma1 Z = refl
lemma1 (S k) = refl

这从减号的定义中很明显，这就是为什么它只是 refl。也许当输入 var 只是 n 时它会犹豫不决，因为如果它是 Z 或其他东西，它可能会有不同的行为？还是递归？

【讨论】：

【解决方案3】：

以防万一，Idris Prelude 中已经定义了很多算术引理，就像你的一样：

total minusZeroRight : (left : Nat) -> left - 0 = left
minusZeroRight Z        = refl
minusZeroRight (S left) = refl

【讨论】：

【解决方案4】：

为了完整起见（策略语言已被弃用以支持详细说明），我将补充一点，在策略语言中证明您的引理的方法是调用induction n。然后，您可以使用trivial 显示每种情况（在归纳情况下使用intros 之后）。

----------                 Goal:                  ----------
{hole0} : (n : Nat) -> minus n 0 = n
-lemma1> intros
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
{hole1} : minus n 0 = n
-lemma1> induction n
----------              Other goals:              ----------
elim_S0,{hole1},{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
elim_Z0 : minus 0 0 = 0
-lemma1> trivial
----------              Other goals:              ----------
{hole1},{hole0}
----------              Assumptions:              ----------
 n : Nat
----------                 Goal:                  ----------
elim_S0 : (n__0 : Nat) ->
          (minus n__0 0 = n__0) -> minus (S n__0) 0 = S n__0
-lemma1> intros
----------              Other goals:              ----------
{hole8},elim_S0,{hole1},{hole0}
----------              Assumptions:              ----------
 n : Nat
 n__0 : Nat
 ihn__0 : minus n__0 0 = n__0
----------                 Goal:                  ----------
{hole9} : minus (S n__0) 0 = S n__0
-lemma1> trivial
lemma1: No more goals.
-lemma1> qed
Proof completed!
lemma1 = proof
  intros
  induction n
  trivial
  intros
  trivial

【讨论】：