euler001.mlw 2.7 KB
 MARCHE Claude committed Apr 10, 2011 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 committed Sep 28, 2011 10 11 12 ``````theory DivModHints use import int.Int `````` MARCHE Claude committed Sep 28, 2011 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 committed Sep 28, 2011 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 `````` MARCHE Claude committed Apr 10, 2011 37 38 39 40 `````` theory SumMultiple use import int.Int `````` MARCHE Claude committed Sep 28, 2011 41 `````` use import int.ComputerDivision `````` MARCHE Claude committed Apr 10, 2011 42 `````` `````` Jean-Christophe Filliâtre committed May 20, 2011 43 `````` (* [sum_multiple_3_5_lt n] is the sum of all the multiples `````` MARCHE Claude committed Apr 10, 2011 44 `````` of 3 or 5 below n] *) `````` Andrei Paskevich committed Jun 29, 2011 45 `````` function sum_multiple_3_5_lt int : int `````` MARCHE Claude committed Apr 10, 2011 46 47 48 49 `````` axiom SumEmpty: sum_multiple_3_5_lt 0 = 0 axiom SumNo : forall n:int. n >= 0 -> `````` Andrei Paskevich committed Jun 29, 2011 50 `````` mod n 3 <> 0 /\ mod n 5 <> 0 -> `````` MARCHE Claude committed Apr 10, 2011 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 committed Jun 29, 2011 54 `````` mod n 3 = 0 \/ mod n 5 = 0 -> `````` MARCHE Claude committed Apr 10, 2011 55 56 `````` sum_multiple_3_5_lt (n+1) = sum_multiple_3_5_lt n + n `````` Andrei Paskevich committed Jun 29, 2011 57 `````` function closed_formula (n:int) : int = `````` MARCHE Claude committed Apr 10, 2011 58 59 60 `````` let n3 = div n 3 in let n5 = div n 5 in let n15 = div n 15 in `````` Jean-Christophe Filliâtre committed May 20, 2011 61 62 63 `````` div (3 * n3 * (n3+1) + 5 * n5 * (n5+1) - 15 * n15 * (n15+1)) 2 `````` MARCHE Claude committed Apr 10, 2011 64 `````` `````` Andrei Paskevich committed Jun 29, 2011 65 `````` predicate p (n:int) = sum_multiple_3_5_lt (n+1) = closed_formula n `````` MARCHE Claude committed Apr 10, 2011 66 67 68 `````` lemma Closed_formula_0: p 0 `````` MARCHE Claude committed Sep 28, 2011 69 70 `````` use DivModHints `````` MARCHE Claude committed Sep 28, 2011 71 72 73 74 `````` lemma mod_15: forall n:int. mod n 15 = 0 <-> mod n 3 = 0 /\ mod n 5 = 0 `````` MARCHE Claude committed Sep 06, 2011 75 `````` lemma Closed_formula_n: `````` Jean-Christophe Filliâtre committed May 20, 2011 76 `````` forall n:int. n > 0 -> p (n-1) -> `````` Andrei Paskevich committed Jun 29, 2011 77 `````` mod n 3 <> 0 /\ mod n 5 <> 0 -> p n `````` MARCHE Claude committed Apr 10, 2011 78 `````` `````` MARCHE Claude committed Sep 06, 2011 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: `````` MARCHE Claude committed Apr 10, 2011 88 `````` forall n:int. n > 0 -> p (n-1) -> `````` MARCHE Claude committed Sep 06, 2011 89 `````` mod n 3 = 0 /\ mod n 5 = 0 -> p n `````` MARCHE Claude committed Apr 10, 2011 90 `````` `````` Andrei Paskevich committed Jun 29, 2011 91 `````` clone int.Induction as I with predicate p = p `````` MARCHE Claude committed Apr 10, 2011 92 `````` `````` Jean-Christophe Filliâtre committed May 20, 2011 93 `````` lemma Closed_formula: `````` MARCHE Claude committed Apr 10, 2011 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 `````` MARCHE Claude committed Sep 28, 2011 102 `````` use import int.ComputerDivision `````` MARCHE Claude committed Apr 10, 2011 103 `````` `````` Jean-Christophe Filliâtre committed May 20, 2011 104 `````` let solve n = `````` MARCHE Claude committed Apr 10, 2011 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 } `````` Jean-Christophe Filliâtre committed May 20, 2011 112 113 114 115 116 117 118 119 ``````end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/euler001.gui" End: *) ``````