Major Section: ANNOTATED-ACL2-SCRIPTS
This example was written almost entirely by Bill Young of Computational Logic, Inc.
We will formalize and prove a small theorem about the famous ``Towers of Hanoi'' problem. This problem is illustrated by the following picture.
| | | | | | --- | | ----- | | ------- | | A B CWe have three pegs --
ndisks of different sizes. The disks are all initially on peg
a. The goal is to move all disks to peg
cwhile observing the following two rules.
1. Only one disk may be moved at a time, and it must start and finish the move as the topmost disk on some peg;
2. A disk can never be placed on top of a smaller disk.
Let's consider some simple instances of this problem. If
n = 1,
i.e., only one disk is to be moved, simply move it from
n = 2, i.e., two disks are to be moved, the following
sequence of moves suffices: move from
b, move from
c, move from
In this doc topic we will show an ACL2 function that generates a suitable
list of moves for a tower of
n disks. Then we will use ACL2 to prove
that the number of moves is
(- (expt 2 n) 1). For an ACL2 script
that proves the correctness of (a version of) this function, see the
"misc/hanoi.lisp" in the
books directory of your ACL2
In general, this problem has a straightforward recursive solution.
Suppose that we desire to move
n disks from
b as the intermediate peg. For the basis, we saw above that we
can always move a single disk from
c. Now if we have
n disks and assume that we can solve the problem for
disks, we can move
n disks as follows. First, move
c as the intermediate peg; move the
single disk from
c; then move
n-1 disks from
a as the intermediate peg.
In ACL2, we can write a function that will return the sequence of
moves. One such function is as follows. Notice that we have two
base cases. If
(zp n) then
n is not a positive integer; we
treat that case as if
n were 0 and return an empty list of moves.
n is 1, then we return a list containing the single
appropriate move. Otherwise, we return the list containing exactly
the moves dictated by our recursive analysis above.
Notice that we give
(defun move (a b) (list 'move a 'to b))
(defun hanoi (a b c n) (if (zp n) nil (if (equal n 1) (list (move a c)) (append (hanoi a c b (1- n)) (cons (move a c) (hanoi b a c (1- n)))))))
hanoifour arguments: the three pegs, and the number of disks to move. It is necessary to supply the pegs because, in recursive calls, the roles of the pegs differ. In any execution of the algorithm, a given peg will sometimes be the source of a move, sometimes the destination, and sometimes the intermediate peg.
After submitting these functions to ACL2, we can execute the
function on various specific arguments. For example:
From the algorithm it is clear that if it takes
ACL2 !>(hanoi 'a 'b 'c 1) ((MOVE A TO C))
ACL2 !>(hanoi 'a 'b 'c 2) ((MOVE A TO B) (MOVE A TO C) (MOVE B TO C))
ACL2 !>(hanoi 'a 'b 'c 3) ((MOVE A TO C) (MOVE A TO B) (MOVE C TO B) (MOVE A TO C) (MOVE B TO A) (MOVE B TO C) (MOVE A TO C))
mmoves to transfer
ndisks, it will take
(m + 1 + m) = 2m + 1moves for
n+1disks. From some simple calculations, we see that we need the following number of moves in specific cases:
The pattern is fairly clear. To move
Disks 0 1 2 3 4 5 6 7 ... Moves 0 1 3 7 15 31 63 127 ...
(2^n - 1)moves. Let's attempt to use ACL2 to prove that fact.
First of all, how do we state our conjecture? Recall that
returns a list of moves. The length of the list (given by the
len) is the number of moves required. Thus, we can state
the following conjecture.
When we submit this to ACL2, the proof attempt fails. Along the way we notice subgoals such as:
(defthm hanoi-moves-required-first-try (equal (len (hanoi a b c n)) (1- (expt 2 n))))
Subgoal *1/1' (IMPLIES (NOT (< 0 N)) (EQUAL 0 (+ -1 (EXPT 2 N)))).
This tells us that the prover is considering cases that are
uninteresting to us, namely, cases in which
n might be negative.
The only cases that are really of interest are those in which
is a non-negative natural number. Therefore, we revise our theorem
and submit it to ACL2 again.
(defthm hanoi-moves-required (implies (and (integerp n) (<= 0 n)) ;; n is at least 0 (equal (len (hanoi a b c n)) (1- (expt 2 n)))))
Again the proof fails. Examining the proof script we encounter the following text. (How did we decide to focus on this goal? Some information is provided in ACLH, and the ACL2 documentation on tips may be helpful. But the simplest answer is: this was the first goal suggested by the ``proof-tree'' tool below the start of the proof by induction. See proof-tree.)
It is difficult to make much sense of such a complicated goal. However, we do notice something interesting. In the conclusion is a term of the following shape.
Subgoal *1/5'' (IMPLIES (AND (INTEGERP N) (< 0 N) (NOT (EQUAL N 1)) (EQUAL (LEN (HANOI A C B (+ -1 N))) (+ -1 (EXPT 2 (+ -1 N)))) (EQUAL (LEN (HANOI B A C (+ -1 N))) (+ -1 (EXPT 2 (+ -1 N))))) (EQUAL (LEN (APPEND (HANOI A C B (+ -1 N)) (CONS (LIST 'MOVE A 'TO C) (HANOI B A C (+ -1 N))))) (+ -1 (* 2 (EXPT 2 (+ -1 N))))))
We conjecture that the length of the
(LEN (APPEND ... ...))
appendof two lists should be the sum of the lengths of the lists. If the prover knew that, it could possibly have simplified this term earlier and made more progress in the proof. Therefore, we need a rewrite rule that will suggest such a simplification to the prover. The appropriate rule is:
We submit this to the prover, which proves it by a straightforward induction. The prover stores this lemma as a rewrite rule and will subsequently (unless we disable the rule) replace terms matching the left hand side of the rule with the appropriate instance of the term on the right hand side.
(defthm len-append (equal (len (append x y)) (+ (len x) (len y))))
We now resubmit our lemma
hanoi-moves-required to ACL2. On this
attempt, the proof succeeds and we are done.
One bit of cleaning up is useful. We needed the hypotheses that:
This is an awkward way of saying that
(and (integerp n) (<= 0 n)).
nis a natural number; natural is not a primitive data type in ACL2. We could define a function
naturalp, but it is somewhat more convenient to define a macro as follows:
Subsequently, we can use
(defmacro naturalp (x) (list 'and (list 'integerp x) (list '<= 0 x)))
(naturalp n)wherever we need to note that a quantity is a natural number. See defmacro for more information about ACL2 macros. With this macro, we can reformulate our theorem as follows:
Another interesting (but much harder) theorem asserts that the list of moves generated by our
(defthm hanoi-moves-required (implies (naturalp n) (equal (len (hanoi a b c n)) (1- (expt 2 n))))).
hanoifunction actually accomplishes the desired goal while following the rules. When you can state and prove that theorem, you'll be a very competent ACL2 user.
By the way, the name ``Towers of Hanoi'' derives from a legend that a group of Vietnamese monks works day and night to move a stack of 64 gold disks from one diamond peg to another, following the rules set out above. We're told that the world will end when they complete this task. From the theorem above, we know that this requires 18,446,744,073,709,551,615 moves:
We're guessing they won't finish any time soon.
ACL2 !>(1- (expt 2 64)) 18446744073709551615 ACL2 !>