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 C
We have three pegs -- a, b, and c -- and n disks of
different sizes. The disks are all initially on peg a. The goal
is to move all disks to peg c while 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 a to
c. If n = 2, i.e., two disks are to be moved, the following
sequence of moves suffices: move from a to b, move from a
to c, move from b to c.
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
community book "misc/hanoi.lisp" in the books directory of your
ACL2 sources.
In general, this problem has a straightforward recursive solution.
Suppose that we desire to move n disks from a to c, using
b as the intermediate peg. For the basis, we saw above that we
can always move a single disk from a to c. Now if we have
n disks and assume that we can solve the problem for n-1
disks, we can move n disks as follows. First, move n-1 disks
from a to b using c as the intermediate peg; move the
single disk from a to c; then move n-1 disks from b to
c using 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.
If 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.
(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)))))))
Notice that we give hanoi four 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 hanoi
function on various specific arguments. For example:
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))From the algorithm it is clear that if it takes
m moves to
transfer n disks, it will take (m + 1 + m) = 2m + 1 moves for
n+1 disks. From some simple calculations, we see that we need
the following number of moves in specific cases:
Disks 0 1 2 3 4 5 6 7 ... Moves 0 1 3 7 15 31 63 127 ...The pattern is fairly clear. To move
n disks requires (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 hanoi
returns a list of moves. The length of the list (given by the
function len) is the number of moves required. Thus, we can state
the following conjecture.
(defthm hanoi-moves-required-first-try
(equal (len (hanoi a b c n))
(1- (expt 2 n))))
When we submit this to ACL2, the proof attempt fails. Along the way
we notice subgoals such as:
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 n
is a non-negative natural number. Therefore, we revise our theorem
as follows:
(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)))))
and submit it to ACL2 again.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.)
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))))))
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.
(LEN (APPEND ... ...))We conjecture that the length of the
append of 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:
(defthm len-append
(equal (len (append x y))
(+ (len x) (len y))))
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.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:
(and (integerp n) (<= 0 n)).This is an awkward way of saying that
n is 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:
(defmacro naturalp (x)
(list 'and (list 'integerp x)
(list '<= 0 x)))
Subsequently, we can use (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:
(defthm hanoi-moves-required
(implies (naturalp n)
(equal (len (hanoi a b c n))
(1- (expt 2 n))))).
Another interesting (but much harder) theorem asserts that the list
of moves generated by our hanoi function 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:
ACL2 !>(1- (expt 2 64)) 18446744073709551615 ACL2 !>We're guessing they won't finish any time soon.
