\documentclass{article} %include polycode.fmt \usepackage{amsthm} \usepackage{sproof} \newtheorem{thm}{Theorem} \begin{document} \begin{code} data Tree a where Empty :: Tree a Node :: a -> Tree a -> Tree a -> Tree a 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 \end{code} \begin{thm} For all trees |t|, |size t == length (flatten t)|. \end{thm} \begin{proof} By induction on |t|. \begin{itemize} \item |t = Empty|. First, note \begin{sproof} \stmt{|size Empty|} \reason{=}{defn of size} \stmt{|0|} \end{sproof} Also, we have \begin{sproof} \stmt{|length (flatten Empty)|} \reason{=}{ defn of flatten } \stmt{|length []|} \reason{=}{ defn of length } \stmt{|0|.} \end{sproof} \end{itemize} \begin{code} * 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. -} \end{code} \end{proof} \end{document}