logic - `true = false` 在 Coq 中是什么意思？

Question

[我不确定这是否适合堆栈溢出，但这里还有许多其他 Coq 问题，所以也许有人可以提供帮助。]

我正在处理来自 http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28 的以下内容(就在 Case 介绍的下方)。请注意，我在这方面是一个完整的初学者，并且正在家里工作 - 我不是学生。

Theorem andb_true_elim1 : forall b c : bool,
  andb b c = true -> b = true.
Proof.
  intros b c H.
  destruct b.
  Case "b = true".
    reflexivity.
  Case "b = false".
    rewrite <- H. reflexivity.
Qed.

我正在研究重写的作用:

  Case := "b = false" : String.string
  c : bool
  H : andb false c = true
  ============================
   false = true

然后 rewrite <- H.被申请;被应用:

  Case := "b = false" : String.string
  c : bool
  H : andb false c = true
  ============================
   false = andb false c

很明显证明将如何成功。

我可以看到如何以机械方式操纵符号来获得证明。没关系。但我对“意义”感到不安。特别是我怎么能有 false = true在证明中间？

似乎我正在提出某种矛盾的论点，但我不确定是什么。我觉得我一直在盲目地遵守规则，不知何故到了我打字胡说八道的地步。

我在上面做什么？

我希望这个问题很清楚。

Answer 1

通常，当您在定理证明器中进行案例分析时，很多案例归结为“不可能发生”。例如，如果您要证明有关整数的一些事实，则可能需要对整数 i 是否进行案例分析。为正、零或负。但是，在您的上下文中，或者您的目标的某些部分，可能还有其他假设与其中一种情况相矛盾。例如，您可能从之前的断言中知道 i永远不能是消极的。

然而，Coq 并不那么聪明。因此，您仍然必须通过实际证明这两个相互矛盾的假设可以粘合在一起成为荒谬证明，从而证明您的定理的机制。

把它想象成一个计算机程序:

switch (k) {
  case X:
    /* do stuff */
    break;
  case Y:
    /* do other stuff */
    break;
  default:
    assert(false, "can't ever happen");
}

false = true目标是“永远不可能发生”。但是你不能只是在 Coq 中断言你的出路。你实际上必须写下一个证明术语。

所以上面，你要证明这个荒谬的目标 false = true .您唯一需要处理的就是假设 H: andb false c = true .稍等片刻，您就会发现这实际上是一个荒谬的假设(因为 andb false y 对于任何 y 都会减少为假，因此不可能为真)。所以你用唯一可以使用的东西(即 H )击中目标，你的新目标是 false = andb false c .

所以你应用一个荒谬的假设来试图实现一个荒谬的目标。瞧，你最终得到了一些你可以通过反身性来展示的东西。 Qed。

更新 正式地，这就是正在发生的事情。

回想一下 Coq 中的每个归纳定义都带有一个归纳原则。以下是等式归纳原则的类型和 False命题(与 false 类型的术语 bool 相反):

Check eq_ind.
eq_ind
  : forall (A : Type) (x : A) (P : A -> Prop),
    P x -> forall y : A, x = y -> P y
Check False_ind.
False_ind
 : forall P : Prop, False -> P

归纳原理为 False说如果你给我证明 False ，我可以给你任何命题的证明 P .
eq的归纳原理更复杂。让我们认为它仅限于 bool .尤其是 false .它说:

Check eq_ind false.
eq_ind false
 : forall P : bool -> Prop, P false -> forall y : bool, false = y -> P y

所以如果你从一些命题开始 P(b)这取决于 bool 值 b ，并且您有 P(false) 的证明，然后对于任何其他 bool 值 y等于 false ，你有 P(y)的证明.

这听起来并不十分令人兴奋，但我们可以将其应用于任何命题 P我们想要的。我们想要一个特别讨厌的。

Check eq_ind false (fun b : bool => if b then False else True).
eq_ind false (fun b : bool => if b then False else True)
 : (fun b : bool => if b then False else True) false ->
   forall y : bool,
   false = y -> (fun b : bool => if b then False else True) y

稍微简化一下，这就是 True -> forall y : bool, false = y -> (if y then False else True) .

所以这需要 True的证明然后是一些 bool 值 y我们可以选择。所以让我们这样做。

Check eq_ind false (fun b : bool => if b then False else True) I true.
eq_ind false (fun b : bool => if b then False else True) I true
 : false = true -> (fun b : bool => if b then False else True) true

我们在这里: false = true -> False .

结合我们对 False的归纳原理的了解，我们有:如果你给我证明 false = true ，我可以证明任何命题。

所以回到 andb_true_elim1 .我们有一个假设 H即 false = true .我们想证明某种目标。正如我在上面所展示的，存在一个证明项可以转换 false = true 的证明。变成你想要的任何证据。所以特别是 H是 false = true的证明，因此您现在可以证明您想要的任何目标。

策略基本上是构建证明项的机器。