renamed example euler290 -> sum_of_digits

parent ed79c65a
(* How many integers 0 <= n < 10^18 have the property that the sum
of the digits of n equals the sum of digits of 137n?
(**
Projet Euler problem #290
The answer is 20444710234716473.
How many integers 0 <= n < 10^18 have the property that the sum
of the digits of n equals the sum of digits of 137n?
It can be easily computer using memoization (or, equivalently, dynamic
It can be easily computed using memoization (or, equivalently, dynamic
programming) once the problem is generalized as follows:
How many integers 0 <= n < 10^m are such that sd(n) = sd(137n + a) + b?
......@@ -38,7 +39,7 @@ module Euler290
function solution(a b m: int) : int = P.num_of (a,b,10) 0 (power 10 m)
(* short cut for the number of n st n mod 10 = c and ... *)
(* shortcut for the number of n st n mod 10 = c and ... *)
function num_of_modc (d: int3) (x y: int) : int =
let (a,b,c) = d in
......@@ -51,7 +52,7 @@ module Euler290
lemma Empty:
forall a b x y: int. P.num_of (a,b,0) x y = 0
lemma Induc:
forall a b c: int,m:int. 0 <= a -> 0 <= c < 10 -> m > 0 ->
let x = 137 * c + a in
......
......@@ -18,18 +18,18 @@
name="CVC4"
version="1.3"/>
<file
name="../euler290.mlw"
name="../sum_of_digits.mlw"
verified="false"
expanded="true">
<theory
name="Euler290"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="17" loccnumb="7" loccnume="15"
verified="false"
expanded="true">
<goal
name="Base"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="49" loccnumb="8" loccnume="12"
sum="38e1ff8cdd036ae501e4e391a4996777"
proved="true"
......@@ -46,7 +46,7 @@
</goal>
<goal
name="Empty"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="52" loccnumb="8" loccnume="13"
sum="c32555c739e47f2cada745d5d7ac6fb2"
proved="true"
......@@ -63,7 +63,7 @@
</goal>
<goal
name="Induc"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="55" loccnumb="8" loccnume="13"
sum="883a60405607ef56e27231e1f0241da3"
proved="false"
......@@ -72,7 +72,7 @@
</goal>
<goal
name="WP_parameter sd"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="66" loccnumb="10" loccnume="12"
expl="VC for sd"
sum="ff8a9c4c092c4724fa7aef9c54ad1d61"
......@@ -92,7 +92,7 @@
</goal>
<goal
name="WP_parameter f"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="VC for f"
sum="fb58dd1a92816376c4c6ba61f456265f"
......@@ -107,7 +107,7 @@
expanded="true">
<goal
name="WP_parameter f.1"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="1. precondition"
sum="f55d9535d79e1ccc5d637bd6a6e36345"
......@@ -127,7 +127,7 @@
</goal>
<goal
name="WP_parameter f.2"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="2. postcondition"
sum="547ae043f7b7b52d37eab6f5275981f9"
......@@ -147,7 +147,7 @@
</goal>
<goal
name="WP_parameter f.3"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="3. postcondition"
sum="995fd7722e21ed62c5df79928f9f3f68"
......@@ -167,7 +167,7 @@
</goal>
<goal
name="WP_parameter f.4"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="4. loop invariant init"
sum="4ff7d3e9f2fa9786badc98d035a263b6"
......@@ -187,7 +187,7 @@
</goal>
<goal
name="WP_parameter f.5"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="5. variant decrease"
sum="7f01d83c2d87ef6f7783cc3ca5c60f76"
......@@ -207,7 +207,7 @@
</goal>
<goal
name="WP_parameter f.6"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="6. precondition"
sum="d8b2404618ce53e5ab434fa4b19ca019"
......@@ -227,7 +227,7 @@
</goal>
<goal
name="WP_parameter f.7"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="7. assertion"
sum="d9119b0de2e1e314a9c20cb5c9aed143"
......@@ -242,7 +242,7 @@
expanded="false">
<goal
name="WP_parameter f.7.1"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="1."
sum="215e63f1c3cf3703c8c03a808a06db04"
......@@ -262,7 +262,7 @@
</goal>
<goal
name="WP_parameter f.7.2"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="2."
sum="d6019d8336f1d68f09dcaa8d1ad8ec00"
......@@ -282,7 +282,7 @@
</goal>
<goal
name="WP_parameter f.7.3"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="3."
sum="3bb90bb3501687aeeb8359768363d908"
......@@ -304,7 +304,7 @@
</goal>
<goal
name="WP_parameter f.8"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="8. loop invariant preservation"
sum="56a5ede9fa7e4fdbdd6361a3be1df3ae"
......@@ -348,7 +348,7 @@
</goal>
<goal
name="WP_parameter f.9"
locfile="../euler290.mlw"
locfile="../sum_of_digits.mlw"
loclnum="74" loccnumb="10" loccnume="11"
expl="9. postcondition"
sum="9a1a94d88241dbd427d2e8c361f130be"
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment