4

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

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，等等。

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

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

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

这里发生了什么 ？

4

1 回答 1

4

要了解为什么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 中的工作方式。
  • 在 return 注释上，我们在 Coq 上玩了一个“技巧”：我们说我们将返回False我们真正关心的情况（即n = 0），但说我们将在其他分支上返回其他内容。
  • 要对 进行类型检查match，每个分支都必须返回出现在return子句中的类型，但是在替换子句上绑定的变量的实际值in之后。
  • 在我们的例子中，等式类型只有一个构造函数，eq_refl。在这里，我们知道n = 1。用1 代替n我们的返回类型，我们得到True，所以我们必须返回一些 type 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的。另请注意，如果被声明为共归纳类型，则为natS n = n不是一个矛盾的假设，两者之间的区别只是在这种情况下我们无法对 进行归纳n。

于 2015-01-06T22:44:41.837 回答