// Dafny module containing functions and lemmas pertaining
// to the Fibonacci sequence.

module Fibonacci {

  /* Defines the classic Fibonacci function, giving rise to the
  ** Fibonacci sequence Fib(0), Fib(1), Fib(2), ..., in which 
  ** each element is the sum of the previous two (with 0 and 1
  ** being the first two, respectively).
  */
  function Fib(n: nat): nat
  {
    if n <= 1 then n
    else Fib(n-2) + Fib(n-1)
  }
  
  
  /* Evaluates to Fib(0) + Fib(1) + ... + Fib(n), the sum of the
  ** first n+1 Fibonacci numbers.
  */
  function FibSum(n: nat): nat
  {
    if n == 0 then Fib(0)
    else Fib(n) + FibSum(n-1)
  }
  

  // Problem FIB.1
  // -------------
  
  /* Proves that the sum of the first n+1 Fibonacci numbers is
  ** one less than the (n+3)-th Fibonacci number.
  */
  lemma {:induction false} FibSumLemma(n: nat)
    ensures FibSum(n) == Fib(n+2) - 1
  {
    // MISSING PROOF
  }
  
  
  function SquareOf(n: int): int { n*n }
  
  /* Evaluates to the sum of the squares of the
  ** first n+1 Fibonacci numbers.
  */
  function FibSquaredSum(n: nat): nat
  {
    if n == 0 then SquareOf(Fib(0))
    else FibSquaredSum(n-1) + SquareOf(Fib(n))
  }
  
  // Problem FIB.2
  // -------------

  /* Proves that the sum of the squares of the first
  ** n+1 Fibonacci numbers is equal to the product
  ** of the (n+1)-st and (n+2)-nd Fibonacci numbers.
  */
  lemma {:induction false} FibSquaredSumLemma(n: nat)
    ensures FibSquaredSum(n) == Fib(n) * Fib(n+1)
  {
    // PROOF MISSING
  }
  
  /* Evaluates to Fib(0) + Fib(2) + ... + Fib(2n), the sum of
  ** the first n+1 even-indexed Fibonacci numbers.
  */
  function FibSumEvenIndexed(n: nat): nat
  {
    if n == 0 then Fib(0) 
    else FibSumEvenIndexed(n-1) + Fib(2*n)
  }
  
  // Problem FIB.3
  // -------------

  /* Proves that Fib(0) + Fib(2) + ... + Fib(2n) == Fib(2n+1) - 1
  ** (i.e., the sum of the first n+1 even-indexed Fibonacci numbers
  ** is one less than the (n+1)-st odd-indexed Fibonacci number).
  */
  lemma {:induction false} FibSumEvenIndexedLemma(n: nat)
    ensures FibSumEvenIndexed(n) == Fib(2*n+1) - 1
  {
    // PROOF MISSING
  }
  
}