euler001.mlw 2.7 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
theory DivModHints

  use import int.Int
13 14 15 16 17
  use import int.ComputerDivision

  lemma mod_div_unique :
    forall x y q r:int. y > 0 /\ x = q*y + r /\ 0 <= r < y ->
      r = mod x y /\ q = div x y
MARCHE Claude's avatar
MARCHE Claude committed
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36

  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

37 38 39 40

theory SumMultiple

  use import int.Int
41
  use import int.ComputerDivision
42

43
  (* [sum_multiple_3_5_lt n] is the sum of all the multiples
44
     of 3 or 5 below n] *)
Andrei Paskevich's avatar
Andrei Paskevich committed
45
  function sum_multiple_3_5_lt int : int
46 47 48 49

  axiom SumEmpty: sum_multiple_3_5_lt 0 = 0

  axiom SumNo : forall n:int. n >= 0 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
50
    mod n 3 <> 0 /\ mod n 5 <> 0 ->
51 52 53
    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
54
    mod n 3 = 0 \/ mod n 5 = 0 ->
55 56
    sum_multiple_3_5_lt (n+1) = sum_multiple_3_5_lt n + n

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

Andrei Paskevich's avatar
Andrei Paskevich committed
65
  predicate p (n:int) = sum_multiple_3_5_lt (n+1) = closed_formula n
66 67 68

  lemma Closed_formula_0: p 0

MARCHE Claude's avatar
MARCHE Claude committed
69 70
  use DivModHints

71 72 73 74
  lemma mod_15:
    forall n:int.
      mod n 15 = 0 <-> mod n 3 = 0 /\ mod n 5 = 0

MARCHE Claude's avatar
MARCHE Claude committed
75
  lemma Closed_formula_n:
76
    forall n:int. n > 0 -> p (n-1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
77
      mod n 3 <> 0 /\ mod n 5 <> 0 -> p n
78

MARCHE Claude's avatar
MARCHE Claude committed
79 80 81 82 83 84 85 86 87
  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:
88
    forall n:int. n > 0 -> p (n-1) ->
MARCHE Claude's avatar
MARCHE Claude committed
89
      mod n 3 = 0 /\ mod n 5 = 0 -> p n
90

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

93
  lemma Closed_formula:
94 95 96 97 98 99 100 101
    forall n:int. 0 <= n -> p n

end

module Euler001

  use import SumMultiple
  use import int.Int
102
  use import int.ComputerDivision
103

104
  let solve n =
105 106 107 108 109 110 111
    { 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 }

112 113 114 115 116 117 118 119
end

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