coq - 覆盖一个明显不正确的假设并不能证明是错误的

Question

我试图证明一个微不足道的引理，这是对我在另一点发现自己的情况的再现。

Lemma Sn_neq_n: forall n, S n <> n.

证明看起来很简单:

Proof. unfold not. intros.

现在我的目标状态显示:

n : nat
H : S n = n
===================
 False

很明显 S n无法与 n 统一，所以我应该能够颠倒这个假设:

inversion H.

但是，我现在的状态不是解决目标，而是显示:

n : nat
H : S n = n
H0 : S n = n
===================
 False    

嗯？我现在只是在一个无限循环中。我可以 inversion H0我只是得到一个 H1 ， ETC。

我能够通过归纳证明引理:

unfold not. intros. induction n.
Case "n = 0". inversion H.
Case "n > 0". inversion H. apply IHn. apply H1.

但这有点傻，因为可以想象，首先允许自反相等的统一算法不应该能够统一 S n。与 n .

这里发生了什么 ？

Answer 1

看看为什么inversion自己无法解决这个目标，我们需要更详细地了解它在做什么。

当您反转(共)归纳类型的假设时，Coq 所做的，粗略地说，就是仅使用模式匹配从中提取尽可能多的信息(请记住，Coq 策略总是在后台生成证明项)。因此，当证明 1 <> 0通过反转，Coq 将产生一个如下所示的术语:

Definition one_neq_zero (p : 1 = 0) : False :=
  match p in _ = n return match n with
                          | 0 => False
                          | _ => True
                          end
  with
  | eq_refl => I (* "I" is the only constructor of the True proposition *)
  end.

return match 上的注释声明对于此工作至关重要。这里发生的事情基本上如下:

我们需要匹配相等证明 p使用它。

为了能够在对其证明进行模式匹配时讨论该等式的右侧，我们必须在匹配中添加一个返回注释。

不幸的是，这个返回注解不能直接提到 0。相反，它需要为通用 n 工作。 ，即使我们知道那个元素实际上是 0。这只是因为 Coq 中模式匹配的工作方式。

在返回注解上，我们在 Coq 上玩了一个“把戏”:我们说我们将返回 False在我们真正关心的情况下(即 n = 0 )，但说我们将在其他分支上返回其他内容。

键入检查 match ，每个分支都必须返回 return 上出现的类型。子句，但在替换了绑定(bind)在 in 上的变量的实际值之后条款。

在我们的例子中，相等类型只有一个构造函数，eq_refl。 .在这里，我们知道 n = 1 .用 1 代替 n在我们的返回类型中，我们获得 True , 所以我们必须返回 True 类型的东西，我们这样做。

最后，由于 p 的右侧为 0，Coq 理解整个匹配的类型为 False ，所以整个定义类型检查。

最后一步之所以有效，是因为 0 是一个构造函数，所以 Coq 能够简化返回类型的匹配，以实现我们返回的是正确的东西。这是尝试反转 S n = n 时失败的原因: 自 n是一个变量，整个匹配不能被简化。

我们可以尝试翻转等式并反转 n = S n相反，这样 Coq 就可以稍微简化返回类型。不幸的是，这也不起作用，并且出于类似的原因。例如，如果您尝试使用 in _ = m return match m with 0 => True | _ => False end 注释匹配。 ，在 eq_refl 内我们必须返回 match n with 0 => True | _ => False end 类型的东西，我们不能。

最后我要提一下，Coq 内部的统一算法不能像你提到的那样“消极地”使用，因为该理论只定义了可证明的事物，而不定义哪些事物是可反驳的。特别是，当我们证明一个否定命题时，例如 S n <> n ，类型检查器总是测试某些统一问题是否有解决方案，而不是测试它们是否没有解决方案。例如，假设 n = m是一件非常好的事情，并且不会导致任何矛盾，即使 n和 m是不可统一的。另请注意，如果 nat被声明为共归纳类型， S n = n不是一个矛盾的假设，两者之间的区别只是在这种情况下我们无法对 n 进行归纳。 .