<![CDATA[
# Induction and Recursion
Today we will practice proving behavioral equivalence of expressions
involving variants and functions.
##### Exercise: behead [✭]
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: noop [✭✭]
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
```
##### Exercise: append assoc [✭✭]
Prove that for all lists `l1`, `l2`, and `l3`,
it holds that `l1 @ (l2 @ l3) ~ (l1 @ l2) @ l3`.
□
##### Exercise: size reflect [✭✭]
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: apply assoc [✭]
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)
```
*Hint: use extensionality; induction is not needed.*
□
## Additional exercises
##### Exercise: map append [✭✭✭]
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: rev_append [✭✭✭]
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: use a previous exercise as a lemma.*
□
##### Exercise: rev [✭✭]
Next, prove that for all lists `xs`, `rev xs ~ nrev xs`, where
`rev` is defined as follows:
```
let rev xs = rev_append xs []
```
*Hint: Make use of previous exercises. You might discover that it would be
helpful to state and prove a relatively simple lemma involving `[]` and `@`.*
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.
□
]]>