Major Section: ANNOTATED-ACL2-SCRIPTS
This example was written almost entirely by Bill Young of Computational Logic, Inc.
This simple example was brought to our attention as one that Paul Jackson has solved using the NuPrl system. The challenge is to prove the theorem:
In ACL2, we could phrase this theorem using quantification. However we will start with a constructive approach, i.e., we will show that values of
for all n > 7, there exist naturals i and j such that: n = 3i + 5j.
jexist by writing a function that will construct such values for given
n. Suppose we had a function
(split n)that returns an appropriate pair
(i . j). Our theorem would be as follows:
That is, assuming that
(defthm split-splits (let ((i (car (split n))) (j (cdr (split n)))) (implies (and (integerp n) (< 7 n)) (and (integerp i) (<= 0 i) (integerp j) (<= 0 j) (equal (+ (* 3 i) (* 5 j)) n)))))
nis a natural number greater than 7,
(split n)returns values
jthat are in the appropriate relation to
Let's look at a few cases:
Maybe you will have observed a pattern here; any natural number larger than 10 can be obtained by adding some multiple of 3 to 8, 9, or 10. This gives us the clue to constructing a proof. It is clear that we can write split as follows:
8 = 3x1 + 5x1; 11 = 3x2 + 5x1; 14 = 3x3 + 5x1; ... 9 = 3x3 + 5x0; 12 = 3x4 + 5x0; 15 = 3x5 + 5x0; ... 10 = 3x0 + 5x2; 13 = 3x1 + 5x2; 16 = 3x2 + 5x2; ...
Notice that we explicitly compute the values of
(defun bump-i (x) ;; Bump the i component of the pair ;; (i . j) by 1. (cons (1+ (car x)) (cdr x)))
(defun split (n) ;; Find a pair (i . j) such that ;; n = 3i + 5j. (if (or (zp n) (< n 8)) nil ;; any value is really reasonable here (if (equal n 8) (cons 1 1) (if (equal n 9) (cons 3 0) (if (equal n 10) (cons 0 2) (bump-i (split (- n 3))))))))
jfor the cases of 8, 9, and 10, and for the degenerate case when
nis not a natural or is less than 8. For all naturals greater than
n, we decrement
nby 3 and bump the number of 3's (the value of i) by 1. We know that the recursion must terminate because any integer value greater than 10 can eventually be reduced to 8, 9, or 10 by successively subtracting 3.
Let's try it on some examples:
Finally, we submit our theorem
ACL2 !>(split 28) (6 . 2)
ACL2 !>(split 45) (15 . 0)
ACL2 !>(split 335) (110 . 1)
split-splits, and the proof succeeds. In this case, the prover is ``smart'' enough to induct according to the pattern indicated by the function split.
For completeness, we'll note that we can state and prove a quantified
version of this theorem. We introduce the notion
split-able to mean
j exist for
Then our theorem is given below. Notice that we prove it by observing that our previous function
(defun-sk split-able (n) (exists (i j) (equal n (+ (* 3 i) (* 5 j)))))
splitdelivers just such an
j(as we proved above).
Unfortunately, understanding the mechanics of the proof requires knowing something about the way
(defthm split-splits2 (implies (and (integerp n) (< 7 n)) (split-able n)) :hints (("Goal" :use (:instance split-able-suff (i (car (split n))) (j (cdr (split n)))))))
defun-skworks. See defun-sk or see Tutorial4-Defun-Sk-Example for more on that subject.