# Thinking Functionally with Haskell勉強メモ: 第６章問題２

### Exercise F

#### 第一部

foldl f e xs = foldr (flip f) e (reverse xs)


##### Case [] 左辺
foldl f e []

= {foldlの定義}
e

##### Case [] 右辺
foldr (flip f) e (reverse [])

= {reverse [] = []}
foldr (flip f) e []

= {foldrの定義}
e


Case []は証明できた。

##### Case x:xs 左辺
foldl f e (x:xs)

= {foldlの定義}
foldl f (f e x) xs

= {induction}
foldr (flip f) (f e x) (reverse xs)

##### Case x:xs 右辺
foldr (flip f) e (reverse (x:xs))

= {reverse (x:xs) = reverse xs ++ [x]}
foldr (flip f) e (reverse xs ++ [x])

= {foldr f e (xs++ys) = foldr f (foldr f e ys) xs}
foldr (flip f) (foldr (flip f) e [x]) (reverse xs)

= {foldrの定義}
foldr (flip f) (flip f x (foldr (flip f) e [])) (reverse xs)

= {foldrの定義}
foldr (flip f) (flip f x e) (reverse xs)

= {flipの定義}
foldr (flip f) (f e x) (reverse xs)


これで{foldr f e (xs++ys) = foldr f (foldr f e ys) xs}が任意の有限リストxsysで成り立つなら、Case x:xsも証明できた。

{foldr f e (xs++ys) = foldr f (foldr f e ys) xs}帰納的証明：

##### Case [] 左辺
foldr f e ([]++ys)

= {[]++xs=xs}
foldr f e ys

##### Case [] 右辺
foldr f (foldr f e ys) []

= {foldrの定義}
foldr f e ys


Case []証明完了。

##### Case x:xs 左辺
foldr f e ((x:xs)++ys)

= {(x:xs)++ys = x:(xs++ys)}
foldr f e (x:(xs++ys))

= {foldrの定義}
f x (foldr f e (xs++ys))

= {induction}
f x (foldr f (foldr f e ys) xs)

##### Case x:xs 右辺
foldr f (foldr f e ys) (x:xs)

= {foldrの定義}
f x (foldr f (foldr f e ys) xs)


Case x:xs証明完了。

{foldr f e (xs++ys) = foldr f (foldr f e ys) xs}が任意の有限リストxsysで成り立つ。

よってfoldl f e xs = foldr (flip f) e (reverse xs)も任意の有限リストxsで成り立つ。

#### 第二部

foldl (@) e xs = foldr (<>) e xs


ただし以下の条件が成り立つ：

(x <> y) @ z = x <> (y @ z)
e @ x        = x <> e


##### case [] 左辺
foldl (@) e []

= {foldlの定義}
e

##### case [] 右辺
foldr (<>) e []

= {foldrの定義}
e


case []証明完了（ほぼ自明）。

##### case x:xs 左辺
foldl (@) e (x:xs)

= {foldlの定義}
foldl (@) (e @ x) xs

= {e @ x = x <> e}
foldl (@) (x <> e) xs

= {to be proven}
x <> (foldl (@) e xs)

= {induction}
x <> (foldr (<>) e xs)

##### case x:xs 右辺
foldr (<>) e (x:xs)

= {foldrの定義}
x <> (foldr (<>) e xs)


Case x:xsはfoldl (@) (x <> e) xs = x <> (foldl (@) e xs)が成り立つなら成り立つ。

foldl (@) (x <> e) xs = x <> (foldl (@) e xs)の証明：

##### case [] 左辺
foldl (@) (x <> e) []

= {foldlの定義}
x <> e

##### case [] 右辺
x <> (foldl (@) e [])

= {foldlの定義}
x <> e


case []証明完了。

##### case y:ys 左辺
foldl (@) (x <> e) (y:ys)

= {foldlの定義}
foldl (@) ((x <> e) @ y) ys

= {(x <> y) @ z = x <> (y @ z)}
foldl (@) (x <> (e @ y)) ys

= {induction}
x <> (foldl (@) (e @ y) ys)

##### case y:ys 右辺
x <> (foldl (@) e (y:ys))

= {foldlの定義}
x <> (foldl (@) (e @ y) ys)


Case x:xs証明完了。

foldl (@) (x <> e) xs = x <> (foldl (@) e xs)は成り立つ。 よってfoldl (@) e xs = foldr (<>) e xsも成り立つ。

（ただ、この証明のこの部分はイマイチ自信がない・・・）

foldl (@) (x <> (e @ y)) ys
= {induction}
x <> (foldl (@) (e @ y) ys)


もうちょっと何が起きているのか考えて自分の中で納得する必要がある。

### Exercise G

#### 第一部

foldl f e (xs ++ ys) = foldl f (foldl f e xs) ys


foldl f e . concat = foldl (foldl f) e


Case []はfoldlの定義から自明（両辺がeになる）。

##### Case undefined 左辺
foldl f e (concat undefined)

= {concatの定義}
foldl f e undefined

= {foldlの定義}
undefined

##### Case undefined 右辺
foldl (fold f) e undefined

= {foldlの定義}
undefined


Case undefined証明完了。

##### Case xs:xss 左辺
foldl f e (concat xs:xss)

= {concatの定義}
foldl f e (xs ++ concat xss)

= {foldl f e (xs ++ ys) = foldl f (foldl f e xs) ys}
foldl f (foldl f e xs) (concat xss)

= {induction}
foldl (foldl f) (foldl f e xs) xss

##### Case xs:xss 右辺
foldl (fold f) e (xs:xss)

={foldlの定義}
foldl (foldl f) (foldl f e xs) xss


Case xs:xss証明完了。

よってfoldl f e . concat = foldl (foldl f) eは成り立つ。

#### 第二部

foldr f e (xs ++ ys) = foldr f (foldr f e ys) xs


foldr f e . concat = foldr (flip (foldr f)) e

##### Case [] 左辺
foldr f e (concat [])

= {concatの定義}
foldr f e []

= {foldrの定義}
e

##### Case [] 右辺
foldr (flip (foldr f)) e []

= {foldrの定義}
e


Case [] 証明完了。

##### Case undefined 左辺
foldr f e (concat undefined)

= {concatの定義}
foldr f e undefined

= {foldrの定義}
undefined

##### Case undefined 右辺
foldr (flip (foldr f)) e undefined

= {foldrの定義}
undefined


Case undefined証明完了。

##### Case xs:xss 左辺
foldr f e (concat xs:xss)

= {concatの定義}
foldr f e (xs ++ concat xss)

= {foldr f e (xs ++ ys) = foldr f (foldr f e ys) xs}
foldr f (foldr f e (concat xss)) xs

##### Case xs:xss 右辺
foldr (flip (foldr f)) e (xs:xss)

= {foldrの定義}
flip (foldr f) xs (foldr (flip (foldr f)) e xss)

= {flipの定義}
foldr f (foldr (flip (foldr f)) e xss) xs

= {induction}
foldr f (foldr f e (concat xss)) xs


Case xs:xss証明完了。

よってfoldr f e . concat = foldr (flip (foldr f)) eは成り立つ。

### Exercise H

sum (scanl (/) 1 [1..])


### Exercise I

scanr f e = map (foldr f e) . tails


scanr f e [] = [e]
scanr f e (x:xs) = f x (head ys) : ys
where ys = scanr f e xs

##### Case []
map (foldr f e) (tails [])

= {tailsの定義}
map (foldr f e) [[]]

= {mapの定義}
(foldr f e []):map (foldr f e) []

= {mapの定義}
(foldr f e []):[]

= {foldrの定義}
[e]


Case []証明完了。

##### Case undefined
map (foldr f e) (tails undefined)

= {tailsの定義}
map (foldr f e) undefined

= {mapの定義}
undefined


scanrの定義では最初のパターンマッチでundefinedになる。

Case undefined証明完了。

##### Case x:xs
map (foldr f e) (tails (x:xs))

= {tailsの定義}
map (foldr f e) ((x:xs) : (tails xs))

= {mapの定義}
(foldr f e (x:xs)) : (map (foldr f e) (tails xs))

= {scanr f e = map (foldr f e) . tails}
(foldr f e (x:xs)) : (scanr f e xs)

= {foldrの定義}
(f x (foldr f e xs)) : (scanr f e xs)

= {to be proven}
(f x (head (scanr f e xs))) : (scanr f e xs)

= {extract identical expressions as ys}
(f x (head ys)) : ys
where ys = scanr f e xs


Case x:xsはfoldr f e xs = head (scanr f e xs)が成り立てば成り立つ。

foldr f e xs = head (scanr f e xs)帰納法で証明する。

##### Case []
head (scanr f e [])

= {scanr f e = map (foldr f e) . tails}
head (map (foldr f e) (tails []))

= {tailsの定義}
head (map (foldr f e) [[]])

= {mapの定義}
head ((foldr f e []) : map (foldr f e) [])

foldr f e []


Case [] 証明完了。

##### Case undefined
head (scanr f e undefined)

= {scanr f e = map (foldr f e) . tails}
head (map (foldr f e) (tails undefined))

= {tailsの定義}
head (map (foldr f e) undefined)

= {mapの定義}

undefined


foldr f e undefinedも定義から自明にundefined

Case undefined証明完了。

##### Case x:xs
head (scanr f e (x:xs))

= {scanr f e = map (foldr f e) . tails}
head (map (foldr f e) (tails (x:xs)))

= {tailsの定義}
head (map (foldr f e) ((x:xs):(tails xs)))

= {mapの定義}
head ((foldr f e (x:xs)) : map (foldr f e) (tails xs))

foldr f e (x:xs)


Case x:xs証明完了。

foldr f e xs = head (scanr f e xs)は成り立つ。

よって

scanr f e = map (foldr f e) . tails


から

scanr f e [] = [e]
scanr f e (x:xs) = f x (head ys) : ys
where ys = scanr f e xs


が導き出される。