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

Tute Exercises Week 9

Equational Reasoning & Induction

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:

= {1st Justification}
= {2nd Justification}
= {nth Justification}

where we use the notation foo.i to refer to the ith equation of the function foo.

Equational Reasoning

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.



(++)         :: [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:

Lemmata & Generalisation

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