<![CDATA[
These notes re-present the proofs from lecture.
## Proof 1
```
let rec length = function
| [] -> 0
| _::xs -> 1 + length xs
let rec append xs1 xs2 = match xs1 with
| [] -> xs2
| h::t -> h :: append t xs2
Theorem.
for all lists xs and ys, length (append xs ys) ~ length xs + length ys.
Proof: by induction on xs
Case: xs = []
Show: for all ys, length (append [] ys) ~ length [] + length ys
length (append [] ys)
~ length ys (eval)
~ 0 + length ys (math)
~ length [] + length ys (eval,symm.)
Case: xs = h::t
Show: for all ys, length (append (h::t) ys) ~ length (h::t) + length ys
IH: for all ys, length (append t ys) ~ length t + length ys
length (append (h::t) ys)
~ length (h :: append t ys) (eval)
~ 1 + length (append t ys) (eval)
~ 1 + length t + length ys (IH,congr.)
~ length (h::t) + length ys (eval,symm.,congr.)
QED
```
We'll start omitting facts about ~ in proofs now, unless they are
especially non-obvious. So symmetry, congruence, and transitivity
aren't going to show up too much more.
## Proof 2
```
let (@@) f g x = f (g x)
let map = List.map
Theorem: for all functions f and g, (map f) @@ (map g) ~ map (f @@ g).
Proof:
By extensionality, we need to show that for all xs,
((map f) @@ (map g)) xs ~ map (f @@ g) xs.
By eval, ((map f) @@ (map g)) xs ~ map f (map g xs).
So by transitivity, it suffices to show that
map f (map g xs) ~ map (f @@ g) xs.
We do so by induction on xs.
Case: xs = []
Show: map f (map g []) ~ map (f @@ g) []
map f (map g [])
~ [] (eval)
~ map (f @@ g) [] (eval)
Case: xs = h::t
Show: map f (map g (h::t)) ~ map (f @@ g) (h::t)
IH: map f (map g t) ~ map (f @@ g) t
We include hints, below, as to what eval steps
are being taken.
map f (map g (h::t))
~ map f ((g h)::map g t) (eval map)
~ (f (g h))::map f (map g t) (eval map)
~ ((f @@ g) h)::map f (map g t) (eval @@)
~ ((f @@ g) h)::map (f @@ g) t (IH)
~ map (f @@ g) (h::t) (eval map)
QED
```
## Proof 3
```
Theorem: for all trees t, reflect(reflect t) ~ t.
Proof: by induction on t.
Case: t = Leaf
Show: reflect(reflect Leaf) ~ Leaf
reflect(reflect Leaf)
~ Leaf (eval)
Case: t = Branch(x,l,r)
Show:
reflect(reflect(Branch(x,l,r))) ~ Branch(x,l,r)
IH:
1. reflect(reflect l) ~ l
2. reflect(reflect r) ~ r
reflect(reflect(Branch(x,l,r)))
~ reflect(Branch(x, reflect r, reflect l)) (eval)
~ Branch(x, reflect(reflect l), reflect(reflect r)) (eval)
~ Branch(x, l, reflect(reflect r)) (IH 1)
~ Branch(x, l, r) (IH 2)
QED
```
]]>