:use hints for enabled :rewrite rules
Major Section: MISCELLANEOUS
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 an enabled :REWRITE or :DEFINITION rule, so you may want to consider disabling (:REWRITE CDR-CONS) in the hint provided for Subgoal *1/1.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.
