COMP1011 Exercises for Week 09
Computing 1A 05s2 Last updated Tue 19 Jul 2005 14:37

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 ... =


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

<various cases of the proof>



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


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

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


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


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


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.