(** {1 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 DivModHints use int.Int use int.ComputerDivision lemma mod_div_unique : forall x y q r:int. x >= 0 /\ y > 0 /\ x = q*y + r /\ 0 <= r < y -> q = div x y /\ r = mod x y lemma mod_succ_1 : forall x y:int. x >= 0 /\ y > 0 -> mod (x+1) y <> 0 -> mod (x+1) y = (mod x y) + 1 lemma mod_succ_2 : forall x y:int. x >= 0 /\ y > 0 -> mod (x+1) y = 0 -> mod x y = y-1 lemma div_succ_1 : forall x y:int. x >= 0 /\ y > 0 -> mod (x+1) y = 0 -> div (x+1) y = (div x y) + 1 lemma div_succ_2 : forall x y:int. x >= 0 /\ y > 0 -> mod (x+1) y <> 0 -> div (x+1) y = (div x y) lemma mod2_mul2: forall x:int. mod (2 * x) 2 = 0 lemma mod2_mul2_aux: forall x y:int. mod (y * (2 * x)) 2 = 0 lemma mod2_mul2_aux2: forall x y z t:int. mod (y * (2 * x) + z * (2 * t)) 2 = 0 lemma div2_mul2: forall x:int. div (2 * x) 2 = x lemma div2_mul2_aux: forall x y:int. div (y * (2 * x)) 2 = y * x lemma div2_add: forall x y:int. mod x 2 = 0 /\ mod y 2 = 0 -> div (x+y) 2 = div x 2 + div y 2 lemma div2_sub: forall x y:int. mod x 2 = 0 /\ mod y 2 = 0 -> div (x-y) 2 = div x 2 - div y 2 end theory TriangularNumbers use int.Int use int.ComputerDivision use int.Div2 use DivModHints as DMH lemma tr_mod_2: forall n:int. n >= 0 -> mod (n*(n+1)) 2 = 0 function tr (n:int) : int = div (n*(n+1)) 2 lemma tr_repr: forall n:int. n >= 0 -> n*(n+1) = 2 * tr n lemma tr_succ: forall n:int. n >= 0 -> tr (n+1) = tr n + n + 1 end theory SumMultiple use int.Int use int.ComputerDivision (* [sum_multiple_3_5_lt n] is the sum of all the multiples of 3 or 5 below n] *) function 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 /\ 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 \/ mod n 5 = 0 -> sum_multiple_3_5_lt (n+1) = sum_multiple_3_5_lt n + n use TriangularNumbers function closed_formula_aux (n:int) : int = let n3 = div n 3 in let n5 = div n 5 in let n15 = div n 15 in 3 * tr n3 + 5 * tr n5 - 15 * tr n15 predicate p (n:int) = sum_multiple_3_5_lt (n+1) = closed_formula_aux n use DivModHints as DMH lemma mod_15: forall n:int. mod n 15 = 0 <-> mod n 3 = 0 /\ mod n 5 = 0 lemma Closed_formula_0: p 0 lemma Closed_formula_n: forall n:int. n > 0 -> p (n-1) -> mod n 3 <> 0 /\ mod n 5 <> 0 -> p n lemma Closed_formula_n_3: forall n:int. n > 0 -> p (n-1) -> mod n 3 = 0 /\ mod n 5 <> 0 -> p n lemma Closed_formula_n_5: forall n:int. n > 0 -> p (n-1) -> mod n 3 <> 0 /\ mod n 5 = 0 -> p n lemma Closed_formula_n_15: forall n:int. n > 0 -> p (n-1) -> mod n 3 = 0 /\ mod n 5 = 0 -> p n constant b : int = 0 clone int.Induction as I with constant bound = b, predicate p = p lemma Closed_formula_ind: forall n:int. 0 <= n -> p n function 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 div_15: forall n:int. 0 <= n -> div n 15 >= 0 lemma div_5: forall n:int. 0 <= n -> div n 5 >= 0 lemma div_3: forall n:int. 0 <= n -> div n 3 >= 0 lemma Closed_Formula: forall n:int. 0 <= n -> sum_multiple_3_5_lt (n+1) = closed_formula n end module Euler001 use SumMultiple use int.Int use mach.int.Int let solve n requires { n >= 1 } ensures { result = sum_multiple_3_5_lt n } = let n3 = (n-1) / 3 in let n5 = (n-1) / 5 in let n15 = (n-1) / 15 in (3 * n3 * (n3+1) + 5 * n5 * (n5+1) - 15 * n15 * (n15+1)) / 2 (** Small test. Run it with why3 examples/euler001.mlw --exec Euler001.run *) let run () = solve 1000 (* should return 233168 *) (** for the Why3 bench *) exception BenchFailure let bench () raises { BenchFailure -> true } = let x = run () in if x <> 233168 then raise BenchFailure; x (** for extraction *) (* use string.Char use io.StdIO use ref.Ref let go () ensures { !cur_linenum = (old !cur_linenum) + 1 } = print_char (chr 71); (* G *) print_char (chr 79); (* O *) print_char (chr 58); (* : *) print_char (chr 32); (* *) print_int (run ()); print_newline () *) end