Continuing the discussion from the answer to that question (main text):

In rare cases, something subtle may be going on that prevents the rewriter from being able to establish a hypothesis -- especially, when a hypothesis is a subterm of the left-hand side of the conclusion occurring in a context in which a term may only be replaced by an equal value, not one that is merely Boolean equivalent. Here is a reasonably small example.

;;; Start ACL2 input (defun f (x) (not (not x))) ; Note: The example should work with (defun f (x) x) instead, but that would ; give the system too much help since its "type-reasoning" system would know ; that (f x) = x. ; The following thorem says in Boolean (iff) contexts that we should always ; rewrite (f x) to (if x t nil). (We could actually use x on the right-hand ; side in place of (if x t nil), but this way we the rule is not an ; abbreviation rule and hence we can use :monitor on it.) (defthm f-x-iff-x (iff (f x) (if x t nil))) (in-theory (disable f)) (defun g (x) x) ; If x is not nil, then (g x) is not nil: (defthm g-x-if-x (implies x (g x))) ; NOTE! The rule g-x-if-x immediately above is a good example of one that ; would be better cast as an unconditional rewrite rule. In this case, the ; rule (iff (g x) x) would allow the THM below to get proved. (in-theory (disable g)) ; The following fails because (f x) is not rewritten, even though it is an ; iff-context, i.e. the HYP. of g-x-if-x ; Now comes the subtle problem. As we will see below, when the rewriter ; attempts to apply the rule g-x-if-x to (g (f x)), it will try to verify that ; (f x) is not nil. But by then it has already attempted to rewrite (f x) to a ; term equal to (f x), not just Boolean equivalent (because (f x) is an ; argument of g), and the best it could do was return (f x) from that attempt. ; It does not try to rewrite (f x) again when relieving the hypothesis of ; g-x-if-x, which is too bad since otherwise it could have applied f-x-iff-x. (thm (implies x (g (f x)))) ; The rest of this FAQ entry is in two parts. First we show the use of the ; break-rewrite utility. Second, we trace parts of the rewriter, an activity ; that is quite obscure and is really intended for those interested in the ACL2 ; implementation. ; First, we use break-rewrite as shown below to try to see why the proof fails. ; Unfortunately, it appears below that f-x-iff-x is not even being tried! #| ACL2 !>:brr t The monitored runes are: NIL T ACL2 !>:monitor (:rewrite f-x-iff-x) t (((:REWRITE F-X-IFF-X) 'T)) ACL2 !>:monitor (:rewrite g-x-if-x) t (((:REWRITE F-X-IFF-X) 'T) ((:REWRITE G-X-IF-X) 'T)) ACL2 !>(thm (implies x (g (f x)))) (1 Breaking (:REWRITE G-X-IF-X) on (G (F X)): 1 ACL2 >:go 1x (:REWRITE G-X-IF-X) failed because :HYP 1 rewrote to (F X). 1) Name the formula above *1. No induction schemes are suggested by *1. Consequently, the proof attempt has failed. Summary Form: ( THM ...) Rules: ((:DEFINITION IMPLIES)) Warnings: None Time: 0.10 seconds (prove: 0.08, print: 0.00, other: 0.02) ******** FAILED ******** See :DOC failure ******** FAILED ******** ACL2 !> |#Finally, here is our trace, carried out in a GCL version of ACL2. NOTE: This version of trace will probably not work in Allegro versions 5.0.1 and earlier.

#| ACL2 !>:q Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2>(trace (rewrite :entry (list (nth 0 si::arglist) ; term (nth 1 si::arglist) ; alist (nth 5 si::arglist) ; geneqv )) (rewrite-with-lemma :entry (list (nth 0 si::arglist) ; term (cadr (access rewrite-rule (nth 1 si::arglist) :rune)) ; lemma name (nth 4 si::arglist) ; geneqv ))) (REWRITE REWRITE-WITH-LEMMA ACL2_*1*_ACL2::REWRITE-WITH-LEMMA ACL2_*1*_ACL2::REWRITE) ACL2>(LP) ACL2 Version 2.5. Level 1. Cbd "/u/kaufmann/test/". Type :help for help. ACL2 !>(thm (implies x (g (f x)))) 1> (REWRITE X NIL ((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL)))> <1 (REWRITE X NIL)> 1> (REWRITE (G (F X)) NIL ((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL)))> ; Notice (second NIL on next line) that we are preserving ; equality, not Boolean equivalence. Hence we are also ; preserving equality in the REWRITE-WITH-LEMMA call that ; follows: 2> (REWRITE (F X) NIL NIL)> 3> (REWRITE X NIL NIL)> <3 (REWRITE X NIL)> 3> (REWRITE-WITH-LEMMA (F X) F-X-IFF-X NIL)> ; The lemma F-X-IFF-X does not apply because the context ; requires preservation of equality, not mere Boolean equivalence. ; At this point that is not a problem; in fact it is entirely ; appropriate. <3 (REWRITE-WITH-LEMMA NIL (F X) NIL)> ; So, (F X) rewrote to itself: <2 (REWRITE (F X) NIL)> 2> (REWRITE-WITH-LEMMA (G (F X)) G-X-IF-X ((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL)))> ; Notice that in the next call, we are not rewriting the term (F X), but ; rather, are rewriting X where X is bound to (F X). This is unfortunate ; since unlike the earlier rewrite of this term, we now have a Boolean ; context (indicated by the IFF below), so this time the lemma F-X-IFF-X ; would have applied. This call of REWRITE is thus doomed simply to ; return (F X). 3> (REWRITE X ((X F X)) ((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL)))> <3 (REWRITE (F X) NIL)> <2 (REWRITE-WITH-LEMMA NIL (G (F X)) NIL)> <1 (REWRITE (G (F X)) NIL)> Name the formula above *1. No induction schemes are suggested by *1. Consequently, the proof attempt has failed. Summary Form: ( THM ...) Rules: ((:DEFINITION IMPLIES)) Warnings: None Time: 0.03 seconds (prove: 0.02, print: 0.00, other: 0.01) ******** FAILED ******** See :DOC failure ******** FAILED ******** ACL2 !> |#