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:

   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.

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.

Induction

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:

• What is the induction principle and why does it work?
• What is an induction hypothesis?

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