### PRACTICE-FORMULATING-STRONG-RULES-2

rules suggested by `(TRUE-LISTP (REV (FOO A)))`

Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

What rules come to mind when looking at the following subterm of a Key
Checkpoint? Think of *strong* rules (see strong-rewrite-rules).

(TRUE-LISTP (REV (FOO A)))

The definition of `rev`

in this problem is

(defun rev (x)
(if (endp x)
nil
(append (rev (cdr x)) (list (car x)))))

Since the definition terminates with an `endp`

test and otherwise `cdr`

s
the argument, the author of `rev`

was clearly expecting `x`

to be a
`true-listp`

. (Indeed, the ``guard'' for `rev`

must require include
`(true-listp x)`

since that is `endp`

's guard.) So you're naturally
justified in limiting your thoughts about `(rev x)`

to `x`

that are
true-lists. This gives rise to the theorem:

(defthm true-listp-rev-weak
(implies (true-listp x)
(true-listp (rev x))))

This is the kind of thinking illustrated in the earlier `append`

example
(see practice-formulating-strong-rules-1) and, to paraphrase Z in *Men in Black*,
it exemplifies ``everything we've come to expect from years of training with
typed languages.''
But logically speaking, the definition of `rev`

does not require `x`

to
be a `true-listp`

. It can be any object at all: ACL2 functions are total.
`Rev`

either returns `nil`

or the result of appending a singleton list
onto the right end of its recursive result. That `append`

always returns
a `true-listp`

since the singleton list is a true
list. (See practice-formulating-strong-rules-1.)

So this is a theorem and a very useful :`rewrite`

rule:

(defthm true-listp-rev-strong
(true-listp (rev x))).

Use your browser's **Back Button** now to return to
practice-formulating-strong-rules.