Power over structured numbers
Recall from lecture the OCaml type nat, the function toInt, and the power function working over
this representation of natural numbers:
type nat = Zero | Succ of nat
let toInt = function
| Zero -> 0
| Succ n -> toInt n + 1
let rec power n x = match n with
| Zero -> 1.0
| Succ n'-> x *. power n' x
What is the principle of induction for the type nat?
Using induction over nat values show that
power n x = x^(toInt(n))
Your proof must explicitly and clearly indicate the base case you prove, the inductive case you prove and what the inductive hypothesis provides in the proof.
Each step in your proof must be accompanied by a justication describing why that step could be taken.