how to deal with a proof failure

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. Books could be written about this, but they haven't been yet. However, see proof-tree for a utility that may be very helpful in locating parts of the failed proof that are of particular interest. See also 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.