プログラミング Haskell 第13章 プログラムの論証 練習問題 その1

最終章「プログラムの論証」の練習問題です。

• 1.
  • 付録A にある重複するパターンをもつ関数定義は zip。 zip の2つの引数がどちらも空リストの時に1番目と2番目のパターン両方にマッチします

• 2.

add n (Succ m) = Succ (add n m) を示す

n = Zero の時
(左辺)
add Zero (Succ m)
=> Succ m  -- add の定義より

(右辺)
Succ (add Zero m)
=> Succ m  -- add の定義より

n == Succ l の場合
add l (Succ m) = Succ (add l m) が成り立つと仮定する

(左辺)
add (Succ l) (Succ m)
=> Succ (add l (Succ m))  -- add の定義より
=> Succ (Succ (add l m))  -- 仮定より

(右辺)
Succ (add (Succ l) m)
=> Succ (Succ (add l m)) -- add の定義より

よって任意の n について
add n (Succ m) = Succ (add n m)
が成り立つ。

• 3.

add n (Succ m) = Succ (add n m) -- (a)
add n Zero = n                  -- (b)
から
add n m = add m n
を示す。

n = Zero の時
(左辺) = add Zero m = m = add m Zero = (右辺) -- (b) より

n = (Succ l) の時
add l m = add m l が成立すると仮定する。

(左辺)
add (Succ l) m
=> Succ (add l m)   -- add の定義より

(右辺)
add m (Succ l)
=> Succ (add m l)   -- (a) より
=> Succ (add l m)   -- 仮定より

よって任意の n について
add n m = add m n
が成り立つ。

実際に自分で証明問題を解くとなかなか楽しいですね。