		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Practice-formulating-strong-rules-1

Rules suggested by (TRUE-LISTP (APPEND (FOO A) (BAR B)))

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