Commit 4b90dab0 authored by MARCHE Claude's avatar MARCHE Claude

Euler project problem 1 in Why3

parent c6bf0618
(* Euler Project, problem 1
If we list all the natural numbers below 10 that are multiples of 3 or
5, we get 3, 5, 6 and 9. The sum of these multiples is 23.
Find the sum of all the multiples of 3 or 5 below 1000.
*)
theory SumMultiple
use import int.Int
use import int.EuclideanDivision
(* [sum_multiple_3_5_lt n] is the sum of all the multiples
of 3 or 5 below n] *)
logic sum_multiple_3_5_lt int : int
axiom SumEmpty: sum_multiple_3_5_lt 0 = 0
axiom SumNo : forall n:int. n >= 0 ->
mod n 3 <> 0 and mod n 5 <> 0 ->
sum_multiple_3_5_lt (n+1) = sum_multiple_3_5_lt n
axiom SumYes: forall n:int. n >= 0 ->
mod n 3 = 0 or mod n 5 = 0 ->
sum_multiple_3_5_lt (n+1) = sum_multiple_3_5_lt n + n
lemma div_minus1_1 :
forall x y:int. x >= 0 and y > 0 ->
mod (x+1) y = 0 -> div (x+1) y = (div x y) + 1
lemma div_minus1_2 :
forall x y:int. x >= 0 and y > 0 ->
mod (x+1) y <> 0 -> div (x+1) y = (div x y)
logic closed_formula (n:int) : int =
let n3 = div n 3 in
let n5 = div n 5 in
let n15 = div n 15 in
div (3 * n3 * (n3+1) +
5 * n5 * (n5+1) -
15 * n15 * (n15+1)) 2
lemma mod_15 :
forall n:int. n >= 0 ->
mod n 15 = 0 <-> (mod n 3 = 0 and mod n 5 = 0)
logic p (n:int) = sum_multiple_3_5_lt (n+1) = closed_formula n
lemma Closed_formula_0: p 0
lemma Closed_formula_n_1:
forall n:int. n > 0 -> p (n-1) ->
mod n 3 <> 0 and mod n 5 <> 0 -> p n
lemma Closed_formula_n_2:
forall n:int. n > 0 -> p (n-1) ->
mod n 3 = 0 or mod n 5 = 0 -> p n
clone int.Induction as I with logic p = p
lemma Closed_formula:
forall n:int. 0 <= n -> p n
end
module Euler001
use import SumMultiple
use import int.Int
use import int.EuclideanDivision
let solve n =
{ n >= 1 }
let n3 = div (n-1) 3 in
let n5 = div (n-1) 5 in
let n15 = div (n-1) 15 in
div (3 * n3 * (n3+1) + 5 * n5 * (n5+1) - 15 * n15 * (n15+1)) 2
{ result = sum_multiple_3_5_lt n }
end
\ No newline at end of file
......@@ -256,10 +256,17 @@ theory Induction
logic p int
axiom Induction :
lemma Induction :
(forall n:int. 0 <= n -> (forall k:int. 0 <= k < n -> p k) -> p n) ->
forall n:int. 0 <= n -> p n
logic bound : int
lemma Induction_bound :
(forall n:int. bound <= n ->
(forall k:int. bound <= k < n -> p k) -> p n) ->
forall n:int. bound <= n -> p n
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