euler001.mlw 2.5 KB
Newer Older
1 2 3 4 5 6 7 8 9
(* 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.

*)

MARCHE Claude's avatar
MARCHE Claude committed
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
theory DivModHints

  use import int.Int
  use import int.EuclideanDivision

  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)

end

33 34 35 36 37 38

theory SumMultiple

  use import int.Int
  use import int.EuclideanDivision

39
  (* [sum_multiple_3_5_lt n] is the sum of all the multiples
40
     of 3 or 5 below n] *)
Andrei Paskevich's avatar
Andrei Paskevich committed
41
  function sum_multiple_3_5_lt int : int
42 43 44 45

  axiom SumEmpty: sum_multiple_3_5_lt 0 = 0

  axiom SumNo : forall n:int. n >= 0 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
46
    mod n 3 <> 0 /\ mod n 5 <> 0 ->
47 48 49
    sum_multiple_3_5_lt (n+1) = sum_multiple_3_5_lt n

  axiom SumYes: forall n:int. n >= 0 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
50
    mod n 3 = 0 \/ mod n 5 = 0 ->
51 52
    sum_multiple_3_5_lt (n+1) = sum_multiple_3_5_lt n + n

Andrei Paskevich's avatar
Andrei Paskevich committed
53
  function closed_formula (n:int) : int =
54 55 56
    let n3 = div n 3 in
    let n5 = div n 5 in
    let n15 = div n 15 in
57 58 59
    div (3 * n3 * (n3+1) +
         5 * n5 * (n5+1) -
         15 * n15 * (n15+1)) 2
60

Andrei Paskevich's avatar
Andrei Paskevich committed
61
  predicate p (n:int) = sum_multiple_3_5_lt (n+1) = closed_formula n
62 63 64

  lemma Closed_formula_0: p 0

MARCHE Claude's avatar
MARCHE Claude committed
65 66
  use DivModHints

MARCHE Claude's avatar
MARCHE Claude committed
67
  lemma Closed_formula_n:
68
    forall n:int. n > 0 -> p (n-1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
69
      mod n 3 <> 0 /\ mod n 5 <> 0 -> p n
70

MARCHE Claude's avatar
MARCHE Claude committed
71 72 73 74 75 76 77 78 79
  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:
80
    forall n:int. n > 0 -> p (n-1) ->
MARCHE Claude's avatar
MARCHE Claude committed
81
      mod n 3 = 0 /\ mod n 5 = 0 -> p n
82

Andrei Paskevich's avatar
Andrei Paskevich committed
83
  clone int.Induction as I with predicate p = p
84

85
  lemma Closed_formula:
86 87 88 89 90 91 92 93 94 95
    forall n:int. 0 <= n -> p n

end

module Euler001

  use import SumMultiple
  use import int.Int
  use import int.EuclideanDivision

96
  let solve n =
97 98 99 100 101 102 103
    { 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 }

104 105 106 107 108 109 110 111
end

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/euler001.gui"
End:
*)