- A simple program using dichotomy, computing (x^(n/2))^2 (power.v)
power x 0 = 1
power x 2n = let v = (power x n) in v*v
power x 2n+1 = x*(power x 2n)
- Using the property x^n=(x^2)^(n/2) when n is even (power2.v)
power x 0 = 1
power x 2n = power (sqr x) n
power x 2n+1 = x*(power x 2n)
- A tail recursive program using dichotomy (power_iter.v)
power x 0 acc = acc
power x 2n acc = power (sqr x) n acc
power x 2n+1 = power x 2n (x*acc)
- A cps-style program (power_cps.v)
power x 0 f = (f 1)
power x 2n f = power (sqr x) n (fun r -> f r)
power x 2n+1 f = power x 2n (fun r -> f (r*x))
- Comments
All these definitions require using well-founded recursion.
To make proving properties about these functions easier, we define a dedicated induction principle on
natural numbers (power_ind.v). This induction principle follows the structure of the power functions.
Each file contains a proof of the following example lemma:
Lemma power_neg_odd_neg :
forall a:Z, (a<0) -> forall n:nat, (odd n)->(0>power a n).