Lp-section-16
Proving Theorems about DO Loop$s
LP16: Proving Theorems about DO Loop$s
Let's prove a theorem about a DO loop$. Specifically, let's
prove
(defthm main
(implies (natp n)
(equal (loop$ with i = n
with ans = 0
do
(if (zp i)
(return ans)
(progn (setq ans (+ 1 ans))
(setq i (- i 1)))))
n)))
A few words of warning are appropriate.
- The Method (see the-method) is a good way to proceed: try to
prove the theorem expecting it to fail and look at the checkpoints.
- Unsurprisingly, the theorem above has to be generalized before it
can be proved. But it can feel strange to generalize a loop$.
- If we prove a lemma that rewrites a loop$ expression we have to
remember that before rewrite rules are applied the interior terms are
rewritten. In particular, ACL2 can rewrite the bodies of the lambda
objects. The most common changes are that non-recursive functions are
generally expanded (depending on the theory in use) and IFs
are normalized. That means we need to normalize the bodies of any loop$
we use in a lemma if we expect that lemma to match a term being rewritten!
This observation is relevant here because zp is non-recursively
defined and so will expand when the body of the loop$ above is
rewritten.
- ACL2 does not display do$ terms as DO loop$s. So get
used to reading do$ terms and thinking of loop$ statements!
(We may fix this someday but at the moment we find it advantageous to really
see the terms the prover is dealing with!)
A Tedious Recipe for Proving Theorems about DO Loop$s
When you first start proving theorems about DO loop$s it might
be helpful to follow the tedious recipe below. It will familiarize you with
the semantics of DO loop$s and teach you certain techniques that
are easy applications of lessons you've already internalized as an
experienced ACL2 user, albeit one unfamiliar with loop$. But after a
little experience you'll find it straightforward to skip some steps!
- Use The Method to find the normal form of the loop$.
- Define a recursive function that computes the value of the loop$
using the same algorithm as the loop$. This function can serve two
purposes. First, it can be an intermediate stop on the way to proving that
the loop$ satisfies your specification. We'll make this clear in the
next point. Second, it can suggest an induction scheme that is probably
useful. We'll return to this point at the end of our recipe for proving
things about DO loop$s.
- Prove that the loop$ computes the same value as the function. We
frequently refer to this as “lemma 1” in the recipe. Generally
you will have to generalize the loop$ to prove it by the induction
suggested by the function. And you will have to write the normal form of the
loop$ body instead of the “pretty” form used in the main
theorem so this lemma can be used to hit the rewritten loop$ in the
proof of the main theorem later.
- Prove that the function satisfies the specification. We
frequently refer to this as “lemma 2”.
- Prove that the loop$ satisfies the specification by chaining
together the two lemmas.
Of course, as with all “recipes”, sometimes you have to adjust
depending on the ingredients at hand. Sometimes you can just write the body of
the loop$ in normal form to begin with. Sometimes you do not have to define a
special function because the loop$ itself or a function already in the
conjecture suggests an appropriate induction. Sometimes you may find it
easier to copy the do$ form revealed by The Method into your statement
of lemma 1 and generalize that form, rather than try to express lemma 1 as a
loop$. You may also be content to skip the “intermediate
stop” of lemma 1 altogether and prove that the loop$ satisfies a
generalized specification, sometimes providing an :induct hint instead
of inserting the special function into the lemma. Sometimes you do not have
to generalize. Sometimes instead of proving lemma 1 and lemma 2 you can just
prove the main goal directly. As an experienced ACL2 user you will recognize
when you can skip steps in this recipe. We spell the recipe out rigidly here
just to give you one promising way to proceed.
We're going to prove the theorem
(defthm main
(implies (natp n)
(equal (loop$ with i = n
with ans = 0
do
(if (zp i)
(return ans)
(progn (setq ans (+ 1 ans))
(setq i (- i 1)))))
n)))
both ways, first by following the tedious recipe, and then the way a user
familiar with DO loop$ proofs might do it.
So here goes! Following the recipe to prove main above, we first try
The Method. The prover tries an induction suggested by the DO
loop$, namely induction on N by -1, but without instantiating
ANS because the initial value of ANS is the constant 0. We
know this proof will fail and it does. The pre-induction checkpoint is shown
below.
*** Key checkpoint at the top level: ***
Goal''
(IMPLIES
(AND (INTEGERP N) (<= 0 N))
(EQUAL
(DO$
(LAMBDA$ (ALIST)
(ACL2-COUNT (CDR (ASSOC-EQ-SAFE 'I ALIST))))
(CONS (CONS 'I N) '((ANS . 0)))
(LAMBDA$
(ALIST)
(IF (INTEGERP (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(IF (< 0 (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(LIST NIL NIL
(LIST (CONS 'I
(+ -1 (CDR (ASSOC-EQ-SAFE 'I ALIST))))
(CONS 'ANS
(+ 1 (CDR (ASSOC-EQ-SAFE 'ANS ALIST))))))
(LIST :RETURN (CDR (ASSOC-EQ-SAFE 'ANS ALIST))
(LIST (CONS 'I (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(CONS 'ANS
(CDR (ASSOC-EQ-SAFE 'ANS ALIST))))))
(LIST :RETURN (CDR (ASSOC-EQ-SAFE 'ANS ALIST))
(LIST (CONS 'I (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(CONS 'ANS
(CDR (ASSOC-EQ-SAFE 'ANS ALIST)))))))
(LAMBDA$ (ALIST)
(LIST NIL NIL
(LIST (CONS 'I (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(CONS 'ANS
(CDR (ASSOC-EQ-SAFE 'ANS ALIST))))))
'(NIL) NIL)
N))
Look carefully at the do-body lambda, the second lambda
object in the do$. The (ZP I) in our original DO loop$
has opened up, introducing (INTEGERP i) and (< 0 i) and IF
normalization -- except instead of seeing the simple variable I we see
its current value in the ALIST being computed on each iteration.
This is valuable information! It tells us what the rewritten body of
the loop$ looks like in the theory in which our proof is being
conducted. If we prove a :rewrite rule expecting it to fire during the
proof of our main theorem, its body must match that shown above!
Now we define the recursive function that is supposed to be operationally
equivalent to the loop$. This will suggest the induction.
(defun copy-nat-ac (i ans)
(if (zp i)
ans
(copy-nat-ac (- i 1)
(+ 1 ans))))
Next comes the hard part. We state the lemma that equates the loop$
to the function, but we have to generalize it so it can be proved by induction
and we have to use the normal form of the body. We could state the lemma
in terms of DO$ of course, but with a little practice you can usually
“reverse engineer” the desired lemma into a loop$. So here
is the so-called “lemma 1”.
(defthm lemma1
(implies (and (natp n)
(natp ans0))
(equal (loop$ with i = n
with ans = ans0
do
(if (integerp i)
(if (< 0 i)
(progn (setq ans (+ 1 ans))
(setq i (- i 1)))
(return ans))
(return ans)))
(copy-nat-ac n ans0))))
Note that we generalized the initial value of ans in the loop$
from 0 to ans0 and used ans0 as the accumulator in
(copy-nat-ac n ans0).
By the way, we could have written lemma1 in terms of the DO$
term shown in the checkpoint, rather than as a loop$. But we have to
generalize that 0 whether we use a loop$ or the DO$ term.
The generalized DO$ form of lemma1 is
(defthm lemma1
(implies
(and (natp n)
(natp ans0))
(equal
(DO$
(LAMBDA$ (ALIST)
(ACL2-COUNT (CDR (ASSOC-EQ-SAFE 'I ALIST))))
(CONS (CONS 'I N) (cons 'ans ans0)) ; note generalization of 0!
(LAMBDA$
(ALIST)
(IF (INTEGERP (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(IF (< 0 (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(LIST NIL NIL
(LIST (CONS 'I
(+ -1 (CDR (ASSOC-EQ-SAFE 'I ALIST))))
(CONS 'ANS
(+ 1 (CDR (ASSOC-EQ-SAFE 'ANS ALIST))))))
(LIST :RETURN (CDR (ASSOC-EQ-SAFE 'ANS ALIST))
(LIST (CONS 'I (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(CONS 'ANS
(CDR (ASSOC-EQ-SAFE 'ANS ALIST))))))
(LIST :RETURN (CDR (ASSOC-EQ-SAFE 'ANS ALIST))
(LIST (CONS 'I (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(CONS 'ANS
(CDR (ASSOC-EQ-SAFE 'ANS ALIST)))))))
(LAMBDA$ (ALIST)
(LIST NIL NIL
(LIST (CONS 'I (CDR (ASSOC-EQ-SAFE 'I ALIST)))
(CONS 'ANS
(CDR (ASSOC-EQ-SAFE 'ANS ALIST))))))
'(NIL) NIL)
(copy-nat-ac n ans0)))).
The UPPERCASE part above was just copied from the checkpoint and then the
pair in the initial alist binding ANS, which was '(ANS . 0), was
replaced by (cons 'ans ans0). So while it looks messy, it's not hard to
enter. Furthermore, it saves us from having to figure out the normal form
— it's already in the checkpoint. The DO$ term in this version of
lemma1 is just the formal translation of the generalized DO
loop$ we wrote in the earlier version of lemma1.
Next we prove “lemma 2” equating the recursive function with
the (generalized) specification. This theorem does not involve loop$
and its proof should be utterly familiar to you.
(defthm lemma2
(implies (and (natp n)
(natp ans0))
(equal (copy-nat-ac n ans0)
(+ n ans0))))
Finally, we prove our main theorem.
(defthm main
(implies (natp n)
(equal (loop$ with i = n
with ans = 0
do
(if (zp i)
(return ans)
(progn (setq ans (+ 1 ans))
(setq i (- i 1)))))
n)))
The proof rewrites the “pretty” do-body lambda into
the normal form, lemma1 rewrites the new form of the loop$ after
instantiating ans0 to 0, to (copy-nat-ac n 0), then
lemma2 hits that to (+ n 0), and arithmetic does the rest.
As we noted, our recipe is overly rigid. Here is another sequence of
events that proves main. The experienced user realizes that the
generalized DO loop$ will in fact suggest the appropriate induction
to ACL2. So no special function is introduced. Furthermore, the user
— who has proved several theorems about loop$s involving IF
and ZP will know how to write the normal form. That user would just do
this.
(defthm lemma
(implies
(and (natp n) (natp ans0))
(equal (loop$ with i = n
with ans = ans0
do
(if (integerp i)
(if (< 0 i)
(progn (setq ans (+ 1 ans))
(setq i (- i 1)))
(return ans))
(return ans)))
(+ n ans0))))
(defthm main
(implies (natp n)
(equal (loop$ with i = n
with ans = 0
do
(if (zp i)
(return ans)
(progn (setq ans (+ 1 ans))
(setq i (- i 1)))))
n)))
For more details about rewriting lambda objects you can leave the
loop$ primer and read rewrite-lambda-object and rewriting-versus-cleaning-up-lambda-objects. But remember to come
back here to lp-section-16!
Now go to lp-section-17 (or return to the Table of Contents).
