mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
113 lines
2.7 KiB
Plaintext
113 lines
2.7 KiB
Plaintext
(* 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. *)
|
|
|
|
(** {2 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
|