Proving the conversion of a natural number to a list of digits (base 10) correct with ACL2

number-to-digits10.lisp

;;; The following code implements the conversion of a natural number
;;; to a list of digits and back.

;;; ACL2 Version 8.5
;;; https://www.cs.utexas.edu/users/moore/acl2/

;;; ACL2 is used to prove that one conversion followed by the other
;;; leads back to the initial value (roundtrip).  This is proved in
;;; both directions:
;;; starting from a natural number (see main/base10-representation-1
;;; below)
;;; and starting from a list of digits (see
;;; main/base10-representation-2 below).

;;; This code is entirely written by myself, but the following video
;;; Proving converting to base10 - YouTube
;;; https://www.youtube.com/watch?v=p3ACK41ipWc
;;; by Ruben Gamboa has provided very valuable insights that have
;;; allowed me to complete the proofs in time :).

(defun digits10-to-number (digits)
  "Convert the list of DIGITS to a natural number."
  ;; NOTE: Digits are represented in "reverse order",
  ;; i.e. most-significant digit last.
  (if (endp digits)
      0
    (+ (car digits)
       (* 10
          (digits10-to-number (cdr digits))))))
;;; Examples:
(thm
 (and (equal (digits10-to-number '(3 2 1)) 123)
      (equal (digits10-to-number '(1)) 1)
      (equal (digits10-to-number '()) 0)
      (equal (digits10-to-number '(3 2 1)) 123)
      (equal (digits10-to-number '(3 2 1 0)) 123)
      (equal (digits10-to-number '(3 2 1 0 0)) 123)))

(encapsulate
 ()
 (local (include-book "arithmetic-5/top" :dir :system))
 ;; The use of the arithmetic book is needed here to prove termination
 ;; of number-to-digits10. It needs to be shown that (floor n 10) is
 ;; smaller than n for the recursive call.
 (defun number-to-digits10 (n)
   "Convert the natural number N to a list of digits."
   (if (zp n)
       nil
     (cons (mod n 10)
           (number-to-digits10 (floor n 10))))))
;;; Examples:
(thm
 (and (equal (number-to-digits10 123) '(3 2 1))
      (equal (number-to-digits10 102030) '(0 3 0 2 0 1))
      (equal (number-to-digits10 7) '(7))
      (equal (number-to-digits10 0) '())))

;;; This is the first main theorem.
(defthm main/base10-representation-1
  (implies (natp n)
           (equal (digits10-to-number
                   (number-to-digits10 n))
                  n)))

;;; In order to prove the second theorem, we need to be able to
;;; specify that the input is a list of digits.
(defun digit-listp (x)
  (if (endp x)
      (equal x nil)
    (and (natp (car x))
         (< (car x) 10)
         (digit-listp (cdr x)))))
;;; Examples:
(thm (and (digit-listp '(1 2 3))
          (digit-listp '())
          (not (digit-listp '(1 X 2 3)))
          (not (digit-listp '(1 2 3 . 4)))))

(defthm digit-listp-implies-true-listp
  ;; NOTE: digit-listp is written in a way that it accepts only true
  ;; lists. This theorem isn't really needed for the main proof.
  (implies (digit-listp x)
           (true-listp x)))

(defthm natp-digits10-to-number
  ;; This is a lemma needed for the main theorem below
  (implies (digit-listp l)
           (natp (digits10-to-number l))))

(encapsulate
 ()
 (local (include-book "arithmetic-5/top" :dir :system))
 ;; These are two more lemmas needed for the main theorem below
 (defthm natp-mod-1
   (implies (natp n)
            (equal (mod n 1) 0)))
 (defthm natp-floor-1
   (implies (natp n)
            (equal (floor n 1) n))))

(encapsulate
 ()
 (local (include-book "arithmetic-5/top" :dir :system))
 ;; This is the second main theorem.
 (defthm main/base10-representation-2
   (implies (and (digit-listp digits)
                 ;; In order for our rountrip result to be equal to
                 ;; where we started, we assume that our list of
                 ;; digits does not have any leading zeroes (in our
                 ;; representation the most-significant digit is
                 ;; last).
                 (not (equal (car (last digits)) 0)))
            (equal (number-to-digits10
                    (digits10-to-number digits))
                   digits))))

;;; Q.E.D. :)