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

Question

我是 Coq 的新手，现在我一直在尝试通过一个简单的定理来理解 Coq "reasons"：

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 的理论允许自动简化少数 select 表达式，例如案例分析定义的表达式。例如，&&是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 的相等性以无穷多个自然数作为输入。更详细地讨论了这种差异。

如果需要，您可以使用蕴涵和等式的替代定义以纯可计算的方式陈述您的定理：

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 中通常更难使用。

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

Understanding Coq through a simple theorem proof

theorem-proving

coq