		Search-engine friendly clone of the ACL2 documentation.

Comment

Variant of prog2$ to help debug evaluation failures during proofs

Semantically, (comment x y) equals y; the value of x is ignored. Thus comment is much like prog2$. However, when you see a call of comment in ACL2 proof output, it will likely be under a call of hide, with information that may be helpful in understanding why the call of hide was inserted. Below we illustrate the various ways in which ACL2 may replace a term tm by (hide (comment "..." tm)). (On occasion you will simply see (hide tm); such cases are not discussed here.)

Also see hide for further discussion of how to avoid such proof failures, and for how to keep the prover from inserting a comment call under a call of hide.

Evaluation during rewriting

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))
(defund h (x) (cons x (cdr (g x))))
(thm (equal (h 3) '(3 . 3)))

Note that the definition of h is disabled, but its executable-counterpart is not. 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;
see :DOC comment"
            (H 3)))
 '(3 . 3))

The first argument of equal is logically just (h 3). But the comment and hide wrappers are telling us that evaluation of (h 3) failed because it led to a call of the constrained function f. It is easy to see why in this case, by looking at the definitions, where h calls g, which calls f. But more complicated such failures may be difficult to understand without such information. In very complicated cases, one might even want to use the Lisp debugger after designating a break$ call using trace$, like this (here, shown using host Lisp CCL).

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.

4. Call h with argument list (3).
3. Call the executable-counterpart of h.
2. Call the executable-counterpart of g.
1. Attempt to call the constrained function, f.

An easy way to avoid this proof failure is to avoid execution of calls of h and g, as follows.

(thm (equal (h 3) '(3 . 3))
     :hints (("Goal" :in-theory (disable (:e g) (:e h)))))

(It actually suffices to disable only (:e h), but the workings of the ACL2 rewriter are out of scope here.)

If the offending function (here, f) is introduced as non-executable rather than constrained, in particular if that function is defined using defun-nx or defund-nx, then in the first argument of comment you will see ``non-executable'' instead of ``constrained''.

Evaluation during substitution

Form:

(HIDE
 (COMMENT
  "Failed attempt (during substitution) to call constrained function <fn>;
see :DOC comment"
  <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 '3 for x, which results in an attempt to evaluate (bar 3). This evaluation fails because bar calls the undefined function foo. The checkpoint is as follows.

(EQUAL
 (HIDE
  (COMMENT
     "Failed attempt (during substitution) to call constrained function FOO;
see :DOC comment"
     (BAR 3)))
 YYY)

Failure to expand using a rule

Form:

(HIDE (COMMENT "Unable to expand using the rule <name>;
see :DOC comment"
               <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 nth-open had a hypothesis that was false when an attempt was made to apply it to the term (nth i y).

(IMPLIES
 (NOT (CONSP Y))
 (EQUAL
  (HIDE (COMMENT "Unable to expand using the rule NTH-OPEN;
see :DOC comment"
                 (NTH I Y)))
  ZZZ))

Failure due to disabled or missing warrants

Forms:

(HIDE (COMMENT "Call failed because the rule apply$-<fn> is disabled;
see :DOC comment"
      <term>))
(HIDE (COMMENT "Call failed because the warrant for <fn> is not known to be true;
see :DOC comment"
      <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 apply$ in the theorem ultimately leads to an attempt to evaluate a call of ev$, which ultimately fails because it leads to a call to evaluate (apply$ 'bar '(3)) bar. That call causes an error because the warrant is unavailable since the rule apply$-bar is disabled, hence cannot rewrite a term (apply$ 'bar args) to (bar (car args)).

(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 thm just above is as follows.

(IMPLIES
 (APPLY$-WARRANT-BAR)
 (EQUAL
  (HIDE
   (COMMENT
      "Call failed because the rule APPLY$-BAR is disabled;
see :DOC comment"
      (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;
see :DOC comment"
    (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 bar expands to create a call of ev$, which cannot be simplified during the proof of the thm below because the necessary warrant hypothesis is missing and cannot be forced, since forcing is disabled (see also disable-forcing).

(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;
see :DOC comment"
   (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))