2.7 再談「讓符號為你工作」

看了這麼多歸納定義，我們做個較複雜的練習，並以此為例再談談「讓符號為你工作」。 本節在初次閱讀時可略過。

以下的函數 ins 將一個元素插到一個串列的空隙中。它和第2.6.4 節中的 fan 類似但稍有不同 --- ins x xs 不會把 x 放到 xs 的結尾。 (註8) 本節不使用 fan 而另外定義了 ins 的原因僅是因為如此使得性質 (2.7 ) 較單純而方便說明。 例如：ins 1 [2,3,4] = [[1,2,3,4],[2,1,3,4],[2,3,1,4]]。

ins :: a -> List a -> List (List a)
ins x []      = []
ins x (y:ys)  = (x:y:ys) : map (y:) (ins x ys) 

請證明對所有 x, ys, 與 zs,

  map (++zs) (ins x ys) ++  map (ys++) (ins x zs) &= ins x (ys ++ zs)     (2.7 )

意即：在 ys ++ zs 之中插入 x 的所有方法， 是 1. 把 x 插入 ys 之中，並把每個結果的右邊接上 zs, 以及 2. 把 x 插入 zs 之中，並把每個結果的左邊接上 ys.

面對一個如此冗長的式子，我們該如何著手？我們可猜想如此複雜的性質大概會需要歸納證明。 但在哪個變數上做歸納呢？ 觀察(2.7 )，等號左手邊最外側的運算子是(++)。 計算 (++) 時，根據定義，先被樣式配對的是 (++) 左邊的參數，也就是 map (++zs) (ins x ys)。 再來，根據 map 的定義，map (++zs) (ins x ys) 的運算要有進展，得先把 ins x ys 算出來。 最後，根據 ins 的定義，計算 ins x ys 會先拆開 ys. 由此可知，等號左手邊的運算是從拆解 ys 開始的。 等號右手邊的情況也一樣：根據 ins 與 (++) 的定義，要計算 ins x (ys ++ zs)，第一個被拆開的是 ys. 因此，欲證明(2.7 )，合理的猜測是在 ys 上做歸納！

我們省略 ys := [] 的情況，僅考慮歸納情況 ys := y:ys。 經代換後的式子是 map (++zs) (ins x (y:ys)) ++ map ((y:ys) ++) (ins x zs). 我們採取的策略和證明定理2.1 時一樣： 想辦法湊出 map (++zs) (ins x ys) ++ map (ys++) (ins x zs), 以便使用歸納假設。 由此論證如下（步驟加上編號以利說明）：

     map (++zs) (ins x (y:ys)) ++ map ((y:ys) ++) (ins x zs)
 ===     {- 1. ins 與 map 之定義 -}
     (x:y:ys++zs) : map (++zs) (map (y:) (ins x ys)) ++ map ((y:ys) ++) (ins x zs)
 ===     {- 2. map 融合 -}
     (x:y:ys++zs) : map ((++zs) . (y:)) (ins x ys) ++ map ((y:ys) ++) (ins x zs)
 ===     {- 3. 由於 (++zs) . (y:) = (y:) . (++zs) (習題 2.30) -}
     (x:y:ys++zs) : map ((y:) . (++zs)) (ins x ys) ++ map ((y:ys) ++) (ins x zs)
 ===     {- 4. map 融合 -}
     (x:y:ys++zs) : map (y:) (map (++zs) (ins x ys)) ++ map ((y:ys) ++) (ins x zs)
 ===     {- 5. 由於 ((y:ys)++) = (y:).(ys++) (習題 2.29) -}
     (x:y:ys++zs) : map (y:) (map (++zs) (ins x ys)) ++ map ((y:).(ys++)) (ins x zs)
 ===     {- 6. map 融合 -}
     (x:y:ys++zs) : map (y:) (map (++zs) (ins x ys)) ++ map (y:) (map (ys++) (ins x zs))
 ===     {- 7. 由於 map f (xs ++ ys) = map f xs ++ map f ys -}
     (x:y:ys++zs) : map (y:) (map (++zs) (ins x ys) ++ map (ys++) (ins x zs))
 ===     {- 8. 歸納假設 -}
     (x:y:ys++zs) : map (y:) (ins x (ys ++ zs))
 ===     {- 9. ins 與 (++) 之定義 -}
     ins x ((y:ys)++zs) 

雖然步驟多、式子長，但策略確定後，整個證明的架構便很清楚。第 1 到 7 步都是為了可在第 8 步使用歸納而做的準備。 為湊出 map (++zs) (ins x ys) ++ map (ys++) (ins x zs), 第 2 至第 4 步把 map (++zs) 往裡推，把第一個 map (y:) 往外提；第 5, 6 步則提出另一個 map (y:)。式子變成 map (y:) ... ++ map (y:) ... 的形式後，共同的 map (y:) 可在第 7 步提出來。 如此，終於可使用歸納假設了。 整個證明中，要配對哪個變數、把式子中的哪些項往哪兒移動，都被符號引導著而有線索可循。 證明中用到的兩個性質 (++zs) . (y:) = (y:) . (++zs) 與 ((y:ys)++) = (y:).(ys++) 並非天外飛來，而是確立了目標後，因為有需求（兩者分別讓我們把 (++zs) 與 (ys++) 往右推，把 (y:) 往左拉）而設計出並另外證明的性質。

初學者常犯的一個錯誤是：以為所有情況下、所有的變數都需要樣式配對。 事實上，過度的樣式配對是形式證明中希望避免的。 藉由觀察 (2.7 )，我們決定對 ys 做歸納，證明過程中發現如此便已經足夠。 如果我們對 ys 和 zs 都做配對，將必須處理四種情況：ys,zs := [],[],[], ys,zs := [],z:zs, ys,zs := [],z:zs ys,zs := y:ys,z:zs。一個待證明的性質若有 n 個串列，似乎得分出 $2^n$ 種情況 --- 只有萬不得已我們才會這麼做。

最嚴重的問題並不是情況數目太多，而是過度的樣式配對破壞了證明的結構。 如果對 zs 做配對，許多人會很自然地想把 ins x (z:zs) 展開。 證明可能如此進行：

   map (++(z:zs)) (ins x (y:ys)) ++ map ((y:ys) ++) (ins x (z:zs))
 ===   {- 將 (++) 的左手邊展開 -}
   (x:y:ys++(z:zs)) : map (++(z:zs)) (map (y:) (ins x ys)) ++
     map ((y:ys) ++) (ins x (z:zs))
 ===   {- 展開 ins x (z:zs) -}
   (x:y:ys++(z:zs)) : map (++(z:zs)) (map (y:) (ins x ys)) ++
     map ((y:ys) ++) ((x:z:zs) : map (z:) (ins x zs))
 ===   {- map 的定義 -}
   (x:y:ys++(z:zs)) : map (++(z:zs)) (map (y:) (ins x ys)) ++
     ((y:ys ++ (x:z:zs)) : map ((y:ys) ++) (map (z:) (ins x zs))) 

要從這樣的式子中再整理出 map (++(z:zs)) (ins x (y:ys)) ++ map ((y:ys) ++) (ins x (z:zs)) 以便做歸納假設， 我們得看出如何把（本來不需展開的）ins x (z:zs) 給收回來。 式子的結構已經被破壞，操作起來的難度便大大提高了。 (註9) 這其實是我於 2019 年開設的程式語言課程的期末考題。在十數位將 ins x (z:zs) 展開的同學中，只有一位成功地將它收了回來。

   ((y:).(ys++)) xs
=   {- definition of (.) -}
   y : (ys ++ xs)
=   {- definition of (++) -}
   (y : ys) ++ xs 

  ((++zs) . (y:)) xs
=   {- definition of (.) -}
  (++zs) (y:xs)
= (y:xs) ++ zs
=   {- definition of (++) -}
   y :(xs ++ zs)
=  (y:) ((++ zs) xs)
=   {- definition of (.) -}
   ((y:) . (++zs)) xs