How to deal with a failure to admit an event

There are many reasons why an event can fail to be admitted.
Generally, an error message will explain the failure, sometimes pointing to
documentation that is specific to the relevant issue. There are tools that
can sometimes help: for example, to debug failures of `encapsulate` or
`progn` events, as well as `certify-book` failures, see redo-flat.

However, proof failures are typically not as trivial to debug as, for
example, syntactic errors (such as spelling errors in the name of a function).
Fortunately, ACL2 offers a variety of techniques for dealing with proof
failures, and some are discussed below. Also see relevant subtopics of the
topic, debugging. Some frequently-used tools for proof debugging that
are discussed in those subtopics include accumulated-persistence, break-rewrite, with-brr-data, cgen, and proof-builder.
Also see nil-goal for ideas about how to proceed when the prover
generates a goal of

We turn now to the problem of dealing with proof failures.

When ACL2 gives up it does not mean that the submitted conjecture is invalid, even if the last formula ACL2 printed in its proof attempt is manifestly false. Since ACL2 sometimes generalizes the goal being proved, it is possible it adopted an invalid subgoal as a legitimate (but doomed) strategy for proving a valid goal. Nevertheless, conjectures submitted to ACL2 are often invalid and the proof attempt often leads the careful reader to the realization that a hypothesis has been omitted or that some special case has been forgotten. It is good practice to ask yourself, when you see a proof attempt fail, whether the conjecture submitted is actually a theorem.

If you think the conjecture is a theorem, then you must figure out from
ACL2's output what you know that ACL2 doesn't about the functions in the
conjecture and how to impart that knowledge to ACL2 in the form of rules. The
``key checkpoint'' information printed at the end of the summary
provides a fine place to start. See the-method for a general
discussion of how to prove theorems with ACL2, and see introduction-to-the-theorem-prover for a more detailed tutorial. Also see
set-gag-mode for discussion of key checkpoints and an abbreviated
output mode that focuses attention on them. You may find it most useful to
start by focusing on key checkpoints that are not under a proof by induction,
if any, both because these are more likely to suggest useful lemmas and
because they are more likely to be theorems; for example, generalization may
have occurred before a proof by induction has begun. If you need more
information than is provided by the key checkpoints — although this
should rarely be necessary — then you can look at the full proof,
perhaps with the aid of certain utilities: see pso, set-gag-mode, and proof-tree. System hackers may want to consider
using the utility, `checkpoint-list`.

Again, see the-method for a general discussion of how to prove theorems with ACL2, and see introduction-to-the-theorem-prover for a more detailed tutorial. See also the book ``Computer-Aided Reasoning: An Approach'' (Kaufmann, Manolios, Moore), as well as the discussion of how to read Nqthm proofs and how to use Nqthm rules in ``A Computational Logic Handbook'' by Boyer and Moore (Academic Press, 1988).

If the failure occurred during a forcing round, see failed-forcing.

- Useless-runes-failures
- Failures caused by useless-runes