DETAILS to question:

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 !>

|#

#|

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 !>

|#