Rewriting a true term to

On rare occasions, a true term can rewrite to

When backchaining to rewrite a hypothesis

===== Maybe stop here (lower-level explanation follows)! =====

The example below shows how tail-biting can happen. As noted above,
beware: this explanation is closer to the implementation than is found in most
of the ACL2 documentation. We give the example in full first, and then we
conclude with a more concise summary. Key to this explanation is the notion
of the *ancestors-stack*, which is a data structure kept by the rewriter
as it backchains through hypotheses, to record the negation of each hypothesis
encountered during backchaining.

We begin with a very simple definition and theorem. Note that we treat
`member` below as `member-equal`, to simplify the exposition.

(defun copylist (x) (if (endp x) nil (cons (car x) (copylist (cdr x))))) (defthm key-rule (implies (not (member a lst)) ; hypothesis later denoted as ``H'' (not (member a (copylist lst)))))

The following ``weird'' rule backchains from

(defthm weird (implies (and (consp lst) (member a lst) (not (equal a (car lst)))) (member a (cdr lst))))

Now here is our main theorem. It ought to follow by simplification from

(defthm main (implies (and (consp (cdr xxx)) (nat-listp xxx) (symbolp aaa)) (not (member aaa (copylist (cdr xxx))))) :hints (("Goal" :do-not-induct t :do-not '(eliminate-destructors))))

So we decide to monitor key-rule and see why it failed:

(monitor! '(:rewrite key-rule) t) (defthm main ...) ; exactly as above :eval :a!

And we see that `brr` reports that ``

But we know it can't be! The hypotheses of main say

(defthm hyps-of-main-imply-hyp-1 (implies (and (consp (cdr xxx)) (nat-listp xxx) (symbolp aaa)) (not (member aaa (cdr xxx)))))

And using that rule we can now prove

(defthm main (implies (and (consp (cdr xxx)) (nat-listp xxx) (symbolp aaa)) (not (member aaa (copylist (cdr xxx))))) :hints (("Goal" :do-not-induct t :do-not '(eliminate-destructors))))

So the question is: why did the hypothesis of

Let's undo back through `member-equal`, and
also trace system function

(ubt! 'hyps-of-main-imply-hyp-1) (monitor '(:rewrite key-rule) ''(:go)) (monitor '(:rewrite weird) ''(:go)) (monitor '(:definition member-equal) ''(:go)) (trace$ ancestors-check-builtin) (defthm main (implies (and (consp (cdr xxx)) (nat-listp xxx) (symbolp aaa)) (not (member aaa (copylist (cdr xxx))))) :hints (("Goal" :do-not-induct t :do-not '(eliminate-destructors))))

Here is the series of breaks on (:REWRITE WEIRD), except that the second
break is elided because you will see at the subsequent ``2x (:REWRITE WEIRD)
failed...'' that everything that goes on there is irrelevant. Also deleted
are some irrelevant calls of

(1 Breaking (:REWRITE KEY-RULE) on (MEMBER-EQUAL AAA (COPYLIST (CDR XXX))): 1 ACL2 >:GO (2 Breaking (:REWRITE WEIRD) on (MEMBER-EQUAL AAA (CDR XXX)): ... 2x (:REWRITE WEIRD) failed because :HYP 2 rewrote to (MEMBER-EQUAL AAA (CDR XXX)). 2) (2 Breaking (:DEFINITION MEMBER-EQUAL) on (MEMBER-EQUAL AAA (CDR XXX)): 2 ACL2 >:GO (3 Breaking (:REWRITE WEIRD) on (MEMBER-EQUAL AAA (CDR (CDR XXX))): 3 ACL2 >:GO 1> (ANCESTORS-CHECK-BUILTIN (MEMBER-EQUAL AAA (CDR XXX)) (((MEMBER-EQUAL AAA (CDR XXX)) (MEMBER-EQUAL AAA (CDR XXX)) 2 2 0 ((:REWRITE KEY-RULE)) . 1)) ((:REWRITE WEIRD))) <1 (ANCESTORS-CHECK-BUILTIN T T) 3 (:REWRITE WEIRD) produced 'T. 3) 2 (:DEFINITION MEMBER-EQUAL) produced 'T. 2) 1x (:REWRITE KEY-RULE) failed because :HYP 1 rewrote to 'NIL. (See :DOC tail-biting if this surprises you.) 1)

So we've entered the break on

This is not unsound; it is just tail biting. Here is a summary of what has happened.

1. Attempt to rewrite

2. Attempt to rewrite

3. Backchain with

4. Assume

5. Expand

6. Rewrite

7. Backchain with weird on (member aaa (cddr xxx)) and relieve its
hypotheses under the substitution

- a.
(consp (cdr xxx)) is true (hypothesis ofmain ). - b.
(member aaa (cdr xxx)) is true (TAIL BITING!). - c.
(not (equal aaa (car (cdr xxx)))) is true, presumably from expansion of hypotheses ofmain .

8. So