(** Exponential algorithm on natural numbers *)
Fixpoint fib0 (n:nat) : nat := 
      match n with O => 0
           | (S O) => 1
           | (S (S q as p)) => fib0 p + fib0 q
      end.

(*
Fixpoint fib0 (n:nat) : nat := 
      match n with O => 0
           | (S p => match p with O => 1
                                         | S q => (fib0 p + fib0 q)
                            end
      end.
*)

Time Eval compute in (fib0 25).
Time Eval vm_compute in (fib0 25).

(** Linear algorithm on natural numbers *)

Fixpoint fib1 (a b n : nat) {struct n} : nat := 
      match n with O => a | (S p) => fib1 b (a+b) p end.

Time Eval compute in (fib1 0 1 25).
Time Eval vm_compute in (fib1 0 1 25).

(** Exponential algorithm on binary numbers *)
Require Export ZArith.
Open Scope Z_scope.

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

Time Eval compute in (fib2 25).
Time Eval vm_compute in (fib2 25).

Time Eval compute in (fib2 30).
Time Eval vm_compute in (fib2 30).

(** Linear algorithm on binary numbers *)
Fixpoint fib3 (a b : Z) (n : nat) {struct n} : Z := 
      match n with O => a | (S p) => fib3 b (a+b) p end.

Time Eval compute in (fib3 0 1 25).
Time Eval vm_compute in (fib3 0 1 25).

Time Eval compute in (fib3 0 1 1000).
Time Eval vm_compute in (fib3 0 1 1000).