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