Binet: THEORY

BEGIN

%
% For Binet's formula, we will index the Fibbonacci sequence from 1
%

fib(n:nat): RECURSIVE nat =
  (IF    n = 0 THEN 1
   ELSIF n = 1 THEN 1
               ELSE fib(n - 1) + fib(n - 2)
   ENDIF)
  MEASURE n

%
% Challenge: prove Binet's formula
%

% Give a name to the square root of 5,
% and axiomatize its existence

rt5: real
rootfive: AXIOM rt5 * rt5 = 5

%
% You may want to develop some lemmas...
%

%
% Binet's formula
%

thm_Binet: THEOREM
  (FORALL (k:nat):
          fib(k) = (expt((1 + rt5)/2, k+1) - expt((1 - rt5)/2, k+1))/rt5  )

END Binet