一般來說，當你在一個定理證明器中做案例分析時，很多案例歸結爲「不可能發生」。例如，如果您證實了整數的一些事實，則可能需要對整數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。
UPDATE形式上，這是發生了什麼事。
回想一下，Coq中的每個歸納定義都帶有歸納原理。以下是誘導原則平等類型和False命題（相對於bool類型的術語false）：
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)依賴於一個布爾b，和你有P(false)證明，那麼對於任何其他布爾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的證明，然後我們可以選擇一些布爾值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的證明，所以你現在可以證明你想要的任何目標。
這種策略基本上是構建證明術語的機器。
你可以嘗試使用['discriminate']（http://www.fing.edu.uy/inco/grupos/mf/man/Coq/node.1.2.8.html）。 （我看到這是一箇舊帖子） – guest