<![CDATA[
These notes re-present the proofs from lecture.
## Proof 1
```
let easy x y z = x * (y + z)
Theorem: easy 1 20 30 ~ 50
Proof:
easy 1 20 30
~ 50 (by eval)
QED
```
## Proof 2
```
let easy x y z = x * (y + z)
Theorem: easy a b c ~ easy a c b
Proof:
easy a b c
~ a * (b + c) (by eval)
~ a * (c + b) (by math)
~ easy a c b (by eval, symm.)
QED
```
## Proof 3
```
let rec even n =
match n with
| 0 -> true
| 1 -> false
| n -> even (n-2)
Theorem:
for all natural numbers n, even (2*n) ~ true.
Proof: by induction on n
Case: n = 0
Show: even (2*0) ~ true
even (2*0)
~ even 0 (math,congr.)
~ true (eval)
Case: n = k+1, where k >= 0
IH: even (2*k) ~ true
Show: even (2*(k+1)) ~ true
even (2*(k+1))
~ even (2*k+2) (math,congr.)
~ even (2*k+2-2) (eval,k>=0)
~ even (2*k) (math,congr.)
~ true (IH)
QED
```
]]>