Commit 3381699c authored by MARCHE Claude's avatar MARCHE Claude

Euler project problem 2, in progress

parent 4b90dab0
(* 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.
*)
theory Fib "Definition of Fibonacci sequence"
use export int.Int
logic fib int : int
axiom fib0: fib 0 = 1
axiom fib1: fib 1 = 2
axiom fibn: forall n:int [fib n].
n >= 2 -> fib n = fib (n-1) + fib (n-2)
end
theory FibSumEven "sum of even-valued Fibonacci numbers"
use import Fib
use import int.EuclideanDivision
(* [fib_sum_even_lt m] is the sum of even-valued terms
of the Fibonacci sequence that are less than m
[fib_sum_even_lt_from m n] is the sum of even-valued terms
of the Fibonacci sequence that are less than m, starting from n
*)
logic fib_sum_even_lt_from int int : int
axiom SumTooLarge: forall m n:int.
n >= 0 -> (fib n) >= m -> fib_sum_even_lt_from m n = 0
(* Note: we take for granted that [fib] is an
increasing sequence *)
axiom SumYes: forall n m s:int.
n >= 0 -> (fib n) < m -> mod (fib n) 2 = 0 ->
fib_sum_even_lt_from m n = fib_sum_even_lt_from m (n+1) + (fib n)
axiom SumOdd: forall n m s:int.
n >= 0 -> mod (fib n) 2 <> 0 ->
fib_sum_even_lt_from m n = fib_sum_even_lt_from m (n+1)
logic fib_sum_even_lt (m:int) : int = fib_sum_even_lt_from m 0
end
theory FibOnlyEven
use export Fib
use import int.EuclideanDivision
goal smoke0 : false
lemma fib_even : forall n:int. n >= 0 ->
(mod (fib n) 2 = 0 <-> mod n 3 = 1)
goal smoke1 : false
(* we pose xn = f(3n+1), that is
x_0 = 2, x_1 = 8, x_{n+2} = 4 x_{n+1} + x_n
*)
logic fib_even int : int
axiom fib_even0: fib_even 0 = 2
axiom fib_even1: fib_even 1 = 8
axiom fib_evenn: forall n:int [fib_even n].
n >= 2 -> fib_even n = 4 * fib_even (n-1) + fib_even (n-2)
lemma fib_even_correct :
forall n:int. fib_even n = fib (3*n+1)
goal smoke2 : false
use export FibSumEven
end
module Solve
use import module stdlib.Ref
use import FibOnlyEven
let f m : int =
{ m >= 0 }
let x = ref 2 in
let y = ref 8 in
let sum = ref 0 in
while !x < m do
let tmp = !x in
x := !y;
y := 4 * !y + tmp;
sum := !sum + tmp
done;
!sum
{ result = fib_sum_even_lt m }
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment