Reference no: EM132101965

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.