-- BEGIN 16_12_06_ProofByStructuralInduction.hs

{-
This script continues the discussion in:
   16_12_01_Reasoning_about_Programs.part_1.lhs
   16_12_01_Reasoning_about_Programs.part_2.lhs
   16_12_01_ProofByStrongInduction.lhs
   16_12_06_CorrectnessOfGCD.lhs
-}

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

collapse :: Tree a -> [a]
collapse Nil = []                                -- (collapse.1)
collapse (Node x t1 t2) = 
        (collapse t1) ++ [x] ++ (collapse t2)    -- (collapse.2)

collapse2 :: Tree a -> [a]
collapse2 t = help t []
              where
              help Nil acc = acc
              help (Node x t1 t2) acc = help t1 (x : help t2 acc)

{-

EXERCISE:

How do you prove that the two functions, collapse and collapse2, are
equivalent?

Hint 1: You will never be wrong in saying "I will prove it by induction".

Hint 2: The real question is, what kind of induction will do? What is
the induction parameter? What is the induction hypothesis (i.e. the
"invariant" of the induction)?

Hint 3: To assert that "collapse and collapse2 are equivalent" means
that for every t :: Tree a, the following equation holds:

          collapse t = collapse2 t

The most natural induction for this exercise is STRUCTURAL induction. The
base step in this induction is when the tree t = Nil. The induction step is 
when the tree t = (Node x t1 t2) for some label x and some subtrees t1 and t2.

Hint 4: Before you conclude that "collapse t = collapse2 t" for all tree t,
prove by structural induction for all tree t and list acc:

     help t acc = (collapse t) ++ acc

As follows for the non-base step:

    help (Node x t1 t2) acc 
      = help t1 (x : help t2 acc)                      -- by def of help
      = help t1 (x : ((collapse t2) ++ acc))           -- by IH
      = (collapse t1) ++ (x : ((collapse t2) ++ acc))  -- by IH
      = (collapse t1) ++ [x] ++ (collapse t2) ++ acc   -- "properties of ++"
      = (collapse t) ++ acc

which is the desired conclusion. Note that "properties of ++" have to be
proved separately (by induction, of course!).

Hint 5: Remaining details left to you!

-}

-- a few expressions for experimentation:

t_1 = Node 1 Nil Nil
t_2 = Node 2 Nil Nil
t_3 = Node 3 Nil Nil
t_4 = Node 4 Nil Nil

t_5 = Node 5 t_1 t_2
t_6 = Node 6 t_5 t_5

-- END 16_12_06_ProofByStructuralInduction.hs