一个简单的 Coq 车祸课程：一阶逻辑¶
约 1926 个字 144 行代码 预计阅读时间 8 分钟
好久没更新，今天还是摸个简单的。这是前几天自己对着文档和各种教程摸出来的东西，随便做个总结。这里的几个例子都来源于 Andrej Bauer 的油管视频。
特别简单的一阶逻辑证明：Frobenius rule¶
我们先写出逻辑形式：
从直觉的解释上讲，证明这玩意并不困难。当然我们只要表明说，存在的这个 \(x\) 是一样的。下面我们用 Coq 写出这个形式：
Theorem frobenius (A : Set) (p : A -> Prop) (q : Prop):
(exists x : A, q /\ p x) <-> (q /\ exists x : A, p x).
这看上去其实和逻辑表达式没什么两样，是吧？为了表明我们下面要证明它，我们用 Proof. 作为下一行的内容，后面的东西就是真正的证明。
如果你偷懒，发现这东西在一阶逻辑内是很自然的，那么不妨直接使用 firstorder 的策略给出结果，整个形式就是：
Theorem frobenius (A : Set) (p : A -> Prop) (q : Prop):
(exists x : A, q /\ p x) <-> (q /\ exists x : A, p x).
Proof.
firstorder.
Qed.
特别完美，而且能过检查。但是作为车祸课程，不如展开写一下证明。
当我们看到一个当且仅当语句的时候，我们很自然地会想到先证明充分性再证明必要性。对于 Coq 来说也是如此。为了表明我们要将其分开来证，我们先使用 split 策略，得到的子目标如下：
2 subgoals
A : Set
p : A -> Prop
q : Prop
========================= (1 / 2)
(exists x : A, q /\ p x) -> q /\ (exists x : A, p x)
========================= (2 / 2)
q /\ (exists x : A, p x) -> (exists x : A, q /\ p x)
可以发现，它只把第一个子目标写清楚了，第二个子目标只是简单地标在下面。然后对于这种蕴含语句，我们的证明策略往往是将 \(\vDash (p \to q)\) 转变成 \(p \vDash q\) 来做。这就意味着，要把前面的东西引入成新假设。因此我们使用 intros 策略。
这时的子目标如下：
2 subgoals
A : Set
p : A -> Prop
q : Prop
H : exists x : A, q /\ p x
========================= (1 / 2)
q /\ (exists x : A, p x)
========================= (2 / 2)
q /\ (exists x : A, p x) -> (exists x : A, q /\ p x)
注意到，在横线上面的假设里面多了一个 H，横线下面的目标则发生了变化。
那么，怎么用这种假设呢？考虑平时的证明思路，往往是把存在命题做类似斯科伦化的想法，取出一个 x0 来满足这个东西。这里用的是 destruct H 来表达这个事情，把假设变成了：
对于与命题，当然我们也可以拆开看，因此我们再 destruct H 一次，这就把 H 变成了：
稍微回顾一下。现在，我们的证明到了这一步：
Theorem frobenius (A : Set) (p : A -> Prop) (q : Prop):
(exists x : A, q /\ p x) <-> (q /\ exists x : A, p x).
Proof.
split.
intros.
destruct H.
destruct H.
这样写看起来还是有点复杂了，所以事实上我们可以在 intros 里面干掉很多事情。先回滚证明的进度，然后把 intros 改成 intros [x0 H]，这时我们注意到假设变成了：
哈，这是不是意味着 intros 事实上可以完成 destruct 的部分工作？答案是肯定的，我们更进一步地把它改成 intros [x0 [H1 H2]]，就能直接得到：
于是我们用下面的代码完成了和上面一样的操作：
Theorem frobenius (A : Set) (p : A -> Prop) (q : Prop):
(exists x : A, q /\ p x) <-> (q /\ exists x : A, p x).
Proof.
split.
intros [x0 [H1 H2]].
再看一眼目标窗口，我们剩下的东西是：
2 subgoals
A : Set
p : A -> Prop
q : Prop
x0 : A
H1 : q
H2 : p x0
========================= (1 / 2)
q /\ (exists x : A, p x)
========================= (2 / 2)
q /\ (exists x : A, p x) -> (exists x : A, q /\ p x)
现在我们把假设拆解得差不多了，我们开始拆解目标。当然咯，目标是一个与公式，我们就想要把两个分开证明，接着用 split 策略，我们的第一个目标就只剩下一个 q 了，于是我们用 assumption 告诉 Coq 这个东西已经在假设里了，这就完成了第一个目标。
第二个目标要证明存在性，这就要我们告诉 Coq 这个存在的东西就是 x0。用 exists x0 来完成这一步。这时就只剩下 p x0 了，以 assumption 收尾。
当然，assumption 也可以用 exact H2 替代，这不过是显式地告诉 Coq 这东西到底是哪个假设。
好，我们已经摆平了第一个子目标。现在我们的代码大概长这样：
Theorem frobenius (A : Set) (p : A -> Prop) (q : Prop):
(exists x : A, q /\ p x) <-> (q /\ exists x : A, p x).
Proof.
split.
intros [x0 [H1 H2]].
split.
assumption.
exists x0.
assumption.
后半部分的证明没什么难度，或者说和前面类似，这里直接给出证明完之后的版本：
Theorem frobenius (A : Set) (p : A -> Prop) (q : Prop):
(exists x : A, q /\ p x) <-> (q /\ exists x : A, p x).
Proof.
split.
intros [x0 [H1 H2]].
split.
assumption.
exists x0.
assumption.
intros [H1 [x0 H2]].
exists x0.
split; assumption.
Qed.
我们用 Qed 来标识证明的结束。这里还需要说明的一点是 split; assumption. 这个句子，它事实上就是
的简写，分号表明对于分裂之后的两个子目标使用相同的策略。
对偶命题和排中律¶
把原来那个东西对偶化一下，我们得到的结果是：
看上去很显然，是……吗？不妨直接用 firstorder 策略做一下。嘿，您猜怎么着，挂了！但是，为什么？虽然 firstorder 并非万能，但是我们不妨思考一下按照常规的思路证明这个东西需要什么。首先，要么 \(q\) 成立，要么 \(q\) 不成立；如果……这里事实上已经出现了问题：我们引入了排中律。因此，这个命题只有在排中律的前提下才能得到证明。为了表明这一点，我们使用 Coq 写一个比较明白的版本：
Definition lem := forall p, p \/ ~p.
Definition dual_frobenius := forall (A : Set) (p : A -> Prop) (q : Prop),
(forall x : A, q \/ p x) <-> (q \/ forall x : A, p x).
Theorem lem_to_dual_frobenius : lem -> dual_frobenius.
Proof.
好，这样我们的证明就可以正式开始了。从此往下，我们将不再避免使用 firstorder 策略完成证明，一方面，验证一阶逻辑不是 Coq 的重点，另一方面，一阶逻辑的解算本身也已经相对成熟。
现在我们的子目标长这样：
第一步是将它展开，使用 unfold，得到的子目标变为：
(forall p : Prop, p \/ ~ p) ->
forall (A : Set) (p : A -> Prop) (q : Prop),
(forall x : A, q \/ p x) <-> (q \/ forall x : A, p x)
然后用 firstorder 整理一下，得到：
1 subgoal
H : forall p : Prop, p \/ ~ p
A : Set
p : A -> Prop
q : Prop
H0 : forall x : A, q \/ p x
========================= (1 / 1)
q \/ (forall x : A, p x)
然后我们要做的就是分类讨论：要么 q，要么 ~q，这由 H 的排中律保证。因此，将 H 应用于 q 然后 destruct，分别用 firstorder 简化得到结果。
最终的结果为：
Theorem lem_to_dual_frobenius : lem -> dual_frobenius.
Proof.
unfold lem, dual_frobenius.
firstorder.
destruct (H q); firstorder.
Qed.
很好玩的是，这条对偶的 Frobenius rule 和排中律正好是等价的。这里写出一个证明：
Theorem dual_frobenius_to_lem : dual_frobenius -> lem.
Proof.
unfold dual_frobenius, lem.
firstorder.
apply H.
firstorder.
Qed.
不妨观察一下每一步发生了什么。事实上，在第一次 firstorder 之后，它已经变成了下面的样子：
1 subgoal
H : forall (A : Set) (p : A -> Prop) (q : Prop),
(forall x : A, q \/ p x) <-> q \/ (forall x : A, p x)
p : Prop
========================= (1 / 1)
p \/ ~p
下一步我们要干嘛？我们想要做的事情是把 H 中的 p 取成恒假命题……稍等，为了避免混淆，我们不妨先把假设中的 p 重命名为 p0：
接下来的步骤在字面上看上去很简单，一个 apply H 就几乎完成了。事实上，这里用到了 tactic-unification 的策略，参见官方文档对 apply 的描述。根据指引，我们在 Theorem 之前加上 Set Debug "tactic-unification". 一行观察一下。
设置完之后，再转到 apply 这行之后，观察一下信息面板中的输出。非常长，不妨直接拉到最后第一个成功的地方：
[tactic-unification] Starting unification: ?M1406 \/
(forall x : ?M1404, ?M1405 x) ~=
p0 \/ ~ p0
[tactic-unification] ?M1406 \/ (forall x : ?M1404, ?M1405 x) ~= p0 \/ ~ p0
...
[tactic-unification] Leaving unification with success
这才是真正起到作用的部分。它事实上类似于对所有假设和目标做了模式匹配，这里成功的部分是对 H 的右半段做了匹配。它发现，取 q 为 p0，取 forall x : A, p x 为 ~ p0 的时候，正好能够完成匹配。在发现这点的能力上，它几乎要比人类还强。
于是，它发现，欲证目标，只需将如此应用之后的 H 的左半边证明，那就只剩下了 p0 -> p0 \/ False，用 firstorder 直接结束了证明。
挖个小坑，这些 ?M1404 之类的东西事实上是 de Bruijn index，后面大概会抽出一点时间讲讲这个东西的用处和实现。
到现在，虽然我们已经证明了一些一阶逻辑的结论，但诚如前面所说，Coq 的威力远不止于一阶逻辑。本文只是为初学者快速上手提供便利，若要深入学习，还需花费更多的精力。