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