Last active
December 16, 2023 19:53
-
-
Save kisp/e0f400646faad1225e3f3f34f60df078 to your computer and use it in GitHub Desktop.
Proving the conversion of a natural number to a list of digits (base 10) correct with ACL2
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;;; 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. :) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment