通常，当您在定理证明器中进行案例分析时，很多案例归结为“不可能发生”。例如，如果您要证明有关整数的某些事实，您可能需要对整数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)依赖于布尔值的命题开始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，所以你现在可以证明你想要的任何目标。
这些策略基本上是构建证明项的机器。