通过一个简单的定理证明来理解 Coq

Question

我对 Coq 很陌生，现在我一直在试图用一个简单的定理来理解 Coq 如何“推理”：

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.

我认为证明只是：

Proof.
  intros b c.
  destruct c.
    - destruct b.
     + reflexivity.
     + reflexivity.
    - destruct b.
     + reflexivity.
     + reflexivity.
  Qed.

但它失败了：

In environtment
H: true && false = true
Unable to unify "true" with "false"

子目标失败是第三个reflexivity，其中c 是false，b 是true：

1 subgoal
______________________________________(1/1)
true && false = true -> false = true

这是为什么呢？不就相当于一个暗示吗？

true && (false = true) -> (false = true)
true && false -> false
false -> false
true

Answer 1

这个证明存在一些问题。首先，你误解了 Coq 想要什么；实际目标如下：

((true && false) = true) -> (false = true)

这不后跟自反性，因为这个公式的结论，false = true，是两个语法不同的表达式之间的相等。

其次，Coq 不会以您描述的方式简化运算符 -> 和 =。 Coq 的理论允许在一些选择表达式中自动简化，例如由案例分析定义的那些。例如，&& 是 andb 函数的语法糖，在标准库中定义如下：

Definition andb b c :=
  if b then c else false.

当 Coq 看到像 false && true 这样的表达式时，它会将其扩展为等价的 if false then true else false，进而简化为 else 分支 true。您可以通过在有问题的分支上调用simpl 策略来测试它。

另一方面，-> 和 = 运算符的定义不同：第一个是逻辑中的原语，而另一个是所谓的归纳命题。这些都不能在 Coq 中自动简化，因为它们表达了通常不可计算的概念：例如，我们可以使用 = 来表达两个函数 f 和 g 的相等性，这两个函数采用无限多个自然数作为输入。 This question 更详细地讨论了这种差异。

如果你愿意，你可以用一种纯粹可计算的方式陈述你的定理，并使用蕴含和相等的替代定义：

Definition negb b := if b then false else true.

Definition eqb b c := if b then c else negb c.

Definition implb b c := if b then c else true.

Lemma test : forall b c, (implb (eqb (andb b c) true) (eqb c true))
                         = true.
Proof. intros [] []; reflexivity. Qed.

然而，像这样的语句在 Coq 中通常更难使用。