		Search-engine friendly clone of the ACL2 documentation.

Simplify

Simplify-failure

Ways to address failed invocations of the simplify transformation.

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

Dealing with a guard verification failure

When (simplify FN ...) fails to prove the measure theorem or verify guards, then unless option :print nil is supplied, an attempt to run defun or verify-guards (respectively) will be made automatically, without hints, and with prover output shown as though :print :all had been supplied. That way, you can look at checkpoints to come up with helpful rules, without having to run simplify again (see ACL2::the-method).

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 simplify command. It might be helpful to try one or more of the following approaches.

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 of simplify, to match the call or defun or verify-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 this simplify call completes successfully, call verify-guards on FN, 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 the prove 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 submit PROVE, you'll see the following checkpoint.
```
Goal'
(IMPLIES (AND (CONSP X) (MY-CONSP (CDR X)))
         (MY-CONSP X))
```
This checkpoint rather clearly suggests enabling my-consp. Indeed, you can do that in the proof-builder: the command (IN-THEORY (ENABLE MY-CONSP)) followed by PROVE 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))))
```

Applicability condition failure

If the failure is in the :assumptions-preserved applicability condition, consider supplying :hints, first proving useful rules, or both.

Preserving special behavior such as side-effects

Maybe your call of simplify succeeded, but the result failed to preserve a desired call of prog2$, ec-call, time$, or another such operator that provides special behavior. See ACL2::return-last-blockers.

Recursion and equivalence relations

As of this writing, the simplify transformation does not fully support the use of the :equiv option for recursive definitions, though it might succeed on occasion. Consider the following example.

(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 :show-only t, we can see the generated definition:

(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.)

General approaches to unsuccessful invocations of simplify

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 for simplify, to get the event form that is actually submitted by your call of simplify. Then use :redo-flat to get to the failed event, perhaps using :pbt to see which event failed by seeing which events from show-simplify are now in the world. Then p submit that failed event and see if the output helps you to fix your simplify 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!)