cleaning up

examples/programs/talk290.mlw

-module M
+
 (* 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? *)
+   of the digits of n equals the sum of digits of 137n?
+
+   The answer is 20444710234716473.
+
+   It can be easily computer 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?
 
-(* answer: 20444710234716473 *)
+   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.
+   Memoization must be added if one wants to solve the initial problem.
+   (See for instance fib_memo.mlw for an example of memoized function.) *)
 
+module M
   use import int.Int
   use import module ref.Ref
   use import int.EuclideanDivision
   use import int.Power
 
-(*
-  function sum_digits (n:int) : int =
-    if n = 0 then 0 else sum_digits (div n 10) + mod n 10
-*)
   function sum_digits int : int
 
   axiom Sum_digits_def : forall n : int. sum_digits n =
@@ -54,33 +60,33 @@ module M
 
   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(137n+a) + b = digitsum(n). *)
-let rec f m a b =
-  { 0 <= m /\ 0 <= a }
-  if m = 0 then begin
-    (* only n = 0 is possible *)
-    if sd 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 /\ !sum = P.num_of (a,b,!c) 0 (power 10 m) }
-      variant   { 10 - !c }
-      let x = 137 * !c + a in
-      let q = div x 10 in
-      let r = mod x 10 in
-      sum := !sum + f (m-1) q (r + b - !c);
-      c := !c + 1
-    done;
-    !sum
-  end
-  { result = solution a b m }
+  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(137n+a) + b = digitsum(n). *)
+  let rec f m a b =
+    { 0 <= m /\ 0 <= a }
+    if m = 0 then begin
+      (* only n = 0 is possible *)
+      if sd 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 /\ !sum = P.num_of (a,b,!c) 0 (power 10 m) }
+        variant   { 10 - !c }
+        let x = 137 * !c + a in
+        let q = div x 10 in
+        let r = mod x 10 in
+        sum := !sum + f (m-1) q (r + b - !c);
+        c := !c + 1
+      done;
+      !sum
+    end
+    { result = solution a b m }
 
 end