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

Question

我试图证明，我认为什么是合理的定理:

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与 m在这里，这然后反射性地是正确的。我错过了什么？

Answer 1

不幸的是，您想在这里证明的定理实际上并不正确，因为 Idris 自然会在 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

我们不能为它 build 一个居民。

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

不过，上面的 pdxleif 解决方案对您的引理很有效。第一个参数上的 case 拆分对于在 minus 中获得模式匹配是必要的。上类。请记住，它在模式匹配中从上到下进行，并且第一个模式在第一个参数上有一个具体的构造函数，这意味着在知道该构造函数是否匹配之前无法进行归约。