Coq中'true = false'是什么意思？

Question

[我不知道这是适当的堆栈溢出，但也有许多其他Coq的问题，这里，所以也许有人可以提供帮助。]

我通过从http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28以下（略低于其中案例介绍）工作。请注意，我是一个完整的初学者，我在家工作 - 我不是学生。

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？

看来我正在用矛盾进行某种争论，但我不确定是什么。我觉得我一直在盲从，遵守规则，不知何故到达了我无意中打字的地步。

我在做什么以上？

我希望问题很清楚。

Answer 1

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

这种策略基本上是构建证明术语的机器。

Answer 2

true = false是一个等同于两个不同布尔值的语句。由于这些值是不同的，这个陈述显然是不可证明的（在空白的情况下）。

考虑到你的证据：你到达目标是false = true的阶段，很明显你不能证明它......但问题是你的背景（假设）也是矛盾的。例如，当你进行案例分析时，这种情况经常发生，其中一种情况与你的其他假设相矛盾。

Answer 3

我意识到这是旧的，但我想澄清一些落后Lambdageek的回答直觉的（如果有人发现了这一点）

我注意到，关键似乎是，我们定义一个函数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。

这意思是，我们所使用的基本属性是定义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，让我们的功能F。