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 }
= 0 (* TODO: replace with a definition *)

(* 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 }
= () (* TODO: provide body and variant *)

(* 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 }
= () (* TODO: provide body and variant *)

(* 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 (* TODO: invariant *)
    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 (* TODO: invariant *)
    b <- a + b;
    a <- b - a
  done;
  return a