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). -}