COMP1011 Exercises for Week 09
Computing 1A 05s2 Last updated Tue 19 Jul 2005 14:37
Mail cs1011@cse.unsw.edu.au

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