## Sum of even-valued Fibonacci numbers

Program inspired from Euler project problem #002: find the sum of the even-valued Fibonacci numbers that do not exceed a given bound

Authors: Claude Marché

Topics: Mathematics / Divisibility / Ghost code

Tools: Why3

References: Project Euler

see also the index (by topic, by tool, by reference, by year)

```(* Euler Project, problem 2

Each new term in the Fibonacci sequence is generated by adding the
previous two terms. By starting with 1 and 2, the first 10 terms will
be:

1, 2, 3, 5, 8, 13, 21, 34, 55, 89, ...

By considering the terms in the Fibonacci sequence whose values do not
exceed four million, find the sum of the even-valued terms. *)

```

## Sum of even-valued Fibonacci numbers

```theory FibSumEven

use int.Int
use int.Fibonacci
use int.ComputerDivision

(* [fib_sum_even m n] is the sum of even-valued terms of the
Fibonacci sequence from index 0 to n-1, that do not exceed m *)
function fib_sum_even int int : int

axiom SumZero: forall m:int. fib_sum_even m 0 = 0

axiom SumEvenLe: forall n m:int.
n >= 0 -> fib n <= m -> mod (fib n) 2 = 0 ->
fib_sum_even m (n+1) = fib_sum_even m n + fib n

axiom SumEvenGt: forall n m:int.
n >= 0 -> fib n > m -> mod (fib n) 2 = 0 ->
fib_sum_even m (n+1) = fib_sum_even m n

axiom SumOdd: forall n m:int.
n >= 0 -> mod (fib n) 2 <> 0 ->
fib_sum_even m (n+1) = fib_sum_even m n

predicate is_fib_sum_even (m:int) (sum:int) =
exists n:int.
sum = fib_sum_even m n /\ fib n > m
(* Note: we take for granted that [fib] is an
increasing sequence *)

end

module FibOnlyEven

use int.Int
use int.ComputerDivision
use int.Fibonacci

let rec lemma fib_even_3n (n:int)
requires { n >= 0 }
variant { n }
ensures { mod (fib n) 2 = 0 <-> mod n 3 = 0 }
= if n > 2 then fib_even_3n (n-3)

function fib_even (n: int) : int = fib (3 * n)

lemma fib_even0: fib_even 0 = 0
lemma fib_even1: fib_even 1 = 2

lemma fib_evenn: forall n:int [fib_even n].
n >= 2 -> fib_even n = 4 * fib_even (n-1) + fib_even (n-2)

end

module Solve

use int.Int
use ref.Ref
use int.Fibonacci
use FibSumEven
use FibOnlyEven

let f m : int
requires { m >= 0 }
ensures  { exists n:int. result = fib_sum_even m n /\ fib n > m }
= let x = ref 0 in
let y = ref 2 in
let sum = ref 0 in
let ghost n = ref 0 in
let ghost k = ref 0 in
while !x <= m do
invariant { !n >= 0 }
invariant { !k >= 0 }
invariant { !x = fib_even !n }
invariant { !x = fib !k }
invariant { !y = fib_even (!n+1) }
invariant { !y = fib (!k+3) }
invariant { !sum = fib_sum_even m !k }
invariant { 0 <= !x < !y }
variant { m - !x }
let tmp = !x in
x := !y;
y := 4 * !y + tmp;
sum := !sum + tmp;
n := !n + 1;
k := !k + 3
done;
!sum

let run () = f 4_000_000 (* should be 4613732 *)

exception BenchFailure

let bench () raises { BenchFailure -> true } =
let x = run () in
if x <> 4613732 then raise BenchFailure;
x

end
```