sum_of_digits.mlw 2.94 KB
 Jean-Christophe Filliatre committed Aug 05, 2011 1 `````` `````` Jean-Christophe Filliatre committed Mar 20, 2014 2 3 ``````(** Projet Euler problem #290 `````` Jean-Christophe Filliatre committed Aug 05, 2011 4 `````` `````` Jean-Christophe Filliatre committed Mar 20, 2014 5 6 `````` 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? `````` Jean-Christophe Filliatre committed Aug 05, 2011 7 `````` `````` Jean-Christophe Filliatre committed Mar 20, 2014 8 `````` It can be easily computed using memoization (or, equivalently, dynamic `````` Jean-Christophe Filliatre committed Aug 05, 2011 9 10 `````` programming) once the problem is generalized as follows: How many integers 0 <= n < 10^m are such that sd(n) = sd(137n + a) + b? `````` 11 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 12 13 `````` In the following, we prove the correctness of a recursive function f which takes m, a, and b as arguments and returns the number of such n. `````` Jean-Christophe Filliatre committed Feb 10, 2014 14 15 `````` Memoization must be added if one wants to solve the initial problem in a reasonable amount of time. `````` Jean-Christophe Filliatre committed Aug 05, 2011 16 `````` (See for instance fib_memo.mlw for an example of memoized function.) *) `````` Jean-Christophe Filliâtre committed Jun 25, 2010 17 `````` `````` Jean-Christophe Filliatre committed Feb 10, 2014 18 19 ``````module Euler290 `````` Jean-Christophe Filliatre committed Dec 30, 2010 20 `````` use import int.Int `````` Andrei Paskevich committed Oct 13, 2012 21 `````` use import ref.Ref `````` Martin Clochard committed Feb 11, 2014 22 `````` use import int.EuclideanDivision as E `````` Jean-Christophe Filliâtre committed Jun 25, 2010 23 `````` use import int.Power `````` Jean-Christophe Filliatre committed Nov 23, 2014 24 `````` use int.NumOf `````` Andrei Paskevich committed Oct 26, 2010 25 `````` `````` Andrei Paskevich committed Jun 29, 2011 26 `````` function sum_digits int : int `````` Andrei Paskevich committed Oct 26, 2010 27 `````` `````` Jean-Christophe Filliatre committed Feb 10, 2014 28 `````` axiom Sum_digits_def: forall n : int. sum_digits n = `````` Andrei Paskevich committed Oct 26, 2010 29 `````` if n <= 0 then 0 else sum_digits (div n 10) + mod n 10 `````` Jean-Christophe Filliâtre committed Jun 25, 2010 30 `````` `````` Jean-Christophe Filliâtre committed Jul 04, 2010 31 32 `````` (* the number of n st 0 <= n mod 10 < c and sd(n) = sd(137n+a)+b *) `````` Jean-Christophe Filliatre committed Nov 23, 2014 33 `````` predicate p (a b c n: int) = `````` Andrei Paskevich committed Jun 29, 2011 34 `````` 0 <= mod n 10 < c /\ sum_digits n = sum_digits (137 * n + a) + b `````` Jean-Christophe Filliâtre committed Jul 02, 2010 35 `````` `````` Jean-Christophe Filliatre committed Nov 23, 2014 36 37 `````` function numof (a b c: int) (l u: int) : int = NumOf.numof (\ n. p a b c n) l u `````` Jean-Christophe Filliâtre committed Jul 02, 2010 38 `````` `````` Jean-Christophe Filliatre committed Nov 23, 2014 39 `````` function solution(a b m: int) : int = numof a b 10 0 (power 10 m) `````` Jean-Christophe Filliâtre committed Jul 01, 2010 40 `````` `````` Jean-Christophe Filliatre committed Mar 20, 2014 41 `````` (* shortcut for the number of n st n mod 10 = c and ... *) `````` Jean-Christophe Filliâtre committed Jun 25, 2010 42 `````` `````` Jean-Christophe Filliatre committed Nov 23, 2014 43 44 `````` function num_of_modc (a b c: int) (x y: int) : int = numof a b (c+1) x y - numof a b c x y `````` Jean-Christophe Filliâtre committed Jul 04, 2010 45 46 `````` (* helper lemmas *) `````` Jean-Christophe Filliâtre committed Jul 01, 2010 47 `````` `````` Jean-Christophe Filliatre committed May 20, 2011 48 `````` lemma Base: `````` Jean-Christophe Filliatre committed Nov 23, 2014 49 `````` forall a b: int. 0 <= a -> sum_digits a + b = 0 -> p a b 10 0 `````` Jean-Christophe Filliâtre committed Jul 02, 2010 50 51 `````` lemma Empty: `````` Jean-Christophe Filliatre committed Nov 23, 2014 52 `````` forall a b x y: int. numof a b 0 x y = 0 `````` Jean-Christophe Filliatre committed Mar 20, 2014 53 `````` `````` Jean-Christophe Filliâtre committed Jul 04, 2010 54 `````` lemma Induc: `````` Martin Clochard committed Feb 11, 2014 55 `````` forall a b c: int,m:int. 0 <= a -> 0 <= c < 10 -> m > 0 -> `````` Jean-Christophe Filliâtre committed Jul 02, 2010 56 57 58 `````` let x = 137 * c + a in let a' = div x 10 in let b' = mod x 10 + b - c in `````` Jean-Christophe Filliatre committed Nov 23, 2014 59 `````` solution a' b' (m-1) = num_of_modc a b c 0 (power 10 m) `````` Jean-Christophe Filliâtre committed Jul 01, 2010 60 `````` `````` Jean-Christophe Filliatre committed Feb 10, 2014 61 62 `````` (* code *) `````` Jean-Christophe Filliâtre committed Aug 18, 2010 63 `````` use import int.ComputerDivision `````` Jean-Christophe Filliâtre committed Jun 25, 2010 64 `````` `````` Jean-Christophe Filliatre committed Feb 10, 2014 65 66 67 68 `````` let rec sd (n: int) : int requires { n >= 0 } ensures { result = sum_digits n } variant { n } `````` Andrei Paskevich committed Oct 13, 2012 69 `````` = if n = 0 then 0 else sd (div n 10) + mod n 10 `````` Jean-Christophe Filliatre committed Aug 05, 2011 70 71 `````` (* f(m,a,b) = the number of 0 <= n < 10^m such that `````` Jean-Christophe Filliatre committed Feb 10, 2014 72 73 `````` digitsum(137n + a) + b = digitsum(n). *) let rec f (m a b: int) : int `````` Andrei Paskevich committed Oct 13, 2012 74 `````` requires { 0 <= m /\ 0 <= a } `````` Jean-Christophe Filliatre committed Feb 10, 2014 75 76 `````` ensures { result = solution a b m } variant { m } `````` Andrei Paskevich committed Oct 13, 2012 77 `````` = if m = 0 then begin `````` Jean-Christophe Filliatre committed Aug 05, 2011 78 `````` (* only n = 0 is possible *) `````` MARCHE Claude committed Sep 15, 2016 79 80 `````` assert { power 10 m = 1 }; assert { numof a b 10 0 (power 10 m) = if sum_digits a + b = 0 then 1 else 0 }; `````` Jean-Christophe Filliatre committed Aug 05, 2011 81 82 83 `````` if sd a + b = 0 then 1 else 0 end else begin let sum = ref 0 in `````` Martin Clochard committed Feb 11, 2014 84 `````` let ghost p = power 10 m in `````` Jean-Christophe Filliatre committed Feb 10, 2014 85 `````` for c = 0 to 9 do (* count the n st n mod 10 = c *) `````` Jean-Christophe Filliatre committed Nov 23, 2014 86 `````` invariant { !sum = numof a b c 0 p } `````` Martin Clochard committed Feb 11, 2014 87 `````` 'L: `````` Jean-Christophe Filliatre committed Feb 10, 2014 88 `````` let x = 137 * c + a in `````` Jean-Christophe Filliatre committed Aug 05, 2011 89 90 `````` let q = div x 10 in let r = mod x 10 in `````` Martin Clochard committed Feb 11, 2014 91 92 93 `````` let b' = (r+b-c) in sum := !sum + f (m-1) q b'; assert { q = E.div x 10 && r = E.mod x 10 && `````` Jean-Christophe Filliatre committed Nov 23, 2014 94 `````` !sum - !(at sum 'L) = num_of_modc a b c 0 p } `````` Jean-Christophe Filliatre committed Aug 05, 2011 95 96 97 `````` done; !sum end `````` Jean-Christophe Filliatre committed May 20, 2011 98 `````` `````` Jean-Christophe Filliatre committed Dec 29, 2010 99 ``end``