Agda 中的證明，從一到一點五

終於寫完了，還請各位聚聚多多包涵哈。原文在這裡Agda 中的證明，從一到一點五

上一篇我們說到了一個只有一步的證明，這一篇我們來看一個稍微複雜點的，組合命題的例子。 到目前為止，按理說所有的字元都還能正常顯示。

為什麼是一點五？看完你就知道啦。

前置知識

• 上一篇文章

以及，由於 Agda 語言的特殊性，本文將繼續使用 LaTeX 和代碼塊來共同展示代碼。 代碼塊唯一的作用在於便於複製，主要的呈現途徑為 LaTeX 。 （其實是因為我的手機顯示不出來很多字元，我又要自己看自己寫的東西）

關於複合命題

這裡修正一個概念。

前文說的 "條件" ，即前文一直強調的 "類型則命題" 中命題的最基本組成元素（好像 Wikipedia 上也稱之為 「命題變元」 ，反正我對這個名稱不負責，就是用來表示命題 中的 p 和 q 的東西）其實也是一種命題，而我之前稱為命題的東西則是 "複合命題" 。

下文將使用 "命題" 統稱他們。

介紹符號

都是初中數學裡面的，並且是只需要小學數學就可以看懂的符號。

與和或

我們知道，門電路裡面都有與門和或門，對應邏輯上的與和或。 與的符號是：

，或的符號是：

。 比如， 表示 p 和 q 都必須成立， r 才成立。 而 表示 p 和 q 中任意成立一個， r 就成立。

充要條件

我們知道，如果兩個條件 p q 能使 和 同時成立，我們稱他們互為充要條件，使用：

表示，比如 。

我們將在接下來的代碼裡面使用這些符號。

定義 GADT

首先定義 對應的 GADT ：

data _∧_ (P Q : Set) : Set wheren ∧-intro : P → Q → (P ∧ Q) n

這個命題是兩個其他命題的組合，它拿到兩個命題變成一個新命題。這也體現在 Agda 代碼中， 這個類型拿到兩個 Set 作為 類型 _∧_ 的參數， 返回一個新類型。 對應的類型構造器我們稱之為 。

有了這個類型，我們首先可以做一些很簡單的證明。

例〇：充要條件

比如，根據充要條件 的定義，我們可以把它表達成一個函數：

_?_ : (P Q : Set) → Setnp ? q = (p → q) ∧ (q → p) n

這裡我們在函數體（證明）裡面使用了 ，這樣的話 就是一個類型為 的東西。 因此，這實際上是一個 「命題組合」 ，有點 「高階函數」 感覺（順帶一提，這個名詞也是我為了便於理解自己編的，不知道有沒有其他人在用 （順帶一提，類型的階（順帶一提， Agda 中表示類型的階的類型正好是 Level ，中文意思就有階的意思， 因此這個說法可以說是很通用了） 在 dependent type 裡面已經變得很模糊了，因此這個 「高階」 的比喻是不太恰當的，這裡就拿 Haskell 之類的簡單語言的概念將就一下））。

再根據前文已經講過的：

只要有 這個函數成立，那麼就證明了 「 「 這個命題

這個函數的作用便變得很清晰了。 不理解沒關係，下面會用到這個東西，然後你或許能從它的應用看懂它的意義。

另外，看到沒有？函數體（證明）（下文不再進行這樣的強調，感覺很辣雞） 和定義 寫起來都是完全一樣的。 這裡可以體現一些 Agda 語言的優勢，就是因為 Unicode 語法的存在，它可以把代碼寫的很接近數學語言。

不過這並不代表 Agda 就只能用於學術，畢竟類型安全的社區和人氣火爆的社區結合起來才是最好的， Idris 都用強大的 ffi 和官方強推的 Control.ST 了，為什麼 Agda 不能寫成 imperative language 呢。

例一：定義

比如，在 成立的時候， p 和 q 分別成立（就是 的定義啦，很簡單的）。 用數學語言表達的話，就是（幾乎就是廢話）：

寫成代碼的話，就是（這裡關於這個證明講的比較略，是因為下文有個更詳細的講解， 已經完全覆蓋了這個證明所需要用到的知識，這個證明放在前面只是因為它本身很簡單，用 Haskell 知識即可理解， 如果讀者看不懂這個證明可以先看後面的，不過我覺得應該都看得懂，因為它太簡單了）：

proof? : ? {P Q} → (P ∧ Q) → Pnproof? (∧-intro p q) = pnnproof? : ? {P Q} → (P ∧ Q) → Qnproof? (∧-intro p q) = q n

例二(詳)：交換律

然後還有一個很簡單的例子——交換律（ Commutative Law ）。 用數學語言表達的話，就是（幾乎也是廢話）：

這個命題寫成 Agda 代碼，就是這樣的類型（我們稱之為 ）：

∧-comm : ? {P Q} → (P ∧ Q) ? (Q ∧ P) n

這裡我們就已經使用到之前的定義—— 啦。

如何證明它呢？

首先，我們的證明需要返回一個由 組合的兩個類型（命題）。 由於這個組合類型是一個由 組合而成的兩個類型，我們可以先把類型構造器寫上，然後兩個參數留白：

∧-comm = ∧-intro ? ?n

我們發現，在 p q 兩個變數可以互相交換的情況下， 這兩個參數的類型（複合命題）都是 。

因此，為了代碼復用，我們不妨把這兩部分提取出來，作為一個單獨的命題去證明它。 這個命題寫成 Agda 代碼，就是：

∧-comm′ : ? {P Q} → (P ∧ Q) → (Q ∧ P) n

它的第一個顯式參數（隱式參數就自動傳遞了，我們不用管）是 ，我們可以使用模式匹配將它拆開：

∧-comm′ (∧-intro p q) = ? n

然後我們把 p q 換個順序，重新使用類型構造器把它們組合起來：

∧-comm′ (∧-intro p q) = (∧-intro q p) n

然後再把這個命題填入剛才的 ∧?comm∧?comm 中：

∧-comm = ∧-intro ∧-comm′ ∧-comm′ n

然後我們就可以喊 Q.E.D. 啦。

例三：結合律

這個結合律（ Associative Law ）的例子其實已經不是例子了（因為我不想詳細講 （因為思路和交換律差不多）），我就只給出類型簽名就可以了。

∧-assoc : ? {P Q R} → (P ∧ (Q ∧ R)) ? ((P ∧ Q) ∧ R) n

為什麼我只給類型簽名呢？因為這個證明啊，

即得易見平凡，仿照上例顯然。留作習題答案略，讀者自證不難。

為什麼是一點五

因為原計劃是把 和 放在一起講的，但是我發現到目前為止的證明在模式匹配上都只有一個分支， 到了 就有兩個了，因此關於它和另外幾個有兩個分支的證明就單獨再開一篇吧 （其實是因為這篇寫長了，我寫博客會控制篇幅的） 。

我說完了。