練習問題 4.6.4

以下の等式を証明せよ．

foldr f a (xs++ys) = foldr f (foldr f a ys) xs
foldl f a (xs++ys) = foldl f (foldl f a xs) ys
もし必要だとすれば， 
xs
， 
ys
に対してどのような制限が必要か． 





foldr f a (xs++ys) = foldr f (foldr f a ys) xs の証明は xs 上の帰納法でおこなう．


⊥の場合
    foldr f a (⊥++ys)
=       { ++ の定義，場合の枯渇 }
    foldr f a ⊥
=       { foldr の定義，場合の枯渇 }
    ⊥
=       { foldr の定義，場合の枯渇 }
    foldr f (foldr f a ys) ⊥

[]の場合
    foldr f a ([]++ys)
=       { ++ の定義 }
    foldr f a ys
=       { foldr の定義 }
    foldr f (foldr f a ys) []

x:xs の場合
    foldr f a (x:xs ++ ys)
=       { ++ の定義 }
    foldr f a (x:(xs ++ ys))
=       { foldr の定義 }
    f x (foldr f a (xs++ys))
=       { 帰納法の仮定 }
    f x (foldr f (foldr f a ys) xs)
=       { foldr の定義 }
    foldr f (foldr f a ys) (x:xs)


foldl f a (xs++ys) = foldl f (foldl f a xs) ys の証明は xs 上の帰納法でおこなう．


⊥の場合

    foldl f a (⊥++ys)
=       { ++ の定義，場合の枯渇 }
    foldl f a ⊥
=       { foldl の定義，場合の枯渇 }
    ⊥

    foldl f (foldl f a []) ys
=       { foldl の定義，場合の枯渇 }
    foldl f ⊥ ys

一般には ⊥ ＝ foldl f ⊥ ys ではない．

[]の場合
    foldl f a ([]++ys)
=       { ++ の定義 }
    foldl f a ys
=       { foldl の定義 }
    foldl f (fold f a []) ys

x:xs の場合
    foldl f a ((x:xs)++ys)
=       { ++ の定義 }
    foldl f a (x:(xs++ys))
=       { foldl の定義 }
    foldl f (f a x) (xs++ys)
=       { 帰納法の仮定 }
    foldl f (foldl f (f a x) xs) ys
=       { foldl の定義 }
    foldl f (foldl f a (x:xs)) ys


foldr に関する法則の場合は任意のxs，ysについて成り立つ foldl に関する法則の場合は任意の有限リストxs，と任意のリストysについて成り立つ