COMP1011 Exercises for Week 09 | |
---|---|
Computing 1A 05s2 |
Last updated
Tue 19 Jul 2005 14:37
Mail cs1011@cse.unsw.edu.au |
This week's tute and lab will be concerned with reasoning about programs. We will do proofs similar to the ones discussed during the lecture last week. For all proofs, use the proof format used in the lecture; i.e, equational derivations should look as follows:
e1
= {1st Justification}
e2
= {2nd Justification}
...
= {nth Justification}
e(n+1)
where we use the notation foo.
i to refer to the
ith equation of the function foo
.
Consider the following two function definitions, which compute the absolute value and signum of an integer, respectively:
abs :: Int -> Int abs k | k >= 0 = k | otherwise = -k signum :: Int -> Int signum k | k > 0 = 1 | k == 0 = 0 | k < 0 = -1
Prove that, for all integer values n
, we have
abs n * signum n
=n
Hint: First, think about which cases you have to distinguish in the proof. Then, prove each case individually and ensure that all cases together cover all possible input values.
Given
(++) :: [a] -> [a] -> [a] [] ++ ys = ys (x:xs) ++ ys = x : (xs ++ ys)
prove that (++)
is associative, i.e.,
(xs ++ ys) ++ zs
=xs ++ (ys ++ zs)
Discuss the following points from the lecture:
Discuss in which situations the two proof techniques of using a lemma and proving a generalised statement are useful as well as how these techniques are applied. (You can use the example from the lecture for this discussion.)