The Towers of Hanoi Example
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 —
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
In this doc topic we will show an ACL2 function that generates a suitable
list of moves for a tower of
In general, this problem has a straightforward recursive solution. Suppose
that we desire to move
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
(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
After submitting these functions to ACL2, we can execute the
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
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
First of all, how do we state our conjecture? Recall that
(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
(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
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
(defmacro naturalp (x) (list 'and (list 'integerp x) (list '<= 0 x)))
Subsequently, we can use
(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
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.