Variant of prog2$ to help debug evaluation failures during proofs
Semantically,
Also see hide for further discussion of how to avoid such proof
failures, and for how to keep the prover from inserting a
Forms:
(HIDE (COMMENT "Failed attempt to call constrained function <fn>" <term>)) (HIDE (COMMENT "Failed attempt to call non-executable function <fn>" <term>))
Consider the following example.
(defstub f (x) t) (defun g (x) (cons (f x) x)) (defun h (x) (cons x (cdr (g x)))) (thm (equal (h 3) '(3 . 3)))
The proof attempt fails for the thm call, indicating the checkpoint shown below.
*** Key checkpoint at the top level: *** Goal' (EQUAL (HIDE (COMMENT "Failed attempt to call constrained function F" (H 3))) '(3 . 3))
The first argument of
ACL2 !>(trace$ (f :entry (break$))) ((F :ENTRY (BREAK$))) ACL2 !>(thm (equal (h 3) '(3 . 3))) > Break: Break > While executing: BREAK$, in process listener(1). > Type :GO to continue, :POP to abort, :R for a list of available restarts. > If continued: Return from BREAK. > Type :? for other options. 1 > :b ; user input to get backtrace (262932A0) : 0 (BREAK$) 157 (262932F0) : 1 (F 3) 141 (26293338) : 2 (FUNCALL #'#<(:INTERNAL ACL2_*1*_ACL2::G ACL2_*1*_ACL2::G)> 3) 37 (26293350) : 3 (FUNCALL #'#<(:INTERNAL ACL2_*1*_ACL2::H ACL2_*1*_ACL2::H)> 3) 37 (26293368) : 4 (RAW-EV-FNCALL H (3) NIL NIL [[.. output elided ..]]
This output from Lisp is quite low-level, but reading from the bottom up provides the following sequence of events.
An easy way to avoid this proof failure is to avoid execution of calls of
(thm (equal (h 3) '(3 . 3)) :hints (("Goal" :in-theory (disable (:e g) (:e h)))))
(It actually suffices to disable only
Note that if the offending function is non-executable rather than constrained, in particular if that function is defined using defun-nx, then in the first argument of comment you will see ``non-executable'' instead of ``constrained''.
Form:
(HIDE (COMMENT "Failed attempt (when building a term) to call constrained function <fn>" <term>))
Consider how ACL2 approaches the proof of the non-theorem below.
(defstub foo (x) t) (defund bar (x) (foo x)) (thm (implies (equal x 3) (equal (bar x) yyy)))
The prover attacks the thm event by substituting the constant
(EQUAL (HIDE (COMMENT "Failed attempt (when building a term) to call constrained function FOO" (BAR 3))) YYY)
Form:
(HIDE (COMMENT "Unable to expand using the rule <name>" <term>))
Consider how ACL2 approaches the proof for the second event below.
(defthm nth-open (implies (and (consp x) (posp n)) (equal (nth n x) (nth (1- n) (cdr x)))) :rule-classes ((:definition :controller-alist ((nth t t)) :install-body t))) (thm (equal (nth i y) zzz) :hints (("Goal" :expand (nth i y) :do-not-induct t)))
The checkpoint is as follows. What happened is that the rule
(IMPLIES (NOT (CONSP Y)) (EQUAL (HIDE (COMMENT "Unable to expand using the rule NTH-OPEN" (NTH I Y))) ZZZ))
Forms:
(HIDE (COMMENT "Call failed because the rule apply$-<fn> is disabled" <term>)) (HIDE (COMMENT "Call failed because the warrant for <fn> is not known to be true" <term>))
The first of these forms may appear when an attempt to evaluate a call of
apply$ fails because a necessary warrant is disable)d. The
second form may appear when the warrant is not known to be true in the present
context, either because it is known to be false or because it cannot be
assumed true because forcing is disabled. In the following example,
the attempt to simplify the call of
(include-book "projects/apply/top" :dir :system) (defun$ bar (x) x) (thm (implies (warrant bar) (equal (apply$ '(lambda (y) (bar y)) '(3)) 3)) :hints (("Goal" :in-theory (disable apply$-bar ev$))))
The checkpoint in the proof for the
(IMPLIES (APPLY$-WARRANT-BAR) (EQUAL (HIDE (COMMENT "Call failed because the rule APPLY$-BAR is disabled" (EV$ '(BAR Y) '((Y . 3))))) 3))
Similarly, if we instead submit the following event, we see the other such message, in this case about a false warrant.
(thm (implies (not (warrant bar)) (equal (apply$ '(lambda (y) (bar y)) '(3)) 3)) :hints (("Goal" :in-theory (disable ev$))))
Here is the resulting checkpoint.
(IMPLIES (NOT (APPLY$-WARRANT-BAR)) (EQUAL (HIDE (COMMENT "Call failed because the warrant for BAR is not known to be true" (EV$ '(BAR Y) '((Y . 3))))) 3))
Our final example illustrates a failure due to forcing being disabled. The
use of loop$ in the definition of
(defun$ hello (x) (declare (xargs :guard t)) (list 'hi x)) (defun bar (lst) (declare (xargs :guard (true-listp lst))) (loop$ for name in lst collect (hello name)))) (thm (equal (bar '(john)) '((hi john))) :hints (("Goal" :in-theory (disable (:e force)))))
Here is the resulting checkpoint.
(EQUAL (HIDE (COMMENT "Call failed because the warrant for HELLO is not known to be true" (EV$ '(RETURN-LAST 'PROGN '(LAMBDA$ (LOOP$-IVAR) (LET ((NAME LOOP$-IVAR)) (DECLARE (IGNORABLE NAME)) (HELLO NAME))) ((LAMBDA (NAME) (HELLO NAME)) LOOP$-IVAR)) '((LOOP$-IVAR . JOHN))))) '(HI JOHN))