`(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-listp`

s. (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`

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