关于布尔值的证明，false = true

Question

我目前在“软件基础”的第5章，但觉得有必要回到第一章来澄清一些事情。特别是有一个我没有完全消化的练习，我们被要求使用两次破坏来证明布尔运算的结果。这里改变了名称和其他细节。

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. 

当在第一跳，背景和目标都是废话：

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

二打勾的假设是错误的。第三个勾号与第一个勾号相同。只有第四个勾号是合理的：

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

我明白，通过重写规则，所有这些东西都可以工作。然而，我的印象是，我们正在放弃虚伪旷野的狭隘道路。更确切地说，和AFAIK，一个虚假的假设可以用来证明任何陈述，是真是假。在这里，我们用它来证明false = true，为什么不呢，但这仍然让我感觉有点不舒服。我不会期望证明助理允许这样做。

阐述了一下

在用反证法一个典型的证据，我会选一个假设随机的，并从中获得了目标，直到我发现无论是重言式或矛盾。然后我会得出结论，我的假设是真的还是假的。

H : fb true true = false 

它适用于这是一个矛盾的目标：

true = false 

这里会发生什么事，在案件1（同为案例3），勒柯克从一个假设，那是假的开始

并结合他们找到重言式。

这不是我知道的推理方法。这回顾了从0 = 1开始的学生“笑话”，可以证明对自然数的任何荒谬结果。

跟进

所以今天早上我上班时我在想什么，我刚刚上面写的。我现在认为案例1和案例3是矛盾的恰当证据。事实上，H是假的，我们用它来证明一个假的目标。假设（a和b的值）必须被拒绝。可能使我困惑的是，使用重写，我们正在从目标开始“落后”的一部分。

我有点拿不定主意的情况下2，其内容为：

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

这基本上是false -> true，在“爆炸原理”同义反复。我不认为这可以直接用于证明。

唉，不知道我完全理解了底层是什么，但对Coq的信任没有改变。要继续并回到第5章。谢谢大家的意见。

Answer 1

首先，感谢您提供一个自包含的代码。

我知道你使用rewrite来证明你的目标不安，因为你知道你应该做的就是从假设中推导一个矛盾。尽管如此，这并不能使推理不正确。诚然，在这样的假设下，你可以证明这一目标。

但是我也认为这并不能使证明脚本真正可读。在你的例子中，你正在考虑所有可能的情况，并且发生这四个中的三个是不可能的。当我们阅读你的证据时，我们看不到这些。要说清楚你是不可能的情况下，有几种策略可以说“看，我现在要证明排除这种情况的矛盾”。其中之一是exfalso。它将用False取代当前目标（因为可以从False得到任何东西，正如@ejgallego在评论中提到的那样）。

第二个是absurd来说“我现在要证明一些陈述和否定”（这基本上相当于证明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.