集合的形式化 #2 逻辑

补充介绍：证明模式

    在 Coq 中，证明一个命题 P 的方式是构造出一个项 p，使得在当前语境下有 p : P。例如，在任意语境下欲证明命题 forall P : Prop, P -> P，可构造项 fun (P : Prop) (p : P) => p（即 fun P : Prop => fun p : P => p）。该项输入一个命题 P，输入一个命题 P 的证明 p，输出 p 本身，具有类型 forall P : Prop, P -> P。

    在 Coq 中建立理论时，可以使用 Definition 指令通过直接构造证明项完成证明：

    然而上述做法的效率很低，即使证明的是一些很简单的命题。针对这个问题，Coq 设计了证明模式。使用证明模式完成证明的示例如下：

    在 Coq 运行到 Proof 和 Qed 之间部分时，用户会在窗口中看到当前的证明状态。横线之上的被称为上下文，上下文与进入证明模式前的环境共同组成了当前的语境。横线之下的被称为目标，是接下来需要证明的。在下文中，一个证明状态用“上下文 ⊢ 目标”表示。

    与证明模式密切相关的一个概念是策略（tactic）。策略是证明模式中的一种指令，若执行成功则可以改变当前的证明状态。证明状态从 A 变为 B，意味着：要完成 A 的证明，只需完成 B 的证明即可。证明状态的转变不一定有助于证明，有时反而会产生一个不可证的目标。在上面的例子中，初始的证明状态为 ⊢ forall P : Prop, P -> P；在 intros P p. 之后，证明状态为 P : Prop; p : P ⊢ P；在 exact p. 之后，证明状态为 ⊢，即证明完成。使用策略完成证明本质上仍然是在构造证明项，不过证明项由 Coq 根据用户使用的策略自动生成。

    Coq 中的策略繁多，由于作者的认知和能力有限，下面只介绍其中最基本的策略的最基本的用法。下文提到的部分策略不是在 Coq 启动时自带的，需要先加载 SSReflect。

    (1) exact x。若语境中有 p : P，而目标恰好为 P，则 exact p. 可以解决当前的目标。

    (2) move=> x。若目标为 forall a : A, P a，则 move=> x. 可以向上下文中加入 x : A，并将目标转化为 P x。

    (3) move: x。若上下文中有 x : A 且 x 不出现于上下文的其他对象中，目标为 P，则 move: x. 可消去上下文中的 x : A, 并将目标转化为 forall x : A, P。

    (4) apply: x。若语境中有 x : P -> Q，目标为 Q，则 apply: x. 可以将目标转化为 P。

    (5) case。当目标为 forall x : A, P x 且 A 为归纳类型时，在一定条件下 case 策略可发挥作用，表现有：

        - 将目标 P /\ Q -> R 转化为目标 P -> Q -> R（即 P -> (Q -> R)）

        - 将目标 P \/ Q -> R 转化为两个子目标 P -> R 和 Q -> R

        - 将目标 (exists x : A, P x) -> Q 转化为目标 forall x : A, P x -> Q

    (6) split。若目标为 P /\ Q，则 split. 可以将目标转化为两个子目标 P 和 Q。

    (7) left 和 right。若目标为 P \/ Q，则 left. 可以将目标转化为 P，right. 可以将目标转化为 Q。

    (8) exists x。若语境中有 x : A，目标为 exists a : A, P a，则 exists x. 可以将目标转化为 P x。

    (9) rewrite x。当 x 在语境中且其类型为 a = b 或 forall ..., a = b 时，在一定条件下 rewrite 策略可发挥作用，可将目标中符合其模式的项按照 x 的规则替换。rewrite 策略的基本原理是 eq_ind 的应用，eq_ind 在相等（eq）被定义时作为其归纳法则由 Coq 自动证明。

    (10) by []。by []. 可以自动解决足够简单的目标，例如 True，x = x，P -> Q -> P 等。当上下文中有 False 时，by []. 也可以自动解决目标（根据 False_ind）。

    （接上一篇专栏第三节）在声明完公理后，我们可以在这些公理的基础上建立理论。首先需要完成的工作是对命题的研究。

    利用排中律，我们可以定义一个新的策略“排中”。当目标为 Q 时，排中 P. 可以将目标转化为两个子目标 P -> Q 和 ~ P -> Q。

    进一步地，我们可以定义新策略“反证”。当目标为 P 时，反证. 可以将目标转化为 ~ P -> False。（注：若需证明的命题由 forall 开头，则可在声明时将变量提至“:”之前）

    命题外延公理可以导出更实用的 PropExt（注：定理的名称在不重复的情况下可以任意选用，这里使用的名称基于作者的个人偏好）。定义 Split 策略可实现将目标 P = Q 转化为两个子目标 P -> Q 和 Q -> P。

    函数外延公理可以导出更实用的 FunExt。

    使用 FunExt 易证以下定理。

    命题外延公理的一个重要推论是证明无关。由于作者的能力有限，下面的代码引用了标准库中的证明。

    以下定理均可通过 PropExt 证明。其中，firstorder 策略可以自动证明一些简单的命题。

    接下来列举的定理都可以使用 PropExt 证明，少数命题还需要用到排中律或反证法。从这里开始，命题的证明往往会省略。

    与全称量词和存在量词有关的定理如下：

    唯一量词定义于 init 标准库中，它的相关定理列举如下：

    对一阶逻辑的研究在这里告一段落。现在，我们还有最后一条公理没有使用：存在实例化。该公理将广泛用于非构造性定义：已知一个存在性命题形式的证明，我们可以得到一个符合的值。

    存在实例化有以下变种：

    利用存在实例化，我们可以定义一个命题的真值。真值的类型为 forall _ : Prop, bool，输入一个命题，输出一个 bool 类型的值，其中 bool 是由 true 和 false 组成的归纳类型。

    在真值的基础上，我们可以定义 If ... then ... else ...。

    至此，形式化集合的准备工作已经完成。在下一篇专栏中，我们将开始研究集合。