SOE ex.11.1
Prove: putCharList cs = map putChar cs
Recall: (Page#58)
putCharList :: String -> [IO()]
putCharList [] = []
putCharList (c:cs) = putChar c : putCharList cs
(a) base step
putCharList [] = []
map putChar [] = []
==> Proven.
(b) induction hypothesis: we assume that putCharList xs = map putChar xs
putCharList (x:xs) = putChar x : putCharList xs
map putChar (x:xs) = putChar x : map putChar xs
Because induction hypothesis, we have putCharList(x:xs) = map putChar (x:xs)
==> Proven.
-----------------------------------------------------------------------------
Prove: listProd xs = fold (*) 1 xs
Recall: (Page#66)
listProd :: [Float] -> [Float]
listProd [] = 1
listProd (x:xs) = x * listProd xs
fold op init [] = init
fold op init (x:xs) = x `op` fold op init xs
(a) base step
listProd [] = 1
fold (*) 1 [] = 1
==> Proven.
(b) induction hypothesis: we assume that listProd ns = fold (*) 1 ns
listProd (n:ns) = n * listProd ns
fold (*) 1 (n:ns) = n * fold (*) 1 ns
Because induction hypothesis, we have listProd (n:ns) = fold (*) 1 (n:ns)
==> Proven.