Stating and proving theorems about

In this topic we give some advice about how to state and prove
theorems involving

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

For example, rather than write instances of

(loop$ for a in x as b in y sum (* a b))

it is better to define

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

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

(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

(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

With that theorem available, the proof of

Now consider defining reverse with a

(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 attept to prove that

(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

ACL2 will prove the lemma above, if the associativity of

**Lesson 1**: If a

The lemma above,

(defthm rev-loop$-is-rev (equal (rev-loop$ x) (rev x))).

But as stated,

Recall that the prover always expands enabled functions that are not
explicitly recursive. And

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

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

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

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 *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

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

After this rewrite, our generalized lemma no longer matches.

**Lesson 2**: Do not prove rewrite rules that target

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

The entire robust script for the

(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

Another issue that comes up when posing lemmas about *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

(defthm secret-setq-problem-main (implies (and (natp k) (< k (len x))) (equal (secret-setq-problem k x) 'good)))

While

(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

Following Lesson 2, we normalized the body. We replaced the

The lemma is proved automatically by ACL2, using the induction suggested
by the

However, the attempt to prove the main theorem above will fail! The lemma
doesn't fire because the

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 `pr` command shows our lemma's true form.
It is the left-hand side,

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 NIL) Rhs: 'GOOD Backchain-limit-lst: NIL Subclass: BACKCHAIN Loop-stopper: NIL

The actual

(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 NIL)

Note that the *except* in one place: the alist constructed
in the

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

One way would be to rephrase the rewrite rule by using the

Another way to accomplish the same effect is to rewrite the

(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

Note that the inclusion of the new “*without changing how we
write the loop$ in the defun.* Writing the

Because this matching problem can repaired by adding an unnecessary

**Lesson 3:** If the left-hand side of a rewrite rule contains an

Another issue you may occasionally confront when dealing with inductions
suggested by

From every `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

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

The derived recursive function corresponding to this

(defun derived-fn (lo j) (if (equal lo j) 'good (derived-fn lo (- j 1)))).

That derived function doesn't terminate.

Now let's try to prove that the

However, the following proof attempt fails. The prover chooses to induct
as suggested by the

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

If the prover had just generated the measure conjecture from the

(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

You can fix this by providing an

(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

Note that the derived function from the

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

(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 *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

(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)))))).

See lp-section-11 of the