Practice-formulating-strong-rules-2
Rules suggested by (TRUE-LISTP (REV (FOO A)))
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 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 call of
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.
