Fibonacci numbers

F(0) = 0 F(1) = 1 F(n) = F(n-2) + F(n-1) for n >= 2

use int.Int
use array.Array

(* 1. define Fibonacci numbers using `let rec function` *)

let rec function fib (n: int) : int
  requires { n >= 0 } variant { n }
= if n <= 1 then n else fib (n - 2) + fib (n - 1)

(* 2. show that Fibonacci numbers are nonnegative using a recursive
   lemma function *)

let rec lemma fib_nonneg (n: int) : unit
  requires { n >= 0 } ensures { fib n >= 0 }
  variant { n }
= if n > 1 then (fib_nonneg (n - 2); fib_nonneg (n - 1))

(* 3. show again that Fibonacci numbers are nonnegative using a lemma
   function, but this time using a `for` loop *)

let lemma fib_nonneg_loop (n: int) : unit
  requires { n >= 0 } ensures { fib n >= 0 }
= for i = 2 to n do invariant { fib (i - 2) >= 0 /\ fib (i - 1) >= 0 } () done

(* 4. verify the following function that computes `fib n` using
   dynamic programming *)

let compute_fib1 (n: int) : int
  requires { n >= 0 }
  ensures  { result = fib n }
= if n <= 1 then return n;
  let a = Array.make (n + 1) 0 in
  a[1] <- 1;
  for i = 2 to n do invariant { forall j. 0 <= j < i -> a[j] = fib j }
    a[i] <- a[i - 2] + a[i - 1]
  done;
  return a[n]

(* 5. verify the following function that computes `fib n` using two
   variables *)

let compute_fib2 (n: int) : int
  requires { n >= 0 }
  ensures  { result = fib n }
= if n <= 1 then return n;
  let ref a = 0 in
  let ref b = 1 in
  for i = 2 to n + 1 do invariant { a = fib (i - 2) /\ b = fib (i - 1) }
    b <- a + b;
    a <- b - a
  done;
  return a