關於布爾值的證明，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.