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.