2.3 自然數上之歸納證明

上一節中我們定出了函數 exp。如果定義正確，exp b n 算的應是 $b^n$. 例如，我們知道 $b^{m+n} = b^m \times b^n$. 我們定出的函數 exp 是否真有此性質呢？

我們試著證明定理2.1 。數學歸納法是我們目前唯一的工具， 而要使用它，第一個問題是：該用 b, m, 或 n 的哪一個來做歸納呢（意即把哪一個拆解）？

觀察定理2.1 中待證明式的等號兩邊，並參照 exp, (+), 與 (*)的定義。 等號左手邊的 exp b (m + n) 之中，化簡 exp b 前得知道 m + n 究竟是 Zero 還是 Suc k。 而根據 (+) 的定義，化簡 m + n 前需知道 m 究竟是 Zero 還是 Suc k. 再看右手邊，根據 (*) 的定義，要化簡 exp b m * exp b n 得先化簡 exp b m, 而後者也得知道 m 是什麼。對兩邊的分析都指向：我們應針對 m 做歸納！

策略擬定後，我們便試試看吧！

   exp b (Zero + n)
 ===    {- (+) 之定義 -}
   exp b n
 ===    {- 因 1 * k = k -}
   1 *: exp b n
 ===    {- exp 之定義 -}
   exp b Zero *: exp b n 

   exp b ((Suc m) + n)
 ===    {- (+) 之定義 -}
   exp b (Suc (m + n))
 ===    {- exp 之定義 -}
   b *: exp b (m + n)
 ===    {- 歸納假設 -}
   b *: (exp b m *: exp b n)
 ===    {- (*) 之結合律 -}
   (b *: exp b m) *: exp b n
 ===    {- exp 之定義 -}
   exp b (Suc m) *: exp b n 

對這個證明，讀者是否有所懷疑？最大的疑問可能在「假設 exp b (m + n) = exp b m * exp b n 成立」這句上。這不就是我們要證明的性質嗎？在證明中假設它成立，似乎是用該性質自己在證明自己。這是可以的嗎？

為清楚說明，我們回顧一下第2.1 節中的數學歸納法（並把區域識別字改為 k 以避免混淆）：

  (∀ k . P k)  <==   P Zero ⋀ (∀ k . P (Suc k) <== P k) 

證明2.1 欲證的是 exp b (m + n) = exp b m * exp b n，並在 m 上做歸納。 更精確地說，就是選用了下述的 P: (註4) 在程式推導圈子中，(<=>) 常用來代表「只用在真假值上、且滿足結合律的等號」。本書中使用 (<=>) 以和 (=) 做區分。

P m <=> (exp b (m + n) = exp b m * exp b n) 

在證明中改變的是 m，而 b 與 n 是固定的。數學歸納法可證明 (∀ m . P m), 展開後正是 (∀ m . exp b (m + n) = exp b m * exp b n). 而根據數學歸納法，我們需提供 P Zero 與 (∀ m . P (Suc m) <== P m) 的證明。

證明2.1 中「{\bf 情況} m := Zero」的部分，就是 P Zero 的證明。 而「{\bf 情況} m := Suc m」則是 (∀ m . P (Suc m) <== P m) 的證明。 「假設 exp b (m + n) = exp b m * exp b n 成立」指的是假設 P m 成立，我們在此前提之下試圖證明 P (Suc m). 因此，證明 2.1 並沒有「用該性質自己證明自己」。 我們是以一個比較小的結果（P m）證明稍大一點的結果（P (Suc m)）。 就如同我們寫歸納程式時，假設 f n 已經算出，試著用它定出 f (Suc n).

在證明之中，如 P m 這種在歸納步驟假設成立的性質被稱作歸納假設(induction hypothesis)。

程式與證明   證明2.1 還有一些能啟發我們之處。方才，我們看到 exp b (m + n) = exp b m * exp b n， 決定以數學歸納法證明，但接下來怎麼著手？怎麼選定在哪個變數上做歸納？

答案是：分析該式中程式的行為。程式怎麼拆其參數，我們在證明中就怎麼拆。 我們試圖證明某些程式的性質，但程式本身便提供了證明可怎麼進行的提示。 「使證明的結構符合程式的結構」是許多證明的秘訣。 並非所有證明都可以如此完成，但本原則在許多情況下適用。

再看看 exp, (+), (*) 等函數的定義。 為何他們都分出了兩個情況：Zero 與 Suc n, 並且 Suc n 的情況使用到該函數對於 n 的值？ 因為自然數的資料型別是這麼定的！ 自然數只可能是Zero 或 Suc n，而後者是由 n 做出來的。 因此程式也如此寫。程式的結構依循與其處理的資料型別之結構。

資料、程式、與證明原來有著這樣的關係：證明的結構依循著程式的結構，而程式的結構又依循著資料型別的結構。歸納定義出了一個型別後，自然知道怎麼在上面寫歸納程式；歸納程式有了，自然知道如何做關於這些程式的歸納證明。一切由定義資料結構開始。掌握這個原則，大部分的證明就不是難事。

讓符號為你工作   再考慮證明2.1 中的狀況m := Suc m. 假想由你做這個證明，由第一行 exp b ((Suc m) + n) 開始。接下來該怎麼進行？

既然我們已經打定主意用數學歸納法，在證明的某處必定會使用exp b (m + n) = exp b m * exp b n這個歸納假設。 因此，證明前幾行的目的便是想辦法將 exp b ((Suc m) + n) 中的 Suc 往外提，將 exp b 往內側推，使得式子中出現 exp b (m + n)。一旦成功，就可運用歸納假設，將其改寫成 exp b m * exp b n！ 接下的就是機械化地收尾、將式子整理成 exp b (Suc m) * exp b n 了。

這呼應到第0.2 節所說的「讓符號為你工作」。 光從語意上想，我們不易理解為何 exp b ((Suc m) + n) 能夠等於 exp b (Suc m) * exp b n. 但符號給我們線索。 我們可觀察式子的結構，暫時不去想語意； 我們的目標是操作、移動這些符號，將它們轉換成可使用歸納假設的形式。 因此，接下來的演算推導便有所依據而非盲目進行：已知目標是把某符號往外提或往內推， 我們就可尋找、使用可達到此目的的規則。 這些規則包括已知函數的定義、或諸如分配律、遞移律、結合律等等數學性質。 若很明顯地缺了一個想要的性質，也許可以把它當作引理另外證證看。 符號幫助我們，使我們的思考清晰而有方向。

最後，說到自然數上的歸納定義，似乎不得不提階層(factorial)。用非正式的寫法，fact n = n * (n-1) * (n-2) * ... * 1. 形式化的定義如下：

fact :: Nat -> Nat
fact Zero     = 1
fact (Suc n)  = (Suc n) *: fact n 

我們在定理 2.5 中將會談到階層與排列的關係。