		Search-engine friendly clone of the ACL2 documentation.

Theories

Using-enabled-rules

Avoiding :use hints for enabled :rewrite rules

Consider the following (admittedly silly) example.

(thm (equal (append (append x y) z) (append x y z))
     :hints (("Subgoal *1/1" :use cdr-cons)))

ACL2's output includes the following warning.

ACL2 Warning [Use] in ( THM ...):  It is unusual to :USE the formula
of an enabled :REWRITE or :DEFINITION rule, so you may want to consider
disabling (:REWRITE CDR-CONS) in the hint provided for Subgoal *1/1.
See :DOC using-enabled-rules.

The warning is saying that if you leave the rewrite rule enabled, ACL2 may simplify away the hypothesis added by the :use hint. We now explain this danger in more detail and show how disabling the rule can solve this problem.

Recall (see hints) how :use hints work. Such a hint specifies a formula, F, which is based on an existing lemma. Then the indicated goal, G, is replaced by the implication (implies F G). The intention is that the truth of F will help in the simplification of G to T (true). The ``[Use]'' warning shown above is telling us of the danger that F may be rewritten to T, reducing the implication above to (implies T G) — thus, sadly, F has disappeared and is not available to help with the simplification of G.

Consider the following tiny example.

(defun p (x) (cons x x))
(defthm car-p
   (equal (car (p x)) x))
(in-theory (disable p (:type-prescription p)))
(thm (implies (equal (p x1) (p x2))
              (equal x1 x2))
     :hints (("Goal"
              :use ((:instance car-p (x x1))
                    (:instance car-p (x x2))))))

The proof of the final thm form fails, because the new hypotheses are rewritten to t using the :rewrite rule CAR-P, in the manner described above. The following proof log shows the new hypotheses and their disappearance via rewriting.

We augment the goal with the hypotheses provided by the :USE hint.
These hypotheses can be derived from CAR-P via instantiation.  We are
left with the following subgoal.

Goal'
(IMPLIES (AND (EQUAL (CAR (P X1)) X1)
              (EQUAL (CAR (P X2)) X2))
         (IMPLIES (EQUAL (P X1) (P X2))
                  (EQUAL X1 X2))).

By the simple :rewrite rule CAR-P we reduce the conjecture to

Goal''
(IMPLIES (EQUAL (P X1) (P X2))
         (EQUAL X1 X2)).

When we disable the rule CAR-P as follows, the proof succeeds.

(thm (implies (equal (p x1) (p x2))
              (equal x1 x2))
     :hints (("Goal"
              :use ((:instance car-p (x x1))
                    (:instance car-p (x x2)))
              :in-theory (disable car-p))))

In general, then, a solution is to disable the rewrite rule that you are supplying in a :use hint.