An efficient way to compute the fibonacci function

Here is a definition of the Fibonacci function.

Fixpoint fib (n:nat) : nat :=
  match n with
    0 => 1
  | 1 => 1
  | S ((S p) as q) => fib p + fib q
  end.

Prove the following statements:

  forall n, fib (2*n) = fib (n) * fib (n) + 
           (fib (n+1) - fib n)*(fib (n+1) - fib n).

  forall n, fib (2*n+1) = 2 * fib n * fib (n+1) - fib n * fib n.

  forall n, fib (S (2*n+1)) = fib (n+1) * (fib (n+1)) + fib n * fib n.

Use these formulas to define another function that computes the values of the Fibonacci function for n, with only a logarithmic number of recursive calls (to compute the values for 17 and 18, this function should only compute the values for 8, 9, 4, 5, 2, and 3).

Solution

Follow this link



Pierre Castéran