Coq中的"true = false"是什么意思？

Question

[我不确定这是否适合堆栈溢出,但此处还有许多其他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在证明中间出现？

我似乎正在与矛盾进行某种争论,但我不确定是什么.我觉得我一直盲目遵守规则,并以某种方式到达了我打字废话的地方.

我上面做了什么？

我希望这个问题很清楚.

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.

更新 正式,这是正在发生的事情.

回想一下,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,所以你现在可以证明你想要的任何目标.

策略基本上是构建证据术语的机器.

Answer 2

true = false是一个等于两个不同布尔值的语句.由于这些值不同,因此该陈述显然不可证明(在空的上下文中).

考虑到你的证据:你到达目标所在的阶段false = true,显然你无法证明它......但事实是你的背景(假设)也是矛盾的.例如,当您进行案例分析时,通常会发生这种情况,其中一个案例与您的其他假设相矛盾.