Stating-and-proving-lemmas-about-loop$s
Stating and proving theorems about loop$s
In this topic we give some advice about how to state and prove
theorems involving loop$s, especially stating lemmas that are intended
to rewrite loop$ statements and proving theorems about loop$
statements inductively.
Name Loop$s When Memorable Names Come to Mind
Just because you can write iterative computations inline, don't get carried
away!
If you can think of a good name for the concept implemented by a
loop$ statement, use defun to define that name. This is especially
the case if you intend to reason about that loop$ statement or to write
more than one instance of it.
For example, rather than write instances of
(loop$ for a in x as b in y sum (* a b))
it is better to define (dot-product x y) with that loop$ as its
body and then write calls of dot-product and lemmas about
dot-product rather than that loop$.
Basically, names are good as long as you can remember them. They give you
a place to hang lemmas and the lemmas match without you having to think about
how lambda objects rewrite, local variables, etc. Not all loop$s
compute concepts with obvious, memorable names, but just because you can
write “anonymous” iterations doesn't mean you should!
Generalizing the Initial Values
Let's start with the most common issue raised by any inductive proof: the
conjecture to be proved must be general enough to permit the provision of
an appropriate inductive hypothesis.
Consider how you would prove the conjecture below after defining rev
and rev1.
(defun rev (x)
(if (endp x)
nil
(append (rev (cdr x)) (list (car x)))))
(defun rev1 (x a)
(if (endp x)
a
(rev1 (cdr x) (cons (car x) a))))
(defthm rev1-is-rev
(equal (rev1 x nil) (rev x)))
The experienced ACL2 user would not attempt to prove rev1-is-rev by induction
because the nil prevents the provision of an appropriate induction hypothesis.
Instead, the user would first prove a generalization obtained by replacing that
nil by a variable and “explaining” the role of that variable on the
right-hand side.
(defthm rev1-is-rev-generalized
(equal (rev1 x a)
(append (rev x) a)))
The proof of the generalized theorem succeeds (though the prover must
“discover” and then prove that append is associative).
With that theorem available, the proof of rev1-is-rev is trivial,
given that nil is the right-identity for append on true-lists and
that rev returns a true-list.
Now consider defining reverse with a do loop$.
(defun rev-loop$ (x)
(loop$ with tail = x
with a = nil
do
(if (endp tail)
(return a)
(progn (setq a (cons (car tail) a))
(setq tail (cdr tail))))))
The experienced ACL2 user would not attempt to prove that (rev-loop$
x) is (rev x) by induction! The problem is the same as before: the
nil initialization of the iterative variable a in the do
loop$ does not permit an appropriate inductive hypothesis. Instead, the
user needs to prove a more general theorem that cannot be stated in terms of
rev-loop$ because that nil is built into the definition. We need
to lift the loop$ out of the definition, generalize it, and prove a
theorem about the generalized loop$. Ideally we'd prove
(defthm rev-loop$-is-rev-generalized
(equal (loop$ with tail = x
with a = a
do
(if (endp tail)
(return a)
(progn (setq a (cons (car tail) a))
(setq tail (cdr tail)))))
(append (rev x) a))).
ACL2's prover can derive induction schemes suggested by some loop$
statements, just as it can from some calls of recursive functions. Because
both iterative variables, tail and a, are initialized to variables,
the DO loop$ above suggests an appropriate induction. But
inductions for loop$s raise some new issues as well as some traditional
ones.
ACL2 will prove the lemma above, if the associativity of append has
first been proved explicitly as a rewrite rule. (The presence of the
loop$ confuses the heuristics that enable the prover to
“discover” the associativity of append.)
Lesson 1: If a loop$ has iterative variables initialized to
non-variables, generalize them before expecting an induction to work! If the
loop$ is buried in a definition you'll have to lift the loop$ out of
the definition to generalize it and prove a theorem about the the generalized
loop$.
Normal Forms in Loop$ Bodies
The lemma above, rev-loop$-is-rev-generalized, is adequate to
subsequently prove the main theorem,
(defthm rev-loop$-is-rev
(equal (rev-loop$ x)
(rev x))).
But as stated, rev-loop$-is-rev-generalized is fragile because
it mentions the non-recursively defined function endp. To explain this
remark we need to walk through the proof of the main theorem.
Recall that the prover always expands enabled functions that are not
explicitly recursive. And rev-loop$ is not explicitly recursive. So
the proof attempt of rev-loop$-is-rev will expand the call of
rev-loop$ and produce
Goal'
(equal (loop$ with tail = x
with a = nil
do
(if (endp tail)
(return a)
(progn (setq a (cons (car tail) a))
(setq tail (cdr tail)))))
(rev x))
If the loop$ term above is immediately rewritten, our generalized
lemma would fire and reduce the goal to
Goal''
(equal (append (rev x) nil)
(rev x))
and the proof would be completed as before with the right-identity
rule.
Indeed, this is what happens in this particular case, but the reason it
works is completely unrelated to loop$s! Our generalized lemma has no
hypotheses — it is an unconditional rewrite rule that is applied early
in the “preprocessing” phase of simplification.
Let's suppose the generalized lemma did have some hypotheses or otherwise
failed to apply during preprocessing. You can cause this to happen by
restating the generalized lemma and the main theorem to have the (unnecessary
but easily dealt with) hypothesis (true-listp x). The proof of the
conditional generalized lemma still goes through, but the proof of the
conditional main theorem fails because the generalized lemma never fires!
The reason it never fires is that it is not tried during prepreprocessing
(because preprocessing doesn't deal with conditional rules because
preprocessing doesn't support backchaining) and Goal' above enters the
rewriter, which rewrites every subterm of the term before trying to apply
rules to the term itself. In particular, before the rewriter tries to
apply our generalized rule it rewrites the subterms of the loop$
statement, including the body. (Technically, it rewrites the lambda
object in the translation of the loop$. See rewrite-lambda-object.)
This transforms
(loop$ with tail = x
with a = nil
do
(if (endp tail)
(return a)
(progn (setq a (cons (car tail) a))
(setq tail (cdr tail)))))
to
(loop$ with tail = x
with a = nil
do
(if (consp tail)
(progn (setq a (cons (car tail) a))
(setq tail (cdr tail)))
(return a)))
because (endp x) expands to (not (consp x)) and the branches of
the if are swapped to eliminate the not.
After this rewrite, our generalized lemma no longer matches.
Lesson 2: Do not prove rewrite rules that target loop$
statements containing terms in non-normal form! That is, as with all other
rewrite rules, make sure your target is normalized under your intended
rewrite regime.
So for example, in addition to watching out for non-recursive functions in
the body, be alert for things like expressions that are rearranged by
associativity and commutativity rules. You wouldn't write a rewrite rule
containing a subterm like (append (append a b) c) if you're
right-associating append nests, nor would you include a subterm like
(+ x 1) if you're normalizing arithmetic expressions (in this case to
(+ 1 x)). So don't use such non-normal terms in lemmas about
loop$s!
The entire robust script for the rev-loop$ proof is given below.
(defun rev (x)
(if (endp x)
nil
(append (rev (cdr x)) (list (car x)))))
(defun rev-loop$ (x)
(loop$ with tail = x
with a = nil
do
(if (endp tail)
(return a)
(progn (setq a (cons (car tail) a))
(setq tail (cdr tail))))))
(defthm assoc-of-append
(equal (append (append a b) c)
(append a (append b c))))
(defthm rev-loop$-is-rev-generalized
(equal (loop$ with tail = x
with a = a
do
(if (consp tail)
(progn (setq a (cons (car tail) a))
(setq tail (cdr tail)))
(return a)))
(append (rev x) a)))
(defthm rev-loop$-is-rev
(equal (rev-loop$ x)
(rev x)))
The script is robust in the sense that even if you conditionalize the
generalized lemma with a hypothesis that can be relieved in the main theorem
the lemma will fire and rewrite the loop$ exposed when rev-loop$ is
expanded. Note that the loop$ was written with (endp tail) in the
defun of rev-loop$ but lemma deals with the normalized form of that
body.
Here is another example, this one involving a do loop without any
WITH clauses. That in itself causes no special proof problems, but as
noted in do-loop$, it necessitates the use of a stobj in the body and
that raises issues similar to those just mentioned. So below we introduce a
stobj, st, with one field, fld. We define warrants for
both fld and update-fld, and then we define a function,
stobj-mem, that uses a do loop to determine whether a given element
occurs in the field, simultaneously shortening the list in the field so that
its car is the element in question. Here is the setup.
(defstobj st fld)
(defwarrant fld)
(defwarrant update-fld)
(defun stobj-mem (e st)
(declare (xargs :stobjs (st)
:guard (true-listp (fld st))))
(loop$ do
:values (st)
:guard (and (stp st)
(true-listp (fld st)))
:measure (acl2-count (fld st))
(if (endp (fld st))
(return st)
(if (equal e (car (fld st)))
(return st)
(setq st (update-fld (cdr (fld st)) st))))))
Note that there is no WITH clause but the size of (fld st) is
decreasing.
Suppose we want to prove that after running (stobj-mem e st) on proper
input, the final value of fld is equal to (member e (fld st)). The
desired formal statement is
(defthm stobj-mem-correct
(implies (and (stp st)
(true-listp (fld st))
(warrant fld update-fld))
(let ((st1 (stobj-mem e st)))
(and (stp st1)
(equal (fld st1)
(member e (fld st))))))
:hints ...)
Note that in the theorem we use st1 to denote the final value of the
stobj whose initial value is st. We have to provide the warrants for the
accessor and updater used in the body of the loop$.
This theorem is a little tricky to prove because we're proving a
conjunction and after the (stobj-mem e st) and the (stp st) expand
we get several conjectures, each of which requires induction. It is simply
easier to prove that the loop$ in stobj-mem has the desired
property and then use that lemma. So we first prove:
(defthm stobj-mem-correct-lemma
(implies (and (stp st)
(true-listp (fld st))
(warrant fld update-fld))
(let ((st1 (loop$ do
:values (st)
:guard (and (stp st)
(true-listp (fld st)))
:measure (acl2-count (fld st))
(if (consp (fld st))
(if (equal e (car (fld st)))
(return st)
(setq st (update-fld (cdr (fld st)) st)))
(return st)))))
(and (stp st1)
(equal (fld st1)
(member e (fld st)))))))
But note that we expanded the endp in the statement of this lemma because
endp is built-in in a way that causes it often to expand even when disabled
(as is actually noted in a warning message if we'd left the endp in place).
We also normalized the resulting (if (not (consp (fld st))) ...) as explained
in Lesson 2 above.
Now we'd like to prove the desired theorem about stobj-mem, expecting that
function to expand and then the lemma to hit it and complete the proof. But
that won't work without a little more help! The problem is that the lemma
mentions stp, fld, and update-fld in its left-hand side and those
are non-recursively defined functions that will expand. So to make the lemma
match the rewritten main theorem we must disable those three functions.
(defthm stobj-mem-correct
(implies (and (stp st)
(true-listp (fld st))
(warrant fld update-fld))
(let ((st1 (stobj-mem e st)))
(and (stp st1)
(equal (fld st1)
(member e (fld st))))))
:hints (("Goal" :in-theory (disable stp fld update-fld))))
The Secret Setq Problem
Another issue that comes up when posing lemmas about loop$s is called
the secret setq problem and is best illustrated by example.
Define the following function.
(defun secret-setq-problem (k x)
(loop$ with x = x
with j = 0
do
(cond ((endp x) (return 'bad))
((equal j k) (return 'good))
(t (progn (setq x (cdr x))
(setq j (+ 1 j)))))))
The function counts j up from 0 until it is equal to k,
while cdring x. It returns good if j reaches k
before the list is exhausted, and returns bad otherwise. Thus, this is
a theorem.
(defthm secret-setq-problem-main
(implies (and (natp k)
(< k (len x)))
(equal (secret-setq-problem k x)
'good)))
While secret-setq-problem-main is provable by ACL2, it should be
clear from Lessons 1 and 2 above that we first need to prove a lemma about
the generalized, normalized loop$. Here is a candidate lemma, which is
proved by ACL2.
(defthm secret-setq-problem-lemma
(implies (and (natp j)
(natp k)
(< k (+ j (len x)))
(<= j k))
(equal (loop$ with x = x
with j = j
do
(if (consp x)
(if (equal j k)
(return 'good)
(progn (setq x (cdr x))
(setq j (+ 1 j))))
(return 'bad)))
'good)))
Following Lesson 1, we generalized the initial value of j, which was
0, to j, and we added the hypotheses that j is a natural less
than or equal to k. We generalized the (< k (len x)) which we see
in the main theorem to (< k (+ j (len x))). This accommodates the
arbitrary initial j and simplifies to (len x) when j is
0. Furthermore, as j goes up and x gets shorter, their sum
stays fixed, which is necessary if the generalized hypothesis is going to
survive induction.
Following Lesson 2, we normalized the body. We replaced the (endp x)
by (not (consp x)) and normalized the resulting IF nest.
The lemma is proved automatically by ACL2, using the induction suggested
by the loop$.
However, the attempt to prove the main theorem above will fail! The lemma
doesn't fire because the loop$ target still doesn't match. (Note: we
could forget about the lemma firing automatically. Instead, we could give a
:hint that disables the lemma and :uses the instance of it with
j replaced by 0. That succeeds. But it is valuable for us to
explore why it didn't work as a rewrite rule.)
Sometimes to debug a failed proof it helps to compare the term that a
lemma targets with its intended target in the checkpoint of the failed proof.
This is especially true for loop$s because their translations are so
different from their outward appearance. (See the sections titled
“Semantics” in for-loop$ and do-loop$.) The
following use of the :pr command shows our lemma's true form.
It is the left-hand side, Lhs, we are interested in because it is the
target pattern of the rewrite rule.
ACL2 !>:pr secret-setq-problem-lemma
Rune: (:REWRITE SECRET-SETQ-PROBLEM-LEMMA)
Enabled: T
Hyps: (AND (NATP J)
(NATP K)
(< K (+ J (LEN X)))
(<= J K))
Equiv: EQUAL
Lhs: (DO$
(LAMBDA$ (ALIST)
(ACL2-COUNT (CDR (ASSOC-EQ-SAFE 'X ALIST))))
(LIST (CONS 'X X)
(CONS 'J J)
(CONS 'K K))
(LAMBDA$ (ALIST)
(IF (CONSP (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(IF (EQUAL (CDR (ASSOC-EQ-SAFE 'J ALIST))
(CDR (ASSOC-EQ-SAFE 'K ALIST)))
(LIST :RETURN 'GOOD
(LIST (CONS 'X (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(CONS 'J (CDR (ASSOC-EQ-SAFE 'J ALIST)))
(CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST)))))
(LIST NIL NIL
(LIST (CONS 'X (CDDR (ASSOC-EQ-SAFE 'X ALIST)))
(CONS 'J (+ 1 (CDR (ASSOC-EQ-SAFE 'J ALIST))))
(CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST))))))
(LIST :RETURN 'BAD
(LIST (CONS 'X (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(CONS 'J (CDR (ASSOC-EQ-SAFE 'J ALIST)))
(CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST)))))))
(LAMBDA$ (ALIST)
(LIST NIL NIL
(LIST (CONS 'X (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(CONS 'J (CDR (ASSOC-EQ-SAFE 'J ALIST)))
(CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST))))))
'(NIL) NIL)
Rhs: 'GOOD
Backchain-limit-lst: NIL
Subclass: BACKCHAIN
Loop-stopper: NIL
The actual do$ term term you'll see in the checkpoint of the failed
proof attempt is:
(DO$
(LAMBDA$ (ALIST)
(ACL2-COUNT (CDR (ASSOC-EQ-SAFE 'X ALIST))))
(LIST (CONS 'X X)
'(J . 0)
(CONS 'K K))
(LAMBDA$ (ALIST)
(IF (CONSP (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(IF (EQUAL (CDR (ASSOC-EQ-SAFE 'J ALIST))
(CDR (ASSOC-EQ-SAFE 'K ALIST)))
(LIST :RETURN 'GOOD
(LIST (CONS 'X (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(CONS 'J (CDR (ASSOC-EQ-SAFE 'J ALIST)))
(CONS 'K (CDR (ASSOC-EQ-SAFE 'J ALIST)))))
(LIST NIL NIL
(LIST (CONS 'X (CDDR (ASSOC-EQ-SAFE 'X ALIST)))
(CONS 'J (+ 1 (CDR (ASSOC-EQ-SAFE 'J ALIST))))
(CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST))))))
(LIST :RETURN 'BAD
(LIST (CONS 'X (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(CONS 'J (CDR (ASSOC-EQ-SAFE 'J ALIST)))
(CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST)))))))
(LAMBDA$ (ALIST)
(LIST NIL NIL
(LIST (CONS 'X (CDR (ASSOC-EQ-SAFE 'X ALIST)))
(CONS 'J (CDR (ASSOC-EQ-SAFE 'J ALIST)))
(CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST))))))
'(NIL) NIL)
Note that the Lhs matches the actual term, when J is
instantiated with 0, except in one place: the alist constructed
in the (LIST :RETURN 'GOOD ...) triple binds 'K to the value of
'K in Lhs but binds 'K to the value of 'J in the actual
term. This happens because the actual term was rewritten under the
assumption that the IF test equating the value of 'J to the value
of 'K, and the rewriter substituted the value of 'J for that of
'K because of term ordering. The ACL2 pattern matching routine does
not take account of tests.
We could possibly fix this problem by changing how ACL2 stores lemmas or
how the pattern matcher works. But such changes could have far reaching
consequences across the entire ACL2 regression suite, so we have made no such
changes.
Absent such changes, it's incumbent on the user to phrase the rewrite
rule appropriately. The question is, “How can you make that particular
'K in Lhs be 'J?”
One way would be to rephrase the rewrite rule by using the DO$ term
from the checkpoint in place of the loop$ statement we wrote in
secret-setq-problem-lemma.
Another way to accomplish the same effect is to rewrite the loop$
statement as shown below.
(defthm secret-setq-problem-lemma
(implies (and (natp j)
(natp k)
(< k (+ j (len x)))
(<= j k))
(equal (loop$ with x = x
with j = j
with k = k ; ``new'' var
do
(if (consp x)
(if (equal j k)
(progn (setq k j) ; new setq!
(return 'good))
(progn (setq x (cdr x))
(setq j (+ 1 j))))
(return 'bad)))
'good)))
You can use :tcp to confirm that the translation of the above
loop$ matches the actual term in the checkpoint.
Note that the inclusion of the new “with k = k” does not
add any new subterms to the translation, it merely allows assignment to a
previously used but never assigned variable. The order of the with
clauses determines the order of the alists being constructed, so pay
attention to where 'k is bound in the alists. Also note that the new
setq does not add any new subterms to the translation; it just affects the
final value of 'k on that branch of the if tree. Finally note that
we phrase the loop$ this way in the lemma without changing how we
write the loop$ in the defun. Writing the loop$ this way in
the defun would add an unnecessary setq in the Common Lisp
execution. But there is no need to change how we write the loop$ in the
defun. This lemma matches what comes up when we prove things about the
loop$ in the defun.
Because this matching problem can repaired by adding an unnecessary setq
in the lemma, we call this the “secret setq problem.”
Lesson 3: If the left-hand side of a rewrite rule contains an
loop$ with an if in the body, remember the secret setq
problem. More practically, if a loop$ lemma you've proved fails to
rewrite its target, compare the output of :pr, specifically the
Lhs, to the intended target printed in the checkpoint, and remember the
secret setq problem.
The Hidden Hypothesis Problem
Another issue you may occasionally confront when dealing with inductions
suggested by do loop$s is indicated when the prover fails to prove
the measure conjecture even though you “know” it is provable.
To explain, we have to explain a little about how induction suggested by
do loop$s are done.
From every do loop$ we can derive a proposed recursive function
definition. When the prover sees a do loop$ in a conjecture that
it has decided requires inductions, it generates that derived function, does
an induction analysis for it, and adds any suggestions it gets to the set of
candidate inductions to consider. However, the derived function may not
terminate “normally.” Recall that do$ checks that the
measure goes down before each iteration and returns a default value if that
check fails. Thus, to justify the induction suggested by the generated
function the proof obligations include those that establish that the measure
decreases under the tests leading to further iterations in the loop$
body.
Those tests are not always sufficient to guarantee termination! If the
loop$ came from a guard verified function definition, termination was
proved. But it was proved as part of guard verification. Remember the main
purpose of guards in loop$s: to allow us to execute the loop$ as a
Common Lisp loop. But that execution only happens when we know guards
hold. But loop$s seen by the prover may not come from guard verified
statements and, besides, guards are stripped out of conjectures to be proved
because they're irrelevant to the logical meaning.
However, it is logically valid to condition the induction-time measure
conjectures on hypotheses from the conjecture being proved — and it is
often ineffective to include all of those hypotheses. So ACL2's induction
mechanism chooses some of the available hypotheses and may not choose enough.
This is the “hidden hypothesis problem.” An example is below.
The following function can be admitted and guard verified, meaning the
termination obligation is proved as part of guard verification.
(defun hidden-hyp-problem (lo j)
(declare (xargs :guard (and (natp lo) (natp j) (<= lo j))))
(loop$ with j = j
do
:guard (and (natp lo) (natp j) (<= lo j))
(if (equal lo j)
(return 'good)
(setq j (- j 1)))))
Since since lo and j are both natural numbers and j
is (weakly) above lo and is decremented on iteration, j will
eventually reach lo and the loop$ will stop.
The derived recursive function corresponding to this loop$, which
we'll call derived-fn here, is
(defun derived-fn (lo j)
(if (equal lo j)
'good
(derived-fn lo (- j 1)))).
That derived function doesn't necessarily terminate.
Now let's try to prove that the loop$ always returns 'good.
Note that it doesn't matter if we include guards in the conjecture or not.
They're logically irrelevant and will be eliminated.
However, the following proof attempt fails. The prover chooses to induct
as suggested by the do loop$. The induction scheme selected is
shown.
ACL2 !>(defthm hidden-hyp-problem-main
(implies (and (natp lo)
(natp j)
(<= lo j))
(equal (loop$ with j = j
do
:guard (and (natp lo) (natp j) (<= lo j))
(if (equal lo j)
(return 'good)
(setq j (- j 1))))
'good)))
...
This suggestion was produced using the :induction rule DO$. If we
let (:P J LO) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (AND (NOT (EQUAL LO J))
(:P (+ -1 J) LO)
(INTEGERP J)
(<= 0 J))
(:P J LO))
(IMPLIES (AND (NOT (EQUAL LO J))
(< (+ -1 J) 0)
(INTEGERP J)
(<= 0 J))
(:P J LO))
(IMPLIES (AND (NOT (EQUAL LO J))
(NOT (INTEGERP (+ -1 J)))
(INTEGERP J)
(<= 0 J))
(:P J LO))
(IMPLIES (AND (EQUAL LO J) (INTEGERP J) (<= 0 J))
(:P J LO))
(IMPLIES (AND (INTEGERP J)
(<= 0 J)
(NOT (EQUAL LO J)))
(L< (LEX-FIX (ACL2-COUNT (+ -1 J)))
(LEX-FIX (ACL2-COUNT J))))).
Note that one or more measure conjectures included in the scheme above
justify this induction if they are provable. When applied to the goal
at hand the above induction scheme produces six nontautological subgoals.
...
The first four proof obligations, which are all proved by the prover,
implicitly include the hypotheses that LO is a natural below J
because they're hypotheses in the four conclusions, (:P J LO). But the
last proof obligation has no hypotheses about LO other than the test in
the body of the loop$, (NOT (EQUAL LO J)). This proof obligation
is not a theorem and the proof attempt will fail.
If the prover had just generated the measure conjecture from the
derived-fn the last proof obligation would be even more inadequate!
(IMPLIES (NOT (EQUAL LO J))
(L< (LEX-FIX (ACL2-COUNT (+ -1 J)))
(LEX-FIX (ACL2-COUNT J)))).
But we see that the prover actually augmented the hypothesis from the body
with two literals it assumed were relevant from the conjecture being proved,
namely (INTEGERP J) and (<= 0 J). (The legality of such
augmentation is illustrated by the book
projects/apply/justification-of-do-induction.lisp.) However, it did not
include any facts about LO other than the test in the loop$ body.
This is a manifestation of the hidden hypothesis problem. In this case, we
wish it had included (NATP LO) and (<= LO J). (One can regard this
as a heuristic inadequacy, but enlarging the set of hypotheses can cause
proofs to fail and we've been conservative in our heuristics for augmenting
do loop$ inductions.)
You can fix this by providing an :induct hint. The loop$
statement in the hint below is exactly the loop$ statement in the
theorem except we've added the UPPERCASE text. This proof succeeds.
(defthm hidden-hyp-problem-main
(implies (and (natp lo)
(natp j)
(<= lo j))
(equal (loop$ with j = j
do
(if (equal lo j)
(return 'good)
(setq j (- j 1))))
'good))
:hints (("Goal"
:induct
(loop$ with j = j
do
(IF (AND (NATP LO) (<= LO J))
(if (equal lo j)
(return 'good)
(setq j (- j 1)))
(RETURN 'IRRELEVANT-BASE-CASE))))))
Lesson 4: You can use loop$ to provide induction hints and
those loop$s don't have to be identical to ones in your goal theorem.
In particular, your hint loop$ might contain more case analysis than
the loop$s in your conjecture. You can use this fact to overcome the
hidden hypothesis problem.
Note that the derived function from the loop$ in the hint doesn't
necessarily terminate either (because no mention is made that J is a
natural). But the induction-time proof obligation is provable because it is
still augmented by (INTEGERP J) and (<= 0 J) as before.
Avoiding Some Specially Defined Hint Functions
Another lesson suggested by the example above is that you don't always
have to define a recursive function to suggest certain inductions. Here is
an example. Recall the function rev1 from the beginning of this topic.
Now define the functions that “mark” every element of a list and
that check that every element is “marked”.
(defun mark-all (x)
(if (consp x)
(cons (list 'mark (car x))
(mark-all (cdr x)))
nil))
(defun all-markedp (x)
(if (consp x)
(and (consp (car x))
(eq (car (car x)) 'mark)
(all-markedp (cdr x)))
t)).
Now prove
(thm (implies (all-markedp a)
(all-markedp (rev1 (mark-all x) a))))
No induction suggested by the functions in this theorem is appropriate.
The appropriate induction assumes the theorem for x replaced by (cdr
x) and a replaced by (cons (list 'mark (car x)) a). (This is an
example of rippling as discussed by Bundy, Basin, Hutter and Ireland, in the
book Rippling: Meta-Level Guidance for Mathematical Reasoning,
Cambridge University, UK, 2005. But ACL2's induction heuristics don't
implement rippling.) We could, of course, define a recursive function that
suggests the appropriate induction and provide it as a hint. But in this case
we needn't define a new function. We can just use a loop$.
(thm (implies (all-markedp a)
(all-markedp (rev1 (mark-all x) a)))
:hints (("Goal" :induct
(loop$ with x = x
with a = a
do
(if (consp x)
(progn (setq a (cons (list 'mark (car x)) a))
(setq x (cdr x)))
(return 'base-case)))))).
Other Relevant :DOC Topics
See lp-section-11 of the Loop$ Primer for a narrative of how
we might solve a certain computational problem with a nest of two FOR
loop$. We also show how we verify the guards and then prove that the
loop$ solution is equivalent to a recursive solution. In
lp-section-12 of the primer you'll find some exercises in
proving theorems about FOR Loop$s
(with answers in a Community Book). In lp-section-16 you'll find a
narrative of how we might go about proving a theorem about a DO
Loop$. And in lp-section-17 you'll find exercises in proving
theorems about DO Loop$s (with answers in a Community Book).
