一般来说，当你在一个定理证明器中做案例分析时，很多案例归结为“不可能发生”。例如，如果您证实了整数的一些事实，则可能需要对整数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