comp :: (b -> c) -> (a -> b) -> (a -> c)
comp f g = \x -> f (g x)
comp' :: (b -> c) -> (a -> b) -> (a -> c)
comp' f g x = f (g x)
comp'' :: (b -> c) -> ((a -> b) -> (a -> c))
comp'' f = \g -> \x -> f (g x)
-- foldRose :: (a -> [b] -> b) -> Rose a -> b
-- foldRose f :: Rose a -> b
-- map (\ra -> foldRose f ra) === map (foldRose f)
foo x = f (g x) -- foo = f . g
------------------------------------------------------------
{-
Example: prove that map preserves length, that is,
for all lists xs, and for all function f,
length (map f xs) == length xs
map _ [] = []
map f (x:xs) = f x : map f xs
length [] = 0
length (_:xs) = 1 + length xs
We can work directly with Haskell expressions and work by replacing
equals by equals (because of purity).
Proof.
By induction on xs.
* xs = []:
length (map f [])
= { definition of map }
length []
* xs = (y:ys):
length (map f (y:ys))
= { definition of map }
length (f y : map f ys)
= { definition of length }
1 + length (map f ys)
= { IH }
1 + length ys
=
length (y:ys)
QED.
-}
------------------------------------------------------------
data Tree a where
Empty :: Tree a
Node :: a -> Tree a -> Tree a -> Tree a
{- Induction principle for Tree a:
If
* P(Empty)
* for all x, l, r, P(l) and P(r) => P(Node x l r)
-}
{- Example:
size :: Tree a -> Integer
size Empty = 0
size (Node _ l r) = 1 + size l + size r
flatten :: Tree a -> [a]
flatten Empty = []
flatten (Node x l r) = flatten l ++ [x] ++ flatten r
Prove: for all trees t, size t == length (flatten t)
Proof. By induction on t.
* t = Empty
First, note
size Empty
= { defn of size }
0
Also, we have
length (flatten Empty)
= { defn of flatten }
length []
= { defn of length }
0.
* Suppose x is any value of type a, and
l, r are trees. Assume as the
inductive hypothesis that
size l == length (flatten l)
and similarly for r. We must show
size (Node x l r) == length (flatten (Node x l r))
We calculate as follows:
size (Node x l r)
= { defn of size }
1 + size l + size r
= { IH }
1 + length (flatten l) + length (flatten r)
Starting from the other end:
length (flatten (Node x l r))
= { defn of flatten }
length (flatten l ++ [x] ++ flatten r)
= { lemma (see HW) }
length (flatten l) + length [x] + length (flatten r)
= { defn of length }
length (flatten l) + 1 + length (flatten r)
= { + is commutative }
1 + length (flatten l) + length (flatten r)
QED.
-}
data Rose a where
RNode :: a -> [Rose a] -> Rose a
{-
Induction principle for Rose?
If
* for all (x :: a), (rs :: [Rose a])
P holds for all r in rs => P(RNode a rs)
then for all r :: Rose a, P(r).
-}