(TRUE-LISTP (APPEND (FOO A) (BAR B)))
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 (APPEND (FOO A) (BAR B)))
Obviously, you must think about the conditions under which (APPEND x y)
returns a true-list. Recall that APPEND concatentates x and y,
with y being the terminal sublist. Its definition is equivalent
to
(defun append (x y)
(if (endp x)
y
(cons (car x)
(append (cdr x) y))))
Technical Note: Append is really a macro that permits you to
write calls of append with more than two arguments.In a sense, append ``expects'' its arguments to be lists ending in nil, so-called
true-listps. (Such expectations are formalized in ACL2 by the notion of
the ``guard'' 
of the function, but we strongly recommend not investigating
guards until you're good at using the system.)
New users frequently start every new theorem by listing all their
expectations on the arguments of functions in the problem. For example, if
the new user wants to make some statement about when (append x y) is a
true-listp, it is not uncommon for him or her first to write:
(implies (and (true-listp x)
(true-listp y))
...)
to get ``comfortable.'' Then, thinking about when (append x y) is a
true-listp is easy: it always returns a true-listp.
It's always a true-listp.'' This thinking produces the theorem:
(defthm true-listp-append-really-weak
(implies (and (true-listp x)
(true-listp y))
(true-listp (append x y))))
You'll note we gave it a name suggesting it is ``really weak.''One sense in which it is weak is that it has an unnecessary hypothesis.
If y is a true-listp, then (append x y) is too, whether
x is a true-listp or not. In ACL2, all functions are total.
Logically speaking, it doesn't matter whether endp expects its argument
to be a true-listp or not, it behaves. (Append x y) either returns
y or a cons whose second argument is generated by append. Thus,
if y is a true-listp, the answer is too. So here is an improved
version of the rule:
(defthm true-listp-append-weak
(implies (true-listp y)
(true-listp (append x y))))
We still think of it as ``weak'' because it has a hypothesis that limits
its applicability.The strong version of the rule is
(defthm true-listp-append-strong
(equal (true-listp (append x y))
(true-listp y))).
That is, append returns a true-listp precisely when its second
argument is a true-listp. We recommend that the strong version be made
a :rewrite rule.The weak version of the rule allows us to reduce (TRUE-LISTP (APPEND x y)) to true if
we can show that (TRUE-LISTP y) is true. But suppose (TRUE-LISTP y) is actually
false. Then (TRUE-LISTP (APPEND x y)) would not simplify under the weak version of
the rule. But under the strong version it would simplify to NIL.
Technical Note: The weak version of the rule is a
useful :type-prescription rule. The type mechanism cannot
currently exploit the strong version of the rule.
The strategy of ``getting comfortable'' by adding a bunch of hypotheses before you know you need them is not conducive to creating strong rules. We tend to state the main relationship that we intuit about some function and then add the hypotheses we need to make it true. In this case, there were no necessary hypotheses. But if there are, we first identify them and then we ask ``what can I say about the function if these hypotheses aren't true?'' and try to strengthen the statement still further.
Use your browser's Back Button now to return to practice-formulating-strong-rules.
