Ways to address failed invocations of the

This topic suggests steps you may take to address failed
invocations of the

When

Note that in some cases, there may be initial attempts at proving the
measure theorem or guard obligation that use a somewhat sophisticated ACL2::proof-builder macro, one that users are not expected to understand.
This explains why the retry mentioned above does not use any hints: this
supports your attempt to make adjustments so that guard verification will
succed for your

- Prove suitable rules, as noted above, towards removing the checkpoints.
You may wish to specify explicitly
:hints nil or:guard-hints nil in your new call ofsimplify , to match the call ordefun orverify-guards that generated the checkpoints that you considered. - Provide a
:hints option (for the measure theorem) or:guard-hints option (for guard verification),(simplify FN :hitns ... :guard-hints ...) , that specifies a suitable theory and, perhaps, include:use (:termination-theorem FN) (for the measure theorem) or:use (:guard-theorem FN) (for guard verification). - If the failure is in guard verification, then you can delay guard
verification with
(simplify FN :verify-guards nil ...) . Then, after thissimplify call completes successfully, call`verify-guards`onFN , perhaps with suitable hints as suggested above. - If you use
:print info or:print :all , you may see a message like the following.Saving proof-builder error state; see :DOC instructions. To retrieve: (RETRIEVE :ERROR1)

If you invoke that command in the ACL2 loop, e.g.,(RETRIEVE :ERROR1) , then you will be in the ACL2::proof-builder. You can run theprove command there and look at the checkpoints. Consider the following (admittedly artificial) example.(defun my-consp (x) (declare (xargs :guard t)) (consp x)) (defun my-cdr (x) (declare (xargs :guard (my-consp x))) (cdr x)) (defun f1 (x) (if (consp x) (if (my-consp (f1 (cdr x))) (cons (car x) (f1 (my-cdr x))) x) x)) (defthm f1-id (equal (f1 x) x)) (verify-guards f1) (in-theory (disable my-consp my-cdr (tau-system))) (simplify f1 :print :info)

If you run(RETRIEVE :ERROR1) and then submitPROVE , you'll see the following checkpoint.Goal' (IMPLIES (AND (CONSP X) (MY-CONSP (CDR X))) (MY-CONSP X))

This checkpoint rather clearly suggests enablingmy-consp . Indeed, you can do that in the proof-builder: the command(IN-THEORY (ENABLE MY-CONSP)) followed byPROVE completes the proof in the proof-builder. With that information you can exit the proof-builder and successfully run the following command in the ACL2 loop.(simplify f1 :guard-hints (("Goal" :in-theory (enable my-consp))))

If the failure is in the

Maybe your call of `prog2$`, `ec-call`, `time$`, or
another such operator that provides special behavior. See ACL2::return-last-blockers.

As of this writing, the

(defun f (x) (and x 3)) (defun g (x) (if (consp x) (equal (g (cdr x)) (car (cons 3 x))) (f x))) (simplify g :equiv iff)

The result is an error with the following message.

ACL2 Error in (APT::SIMPLIFY G ...): An attempt to simplify the definition of G has failed, probably because the definition of the new function, G$1, is recursive and the equivalence relation specified by :EQUIV is IFF, not EQUAL. See :DOC apt::simplify-failure.

By adding the option

(DEFUN G$1 (X) (DECLARE (XARGS :GUARD T :MEASURE (ACL2-COUNT X) :VERIFY-GUARDS NIL)) (IF (CONSP X) (EQUAL (G$1 (CDR X)) 3) (AND X 3)))

In this example, the original and proposed simplified definitions are
actually *not* Boolean equivalent. But in some cases, they might be
equivalent but ACL2 fails to prove this.

A solution for these other cases, where equivalence holds but was not successfully proved, might be first to prove suitable congruence rules, so that at each recursive call in the simplified definition (usually the new definition, as in the error above), it suffices to preserve the specified congruence relation. This may eventually be worked into a new applicability condition. (A comment about this may be found in the source code for this :doc topic.)

Here are several ways to get more information about what is happening.

- Use
:print :info to get a running commentary and perhaps a more detailed error. - Use
:print :all to get even more output. This maximal level of output may be distracting, but near the end of it you might find useful simplification checkpoints, for example from a failed attempt to prove the measure conjecture. Those checkpoints may serve, as is common when using ACL2, to help you to discover additional theorems to prove first, in particular, to be stored as rewrite rules. - Use
show-simplify with the same arguments as you used forsimplify , to get the event form that is actually submitted by your call ofsimplify . Then use: `redo-flat`to get to the failed event, perhaps using: `pbt`to see which event failed by seeing which events fromshow-simplify are now in the world. Then p submit that failed event and see if the output helps you to fix yoursimplify call.

(If you have any suggestions for other steps to take upon failure, by all means add them here or ask someone to do so!)