\begin{code}
{-# OPTIONS_GHC -Wall #-}
module Feb09 where
\end{code}
Learning objectives:
\begin{itemize}
\item Structural Induction
\item typechecking
\end{itemize}
\begin{code}
data Tree a =
Leaf a — case 1
| Node (Tree a) a (Tree a) — case 2
collapse :: Tree a -> [a]
collapse (Leaf a) = [a] — coll.1
collapse (Node l a r) = collapse l ++ (a : collapse r) — coll.2
mapTree :: (a -> b) -> Tree a -> Tree b
mapTree f (Leaf a) = Leaf $ f a — mt.1
mapTree f (Node l a r) = Node (mapTree f l) (f a) (mapTree f r) — mt.2
\end{code}
\begin{verbatim}
Would like to prove:
P t := map f (collapse t) == collapse (mapTree f t)
Induction principle for Tree is
– prove it for (Leaf a)
– assuming property true for tree l and r, prove true for (Node l a r)
Proof:
assume f :: a -> b
assume a :: a
case 1
map f (collapse (Leaf a)) == — coll.1
map f [a] == — map.2
f a == — coll.1
collapse (Leaf (f a)) == — mt.1
collapse (mapTree f (Leaf a))
assume P l and P r
case 2
map f (collapse (Node l a r)) == — coll.2
map f (collapse l ++ (a : collapse r) == — lemma map++
map f (collapse l) ++ (map f (a : collapse r)) == — map.2
map f (collapse l) ++ f a : map f (collapse r) == — ind. hyp. times 2
collapse (mapTree f l) ++ (f a : collapse (mapTree f r)) == — coll.2
collapse (Node (mapTree f l) (f a) (mapTree f r)) == — mt.2
collapse (mapTree f (Node l a r))
Much harder…
forall re : RE. forall x \in enumerate re. toRecog re x == True
by inductions on RE
Easy:
recall Jan28’s Expr type
P : forall e1 e2 :: Expr, eval (Add e1 e2) == eval (Add e2 e1)
Proof:
eval (Add e1 e2) == — eval.2
eval e1 + eval e2 == — + commutative
eval e2 + eval e1 == — eval.2
eval (Add e2 e1)
\end{verbatim}
Comment: Some “proofs” are do not follow straight induction. Proving properties
of |simplify| requires different mechanisms.
\newpage
– ex.1
f :: Bool -> Bool
f x = (not False) && x
How?
False :: Bool
not :: Bool -> Bool
(&&) :: Bool -> Bool -> Bool
g = \y -> …. :: a -> b
x ~ Bool
f ~ a -> b
a ~ x ~ Bool
b ~ Bool
f :: Bool -> Bool
– ex.2
f (x, y) = (x, [‘a’..y])
assume
x :: a
y :: b
f :: (a, b) -> c
c ~ (a , [d])
[ q .. w ] :: Enum a => a -> a -> [a]
d ~ Char
y ~ d
f :: (a, Char) -> (a, [Char])