模式匹配证明（Pattern Matching Proofs）

本节我们将通过编写模式匹配定义，直接给出 plus_commutes 的证明。我们会大量使用交互式编辑功能，因为当机器能够给出中间值的类型并自动构造部分证明时，证明过程会更容易。下表总结了我们将用到的命令。文中直接提及命令时采用 Vim 版本，但这些命令在 Emacs 中也有对应。

命令（Command）	Vim 快捷键（Vim binding）	Emacs 快捷键（Emacs binding）	说明（Explanation）
检查类型（Check type）	\t	C-c C-t	显示光标下标识符或空洞的类型。
证明搜索（Proof search）	\s	C-c C-a	尝试通过简单的证明搜索解决光标下的空洞。
新建定义（Make new definition）	\a	C-c C-s	为光标下定义的类型添加模板定义。
新建引理（Make lemma）	\l	C-c C-e	添加一个顶层函数，其类型可解决光标下的空洞。
分割情况（Split cases）	\c	C-c C-c	为光标下变量的每种可能情况创建新的构造器模式。

创建定义（Creating a Definition）

首先，新建一个文件 pluscomm.idr，并包含如下类型声明：

plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n

要为该证明创建模板定义，在类型声明行按下 ``a``（或你所用编辑器的等效命令）。你应该会看到：

plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes n m = ?plus_commutes_rhs

要通过在 n 上进行归纳来证明这一点，正如我们在 归纳证明（Inductive Proofs） 节中概述的那样，我们首先对 n 进行情况分割（将光标放在定义中的 n 上，然后按 \c）。你应该会看到：

plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes Z m = ?plus_commutes_rhs_1
plus_commutes (S k) m = ?plus_commutes_rhs_2

检查新创建的空洞 plus_commutes_rhs_1 和 plus_commutes_rhs_2 的类型，可以看到 n 在每个相应情况下都被细化为了 Z 和 S k。将光标放在 plus_commutes_rhs_1 上按 \t 会显示：

   m : Nat
-------------------------------------
plus_commutes_rhs_1 : m = plus m Z

同样地，对于 plus_commutes_rhs_2：

  k : Nat
  m : Nat
--------------------------------------
plus_commutes_rhs_2 : (S (plus k m)) = (plus m (S k))

给这些空洞起稍微更有意义的名字是个好主意：

plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes Z m = ?plus_commutes_Z
plus_commutes (S k) m = ?plus_commutes_S

基例（Base Case）

我们可以通过将光标放在 plus_commutes_Z 上并按 \l 来交互式地为基例创建一个独立的引理。这将产生：

plus_commutes_Z : (m : Nat) -> m = plus m Z

plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes Z m = plus_commutes_Z m
plus_commutes (S k) m = ?plus_commutes_S

也就是说，空洞被填充为对顶层函数 plus_commutes_Z 的调用，该函数应用于作用域中的变量 m。

不幸的是，我们无法直接证明这个引理，因为 plus 是通过匹配其*第一个*参数来定义的，而这里 plus m Z 的*第二个参数*是一个具体值（实际上，等式的左侧已经从 plus Z m 归约而来）。同样，我们可以通过归纳法来证明这一点，这次是对 m 进行归纳。

首先，用 \d 创建一个模板定义：

plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z m = ?plus_commutes_Z_rhs

现在，用 \c 对 m 进行情况分割：

plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z Z = ?plus_commutes_Z_rhs_1
plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2

检查 plus_commutes_Z_rhs_1 的类型，可以看到如下内容，这是由 Refl 证明的：

--------------------------------------
plus_commutes_Z_rhs_1 : Z = Z

对于这种直接的证明，我们可以在光标位于 plus_commutes_Z_rhs_1 时按下 \s，自动生成证明。结果如下：

plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z Z = Refl
plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2

对于 plus_commutes_Z_rhs_2，我们就没那么幸运了：

   k : Nat
-------------------------------------
plus_commutes_Z_rhs_2 : S k = S (plus k Z)

根据归纳假设，我们应当知道 k = plus k Z，可以通过对 k 递归调用来获得这个归纳假设，如下所示：

plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z Z = Refl
plus_commutes_Z (S k)
   = let rec = plus_commutes_Z k in
         ?plus_commutes_Z_rhs_2

此时对于 plus_commutes_Z_rhs_2，我们可以看到：

   k : Nat
   rec : k = plus k Z
-------------------------------------
plus_commutes_Z_rhs_2 : S k = S (plus k Z)

我们已经知道 k = plus k Z，但如何利用这一点将目标变为 S k = S k 呢？

为此，Idris 在 prelude（前置库）中提供了 replace 函数：

Main> :t replace
Builtin.replace : (0 rule : x = y) -> p x -> p y

给定 x = y 的证明，以及对 x 成立的性质 p，我们就能得到该性质对 y 也成立的证明，因为我们知道 x 和 y 必然相等。注意 rule 上的 multiplicity（多重性）意味着它在运行时会被擦除。实际上，这个函数有时不太好用，因为隐式参数 p 一般难以通过统一推断出来，所以 Idris 提供了高级语法来自动计算性质并应用 replace：

rewrite prf in expr

如果我们有 prf : x = y，且 expr 的目标类型是关于 x 的某个性质，那么 rewrite ... in 语法会在目标类型中查找所有 x 并替换为 y。我们希望将 plus k Z 替换为 k，因此需要反向应用我们的 rec 规则，这可以通过 Prelude 中的 sym 实现。

Main> :t sym
Builtin.sym : (0 rule : x = y) -> y = x

具体到本例，我们可以这样写：

plus_commutes_Z (S k)
   = let rec = plus_commutes_Z k in
         rewrite sym rec in ?plus_commutes_Z_rhs_2

此时检查 plus_commutes_Z_rhs_2 的类型会得到：

   k : Nat
   rec : k = plus k Z
-------------------------------------
plus_commutes_Z_rhs_2 : S k = S k

应用 rewrite 规则 rec 后，目标类型中的 plus k Z 已被替换为 k。

我们可以使用证明搜索（\s）来完成证明，结果为：

plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z Z = Refl
plus_commutes_Z (S k)
   = let rec = plus_commutes_Z k in
         rewrite sym rec in Refl

至此，plus_commutes 的基例部分已完成。

归纳步骤（Inductive Step）

我们的主定理 plus_commutes 此时应处于如下状态：

plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes Z m = plus_commutes_Z m
plus_commutes (S k) m = ?plus_commutes_S

再次查看 plus_commutes_S 的类型，可以看到：

   k : Nat
   m : Nat
-------------------------------------
plus_commutes_S : S (plus k m) = plus m (S k)

方便的是，通过归纳我们可以直接得到 plus k m = plus m k，因此可以直接递归调用 plus_commutes 进行重写。手动添加如下：

plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes Z m = plus_commutes_Z
plus_commutes (S k) m = rewrite plus_commutes k m in ?plus_commutes_S

此时检查 plus_commutes_S 的类型会得到：

   k : Nat
   m : Nat
-------------------------------------
plus_commutes_S : S (plus m k) = plus m (S k)

好消息是 m 和 k 现在已经出现在正确的位置。但我们还需要证明右侧的后继符号 S 可以移到最前面。这个剩余的引理形式与 plus_commutes_Z 类似；我们先用 \l 新建一个顶层引理。结果如下：

plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)

同样地，我们用 \a 创建模板定义：

plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
plus_commutes_S k m = ?plus_commutes_S_rhs

与 plus_commutes_Z 类似，我们可以对 m 归纳来定义它，因为 plus 是按第一个参数模式匹配定义的。完整定义如下：

total
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
plus_commutes_S k Z = Refl
plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl

所有空洞现已解决。

total 注解表示我们要求最终函数通过全性检查（totality checker）；即它会在所有可能的良类型输入上终止。这对于证明来说很重要，因为它保证了证明在*所有*情况下都成立，而不仅仅是在定义良好的情况下。

现在 plus_commutes 已加上 total 注解，我们已经完成了自然数加法交换律的证明。