BEGIN 16_12_01_Reasoning_about_Programs.part_2.lhs

REASONING ABOUT PROGRAMS AND VERIFICATION OF PROGRAMS (PART 2)

REASONING WITH ALGEBRAIC DATA TYPES

We recall several definitions. To make it easier for a proof, we
define "map" using pattern-matching (instead of list comprehension,
as in Prelude.hs):

> map' f [] = []                       -- (map.1)
> map' f (x:xs) = (f x) : (map' f xs)  -- (map.2)

Once more, the datatype of binary trees where leaf nodes are not labelled:

> data Tree a = Nil | Node a (Tree a) (Tree a)
>               deriving (Eq,Ord,Show)

> mapTree :: (a -> b) -> Tree a -> Tree b
> mapTree f Nil = Nil                           -- (mapTree.1)
> mapTree f (Node x t1 t2) =
>     Node (f x) (mapTree f t1) (mapTree f t2)  -- (mapTree.2)

The function "collapse" is the same as inorder traversal:
 
> collapse :: Tree a -> [a]
> collapse Nil = []                             -- (collapse.1)
> collapse (Node x t1 t2) = 
>         (collapse t1) ++ [x] ++ (collapse t2) -- (collapse.2)

We want to verify, with a proof, that the following equation holds
for every tree "tr":

map f (collapse tr) = collapse (mapTree f tr)   -- (map-collapse)

We proceed by induction. But the induction here is a little more 
complicated. This will NOT be an induction on the natural numbers, 
but an induction on the STRUCTURE (or, if you will, the SHAPE) of 
"tr". This is why it is called a STRUCTURAL INDUCTION.

Before we start the proof, we mention another fact which we call
(map++) for later reference:

map f (ys ++ zs) = map f ys ++ map f zs         -- (map++)

(map++) can be proved by induction on the size of ys, which we leave
to you. It is also an exercise in the book [HCFP, Ex 11.31, p 261]. 

(1) BASE STEP: This is when "tr" in the equation (map-collapse) is 
"Nil". We examine both sides of (map-collapse) separately.

map f (collapse Nil) = map f []              -- by (collapse.1)
                     = []                    -- by (map.1)

collapse (mapTree f Nil) = collapse Nil      -- by (mapTree.1)
                         = []                -- by (collapse.1)

This completes the proof of the base step.

(2) INDUCTION STEP: We have to prove:

map f (collapse (Node x tr1 tr2))  
    =  collapse (mapTree f (Node x tr1 tr2))     -- (ind)

using two induction hypotheses:

map f (collapse tr1) = collapse (mapTree f tr1)   -- (hyp.1)
map f (collapse tr2) = collpase (mapTree f tr2)   -- (hyp.2)

First, consider the LHS of (ind):

map f (collapse (Node x tr1 tr2))  
   =  map f (collapse tr1 ++ [x] ++ collapse tr2)           
      --  by (collapse.2)
   =  map f (collapse tr1) ++ [f x] ++ map f (collapse tr2)
      --  by (map++)
   =  collapse (mapTree f tr1) ++ [f x] ++ collapse (mapTree f tr2)
      --  by (hyp.1) and (hyp.2)

Next, consider the RHS of (ind):

collapse (mapTree f (Node x tr1 tr2))
   =  collapse (Node (f x) (mapTree f tr1) (mapTree f tr2))   
      --  by (mapTree.2)
   =  collapse (mapTree f tr1) ++ [f x] ++ collapse (mapTree f tr2)
      --  by (collapse.2)

This proves that the LHS and the RHS evaluate to the same expression.
Which concludes the induction and the proof.

END 16_12_01_Reasoning_about_Programs.part_2.lhs