2.5 從資料、程式、到證明

本節再用一個例子談談「讓符號為我們工作」。考慮證明下述性質：

 sum . concat = sum . map sum    (2.3 )

根據外延相等，這相當於證明對所有xss, sum (concat xss) = sum (map sum xss). 當 xss := [], 等號兩邊都歸約成 0. 考慮 xss := xs :xss 的情況：

      sum (concat (xs:xss))
 ===    {- concat 之定義 -}
      sum (xs ++ concat xss)
 ===    {- 因 sum (xs ++ ys) = sum xs + sum ys -}
      sum xs + sum (concat xss)
 ===    {- 歸納假設 -}
      sum xs + sum (map sum xss)
 ===    {- sum 之定義 -}
      sum (sum xs : map sum xss)
 ===    {- map 之定義 -}
      sum (map sum (xs:xss)) 

讀者對這個證明最大的疑問可能是：我們怎麼知道該用 sum (xs ++ ys) = sum xs + sum ys 呢？ 為什麼當我們遇到 sum (xs ++ concat xss), 我們不是把 xs 再拆成首和尾，甚至把 xss 拆開？ 這是許多綜合考量的結果。 首先，我們預期會使用歸納假設，因此證明前幾步的目的均為把 sum 推到 concat xss 左側，試圖做出 sum (concat xss). 此處我們再強調一個觀念：證明中的步驟不是瞎猜的，而是有目的的。 符號給我們提示：我們需要把 sum 往右推，因此我們試圖尋找能完成這個目標的性質。

其次，證明的結構跟隨著程式的結構。由於 concat 是由 (++) 定義的，每一個關於 concat 的定理，均很有可能奠基在一個關於 (++) 的相對定理上。為了證明一個描述 sum 與 concat 的關係的定理，我們可能會需要一個關於 sum 與 (++) 的性質。

有了符號給我們的這兩個線索，我們便可以運用我們對語意的了解：sum 與 (++) 應該會滿足什麼性質？ 我們可猜測應該是 sum (xs ++ ys) = sum xs + sum ys --- 根據我們對 sum 與 (++) 的語意上的理解，這性質成立的機會很大。 而且，這個性質允許我們把 sum 推到右邊。

符號仍舊幫助了我們。 我們不可能期待所有定理都只靠符號推導出，在關鍵時刻我們仍會需要對於特定領域的、語意上的知識。但符號給了我們許多引導， 縮小我們需要猜測的範圍。

至於 sum (xs ++ ys) = sum xs + sum ys 該怎麼證明呢？ 不要急著把 xs 與 ys 都拆開。 觀察等號左右邊的式子，根據 (++), (+) 與 sum 的定義，兩個式子的歸約都是先對 xs 做情況分析。 因此我們可試著在 xs 上做歸納。

證明的結構跟隨著程式的結構 --- 這是做證明時相當好用的指引。 程式對哪個參數做歸納，我們做證明時就在那個參數上做歸納。 函數 f 用函數 g 定義，我們證明 f 的性質時就可以預期會需要一個 g 的相關性質。 並非所有證明都可以如此做出，但這個模式在許多情況下都適用。

而如我們所知，程式的結構又跟隨著資料的結構： 例如，串列有 [] 和 x:xs 兩個情況，我們定義串列上的程式時也分出這兩個情況， 定義 f (x:xs) 時可以使用 f xs 的值。 資料結構、程式、與證明於是有著這樣的連續關係： 歸納定義出一個資料結構，我們就有了一個在上面歸納定義程式的方法； 有了歸納定義的程式，我們便知道怎麼做關於它的歸納證明。 一切由資料結構開始。

     length (concat (xs:xss))
===  length (xs ++ concat xss)
===    {- 因 length (xs ++ ys) = length xs + length ys -}
     length xs + length (concat xss)
===    {- 歸納假設 -}
     length xs + sum (map length xss)
===  sum (length xs : map length xss)
===  sum (map length (xs:xss)) 

     map f (concat (xs:xss))
===  map f (xs ++ concat xss)
===   {- 因 map f (xs ++ ys) = map f xs ++ map f ys -}
     map f xs ++ map f (concat xss)
===   {- 歸納假設 -}
     map f xs ++ concat (map (map f xss))
===  concat (map f xs : map (map f xss))
===  concat (map (map f (xs : xss)))