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))
As of this writing, we consider every
How ``useless'' attempts can be critical for a proof's success. The
; 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
Remark. The example above suggests a surprising fact: on rare occasions, a
proof may fail when you give an
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