16

我试图证明，在我看来是一个合理的定理：

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 应该只是替换minus m 0为mhere，然后这是反身成立的。我错过了什么？

4

4 回答 4

26

不幸的是，您要在这里证明的定理实际上并不正确，因为 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))))。查看的定义minus，第一个模式适用，因为第一个参数是Z。所以我们有：

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

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

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

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

S (S (S Z)) = Z

我们无法为其建造居民。

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

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

于 2014-05-08T07:49:52.427 回答
10

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

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

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

于 2014-05-08T07:06:13.793 回答
1

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

total minusZeroRight : (left : Nat) -> left - 0 = left
minusZeroRight Z        = refl
minusZeroRight (S left) = refl
于 2014-12-02T15:04:35.210 回答
1

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

----------                 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
于 2015-11-02T10:03:02.450 回答