COMP1011 Exercises for Week 09 | |
---|---|
Computing 1A 05s2 |
Last updated
Tue 19 Jul 2005 14:37
Mail cs1011@cse.unsw.edu.au |
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 -}
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.
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.
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.
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.