[我不确定这是否适合堆栈溢出，但此处还有许多其他Coq问题，所以也许有人可以提供帮助。]
我正在从http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28（正好在Case的介绍下面）处理以下内容。请注意，我是一个完全的初学者，我在家工作 - 我不是学生。
Theorem andb_true_elim1 : forall b c : bool,
andb b c = true -> b = true.
Proof.
intros b c H.
destruct b.
Case "b = true".
reflexivity.
Case "b = false".
rewrite <- H. reflexivity.
Qed.
我正在看重写的内容：
Case := "b = false" : String.string
c : bool
H : andb false c = true
============================
false = true
然后应用rewrite <- H.：
Case := "b = false" : String.string
c : bool
H : andb false c = true
============================
false = andb false c
并且很清楚证据如何成功。
我可以看到在机械方式操纵符号方面我是如何得出证据的。没关系。但我对“意义”感到不安。特别是，如何在证明中间使用false = true？
我似乎正在与矛盾进行某种争论，但我不确定是什么。我觉得我一直盲目遵守规则，并以某种方式到达了我打字废话的地步。
我上面做了什么？
我希望这个问题很清楚。
通常，当您在定理证明器中进行案例分析时，很多案例归结为“不可能发生”。例如，如果您要证明关于整数的一些事实，您可能需要对整数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)的证明。
这听起来并不令人兴奋，但我们可以将它应用于我们想要的任何命题qazxsw poi。我们想要一个特别讨厌的人。
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是一个等于两个不同布尔值的语句。由于这些值不同，因此该陈述显然不可证明（在空的上下文中）。
考虑到你的证据：你到达目标是true = false的阶段，所以显然你无法证明它...但事实是你的背景（假设）也是矛盾的。例如，当您进行案例分析时，通常会发生这种情况，其中一个案例与您的其他假设相矛盾。
我意识到这已经过时了，但我想澄清Lambdageek的答案背后的一些直觉（如果有人发现这个）
我注意到关键点似乎是我们在每个点定义了一个具有不同值的函数false = true（即.F:bool->Prop和true => True）。然而，它可以很容易地从感应原则显示相等false => False直观的想法
eq_ind但这意味着假设forall A:Type, forall P:A->Prop, forall x y:A, (x=y) -> (P x = P y),
我们有true=false，但因为我们知道True=False，我们得到True。
这意味着我们使用的基本属性是定义False的能力，它由bool，F的递归原理给出：
bool_rect通过设置forall P:bool -> Type, P true -> P false -> (forall b:bool, P b)
，那么这是相同的
P (b:bool) := b=>Prop我们在哪里输入Prop -> Prop -> (forall b:bool, Prop),
和True以获得我们的功能False。