Lab Exercises Week 9

Equational Reasoning & Induction

For this week's lab exercises, create a file Lab09.hs. In this file enter the function definitions appearing in the exercises below. Then, following the function definitions, in a multi-line comment, state the property you are proving, followed by the proof. So, overall, the structure should be as follows:

foo :: <some type signature>
foo ...<definition of the function>

{- ------------

Property:  foo ... = ..foo...

PROOF:

Explain here, how your proof works (eg, induction proof over 
a particular variable).

<various cases of the proof>

QED

-}

Ex 1: Induction over natural numbers

Given the following functions:

mulNats   :: Int -> Int
mulNats 0  = 1
mulNats n  = n * mulNats (n - 1)

natList   :: Int -> [Int]
natList 0  = []
natList n  = n : natList (n - 1)

prodList        :: [Int] -> Int
prodList []      = 1
prodList (x:xs)  = x * prodList xs

prove that, for every natural number n, we have

mulNats n   =   prodList (natList n)

When you have completed the above exercise show it to your tutor for this week's core mark.

Ex 2: Structural induction over lists

Given

concat          :: [[a]] -> [a]
concat []        = []
concat (xs:xss)  = xs ++ concat xss

(++)         :: [a] -> [a] -> [a]
[]     ++ ys  = ys
(x:xs) ++ ys  = x : (xs ++ ys)

prove

concat (xss ++ yss)   =   concat xss ++ concat yss

When you have completed the above exercise show it to your tutor for this week's advanced mark.

Additional Exercise

The following is an additional exercise to help you getting practice in proving. It is not part of the lab mark, but it should help you understand some of the material covered in the lecture.

Lemmata and Generalisation

Given

reverse       :: [a] -> [a]
reverse []     = []
reverse (x:xs) = reverse xs ++ [x]

prove

reverse (reverse xs)   =   xs

Hint: This one is a bit more tricky than the other two proofs of this week's lab. You will find that you need to prove a lemma and apply generalisation - a bit like in the Wednesday lecture last week.