[我不确定这是否适合堆栈溢出，但这里有许多其他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 .
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的证明，所以你现在可以证明任何你想证明的目标。
策略基本上是构建证明项的机制。
true = false是一个等于两个不同布尔值的语句。因为这些值是不同的，这个陈述显然是不可证明的(在空上下文中)。
考虑你的证明:你到达了目标是false = true的阶段，所以很明显你无法证明它…但问题是你的背景(假设)也是矛盾的。这种情况经常发生在你做案例分析时，其中一个案例与你的其他假设相矛盾。
我知道这是旧的，但我想澄清一些背后的直觉Lambdageek的答案(万一有人发现这个)
我注意到关键点似乎是我们在每个点定义一个具有不同值的函数F:bool->Prop(即。true => True和false => False)。然而，它可以很容易地从等式的归纳法原理eq_ind中显示出直观的想法(这实际上是"莱布尼茨"定义等式的方式)
forall P:bool -> Prop, forall x,y:bool, (x = y) -> (P x) -> (P y),
但这意味着从true=false和I:True，我们可以得出False。
F的能力，这是由bool的递归原则给出的，bool_rect:
forall P:bool -> Type, P true -> P false -> (forall b:bool, P b)
选择P := (fun b:bool => Prop)，则得到
(bool_rect P) : Prop -> Prop -> (bool -> Prop),
输入True和False，得到函数F。
如果我们把这些放在一起，我们会得到
(eq_ind true (bool_rect (fun b => Prop) True False) I false) : true = false -> False
值得指出的是，Coq采用eq_ind或bool_rect等归纳/递归原则作为公理，定义单位和布尔类型。
证明这一点的正常、人类的方法是说，由于在这种情况下假设不匹配，我们不需要证明续集。在Coq中，有一种表达方式。这是通过一个名为inversion的策略实现的。
下面是一个例子:
Theorem absurd_implies_absurd :
true = false -> 1 = 2.
Proof.
intros H.
inversion H.
Qed.
第一步设H为假设true = false，因此要证明的目标是1 = 2。
inversion H步骤将自动证明目标!正是我们想要的，魔法!
为了理解这个魔法，我们转向inversion含义的文档。
对于初学者(像我一样)来说，反转的官方文档是简洁而晦涩的，这里有一个更好的解释。在页面上搜索关键字反转，你会发现这个:
如果c和d是不同的构造函数，则假设H是矛盾的。也就是说，一个错误的假设潜入了上下文，这意味着任何目标都是可以证明的!在这种情况下，反转H将当前目标标记为已完成，并将其从目标堆栈中弹出。
这正好表达了我们想要的。唯一的问题是，这是在书的计划之前。当然，将true重写为false也可以。问题不在于它不起作用，而在于它不是我们想要的。