DETAILS to question:

Why isn't this rewrite rule being applied?

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:
ACL2 !>:monitor (:rewrite f-x-iff-x) t
ACL2 !>:monitor (:rewrite g-x-if-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).

Name the formula above *1.

No induction schemes are suggested by *1.  Consequently, the proof
attempt has failed.

Form:  ( THM ...)
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
	     :entry (list (nth 0 si::arglist) ; term
			  (cadr (access rewrite-rule (nth 1 si::arglist) :rune)) ; lemma name
			  (nth 4 si::arglist) ; geneqv


ACL2 Version 2.5.  Level 1.  Cbd 
Type :help for help.

ACL2 !>(thm (implies x (g (f x))))
              ((NIL IFF
  1> (REWRITE (G (F X))
              ((NIL IFF
    ; 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)>
      ; 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.
    ; So, (F X) rewrote to itself:
    <2 (REWRITE (F X) NIL)>
                           ((NIL IFF
      ; 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
      <3 (REWRITE (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.

Form:  ( THM ...)
Warnings:  None
Time:  0.03 seconds (prove: 0.02, print: 0.00, other: 0.01)

******** FAILED ********  See :DOC failure  ******** FAILED ********
ACL2 !>