euler001.mlw 1.98 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
(* 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