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

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

• 4. ヒントより、 all (== x) (replicate n x) = True を証明します。

n = 0 の時
all (== x) (repliicate 0 x)
=> all (== x) []   -- replicate の定義より
=> True            -- all の定義より

n = m + 1 の時
all (== x) (replicate m x) は True と仮定する

all (== x) (replicate (m+1) x)
=> all (== x) (x : replicate m x)  -- replicate の定義より
=> (x == x) && all (== x) (replicate m x) -- all の定義より
=> True && all (== x) (replicate m x) -- `==` の定義？より
=> True && True                    -- 仮定より
=> True

よって任意の n に対して all (==x) (replicate n x) = True

• 5.

以下の定義が与えられているものとする
[] ++ ys = ys                      -- (a)
(x:xs) ++ ys = x:(xs ++ ys)        -- (b)

• • 5-1. xs ++ [] = xs を証明

xs = [] の時
[] ++ [] = []  -- 定義 (a) より

xs = (z:zs) の時、zs ++ [] = zs と仮定して
(z:zs) ++ []
=> z:(zs ++ [])  -- 定義 (b) より
=> z:zs          -- 仮定より
=> xs            -- 場合分けの条件より

• • 6-2. xs ++ (ys ++ zs) = (xs ++ ys) ++ zs を証明

xs = [] の時
(左辺) => [] ++ (ys ++ zs)
=> ys ++ zs                 -- 定義 (a) より
=> ([] ++ ys) ++ zs         -- 定義 (a) を ys に対して逆向きに適用
=> 右辺

xs = (a:as) の時、 as ++ (ys ++ zs) = (as ++ ys) ++ zs と仮定する

(左辺) => (a:as) ++ (ys ++ zs)
=> a:(as ++ (ys ++ zs))        -- 定義 (b) より
=> a:((as ++ ys) ++ zs)        -- 仮定より
=> (a:(as ++ ys)) ++ zs        -- 定義 (b) より
=> ((a:as) ++ ys) ++ zs        -- 定義 (b) より
=> (xs ++ ys) ++ zs => (右辺)