<![CDATA[
**Exercise:** Prove that for all integers `x`, `double x ~ 2*x`, where `double`
is defined as follows:
```
let double n =
n + n
```
**Exercise:** Prove that for all integers `a` and natural numbers `x`,
`exp a x ~ a ** x`, where `**` denotes the mathematical operation
of integer exponentiation (hence overloading the built-in `**` operator),
and where `exp` is defined as follows:
```
let rec exp a x =
if x = 0 then 1
else a*(exp a (x-1))
```
Use the following as a template for your proof about `exp`:
```
Theorem: for all ints a, for all naturals x, exp a x ~ a ** x
Proof: by induction on x
Case: x=0
Show: TODO
TODO
Case: x=k+1, where k >= 0
Show: TODO
IH: TODO
TODO
QED
```
**Exercise:** Prove that for all natural numbers n,
`sum_sqrs n ~ (n * (n+1) * (2*n + 1))/6`, where
`sum_sqrs` is defined as follows:
```
let rec sum_sqrs n =
if n <= 0 then 0
else (n*n) + sum_sqrs(n-1)
```
**Exercise:** Prove that for all natural numbers n and
for all ints p,
`facti n p ~ n! * p`, where `facti` is defined as follows:
```
(* A tail-recursive (sometimes called *iterative*) generalization of the
usual factorial function.
precondition: n >= 0 *)
let rec facti n p =
if n = 0 then p
else facti (n-1) (n*p)
```
Use the following as a template for your proof about `facti`.
Note carefully how induction on `n` leaves `p` universally
quantified—which you will need to finish the second case.
```
Theorem: for all naturals n, for all ints p, facti n p ~ n! * p
Proof: by induction on n
Case: n=0
Show: for all ints p, facti 0 p ~ 0! * p
TODO
Case: n=k+1, where k >= 0
Show: for all ints p, facti (k+1) p ~ (k+1)! * p
IH: for all ints p, facti k p ~ k! * p
TODO
QED
```
**Exercise:** Prove that for all natural numbers n,
`fact n ~ n!`, where `fact` is defined as follows:
```
let fact n = facti n 1
```
*Hint: use the previous theorem as a lemma.*
**Note:** Let `fact` have the following *specification*:
```
(* precondition: n >= 0 *)
(* postcondition: (fact n) = n! *)
val fact : int -> int
```
You have proven the correctness of a tail-recursive implementation
of the factorial function. Reflect on why that is so.
** *Exercise:**
The recursive implementation of `exp`, above, is inefficient.
Implement [exponentiation by squaring][exp-square]
in OCaml. Prove the correctness of your implementation. Use the proofs
you did for `fact` as an inspiration.
*Hint: recall strong induction (aka [complete induction][compl-ind]).*
[exp-square]: https://en.wikipedia.org/wiki/Exponentiation_by_squaring
[compl-ind]: https://en.wikipedia.org/wiki/Mathematical_induction#Complete_induction
]]>