????在《集合的形式化》中，我們?cè)?Coq 的框架下定義了與集合相關(guān)的基本概念，形式化地證明了相關(guān)定理。在《實(shí)數(shù)的形式化》中，我們將在此基礎(chǔ)上形式化實(shí)數(shù)。

????實(shí)數(shù)作為數(shù)學(xué)的核心概念之一，涉及到的內(nèi)容非常豐富?！秾?shí)數(shù)的形式化》將圍繞高中數(shù)學(xué)展開，以實(shí)現(xiàn)對(duì)其的明確化為目的。

????不明確性是高中數(shù)學(xué)的顯著特點(diǎn)之一。由于沒有明確數(shù)學(xué)表達(dá)與操作的基本規(guī)則，高中數(shù)學(xué)在邏輯方面的表達(dá)往往是混亂的，依賴于感性認(rèn)知。例如，高中數(shù)學(xué)中常見的表達(dá) { x?| x?= f(k), k ∈ Z?} 是不合理的，正確表達(dá)應(yīng)為 { x?|???k ∈ Z,?x?= f(k)?}。另一個(gè)例子是：設(shè) P、Q 為命題，當(dāng) P 為真命題時(shí)有 Q => P（任意命題都可推出真命題），即 P 是 Q 的必要條件；當(dāng) P 為假命題時(shí)有 P => Q（假命題可推出任意命題），即 P 是 Q 的充分條件；因此 P 不可能既不是 Q 的充分條件也不是 Q 的必要條件，而這與我們的認(rèn)知相反。這是由于高中數(shù)學(xué)對(duì)充分條件與必要條件的解釋不明確。充分條件與必要條件事實(shí)上是數(shù)學(xué)外部的概念，我們習(xí)慣性地將?? x, P(x) -> Q(x) 表述為 P(x) 是 Q(x) 的充分條件，Q(x) 是 P(x) 的必要條件，而這種表述并不是嚴(yán)格的。通過形式化，這樣的問題可以得到解決。

????除此之外，形式化還可以將部分的做題方法明確化。一些方法實(shí)質(zhì)上是使用某些定理的體現(xiàn)，通過提出形式化的定理可以使方法更加明確。例如，通過明確“? x ∈ S, P(f(x)) 等價(jià)于 ? x ∈ f[S], P(x)”（f[S] 即 f 在 S 上的像），我們就能以等價(jià)變形的方式更清晰地處理取值范圍等問題，而無需被“換元法”困擾。

????需要注意的是，形式化也有其局限性。在推理與證明中，并不是所有的合理的數(shù)學(xué)操作都是簡(jiǎn)單地應(yīng)用形式化定理。例如：我們能在一個(gè)由加號(hào)連接的算式中任意地重排加數(shù)的運(yùn)算次序，這種操作是加法交換律和加法結(jié)合律的宏觀體現(xiàn)，本身難以用一個(gè)形式系統(tǒng)內(nèi)部的定理來表達(dá)；我們能通過“數(shù)形結(jié)合”直觀地做出判斷并得出正確的結(jié)果，但由于這本身是一個(gè)復(fù)雜的思維過程，很難被形式化。

????接下來，我們將以自然數(shù)為起點(diǎn)，開始實(shí)數(shù)的形式化之旅。

????自然數(shù)以歸納類型的形式定義于標(biāo)準(zhǔn)庫(kù)中：

????我們可以這樣理解：該定義聲明了 nat : Set（同時(shí)有 nat : Type）, O : nat, S : nat -> nat，其中 nat 表示自然數(shù)類型，O 表示零，S 表示后繼。通過 O 和 S，我們可以寫出一系列自然數(shù)：O, S O, S (S O), S (S (S O)), ... ，它們都有類型 nat，依次對(duì)應(yīng)零、一、二、三、... 。Coq 為它們提供了專門的數(shù)字記法：0, 1, 2, 3, ... ，這樣我們就能用我們熟悉的十進(jìn)制計(jì)數(shù)法來表示自然數(shù)。注意：這只是一種記法，并沒有定義與十進(jìn)制有關(guān)的數(shù)學(xué)對(duì)象，"10"?只是?S (S (S (S (S (S (S (S (S (S O))))))))) 的記法。

????由于自然數(shù)由歸納類型定義，match 表達(dá)式可以作用于自然數(shù)。以下代碼定義了 pred，即自然數(shù)的前驅(qū)。pred 0 可轉(zhuǎn)換為?match 0 with | 0 => 0 | S u => u end，進(jìn)而可轉(zhuǎn)換為 0；對(duì)于自然數(shù) n，pred (S n) 可轉(zhuǎn)換為?match S n?with | 0 => S n | S u => u end，進(jìn)而可轉(zhuǎn)換為 n。因此有 pred 0 = 0，pred 1 = 0，pred 2 = 1，pred 3 = 2，以此類推。

????對(duì)于自然數(shù) n，S n 可簡(jiǎn)寫為 n.+1，pred n 可簡(jiǎn)寫為 n.-1，而 n.+1.+1 可簡(jiǎn)寫為 n.+2，n.-1.-1 可簡(jiǎn)寫為 n.-2。注意這里的符號(hào)“.+1”“.-1”不是“+1”“-1”。

????利用 match 表達(dá)式，我們可以證明自然數(shù)的以下的基本性質(zhì)：

????forall a b : nat, a.+1 = b.+1 -> a = b：對(duì)于 a.+1 = b.+1，兩邊同時(shí)取前驅(qū)，得到 a.+1.-1 = b.+1.-1，而這根據(jù)前驅(qū)的定義和 match 表達(dá)式的規(guī)則可轉(zhuǎn)換為 a = b。

????forall a : nat, a.+1 <> 0：即已知 a.+1 = 0，要證 False。定義 f := fun n => match n with | 0 => True | p.+1 => False end。因?yàn)?f 0 可轉(zhuǎn)換為?True，所以可以得到?f 0。用?a.+1 = 0 改寫 f 0 得 f a.+1，而 f a.+1 可轉(zhuǎn)換為 False，這就在 a.+1 = 0 的語(yǔ)境下證明了 False。

????利用這兩個(gè)性質(zhì)，我們現(xiàn)在可以證明 3 <> 5：已知 3 = 5，由?forall a b?:?nat, a.+1 = b.+1 -> a =?b 得到 2 = 4，進(jìn)一步得到 1 = 3，0 = 2，由 0 = 2 可推出 2 = 0，然后通過?forall a : nat, a.+1 <> 0 推出 False。在實(shí)際證明時(shí)，像 3 <> 5 這樣的目標(biāo)可以被 Coq 自動(dòng)解決。

????自然數(shù)還有一個(gè)重要的基本性質(zhì)：forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P n.+1) -> forall n : nat, P n。這是自然數(shù)類型的歸納法則，在自然數(shù)被定義時(shí)由 Coq 自動(dòng)證明，產(chǎn)生的證明項(xiàng)為?nat_ind。使用?Print nat_ind. 指令，我們看到：

????其中，fix 表達(dá)式可以針對(duì)歸納類型給出遞歸定義的函數(shù)，但有一些限制（例如 (fix f (n : nat) : False := f n) 是語(yǔ)法錯(cuò)誤）來確保遞歸可以終止。match ... as ... return ... with ... end 是 match 表達(dá)式的完整形式。

????Coq 專門為應(yīng)用歸納類型的歸納法則提供了一個(gè)策略：elim。當(dāng)目標(biāo)為?forall n : nat, P n 時(shí)，該策略可將其轉(zhuǎn)化成兩個(gè)子目標(biāo)：P 0 和?forall n : nat, P n -> P n.+1。這就是數(shù)學(xué)歸納法，其實(shí)質(zhì)是應(yīng)用 nat_ind 的過程。

????到目前為止的內(nèi)容都是對(duì)標(biāo)準(zhǔn)庫(kù)中的自然數(shù)類型的介紹。接下來，我們將開始建立自然數(shù)的理論。

????與自然數(shù)的后繼與前驅(qū)相關(guān)的一些定理如下：

????由于自然數(shù)類型非空，因此可以定義 Nfapp，將一個(gè) A -> option nat 類型的函數(shù)轉(zhuǎn)換成 A -> nat 類型的函數(shù)。

????下面我們來定義自然數(shù)的加法。對(duì)于自然數(shù) 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 實(shí)現(xiàn)（其實(shí)質(zhì)是 fix 表達(dá)式）：

????根據(jù)加法的定義，給定兩個(gè)具體的自然數(shù)形式，我們可以計(jì)算它們的和。例如，表達(dá)式 1 + 1 可依次化簡(jiǎn)為：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 自動(dòng)證明。

????關(guān)于自然數(shù)的加法，有以下定理：（部分定理的證明需要通過歸納完成）

????自然數(shù)的序的定義如下：

????可以證明自然數(shù)的序的一些性質(zhì)：

????Nleq 具有自反性、反對(duì)稱性、傳遞性、完全性，因此它是全序。

????對(duì)于任意的自然數(shù)的集合 S，定義 [Nmax] S 表示 S 的最大值（類型為 option nat），Nmax S 表示 S 有最大值時(shí) [Nmax] S 對(duì)應(yīng)的自然數(shù)（類型為 nat），最小值同理。?我們可以證明：任意非空的自然數(shù)的集合都有最小值。在證明這個(gè)定理時(shí)，可以在已知?[Nmin] S = None 的語(yǔ)境下通過歸納證明?forall a b : nat, b <= a -> ~ b ∈ S（對(duì) a 歸納），進(jìn)而得到?S = ?。該定理表明：Nleq 不僅是全序，還是良序。

? ? 可以證明 Nleq良序關(guān)系 對(duì)應(yīng)的嚴(yán)格良序關(guān)系與 Nle 是一致的，這樣我們從良序本身的性質(zhì)出發(fā)，就能得到自然數(shù)的序的大量性質(zhì)。

????當(dāng)自然數(shù)的序與后繼、前驅(qū)、加法結(jié)合時(shí)，有以下定理：

????對(duì)于自然數(shù) a 和 b，定義 Nmax2 a b 表示 a 與?b 中的較大者，Nmin2 a b 表示 a 與?b 中的較小者。具體定義與相關(guān)定理如下：

????與自然數(shù)的集合的最大值與最小值有關(guān)的定理如下：

????下面我們來定義自然數(shù)的乘法。與加法類似，對(duì)于自然數(shù) 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 實(shí)現(xiàn)以上效果：

????關(guān)于自然數(shù)的乘法，有以下定理：

????自然數(shù)的乘方與加法和乘法類似。對(duì)于自然數(shù) 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。具體定義與相關(guān)定理如下：