布尔值证明，false = true

Question

我目前正在阅读 "Software foundations" 的第 5 章，但觉得有必要回到第一章来澄清一些事情。特别是有一个我没有完全消化的练习，其中要求我们使用 destruct 两次来证明布尔值的结果。这里是名称和其他详细信息已更改。

Inductive bool: Type :=
|true: bool
|false: bool.

Definition fb (b1:bool) (b2:bool) : bool :=
match b1, b2 with
| false, false => false
| _, _ => true
end.

Theorem th: forall a b: bool,
  fb a b = false -> b = false.
Proof.
intros [] [] H.
- rewrite <- H. reflexivity.
- reflexivity.
- rewrite <- H. reflexivity.
- reflexivity.
Qed.

在第一个 tick 时，上下文和目标都是无意义的：

H : fb true true = false
______________________________________(1/1)
true = false

第二次勾选假设是错误的。第三个滴答声与第一个滴答声是一样的废话。只有第四个刻度是合理的：

H : fb false false = false
______________________________________(1/1)
false = false

我知道根据重写规则，所有这些都有效。然而，我的印象是我们正在离开真理的窄路，进入虚假的荒野。更准确地说，据我所知，可以做出错误的假设来证明任何陈述，无论是对还是错。这里我们用它来证明false = true，好吧，为什么不呢，但还是让我觉得有些不舒服。我不会期望证明助理允许这样做。

详细一点

在一个典型的反证法中，我会随机选择一个假设，然后推导出目标，直到找到同义反复或矛盾为止。然后我会得出我的假设是对还是错的结论。

这里发生了什么，在情况 1 中（与情况 3 相同），Coq 从一个错误的假设开始：

H : fb true true = false

将其应用于矛盾的目标：

true = false

并将它们组合起来找到重言式。

这不是我所知道的推理方式。这回想起学生 'jokes'，从 0=1 开始，自然数上任何荒谬的结果都可以被证明。

跟进

所以今天早上在我上下班的路上，我在想我刚才写的东西。我现在相信案例 1 和案例 3 是正确的反证法。事实上 H 是错误的，我们用它来证明一个错误的目标。必须拒绝假设（a 和 b 的值）。可能让我感到困惑的是，使用 rewrite 我们正在从目标开始 "backward" 的一部分。

案例2我有点拿不定主意，上面写着：

H : fb true false = false
______________________________________(1/1)
false = false

基本上是false -> true，"principle of explosion"下的同义反复。我不认为可以在证明中直接使用它。

哦，我不确定我是否完全理解引擎盖下的内容，但对 Coq 的信任没有受到影响。要继续 return 到第 5 章。感谢大家的评论。

Answer 1

首先，感谢您提供 self-contained 代码。

我理解你在使用 rewrite 证明目标时的不安，因为你知道你真正应该做的是从假设中得出矛盾。但这并不会使推理不正确。确实，在这样的假设下你可以证明这个目标。

不过我也认为这并不能使证明脚本真正具有可读性。在您的示例中，您正在考虑所有可能的情况，而碰巧这四种情况中有三种是不可能的。当我们阅读您的证明时，我们看不到这一点。为了明确表示您处于不可能的情况，有一些有用的策略可以说明 "look, I am now going to prove a contradiction to rule out this case"。

其中之一是exfalso。它将用 False 替换当前目标（因为任何东西都可以从 False 派生，正如@ejgallego 在评论中提到的那样）。

第二个是absurd说"I am now going to prove some statement and its negation"（这基本上等同于证明False）。

对你的情况来说足够的第三个是 discriminate。它试图在假设中找到一个矛盾的等式，例如 true = false.

Theorem th: forall a b: bool,
  fb a b = false -> b = false.
Proof.
  intros [] [] H.
  - discriminate.
  - discriminate.
  - discriminate.
  - reflexivity.
Qed.

现在，如你所知，discriminate 和 reflexivity 都由 easy战术。因此，以下证明也将有效（但它没有显示正在发生的事情，因此超出了这个问题的范围）：

Theorem th: forall a b: bool,
  fb a b = false -> b = false.
Proof.
  intros [] [] H; easy.
Qed.

这是同一个证明的语法糖：

Theorem th: forall a b: bool,
  fb a b = false -> b = false.
Proof.
  now intros [] [] H.
Qed.

布尔值证明，false = true

Proof on booleans, false = true

coq