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
In a sense,
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
(implies (and (true-listp x) (true-listp y)) ...)
to get ``comfortable.'' Then, thinking about when
(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
(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))).
The weak version of the rule allows us to reduce
Technical Note: The weak version of the rule is a useful
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.