補充介紹：證明模式

????在 Coq 中，證明一個命題 P 的方式是構(gòu)造出一個項 p，使得在當前語境下有 p : P。例如，在任意語境下欲證明命題 forall P : Prop, P -> P，可構(gòu)造項 fun (P : Prop) (p : P) => p（即 fun P : Prop => fun p : P => p）。該項輸入一個命題 P，輸入一個命題 P 的證明 p，輸出 p 本身，具有類型 forall P : Prop, P -> P。

????在 Coq 中建立理論時，可以使用?Definition 指令通過直接構(gòu)造證明項完成證明：

????然而上述做法的效率很低，即使證明的是一些很簡單的命題。針對這個問題，Coq 設計了證明模式。使用證明模式完成證明的示例如下：

????在 Coq 運行到 Proof?和 Qed 之間部分時，用戶會在窗口中看到當前的證明狀態(tài)。橫線之上的被稱為上下文，上下文與進入證明模式前的環(huán)境共同組成了當前的語境。橫線之下的被稱為目標，是接下來需要證明的。在下文中，一個證明狀態(tài)用“上下文 ? 目標”表示。

????與證明模式密切相關(guān)的一個概念是策略（tactic）。策略是證明模式中的一種指令，若執(zhí)行成功則可以改變當前的證明狀態(tài)。證明狀態(tài)從 A 變?yōu)?B，意味著：要完成 A 的證明，只需完成 B 的證明即可。證明狀態(tài)的轉(zhuǎn)變不一定有助于證明，有時反而會產(chǎn)生一個不可證的目標。在上面的例子中，初始的證明狀態(tài)為???forall P : Prop, P -> P；在 intros P p. 之后，證明狀態(tài)為 P : Prop; p : P ? P；在 exact p. 之后，證明狀態(tài)為??，即證明完成。使用策略完成證明本質(zhì)上仍然是在構(gòu)造證明項，不過證明項由?Coq 根據(jù)用戶使用的策略自動生成。

????Coq 中的策略繁多，由于作者的認知和能力有限，下面只介紹其中最基本的策略的最基本的用法。下文提到的部分策略不是在 Coq 啟動時自帶的，需要先加載 SSReflect。

????(1) exact x。若語境中有 p : P，而目標恰好為 P，則 exact p. 可以解決當前的目標。

????(2) move=> x。若目標為 forall a : A, P a，則 move=> x. 可以向上下文中加入 x : A，并將目標轉(zhuǎn)化為 P x。

????(3) move: x。若上下文中有 x : A 且 x 不出現(xiàn)于上下文的其他對象中，目標為 P，則 move: x. 可消去上下文中的 x : A, 并將目標轉(zhuǎn)化為 forall x : A, P。

????(4) apply: x。若語境中有 x : P -> Q，目標為 Q，則 apply: x. 可以將目標轉(zhuǎn)化為 P。

????(5) case。當目標為 forall x : A, P x 且 A 為歸納類型時，在一定條件下 case 策略可發(fā)揮作用，表現(xiàn)有：

????????- 將目標?P /\ Q -> R 轉(zhuǎn)化為目標?P -> Q -> R（即 P -> (Q -> R)）

????????- 將目標 P \/ Q -> R 轉(zhuǎn)化為兩個子目標 P -> R 和 Q -> R

????????- 將目標 (exists x : A, P x) -> Q 轉(zhuǎn)化為目標?forall x : A, P x -> Q

????(6) split。若目標為 P /\ Q，則 split. 可以將目標轉(zhuǎn)化為兩個子目標 P 和 Q。

????(7) left 和 right。若目標為 P \/ Q，則 left. 可以將目標轉(zhuǎn)化為 P，right. 可以將目標轉(zhuǎn)化為 Q。

????(8) exists x。若語境中有 x : A，目標為 exists a : A, P a，則 exists x. 可以將目標轉(zhuǎn)化為 P x。

????(9) rewrite x。當 x 在語境中且其類型為 a = b 或 forall ..., a = b 時，在一定條件下?rewrite 策略可發(fā)揮作用，可將目標中符合其模式的項按照 x 的規(guī)則替換。rewrite 策略的基本原理是 eq_ind 的應用，eq_ind 在相等（eq）被定義時作為其歸納法則由 Coq 自動證明。

????(10) by []。by []. 可以自動解決足夠簡單的目標，例如 True，x = x，P -> Q -> P 等。當上下文中有 False 時，by []. 也可以自動解決目標（根據(jù)?False_ind）。

????（接上一篇專欄第三節(jié)）在聲明完公理后，我們可以在這些公理的基礎上建立理論。首先需要完成的工作是對命題的研究。

????利用排中律，我們可以定義一個新的策略“排中”。當目標為 Q 時，排中 P. 可以將目標轉(zhuǎn)化為兩個子目標 P -> Q 和 ~ P -> Q。

????進一步地，我們可以定義新策略“反證”。當目標為 P 時，反證. 可以將目標轉(zhuǎn)化為 ~ P -> False。（注：若需證明的命題由 forall 開頭，則可在聲明時將變量提至“:”之前）

????命題外延公理可以導出更實用的?PropExt（注：定理的名稱在不重復的情況下可以任意選用，這里使用的名稱基于作者的個人偏好）。定義?Split?策略可實現(xiàn)將目標 P = Q 轉(zhuǎn)化為兩個子目標 P -> Q 和 Q -> P。

????函數(shù)外延公理可以導出更實用的 FunExt。

????使用 FunExt 易證以下定理。

????命題外延公理的一個重要推論是證明無關(guān)。由于作者的能力有限，下面的代碼引用了標準庫中的證明。

????以下定理均可通過 PropExt 證明。其中，firstorder 策略可以自動證明一些簡單的命題。

????接下來列舉的定理都可以使用?PropExt 證明，少數(shù)命題還需要用到排中律或反證法。從這里開始，命題的證明往往會省略。

????與全稱量詞和存在量詞有關(guān)的定理如下：

????唯一量詞定義于?init 標準庫中，它的相關(guān)定理列舉如下：

????對一階邏輯的研究在這里告一段落。現(xiàn)在，我們還有最后一條公理沒有使用：存在實例化。該公理將廣泛用于非構(gòu)造性定義：已知一個存在性命題形式的證明，我們可以得到一個符合的值。

????存在實例化有以下變種：

????利用存在實例化，我們可以定義一個命題的真值。真值的類型為 forall _ : Prop, bool，輸入一個命題，輸出一個 bool 類型的值，其中 bool 是由 true 和 false 組成的歸納類型。

????在真值的基礎上，我們可以定義 If ... then ... else ...。

????至此，形式化集合的準備工作已經(jīng)完成。在下一篇專欄中，我們將開始研究集合。