我无法用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.我的理解是,伊德里斯应该只是更换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)))).看一下定义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起作用是必要的.请记住,它在模式匹配中从上到下进行,第一个模式在第一个参数上有一个具体的构造函数,这意味着在知道该构造函数是否匹配之前,还原不能进行.

Answer 2

只是玩弄交互式编辑,进行了案例分割和证明搜索,产生:

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

从减号的定义可以看出这一点,这就是为什么它只是简单的反映.当输入变量只是n时,它可能会徘徊,因为它可能有不同的行为,如果它是Z或其他什么？还是递归？