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:
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)))
(defthm f1-id (equal (f1 x) x))
(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
(IMPLIES (AND (CONSP X) (MY-CONSP (CDR 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
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)))
(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
(DEFUN G$1 (X)
(DECLARE (XARGS :GUARD T
:MEASURE (ACL2-COUNT X)
(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
- 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
(If you have any suggestions for other steps to take upon failure, by all
means add them here or ask someone to do so!)