<![CDATA[
**Exercise:** Prove that for any list `xs` and element `x`,
`behead (prepend xs x) ~ xs`, where `prepend` and `behead`
are defined as follows:
```
let prepend xs x =
x::xs
let behead = function
| [] -> []
| _::t -> t
```
*Hint: induction is not needed.*
**Exercise:** Prove that for any list `xs`, `noop xs ~ xs`,
where `noop` is defined as follows:
```
let rec noop = function
| [] -> []
| h::t -> h :: noop t
```
Use the following template for an inductive proof:
```
Theorem: TODO(xs)
Proof: by induction on xs
Case: xs = []
Show: TODO
TODO
Case: xs=h::t
Show: TODO
IH : TODO
TODO
QED
```
* * *
*In the rest of the exercises, continue to use that template for proofs,
and to use structural induction. Make sure for each case to state what you are
trying to show for that case and what the inductive hypotheses are.*
* * *
**Exercise:** Prove that for all `f`, `xs`, and `ys`,
`map f (xs @ ys) = (map f xs) @ (map f ys)`, where
`map` and `(@)` are defined as follows:
```
let rec append l1 l2 =
match l1 with
| [] -> l2
| h::t -> h :: (append t l2)
let (@) = append
let rec map f = function
| [] -> []
| h::t -> (f h) :: map f t
```
**Exercise:** Prove that for all trees `t`, `size (reflect t) ~ size t`,
given the following definitions:
```
type 'a tree = Leaf | Branch of 'a * 'a tree * 'a tree
let rec reflect = function
| Leaf -> Leaf
| Branch(x,l,r) -> Branch(x, reflect r, reflect l)
let rec size = function
| Leaf -> 0
| Branch(x,l,r) -> 1 + size l + size r
```
**Exercise:** Prove that for all functions `f`, `g`, and `h` (of
appropriate types), `(f @@ g) @@ h ~ f @@ (g @@ h)`, where `(@@)`
is defined as follows:
```
let (@@) f g x = f (g x)
```
** *Exercise:** Prove that for all lists `xs`, and for all
lists `ys`, `rev_append xs ys ~ (nrev xs) @ ys`, where `rev_append`
and `nrev` are defined as follows:
```
let rec rev_append l1 l2 =
match l1 with
| [] -> l2
| h :: t -> rev_append t (h :: l2)
let rec nrev = function
| [] -> []
| h::t -> (nrev t) @ [h]
```
*Hint: you will need to use and prove the following lemma.*
```
Lemma: for all lists l1, l2, l3, l1 @ (l2 @ l3) ~ (l1 @ l2) @ l3
```
Next, prove that for all lists `xs`, `rev xs ~ nrev xs`, where
`rev` is defined as follows:
```
let rev xs = rev_append xs []
```
*Hint: state and prove a lemma.*
Note that this definition of `rev` is, in fact, how OCaml's `List.rev` is defined.
You have therefore proved the correctness of a tail-recursive implementation of list
reversal by showing its equivalence to a non-tail-recursive implementation.
]]>