fibonacci.mlw

theory Fibonacci "Fibonacci numbers"

  use export int.Int

  function fib int : int

  axiom fib0: fib 0 = 0
  axiom fib1: fib 1 = 1
  axiom fibn: forall n:int. n >= 2 -> fib n = fib (n-1) + fib (n-2)

end

theory FibonacciTest

  use import Fibonacci

  lemma isfib_2_1 : fib 2 = 1
  lemma isfib_6_8 : fib 6 = 8

  lemma not_isfib_2_2 : fib 2 <> 2

end

module FibonacciLinear

  use import Fibonacci
  use import int.Int
  use import ref.Ref

  let fib (n:int) : int
    requires { n >= 0 }
    ensures { fib n = result}
  = let y = ref 0 in
    let x = ref 1 in
    for i = 0 to n - 1 do
      invariant { 0 <= i <= n /\ fib (i+1) = !x /\ fib i = !y }
      let aux = !y in
      y := !x;
      x := !x + aux
    done;
    !y

end

module FibRecGhost "recursive version, using ghost code"

  use import Fibonacci
  use import int.Int

  let rec fib_aux (ghost n: int) (a b k: int) : int
    requires { 0 <= n && a = fib n && b = fib (n+1) }
    ensures  { result = fib (n+k) }
  = if k = 0 then a else fib_aux (n+1) b (a+b) (k-1)

  let fib (n: int) : int
    requires { 0 <= n }
    ensures  { result = fib n }
  = fib_aux 0 0 1 n

end

module FibRecNoGhost "recursive version, without ghost code"

  use import Fibonacci
  use import int.Int

  let rec fib_aux (a b k: int) : int
    requires { exists n: int. 0 <= n && a = fib n && b = fib (n+1) }
    ensures  { forall n: int. 0 <= n && a = fib n && b = fib (n+1) ->
                              result = fib (n+k) }
  = if k = 0 then a else fib_aux b (a+b) (k-1)

  let fib (n: int) : int
    requires { 0 <= n }
    ensures  { result = fib n }
  = fib_aux 0 1 n

end

theory Mat22 "2x2 integer matrices"

  use import int.Int

  type t = { a11: int; a12: int; a21: int; a22: int }

  constant id : t = { a11 = 1; a12 = 0; a21 = 0; a22 = 1 }

  function mult (x: t) (y: t) : t =
    {
    a11 = x.a11 * y.a11 + x.a12 * y.a21; a12 = x.a11 * y.a12 + x.a12 * y.a22;
    a21 = x.a21 * y.a11 + x.a22 * y.a21; a22 = x.a21 * y.a12 + x.a22 * y.a22;
    }

  (* holds, but not useful *)
  (* clone algebra.Assoc with type t = t, function op = mult, lemma Assoc *)

  clone export
    int.Exponentiation with type t = t, function one = id, function (*) = mult

end

module FibonacciLogarithmic

  use import Fibonacci
  use import int.EuclideanDivision
  use import Mat22

  constant m1110 : t = { a11 = 1; a12 = 1;
                         a21 = 1; a22 = 0 }

  (* computes ((1 1) (1 0))^n in O(log(n)) time

     since it is a matrix of the shape ((a+b b) (b a)),
     we only return the pair (a, b) *)

  let rec logfib n variant { n }
    requires { n >= 0 }
    ensures  { let a, b = result in
      power m1110 n = { a11 = a+b; a12 = b; a21 = b; a22 = a } }
  = if n = 0 then
      (1, 0)
    else begin
      let a, b = logfib (div n 2) in
      let c = a + b in
      if mod n 2 = 0 then
        (a*a + b*b, b*(a + c))
      else
        (b*(a + c), c*c + b*b)
    end

  (* by induction, we easily prove that

     (1 1)^n = (F(n+1) F(n)  )
     (1 0)     (F(n)   F(n-1))

    thus, we can compute F(n) in O(log(n)) using funtion logfib above
  *)

  lemma fib_m :
    forall n: int. n >= 0 ->
    let p = power m1110 n in fib (n+1) = p.a11 /\ fib n = p.a21

  let fibo n requires { n >= 0 } ensures { result = fib n } =
    let _, b = logfib n in b


  let test0 () = fibo 0
  let test1 () = fibo 1
  let test7 () = fibo 7
  let test42 () = fibo 42

end