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