(* 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? *) (* answer: 20444710234716473 *) { use import int.EuclideanDivision use import int.Power logic sum_digits (n:int) : int = if n = 0 then 0 else sum_digits (div n 10) + mod n 10 logic p (n:int) = sum_digits(n) = sum_digits(137 * n) clone int.NumOf as P with logic pr = p type int2 = (int,int) logic q (d:int2) (n:int) = let (a,b) = d in sum_digits(n) = sum_digits(137 * n + a) = b clone int.NumOfParam as Q with type param = int2, logic pr = q type int3 = (int,int,int) logic r (d:int3) (n:int) = let (a,b,c) = d in 0 <= mod n 10 < c and sum_digits(n) = sum_digits(137 * n + a) = b clone int.NumOfParam as R with type param = int3, logic pr = r goal Test : forall n:int. 0 <= n < power 10 0 -> n = 0 } { (* use import int.ComputerDivision *) } let rec sd n = { n >= 0 } if n = 0 then 0 else sd (div n 10) + mod n 10 { result = sum_digits n } (* f(m,a,b) = the number of 0 <= n < 10^m such that digitsum(n) = digitsum(137n+a) + b. *) let rec f m a b = { 0 <= m } if m = 0 then begin (* only n = 0 is possible *) if sum_digits a + b = 0 then 1 else 0 end else begin let sum = ref 0 in let c = ref 0 in while !c <= 9 do (* n = 10n' + c *) invariant { 0 <= !c <= 10 } variant { !c } let x = 137 * !c + a in let a' = div x 10 in let c' = mod x 10 in sum := !sum + f (m-1) a' (c' + b - !c); c := !c + 1 done; !sum end { result = Q.num_of (a,b) 0 (power 10 m) } (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/talk290" End: *)