Some subtle aspects of the counting done by `accumulated-persistence`

In this topic we cover the overcounting of ``useful'' rune application attempts, and we describe how ``useless'' rune application attempts can actually be critical for a proof's success. We conclude with a few words about counting frames when there are nested (recursive) applications of a rune.

*Overcounting of ``useful'' rune application attempts.* Not every
rune application may be necessary for a proof's success. Consider for
example:

(thm (equal (car (cons a (cdr (cons b x)))) a))

Then `rewrite` rules

As of this writing, we consider every `forward-chaining` rule
application to be ``useful'', for simplicity of the implementation. Moreover,
our counting of these rules is such that a single rule may be counted more
than once.

*How ``useless'' attempts can be critical for a proof's success.* The
command

; Assume p0. We want to prove p1. ; Key rule: p0 -> p1 = t ; Bad rule that could ruin the proof: p3 -> p1 = p2 ; But unfortunately, we know p3: p0 -> p3 ; Important ``useless'' rule, preventing ``bad rule'' above from firing: p3 = p4

The following event captures the rules described above.

(encapsulate ((p0 (x) t) (p1 (x) t) (p2 (x) t) (p3 (x) t) (p4 (x) t)) (local (defun p0 (x) x)) (local (defun p1 (x) x)) (local (defun p2 (x) x)) (local (defun p3 (x) x)) (local (defun p4 (x) x)) ; Key rule: (defthm p0-implies-p1 (implies (p0 x) (p1 x))) ; Bad rule that could ruin the proof: (defthm p3-implies-p1-is-p2 (implies (p3 x) (equal (p1 x) (p2 x)))) ; But unfortunately, we know p3: (defthm p0-implies-p3 (implies (p0 x) (p3 x))) ; Important ``useless'' rule, preventing p3-implies-p1-is-p2 from firing: (defthm p3-is-p4 (equal (p3 x) (p4 x))))

Now we can see that

(accumulated-persistence t) (thm (implies (p0 x) (p1 x))) (show-accumulated-persistence)

If instead we first evaluate

Nevertheless, in general it is probably safe to disable rules reported as
``useless'' by

Remark. The example above suggests a surprising fact: on rare occasions, a
proof may fail when you give an `in-theory` hint consisting of
exactly the runes reported in a proof that succeeds. For, imagine a
rule R that is needed in part of the proof but is ``bad'' in a second part,
and that some other, ``useless'' rule prevents the application of R in that
second part. The example above suggests that disabling this ``useless'' rule
can allow the second application of R, thus preventing the proof.

Finally we discuss accumulation into frame counts in the case of a nested (recursive) application of a rule: that is, the case that during the application of a rule, the rule is applied again — in particular, while relieving a hypothesis or rewriting the right-hand side from the original rule application. Recall that the implementation of accumulated-persistence keeps a stack of runes currently being applied; thus, we are considering here the case that a rune is pushed onto a stack on which it already resides. In that case, we count tries as usual but we avoid accumulating until we reach the outermost (topmost) application of that rune. Consider the following example.

(defun mem (a x) (if (atom x) nil (or (equal a (car x)) (mem a (cdr x)))))

Now suppose we consider the theorem