why change the default action on rewriting

See rewrite-lambda-object and `rewrite-lambda-object-actions` for background information on how the ACL2
rewriter behaves on certain quoted

There are three basic actions the rewriter might take when it encounters
a suitable

- recursively rewrite the body to get a new body,

by rewriting in the theory described in`rewrite-lambda-objects-theory` - just clean it up syntactically,

by rewriting in the theory described by`syntactically-clean-lambda-objects-theory`, or - do nothing — leave
lambda object constants untouched.

by rewriting in the theory described by`hands-off-lambda-objects-theory`.

The reason we have several options has to do with the representation of
`ev$` they can become identical.

For example,

The problem is greatly magnified by the way `ilk`

Consider the translation of a

ACL2 !>:trans (loop$ for x on a thereis (if (equal (car x) b) x nil)) (RETURN-LAST 'PROGN '(LOOP$ FOR X ON A THEREIS (IF (EQUAL (CAR X) B) X NIL)) (THEREIS$+ '(LAMBDA (LOOP$-GVARS LOOP$-IVARS) (DECLARE (XARGS :GUARD (IF (TRUE-LISTP LOOP$-GVARS) (IF (EQUAL (LEN LOOP$-GVARS) '1) (IF (TRUE-LISTP LOOP$-IVARS) (EQUAL (LEN LOOP$-IVARS) '1) 'NIL) 'NIL) 'NIL) :SPLIT-TYPES T) (IGNORABLE LOOP$-GVARS LOOP$-IVARS)) (RETURN-LAST 'PROGN '(LAMBDA$ (LOOP$-GVARS LOOP$-IVARS) (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOOP$-GVARS) (EQUAL (LEN LOOP$-GVARS) 1) (TRUE-LISTP LOOP$-IVARS) (EQUAL (LEN LOOP$-IVARS) 1)))) (LET ((B (CAR LOOP$-GVARS)) (X (CAR LOOP$-IVARS))) (DECLARE (IGNORABLE E X)) (IF (EQUAL (CAR X) B) X NIL))) ((LAMBDA (B X) (IF (EQUAL (CAR X) B) X 'NIL)) (CAR LOOP$-GVARS) (CAR LOOP$-IVARS)))) (CONS B 'NIL) (LOOP$-AS (CONS (TAILS A) 'NIL)))) => *

The predicate being mapped is the quoted

'(LAMBDA (LOOP$-GVARS LOOP$-IVARS) ((LAMBDA (B X) (IF (EQUAL (CAR X) B) X 'NIL)) (CAR LOOP$-GVARS) (CAR LOOP$-IVARS)))

But now consider the closely related

(loop$ for y on aaa thereis (if (equal (car y) bbb) y nil))

The

'(LAMBDA (LOOP$-GVARS LOOP$-IVARS) ((LAMBDA (BBB Y) (IF (EQUAL (CAR Y) BBB) Y 'NIL)) (CAR LOOP$-GVARS) (CAR LOOP$-IVARS)))

But note that this

Thus, the translations of those two

Fortunately, it is sound to replace the body of a `ev$`. That can be done either by
rewriting the body or by syntactically cleaning the body. It turns out that
both rewriting and syntactic cleaning produce the same result in this case
and reduce these two distinct

'(LAMBDA (LOOP$-GVARS LOOP$-IVARS) (IF (EQUAL (CAR (CAR LOOP$-IVARS)) (CAR LOOP$-GVARS)) (CAR LOOP$-IVARS) 'NIL))

Actually, all that is needed in this case is the beta reduction of the two bodies.

Syntactic cleaning eliminates declarations, guards, and other
compiler-related tags introduced by translation of `do$` by `tc`.

ACL2 !>:tc (loop$ for x on a thereis (if (equal (car x) b) x nil)) (THEREIS$+ '(LAMBDA (LOOP$-GVARS LOOP$-IVARS) (IF (EQUAL (CAR (CAR LOOP$-IVARS)) (CAR LOOP$-GVARS)) (CAR LOOP$-IVARS) 'NIL)) (CONS B 'NIL) (LOOP$-AS (CONS (TAILS A) 'NIL)))

Note that the free variables of the term are

(Note: The related command `tcp` translates, cleans, and then
converts the internal form of the term into the “pretty”
user-level syntax. E.g., it converts the quoted

**Before a newly proved : rewrite or :linear
rule is stored, the conclusion is syntactically cleaned.**

Like syntactic cleaning, rewriting eliminates declarations, guards, and
other compiler-related tags and does beta reduction — but these
transformations are generally carried out by rules whose enabled status can
be altered. Furthermore, rewriting applies

As noted earlier, there are three basic actions the rewriter might take
when it encounters a suitable

- recursively rewrite the body to get a new body,
- just clean it up syntactically, or
- do nothing — leave
lambda object constants untouched.

Since rules are cleaned before storage, it is almost always the case that
you will want the prover either to rewrite

So which of the three actions do you want the rewriter to take when it
encounters an eligible

- rewrite the body — best if there are multiple
lambda objects in the conjecture that need to be written to be identified, and in simple cases rewriting is equivalent to syntactic cleaning - syntactic cleaning — best if you want the
lambda objects in the conjecture to match:rewrite or:linear rules containing closely relatedlambda objects, but you find that otherwise necessary:rewrite rules cause the rewriter to “overshoot” the syntactically cleaned term as illustrated further below - hands off — fairly unuseful since rules are cleaned up before
storage. However, one use of this is if you prove a lemma containing a
lambda object but store it with:rule-classes nil and then:use an instance of it in the:hints for some conjecture that involves the very samelambda objects.

We now illstrate some typical problems that arise when proving theorems
about

**Why you might want to use syntactic cleaning:** Suppose you prove the
`last`.

(defthm loop$-can-be-last (implies (listp a) (equal (loop$ for x on a thereis (if (atom (cdr x)) x nil)) (last a))))

What term does this rule target? We can answer that by using the
`tc` command.

ACL2 !>:tc (loop$ for x on a thereis (if (atom (cdr x)) x nil)) (THEREIS$ '(LAMBDA (LOOP$-IVAR) (IF (ATOM (CDR LOOP$-IVAR)) LOOP$-IVAR 'NIL)) (TAILS A))

By the way, a more common way to see the rules created by an event is to
use the `pr` command. But that command displays the terms of the
rule in user-level syntax and we want to see the internal form here. The
“

Now imagine you are proving a conjecture that involves that identical (!)
`rewrite-lambda-objects-theory`. ACL2 starts up in such a
theory and unless you've changed the enabled status of the

You might expect the

The reason is that before the rewriter rewrites the

'(LAMBDA (LOOP$-IVAR) (IF (CONSP (CDR LOOP$-IVAR)) 'NIL LOOP$-IVAR))

So when the rewriter then tries to rewrite the

If the rewritten goal is printed, as it is likely to be a checkpoint, you
will see the rewritten body with the

One way to respond to this problem would be to “hobble” the rewriter
by shifting over to syntactic cleaning of quoted

:in-theory (syntactically-clean-lambda-objects-theory)

which would prevent the rewriter from diving into the bodies of

**Why you should probably use rewriting:** There is a deeper lesson
here than just that you might want to hobble the rewriter to prevent it from
diving into quoted

(defthm loop$-can-be-last (implies (listp a) (equal (loop$ for x on a thereis (if (consp (cdr x)) nil x)) (last a))))

This version of the rule would not only rewrite the

(loop$ for x on a thereis (if (atom (cdr x)) x nil))

because, as illustrated above, the rewriter by default dives into the
translated

Furthermore, because

(loop$ for rest on (aaa aa) thereis (let ((z (cdr rest))) (and (atom z) rest))

**But not all such problems can be solved by switching between rewriting
quoted lambda objects and just cleaning them up!**

Consider this rewrite rule. The

(defthm loop$-can-be-member (equal (loop$ for x on a thereis (if (equal (car x) b) x nil)) (member b a)))

You might expect that when the rewriter encounters (an instance of) such a

For example, if we then tried to prove a conjecture mentioning

(loop$ for x on aaa thereis (if (equal (car x) bbb) x nil))

the

But it is easy to misjudge whether a given

Suppose our goal conjecture contained

(loop$ for x on (aaa aa) thereis (if (equal (car x) (bbb bb)) x nil))

This

Will that

To understand why not, we first have to compare the internal forms of the
two

lhs of rule target (thereis$+ (thereis$+ '(lambda '(lambda (loop$-gvars loop$-ivars) (loop$-gvars loop$-ivars) (if (equal (if (equal (car (car loop$-ivars)) (car (car loop$-ivars)) (CAR LOOP$-GVARS)) (BBB (CAR LOOP$-GVARS))) ; [1] (car loop$-ivars) (car loop$-ivars) 'nil)) 'nil)) (cons B 'nil) (cons BB 'nil) ; [2] (loop$-as (loop$-as (cons (tails A) 'nil))) (cons (tails (AAA AA)) 'nil))) ; [3]

Note that the target is not an instance of the lefthand side of the rule
— but only because of the difference on line [1]. Lines [2] and [3] of
the lefthand side can be instantiated to become those lines in the target.
But because of [1] our

This kind of problem cannot be fixed by fiddling with how the prover
treats

target target' (thereis$+ (thereis$+ '(lambda '(lambda (loop$-gvars loop$-ivars) (loop$-gvars loop$-ivars) (if (equal (if (equal (car (car loop$-ivars)) (car (car loop$-ivars)) (BBB (CAR LOOP$-GVARS))) (CAR LOOP$-GVARS)) ; [1] (car loop$-ivars) (car loop$-ivars) 'nil)) 'nil)) (cons BB 'nil) (cons (BBB BB) 'nil) ; [2] (loop$-as (loop$-as (cons (tails (aaa aa)) 'nil))) (cons (tails (aaa aa)) 'nil)))

Note that

Here is a suitable rewrite rule for this particular instance of this
phenomenon. We write it as a

(defthm example-of-constant-subterm-abstraction (implies (warrant bbb) (equal (loop$ for xxx on a thereis (if (equal (car xxx) (bbb bb)) xxx nil)) (let ((zzz (bbb bb))) (loop$ for xxx on a thereis (if (equal (car xxx) zzz) xxx nil))))))

This illustrates another lesson. Remember that we're imagining a proof of
some conjecture that involves a

Put another way, by writing the

**Keep unchanging subterms of loop$ bodies as variables and compute
their values outside of the lambda.** Basically, try to write the most
general

Finally, these difficulties are exacerbated by the ease with which
**don't use
loop$!** Instead, learn to write the corresponding terms, e.g., try
writing a