:usehints for enabled
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
:usehint. 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
F, which is based on an existing lemma. Then the indicated
G, is replaced by the implication
(implies F G). The intention
is that the truth of
F will help in the simplification of
T (true). The ``[Use]'' warning shown above is telling us of the danger
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
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
thmform fails, because the new hypotheses are rewritten to
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-Pas 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