talk290.mlw 1.7 KB
Newer Older
1
2
3
4
(* 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 *)
5
6
7
8
9
10
11
12
13

{ 
  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)
14
  clone int.NumOf as P with logic pr = p
15
16
17
18

  type int2 = (int,int)
  logic q (d:int2) (n:int) = 
    let (a,b) = d in sum_digits(n) = sum_digits(137 * n + a) = b
19
20
21
22
23
24
25
  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
26
27
28
29
30
31
32
33
34
35
36
37
38
39

  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 
40
   digitsum(n) = digitsum(137n+a) + b. *)
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
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: 
*)