euler001.mlw 4.58 KB
 Andrei Paskevich committed Oct 13, 2012 1 ``````(** {1 Euler Project, problem 1} `````` MARCHE Claude committed Apr 10, 2011 2 3 4 5 `````` 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. `````` Andrei Paskevich committed Oct 13, 2012 6 ``````Find the sum of all the multiples of 3 or 5 below 1000.*) `````` MARCHE Claude committed Apr 10, 2011 7 `````` `````` MARCHE Claude committed Sep 28, 2011 8 9 ``````theory DivModHints `````` Andrei Paskevich committed Jun 15, 2018 10 11 `````` use int.Int use int.ComputerDivision `````` MARCHE Claude committed Sep 28, 2011 12 13 `````` lemma mod_div_unique : `````` MARCHE Claude committed Sep 29, 2011 14 `````` forall x y q r:int. x >= 0 /\ y > 0 /\ x = q*y + r /\ 0 <= r < y -> `````` MARCHE Claude committed May 08, 2012 15 `````` q = div x y /\ r = mod x y `````` MARCHE Claude committed Sep 28, 2011 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 `````` 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) `````` MARCHE Claude committed May 08, 2012 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 `````` 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 `````` Andrei Paskevich committed Jun 15, 2018 60 61 62 `````` use int.Int use int.ComputerDivision use int.Div2 `````` Andrei Paskevich committed Jun 15, 2018 63 `````` use DivModHints as DMH `````` MARCHE Claude committed May 08, 2012 64 65 66 67 68 69 70 71 72 73 74 75 `````` 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 `````` MARCHE Claude committed Sep 28, 2011 76 77 ``````end `````` MARCHE Claude committed Apr 10, 2011 78 79 80 `````` theory SumMultiple `````` Andrei Paskevich committed Jun 15, 2018 81 82 `````` use int.Int use int.ComputerDivision `````` MARCHE Claude committed Apr 10, 2011 83 `````` `````` Jean-Christophe Filliatre committed May 20, 2011 84 `````` (* [sum_multiple_3_5_lt n] is the sum of all the multiples `````` MARCHE Claude committed Apr 10, 2011 85 `````` of 3 or 5 below n] *) `````` Andrei Paskevich committed Jun 29, 2011 86 `````` function sum_multiple_3_5_lt int : int `````` MARCHE Claude committed Apr 10, 2011 87 88 89 90 `````` axiom SumEmpty: sum_multiple_3_5_lt 0 = 0 axiom SumNo : forall n:int. n >= 0 -> `````` Andrei Paskevich committed Jun 29, 2011 91 `````` mod n 3 <> 0 /\ mod n 5 <> 0 -> `````` MARCHE Claude committed Apr 10, 2011 92 93 94 `````` 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 95 `````` mod n 3 = 0 \/ mod n 5 = 0 -> `````` MARCHE Claude committed Apr 10, 2011 96 97 `````` sum_multiple_3_5_lt (n+1) = sum_multiple_3_5_lt n + n `````` Andrei Paskevich committed Jun 15, 2018 98 `````` use TriangularNumbers `````` MARCHE Claude committed May 08, 2012 99 100 `````` function closed_formula_aux (n:int) : int = `````` MARCHE Claude committed Apr 10, 2011 101 102 103 `````` let n3 = div n 3 in let n5 = div n 5 in let n15 = div n 15 in `````` MARCHE Claude committed May 08, 2012 104 `````` 3 * tr n3 + 5 * tr n5 - 15 * tr n15 `````` MARCHE Claude committed Apr 10, 2011 105 `````` `````` MARCHE Claude committed May 08, 2012 106 `````` predicate p (n:int) = sum_multiple_3_5_lt (n+1) = closed_formula_aux n `````` MARCHE Claude committed Apr 10, 2011 107 `````` `````` Andrei Paskevich committed Jun 15, 2018 108 `````` use DivModHints as DMH `````` MARCHE Claude committed Sep 28, 2011 109 `````` `````` MARCHE Claude committed Sep 28, 2011 110 111 112 113 `````` lemma mod_15: forall n:int. mod n 15 = 0 <-> mod n 3 = 0 /\ mod n 5 = 0 `````` MARCHE Claude committed May 08, 2012 114 `````` lemma Closed_formula_0: p 0 `````` MARCHE Claude committed Sep 29, 2011 115 `````` `````` MARCHE Claude committed Sep 06, 2011 116 `````` lemma Closed_formula_n: `````` MARCHE Claude committed May 08, 2012 117 118 `````` forall n:int. n > 0 -> p (n-1) -> mod n 3 <> 0 /\ mod n 5 <> 0 -> p n `````` MARCHE Claude committed Apr 10, 2011 119 `````` `````` MARCHE Claude committed Sep 06, 2011 120 `````` lemma Closed_formula_n_3: `````` MARCHE Claude committed May 08, 2012 121 122 `````` forall n:int. n > 0 -> p (n-1) -> mod n 3 = 0 /\ mod n 5 <> 0 -> p n `````` MARCHE Claude committed Sep 06, 2011 123 124 `````` lemma Closed_formula_n_5: `````` MARCHE Claude committed May 08, 2012 125 126 `````` forall n:int. n > 0 -> p (n-1) -> mod n 3 <> 0 /\ mod n 5 = 0 -> p n `````` MARCHE Claude committed Sep 06, 2011 127 128 `````` lemma Closed_formula_n_15: `````` MARCHE Claude committed May 08, 2012 129 130 `````` forall n:int. n > 0 -> p (n-1) -> mod n 3 = 0 /\ mod n 5 = 0 -> p n `````` MARCHE Claude committed Apr 10, 2011 131 `````` `````` MARCHE Claude committed May 08, 2012 132 `````` constant b : int = 0 `````` MARCHE Claude committed Apr 10, 2011 133 `````` `````` MARCHE Claude committed May 08, 2012 134 135 136 `````` clone int.Induction as I with constant bound = b, predicate p = p lemma Closed_formula_ind: `````` MARCHE Claude committed Apr 10, 2011 137 138 `````` forall n:int. 0 <= n -> p n `````` MARCHE Claude committed May 08, 2012 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 `````` 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 `````` MARCHE Claude committed Apr 10, 2011 154 155 156 157 ``````end module Euler001 `````` Andrei Paskevich committed Jun 15, 2018 158 159 160 `````` use SumMultiple use int.Int use mach.int.Int `````` MARCHE Claude committed Apr 10, 2011 161 `````` `````` Andrei Paskevich committed Oct 13, 2012 162 163 164 `````` let solve n requires { n >= 1 } ensures { result = sum_multiple_3_5_lt n } `````` Mário Pereira committed Feb 19, 2017 165 166 167 168 `````` = 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 `````` MARCHE Claude committed Apr 10, 2011 169 `````` `````` MARCHE Claude committed Apr 24, 2014 170 171 172 173 174 `````` (** Small test. Run it with why3 examples/euler001.mlw --exec Euler001.run *) `````` MARCHE Claude committed Aug 22, 2013 175 `````` let run () = solve 1000 `````` MARCHE Claude committed Jan 14, 2014 176 177 `````` (* should return 233168 *) `````` MARCHE Claude committed Apr 24, 2014 178 `````` (** for the Why3 bench *) `````` Jean-Christophe Filliatre committed Feb 18, 2014 179 `````` exception BenchFailure `````` MARCHE Claude committed Jan 14, 2014 180 181 `````` let bench () raises { BenchFailure -> true } = `````` MARCHE Claude committed Feb 03, 2014 182 183 184 `````` let x = run () in if x <> 233168 then raise BenchFailure; x `````` MARCHE Claude committed Jan 14, 2014 185 `````` `````` MARCHE Claude committed Apr 24, 2014 186 187 `````` (** for extraction *) `````` MARCHE Claude committed Jul 19, 2016 188 ``````(* `````` Andrei Paskevich committed Jun 15, 2018 189 190 191 `````` use string.Char use io.StdIO use ref.Ref `````` MARCHE Claude committed Apr 24, 2014 192 `````` `````` MARCHE Claude committed Jul 19, 2016 193 `````` let go () `````` MARCHE Claude committed Apr 26, 2014 194 `````` ensures { !cur_linenum = (old !cur_linenum) + 1 } `````` MARCHE Claude committed Jul 19, 2016 195 `````` = `````` MARCHE Claude committed Apr 24, 2014 196 197 198 199 200 201 `````` print_char (chr 71); (* G *) print_char (chr 79); (* O *) print_char (chr 58); (* : *) print_char (chr 32); (* *) print_int (run ()); print_newline () `````` MARCHE Claude committed Jul 19, 2016 202 ``````*) `````` MARCHE Claude committed Apr 24, 2014 203 `````` `````` Jean-Christophe Filliatre committed May 20, 2011 204 ``end``