-- BEGIN 16_12_08_AnotherProofByStructuralInduction.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
   16_12_06_ProofByStructuralInduction.hs
-}

-- The example in this script is NOT to prove that a program is 
-- correct, or that a loop/iteration/recursion in a program satisfies  
-- an invariant, or that two programs are equivalent. The example
-- is to show how we can prove a more general equational relation
-- involving several programs (in this case just two programs). And,
-- of course, the proof will be by induction!

mySum       [] = 0
mySum (x : xs) = x + mySum xs

doubleAll       [] = []
doubleAll (z : zs) = 2*z : (doubleAll zs)

{-

We want to prove the following relation involving the two functions,
mySum and doubleAll. For all list xs of number:

      mySum (doubleAll xs) = 2 * mySum xs

Hint 1: Use structural induction on lists. (You can also use simple induction
on the length of lists, but structural induction is a bit simpler.)

Hint 2: The base step of the induction is very simple. This is when xs = [].

EXERCISE: Write all the details of the induction step of the proof (by
structural induction).

-}

-- END 16_12_08_AnotherProofByStructuralInduction.hs