在《集合的形式化》中，我们在 Coq 的框架下定义了与集合相关的基本概念，形式化地证明了相关定理。在《实数的形式化》中，我们将在此基础上形式化实数。

(资料图片仅供参考)

实数作为数学的核心概念之一，涉及到的内容非常丰富。《实数的形式化》将围绕高中数学展开，以实现对其的明确化为目的。

不明确性是高中数学的显著特点之一。由于没有明确数学表达与操作的基本规则，高中数学在逻辑方面的表达往往是混乱的，依赖于感性认知。例如，高中数学中常见的表达 { x | x = f(k), k ∈ Z } 是不合理的，正确表达应为 { x | ∃ k ∈ Z, x = f(k) }。另一个例子是：设 P、Q 为命题，当 P 为真命题时有 Q => P（任意命题都可推出真命题），即 P 是 Q 的必要条件；当 P 为假命题时有 P => Q（假命题可推出任意命题），即 P 是 Q 的充分条件；因此 P 不可能既不是 Q 的充分条件也不是 Q 的必要条件，而这与我们的认知相反。这是由于高中数学对充分条件与必要条件的解释不明确。充分条件与必要条件事实上是数学外部的概念，我们习惯性地将 ∀ x, P(x) -> Q(x) 表述为 P(x) 是 Q(x) 的充分条件，Q(x) 是 P(x) 的必要条件，而这种表述并不是严格的。通过形式化，这样的问题可以得到解决。

除此之外，形式化还可以将部分的做题方法明确化。一些方法实质上是使用某些定理的体现，通过提出形式化的定理可以使方法更加明确。例如，通过明确“∀ x ∈ S, P(f(x)) 等价于 ∀ x ∈ f[S], P(x)”（f[S] 即 f 在 S 上的像），我们就能以等价变形的方式更清晰地处理取值范围等问题，而无需被“换元法”困扰。

需要注意的是，形式化也有其局限性。在推理与证明中，并不是所有的合理的数学操作都是简单地应用形式化定理。例如：我们能在一个由加号连接的算式中任意地重排加数的运算次序，这种操作是加法交换律和加法结合律的宏观体现，本身难以用一个形式系统内部的定理来表达；我们能通过“数形结合”直观地做出判断并得出正确的结果，但由于这本身是一个复杂的思维过程，很难被形式化。

接下来，我们将以自然数为起点，开始实数的形式化之旅。

自然数以归纳类型的形式定义于标准库中：

我们可以这样理解：该定义声明了 nat : Set（同时有 nat : Type）, O : nat, S : nat -> nat，其中 nat 表示自然数类型，O 表示零，S 表示后继。通过 O 和 S，我们可以写出一系列自然数：O, S O, S (S O), S (S (S O)), ... ，它们都有类型 nat，依次对应零、一、二、三、... 。Coq 为它们提供了专门的数字记法：0, 1, 2, 3, ... ，这样我们就能用我们熟悉的十进制计数法来表示自然数。注意：这只是一种记法，并没有定义与十进制有关的数学对象，"10" 只是 S (S (S (S (S (S (S (S (S (S O))))))))) 的记法。

由于自然数由归纳类型定义，match 表达式可以作用于自然数。以下代码定义了 pred，即自然数的前驱。pred 0 可转换为 match 0 with | 0 => 0 | S u => u end，进而可转换为 0；对于自然数 n，pred (S n) 可转换为 match S n with | 0 => S n | S u => u end，进而可转换为 n。因此有 pred 0 = 0，pred 1 = 0，pred 2 = 1，pred 3 = 2，以此类推。

对于自然数 n，S n 可简写为 n.+1，pred n 可简写为 n.-1，而 n.+1.+1 可简写为 n.+2，n.-1.-1 可简写为 n.-2。注意这里的符号“.+1”“.-1”不是“+1”“-1”。

利用 match 表达式，我们可以证明自然数的以下的基本性质：

forall a b : nat, a.+1 = b.+1 -> a = b：对于 a.+1 = b.+1，两边同时取前驱，得到 a.+1.-1 = b.+1.-1，而这根据前驱的定义和 match 表达式的规则可转换为 a = b。

forall a : nat, a.+1 <> 0：即已知 a.+1 = 0，要证 False。定义 f := fun n => match n with | 0 => True | p.+1 => False end。因为 f 0 可转换为 True，所以可以得到 f 0。用 a.+1 = 0 改写 f 0 得 f a.+1，而 f a.+1 可转换为 False，这就在 a.+1 = 0 的语境下证明了 False。

利用这两个性质，我们现在可以证明 3 <> 5：已知 3 = 5，由 forall a b : nat, a.+1 = b.+1 -> a = b 得到 2 = 4，进一步得到 1 = 3，0 = 2，由 0 = 2 可推出 2 = 0，然后通过 forall a : nat, a.+1 <> 0 推出 False。在实际证明时，像 3 <> 5 这样的目标可以被 Coq 自动解决。

自然数还有一个重要的基本性质：forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P n.+1) -> forall n : nat, P n。这是自然数类型的归纳法则，在自然数被定义时由 Coq 自动证明，产生的证明项为 nat_ind。使用 Print nat_ind. 指令，我们看到：

其中，fix 表达式可以针对归纳类型给出递归定义的函数，但有一些限制（例如 (fix f (n : nat) : False := f n) 是语法错误）来确保递归可以终止。match ... as ... return ... with ... end 是 match 表达式的完整形式。

Coq 专门为应用归纳类型的归纳法则提供了一个策略：elim。当目标为 forall n : nat, P n 时，该策略可将其转化成两个子目标：P 0 和 forall n : nat, P n -> P n.+1。这就是数学归纳法，其实质是应用 nat_ind 的过程。

到目前为止的内容都是对标准库中的自然数类型的介绍。接下来，我们将开始建立自然数的理论。

与自然数的后继与前驱相关的一些定理如下：

由于自然数类型非空，因此可以定义 Nfapp，将一个 A -> option nat 类型的函数转换成 A -> nat 类型的函数。

下面我们来定义自然数的加法。对于自然数 a，我们希望 a + 0 = a，a + 1 = a.+1，a + 2 = a.+1.+1 = (a + 1).+1，a + 3 = a.+1.+1.+1 = (a + 2).+1，以此类推。这种效果可以通过 Fixpoint 实现（其实质是 fix 表达式）：

根据加法的定义，给定两个具体的自然数形式，我们可以计算它们的和。例如，表达式 1 + 1 可依次化简为：match 1 with | 0 => 1 | p.+1 => (1 + p).+1 end，(1 + 0).+1，(match 0 with | 0 => 1 | p.+1 => (1 + p).+1 end).+1，1.+1，而 1.+1 即为 2。像 1 + 1 = 2 这样的命题可以被 Coq 自动证明。

关于自然数的加法，有以下定理：（部分定理的证明需要通过归纳完成）

自然数的序的定义如下：

可以证明自然数的序的一些性质：

Nleq 具有自反性、反对称性、传递性、完全性，因此它是全序。

对于任意的自然数的集合 S，定义 [Nmax] S 表示 S 的最大值（类型为 option nat），Nmax S 表示 S 有最大值时 [Nmax] S 对应的自然数（类型为 nat），最小值同理。 我们可以证明：任意非空的自然数的集合都有最小值。在证明这个定理时，可以在已知 [Nmin] S = None 的语境下通过归纳证明 forall a b : nat, b <= a -> ~ b ∈ S（对 a 归纳），进而得到 S = ∅。该定理表明：Nleq 不仅是全序，还是良序。

可以证明 Nleq良序关系 对应的严格良序关系与 Nle 是一致的，这样我们从良序本身的性质出发，就能得到自然数的序的大量性质。

当自然数的序与后继、前驱、加法结合时，有以下定理：

对于自然数 a 和 b，定义 Nmax2 a b 表示 a 与 b 中的较大者，Nmin2 a b 表示 a 与 b 中的较小者。具体定义与相关定理如下：

与自然数的集合的最大值与最小值有关的定理如下：

下面我们来定义自然数的乘法。与加法类似，对于自然数 a，我们希望 a * 0 = 0，a * 1 = a = (a * 0) + a，a * 2 = a + a = (a * 1) + a，a * 3 = a + a + a = (a * 2) + a，以此类推。同样地，可通过 Fixpoint 实现以上效果：

关于自然数的乘法，有以下定理：

自然数的乘方与加法和乘法类似。对于自然数 a，我们希望 a ^ 0 = 1，a ^ 1 = a = (a ^ 0) * a，a ^ 2 = a * a = (a ^ 1) * a，a ^ 3 = a * a * a = (a ^ 2) * a。具体定义与相关定理如下：