		Search-engine friendly clone of the ACL2 documentation.

Debugging

Tail-biting

Rewriting a true term to NIL

On rare occasions, a true term can rewrite to NIL. Such ``tail-biting'' behavior can make the prover fail to prove a theorem but will not make it ``prove'' a non-theorem. This topic explains this behavior, first with one paragraph explaining it in high-level terms and then, for those interested in details, with a specific example. That example includes discussion that exposes more of the ACL2 implementation than is usually exposed in documentation topics, so we expect that most readers will skip it.

When backchaining to rewrite a hypothesis H of a rewrite or linear rule, ACL2 uses the following heuristic: assume that H is false when trying to prove it. That is sound: proposition P is equivalent to proposition (implies (not P) P). We do not discuss why ACL2 does this or why it rarely results in so-called ``tail-biting'': rewriting the hypothesis to NIL by using the fact that it has been assumed false. But that can happen on rare occasions. So if you see a term rewrite to NIL when you know it to be true, consider whether this is because it was encountered earlier during the backchaining process, when it was assumed false.

===== 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 (member a (cdr lst)) to (member a lst), sort of un-opening member.

(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 key-rule above, if we can just establish the hypothesis H of key-rule from the hypotheses of main. The instance of H is (not (member aaa (cdr xxx))). The rewriter cannot establish this because it requires a proof by induction. So the proof is bound to fail here.

(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 ``:HYP 1 rewrote to 'NIL'', i.e., that the relevant instance of H, (not (member aaa (cdr xxx))), rewrote to NIL. This seems to suggest aaa is in (cdr xxx).

But we know it can't be! The hypotheses of main say aaa is a symbol and xxx is a list of natural numbers. So aaa can't be in (cdr xxx). We can prove it:

(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 main:

(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 key-rule rewrite to NIL?

Let's undo back through hyps-of-main-imply-hyp-1 and monitor key-rule, weird, and the definition of member-equal, and also trace system function ancestors-check-builtin, which queries the ancestor-stack, and then repeat the doomed proof attempt for main.

(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 ancestors-check-builtin, but the important one remains.

(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 key-rule and backchained to prove its hypothesis, (not (member aaa (cdr xxx))). We thus assume the negation, (member aaa (cdr xxx)), on the ancestors stack and then open (member aaa (cdr xxx)) with the definition. That results in a call of (member aaa (cdr (cdr xxx))) and we backchain through weird to (member aaa (cdr xxx)) and find it assumed true (on the ancestors-stack). So weird rewrites (member-aaa (cdr (cdr xxx))) to T (propositionally) and so member-equal returns T, so H rewrites to NIL.

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

1. Attempt to rewrite (not (member aaa (copylist (cdr xxx)))) to T.

2. Attempt to rewrite (member aaa (copylist (cdr xxx))) to NIL.

3. Backchain with key-rule to (not (member aaa (cdr xxx))).

4. Assume (member aaa (cdr xxx)) by putting it on the ancestors-stack. This is sound because we are trying to prove (not (member aaa (cdr xxx))), and it is sound to assume (not P) when proving P.

5. Expand (member aaa (cdr xxx)), given (consp (cdr xxx)), to (or (equal aaa (cadr xxx)) (member aaa (cddr xxx)))

6. Rewrite (member aaa (cddr xxx))) using weird.

7. Backchain with weird on (member aaa (cddr xxx)) and relieve its hypotheses under the substitution a := aaa, lst := (cdr xxx).

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

8. So weird applies, hence the following are true:

From 6. (member aaa (cddr xxx))
From 5. (member aaa (cdr xxx))

So 3 fails because (not (member aaa (cdr xxx))) rewrites to NIL.