一、序言

1. 形式化

????形式化的本質(zhì)是明確規(guī)則。我們希望明確表達(dá)、定義、證明的規(guī)則：表達(dá)一個(gè)數(shù)學(xué)對(duì)象時(shí)，應(yīng)遵循什么語法規(guī)則？如何定義一個(gè)數(shù)學(xué)對(duì)象？證明時(shí)有哪些推理規(guī)則？為了解決這些問題，我們需要從零開始，建立一個(gè)形式化的系統(tǒng)。

????與形式化對(duì)立的是使用自然語言。我們已經(jīng)習(xí)慣于使用“為定值”“是動(dòng)點(diǎn)”“取最大值”“的取值范圍”等詞匯，但事實(shí)上它們是不精確的?？紤]以下表述：

????(1) 已知 x = -1，求 x 的絕對(duì)值

????(2) 已知 x = -1，x2 =1，求 x 的絕對(duì)值

????(3) 已知 x + 1?< 0，求 x 的取值范圍

????(4) 已知 x + 1 < 0, x2 < 2，求 x 的取值范圍

????同樣是“已知 ... ，求 x 的 ...”的形式，“絕對(duì)值”和“取值范圍”的表現(xiàn)是不同的。對(duì)“絕對(duì)值”而言，若從已知中的一個(gè)條件即可推出絕對(duì)值，那么就不需要再看其他條件；對(duì)“取值范圍”而言，需要綜合所有的條件進(jìn)行判斷。而所謂的“綜合所有的條件進(jìn)行判斷”具體又遵循什么規(guī)則呢？是通過不斷地推理限制 x 的范圍嗎？當(dāng)條件更復(fù)雜時(shí)，我們又如何才能確信這個(gè)范圍已經(jīng)不能再繼續(xù)縮小了？總之，我們可能并不能說清楚其中的規(guī)則。這樣的問題經(jīng)常困擾著廣大學(xué)生，而形式化是解決此類問題的方案之一。

????形式化并不意味著像下面這樣“強(qiáng)行塞符號(hào)，讓讀者看不懂”：

????事實(shí)上，形式化可以實(shí)現(xiàn)在嚴(yán)謹(jǐn)性的基礎(chǔ)上保證一定的可讀性：

????此外，形式化也并不意味著完全拋棄自然語言。在確?？梢噪S時(shí)翻譯成形式化表述的前提下，我們可以使用自然語言進(jìn)行描述。在交流證明思路等需要?jiǎng)?chuàng)造性的情境下，也可以使用不太嚴(yán)謹(jǐn)?shù)淖匀徽Z言。

2. ZFC

??? 一種經(jīng)典的形式化方案是 ZFC。ZFC 基于一階邏輯，在公理體系中初始地聲明了以下用于組成公式的符號(hào)：??，并給出了一系列推理規(guī)則、公理、公理模式。然而，ZFC 有其局限性：很多操作并不符合 ZFC 給定的這些規(guī)則。

????一個(gè)很常見的例子是“公式的等價(jià)替換”。設(shè)公式??中含有公式??，若在??所在環(huán)境下可證??，那么就有? （將??中的??替換為??）。例如，根據(jù)??，即可得到??。這種操作不符合 ZFC 給定的規(guī)則，也無法對(duì)應(yīng)于一個(gè)定理。

????一般對(duì)此的解釋是：ZFC 所基于的一階邏輯并不是“元語言”（最底層的形式系統(tǒng)）。ZFC 實(shí)際上是元語言中的一個(gè)研究對(duì)象（形式系統(tǒng)作為數(shù)學(xué)對(duì)象）。在底層的元語言中，我們可以斷定：這種操作是合理的。然而，對(duì)作者而言，這樣的解釋并不令人滿意。如果 ZFC 之下還有另一個(gè)元語言，那么這個(gè)元語言究竟是什么？既然有這樣一個(gè)元語言，為什么不直接在其上建立理論，而非要定義一個(gè)形式系統(tǒng)再在其上建立理論？（這里不考慮對(duì)數(shù)理邏輯的單獨(dú)研究）

3. Coq

????最終，作者選擇的形式化方案是 Coq。Coq 實(shí)際上是一個(gè)編程語言，但它并不會(huì)生成可執(zhí)行程序，而是會(huì)逐行地對(duì)輸入的代碼輸出反饋。通過使用 Coq，用戶可以在給定的規(guī)則內(nèi)建立數(shù)學(xué)理論，從而實(shí)現(xiàn)形式化。

????這個(gè)專欄系列將介紹一種【使用 Coq，從標(biāo)準(zhǔn)庫(kù)中的?Init 和 ssreflect 出發(fā)，形式化與集合相關(guān)的基本概念、定理】的方案。由于作者從未系統(tǒng)學(xué)習(xí)過 Coq，如有錯(cuò)誤或不當(dāng)之處，敬請(qǐng)諒解。

二、Coq 簡(jiǎn)介

Coq 的官方手冊(cè)：https://coq.inria.fr/distrib/current/refman/

以下內(nèi)容是一個(gè)簡(jiǎn)化的、粗略的、可能不準(zhǔn)確的、基于作者理解的介紹。

1. 項(xiàng)

????項(xiàng)是 Coq 中的基本概念之一。項(xiàng)可通過以下規(guī)則形成：

????(1) Type 是一個(gè)項(xiàng)（粗體字表示這里的 Type 不是一個(gè)指代詞，而是字符串"Type"）

????(2) Prop 是一個(gè)項(xiàng)

????(3) 所有的變量（identifier）都是項(xiàng)，其中變量（不精確地說）是不引起混淆的字符串，例如 a，b，c，x，y，z，fxy，pqrs'，x_0 等等

????(4) 對(duì)于任意的變量 x，項(xiàng) T, U，forall x : T, U 是一個(gè)項(xiàng)（forall 就是全稱量詞）

????(5)?對(duì)于任意的變量 x，項(xiàng) T, u，fun?x?:?T?=>?u?是一個(gè)項(xiàng)（表示函數(shù)建構(gòu)式）

????(6) 對(duì)于任意的項(xiàng) t, u，t u 是一個(gè)項(xiàng)（t 和 u 之間有一個(gè)空格，表示函數(shù)應(yīng)用）

????(7) match 表達(dá)式也可以用于形成項(xiàng)（較為復(fù)雜，這里不介紹）

2. 語境

????每個(gè)語境可理解為一個(gè)（有限的）集合，可能包含了以下種類的信息：

????(1) 對(duì)于任意的項(xiàng) t, T，t : T 可用于組成語境

????(2) 對(duì)于任意的項(xiàng) c, t, T, c := t : T 可用于組成語境

????(3) 與歸納類型相關(guān)的一些信息也可以用于形成語境（較為復(fù)雜，這里不介紹）

????對(duì)于一個(gè)語境，Coq 給定了一些規(guī)則來判斷這個(gè)語境是否是?well-formed 的。在一個(gè)?well-formed 的語境中，有規(guī)則可以判斷項(xiàng) t, T 是否滿足【t 有類型 T】（可寫作 t : T），這些用于判斷類型關(guān)系的規(guī)則被稱為類型規(guī)則（typing rules）。還有一些規(guī)則可以判斷項(xiàng) t, T 是否滿足【t 可轉(zhuǎn)換為 T】，這些用于判斷轉(zhuǎn)換關(guān)系的規(guī)則被稱為轉(zhuǎn)換規(guī)則（conversion rules）。例如，設(shè)語境中有 P :?forall _?: nat, Prop，則 forall x : nat, P x 可轉(zhuǎn)換為 forall y : nat, P y。類型規(guī)則和轉(zhuǎn)換規(guī)則一起可被視為 Coq 的推理規(guī)則。

3. 定義與證明

????在 Coq 中建立理論時(shí)，定義新的項(xiàng)可通過使用 Definition 指令、聲明歸納類型（較為復(fù)雜，這里不介紹）以及其他方式實(shí)現(xiàn)。在使用 Definition?指令時(shí)，我們需要寫出一個(gè)項(xiàng) t，使得在當(dāng)前語境下 t 有某個(gè)類型 T，從而完成指令：?Definition c : T := t。?定義完 c 之后，c := t : T 就被加入到語境中。

????如果一個(gè)項(xiàng) P 在某語境下有類型 Prop，那么在這個(gè)語境下 P 就被稱為命題。如果有項(xiàng) p 滿足 p 在某語境下有類型 P，并且 P 有類型 Prop，那么在這個(gè)語境下 P 就被視為被證明了，而 p 則被稱為 P 的一個(gè)證明。Coq 設(shè)計(jì)了專門的證明模式方便用戶使用策略（tactics）更高效地構(gòu)造證明。

4.?init 標(biāo)準(zhǔn)庫(kù)

????init 標(biāo)準(zhǔn)庫(kù)中定義了基本的邏輯對(duì)象與數(shù)據(jù)結(jié)構(gòu)，規(guī)定了一些符號(hào)記法。

????(1) P -> Q 是 forall _ : P, Q 的記法，當(dāng) P,?Q 為命題時(shí)表示蘊(yùn)含關(guān)系

????(2) True : Prop 表示真命題（通過歸納類型定義）

????(3) False : Prop 表示假命題（通過歸納類型定義）

????(4) not : Prop -> Prop 表示否定，輸入一個(gè)命題 P，輸出一個(gè)命題 ~ P （定義為 ~ P := P -> False）

? ? (5) and : Prop -> Prop -> Prop 表示合取，輸入兩個(gè)命題 P,?Q，輸出一個(gè)命題 P /\ Q（通過歸納類型定義）

????(6) or : Prop -> Prop -> Prop 表示析取，輸入兩個(gè)命題 P, Q, 輸出一個(gè)命題 P \/ Q（通過歸納類型定義）

????(7) iff : Prop -> Prop -> Prop 表示當(dāng)且僅當(dāng)，輸入兩個(gè)命題 P, Q，輸出一個(gè)命題 P <-> Q（定義為 P <-> Q := (P -> Q) /\ (Q -> P)）

????(8) ex :?forall A : Type, (A -> Prop) -> Prop 表示存在量詞，ex A P 記作 exists x : A, P x（通過歸納類型定義）

? ? (9) eq : forall A : Type, A -> A -> Prop 表示相等，eq A x y?記作 x =?y（通過歸納類型定義）

????(10) nat : Type 表示自然數(shù)，其中 O?: nat 表示零，S : nat -> nat 表示后繼（通過歸納類型定義）

三、公理

現(xiàn)在我們正式開始建立理論。

????我們添加了四條公理。

????(1) 函數(shù)外延。該公理說明：任意兩個(gè)同類型的函數(shù)，若函數(shù)值總是相等的，那么這兩個(gè)函數(shù)相等。該命題在原始語境下不可判定（既無法證明該命題，也無法證明該命題的否定）。

????(2) 命題外延。該公理說明：等價(jià)的命題相等。由于相等可以進(jìn)行“替換”（根據(jù)相等的歸納類型定義），這條公理部分地解決了序言中提到的“公式的等價(jià)替換”問題。該命題在原始語境下不可判定。

????(3) 排中律。該公理允許我們?cè)谧C明時(shí)對(duì) P 和 ~ P 兩種情況進(jìn)行分類討論。該命題在原始語境下不可判定，但這并不意味著在添加排中律公理之前一個(gè)命題可能有“非真非假”的第三種情況。在原始語境下，我們可以證明 forall P : Prop,?~ ~ (P \/ ~ P)，但不能證明 forall P : Prop, ~ ~ P -> P。

????(4)?存在實(shí)例化。該公理在效果上允許我們解構(gòu)一個(gè) exists x : A, P x 的證明，得到一個(gè) a : A 和一個(gè) P a 的證明。這為我們之后的一些操作提供了便利，在后續(xù)專欄會(huì)提到。事實(shí)上，該公理蘊(yùn)含了選擇公理。