The Eights Problem Example

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:

for all n > 7, there exist naturals i and j such that: n = 3i + 5j.

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

(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)))))

That is, assuming that

Let's look at a few cases:

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; ...

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:

(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))))))))

Notice that we explicitly compute the values of

Let's try it on some examples:

ACL2 !>(split 28) (6 . 2) ACL2 !>(split 45) (15 . 0) ACL2 !>(split 335) (110 . 1)

Finally, we submit our theorem

For completeness, we'll note that we can state and prove a quantified
version of this theorem. We introduce the notion

(defun-sk split-able (n) (exists (i j) (equal n (+ (* 3 i) (* 5 j)))))

Then our theorem is given below. Notice that we prove it by observing that
our previous function

(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)))))))

Unfortunately, understanding the mechanics of the proof requires knowing
something about the way `defun-sk` works. See defun-sk or see
Tutorial4-Defun-Sk-Example for more on that subject.