練習問題 4.6.2

foldr
に対する融合定理を証明せよ． 





foldrの融合定理


f は正格，かつ，f a = b，かつ，f (g x y) = h x (f y) ならば
f . foldr g a = foldr h b


xs上の帰納法により任意のxsについて以下が成り立つことを示す． f (foldr g a xs) = foldr h b xs


[]の場合
    f (foldr g a [])
=       { foldr の定義 }
    f a
=       { f a = b だから }
    b
=       { foldr の定義 }
    foldr h b []

x:xs の場合
    f (foldr g a (x:xs))
=       { foldr の定義 }
    f (g x (foldr g a xs))
=       { f (g x y) = h x (f y) だから }
    h x (f (foldr g a xs))
=       { 帰納法の仮定 }
    h x (foldr h b xs)
=       { foldr の定義 }
    foldr h b (x:xs)