归纳证明（Inductive Proofs）

在正式用 Idris 证明 plus_commutes 之前，让我们先回顾一下自然数某些性质证明的整体结构。请记住，自然数是递归定义的，如下所示：

data Nat : Type where
     Z : Nat
     S : Nat -> Nat

一个*全函数（total function）*在自然数上必须终止，并覆盖所有可能的输入。Idris 通过检查所有输入是否被覆盖，以及所有递归调用是否作用于*结构上更小*的值，来判断函数的全性（totality）。回顾一下 plus 的定义：

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

该函数是全的，因为它覆盖了所有可能的输入（第一个参数只能是 Z 或某个 S k，第二个参数 m 覆盖了所有可能的 Nat），并且在递归调用中，k 结构上小于 S k，因此在任意递归调用序列中，第一个参数最终都会到达基例 Z。

在某种意义上，这类似于数学中的归纳法证明（这并非巧合！）。对于自然数 x 的某个性质 P，我们可以通过以下方式证明 P 对所有 x 都成立：

P 对零成立（基例）。
假设 P 对 k 成立，则可以证明 P 对 S k 也成立（归纳步骤）。

在 plus 的例子中，我们要证明的性质其实很简单（对于所有自然数 x，都存在一个 Nat，它不一定与 x 有任何关系）。不过，这依然采用了基例和归纳步骤的形式。在基例中，我们展示当 n = Z 时，plus n m 会得到一个 Nat；在归纳步骤中，我们展示当 n = S k 且已知 plus k m 可以归纳得到一个 Nat 时，plus n m 也能得到一个 Nat。我们甚至可以写一个函数来抽象所有类似的归纳定义：

nat_induction :
    (prop : Nat -> Type) ->                -- Property to show
    (prop Z) ->                            -- Base case
    ((k : Nat) -> prop k -> prop (S k)) -> -- Inductive step
    (x : Nat) ->                           -- Show for all x
    prop x
nat_induction prop p_Z p_S Z = p_Z
nat_induction prop p_Z p_S (S k) = p_S k (nat_induction prop p_Z p_S k)

利用 nat_induction，我们可以实现一个等价的 plus 归纳版本：

plus_ind : Nat -> Nat -> Nat
plus_ind n m
   = nat_induction (\x => Nat)
                   m                      -- Base case, plus_ind Z m
                   (\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m
                                          -- where k_rec = plus_ind k m
                   n

要证明对所有自然数 n 和 m 都有 plus n m = plus m n，我们同样可以使用归纳法。可以固定 m，对 n 归纳，也可以反过来。我们可以勾勒出证明的轮廓：对 n 归纳时，有：

性质 prop 为 \x => plus x m = plus m x。
证明 prop 在基例和归纳步骤中都成立：
- 基例：prop Z，即
  
  plus Z m = plus m Z，可化简为
  
  根据 plus 的定义，m = plus m Z。
- 归纳步骤：归纳假设 prop k 对某个固定的 k 成立，即
  
  plus k m = plus m k``（归纳假设）。在此基础上，证明 ``prop (S k)，即
  
  plus (S k) m = plus m (S k)，可化简为
  
  S (plus k m) = plus m (S k)。根据归纳假设，我们可以将其重写为
  
  S (plus m k) = plus m (S k)。

因此，要完成证明，我们还需要证明对所有自然数 m 都有 m = plus m Z，以及对所有自然数 m 和 k 都有 S (plus m k) = plus m (S k)。这两者同样可以用归纳法证明，这次是对 m 归纳。

现在，我们已经准备好在 Idris 中正式证明 plus 的交换律了。