Nonproductive proof steps

Occasionally the ACL2 theorem prover reports that the current goal
simplifies to itself or to a set including itself. Such simplifications are
said to be ``specious'' and are ignored in the sense that the theorem prover
acts as though no simplification were possible and tries the next available
proof technique. Specious simplifications are almost always caused by the use
of `force` or `case-split`.

The simplification of a formula proceeds primarily by the local application
of `rewrite`, `type-prescription`, and other rules to
its various subterms. If no rewrite rules apply, the formula cannot be
simplified and is passed to the next ACL2 proof technique, which is generally
the elimination of destructors. The experienced ACL2 user pays special
attention to such ``maximally simplified'' formulas; the presence of
unexpected terms in them indicates the need for additional rules or the
presence of some conflict that prevents existing rules from working
harmoniously together.

However, consider the following interesting possibility: local rewrite
rules apply but, when applied, reproduce the goal as one of its own subgoals.
How can rewrite rules apply and reproduce the goal? Of course, one way is for
one rule application to undo the effect of another, as when commutativity is
applied twice in succession to the same term. Another kind of example is when
two rules conflict and undermine each other. For example, under suitable
hypotheses, `definition` of `length` and then a `rewrite` rule might be used to ``fold'' that back to `loop-stopper` or to cause a stack
overflow because of indefinite recursion.

A more insidious kind of loop can be imagined: two rewrites in different parts of the formula undo each other's effects ``at a distance,'' that is, without ever being applied to one another's output. For example, perhaps the first hypothesis of the formula is simplified to the second, but then the second is simplified to the first, so that the end result is a formula propositionally equivalent to the original one but with the two hypotheses commuted. This is thought to be impossible unless forcing or case-splitting occurs, but if those features are exploited (see force and see case-split) it can be made to happen relatively easily.

Here is a simple example. Declare

(defstub p1 (x) t)

Prove the following silly rule:

(defthm bad (implies (case-split (p1 x)) (p1 x)))

Now suppose we try the following.

(thm (p1 x))

The rewrite rule *specious* and consider the attempted simplification to
have failed.

In other words, despite the rewriting, no progress was made! In more common cases, the original goal may simplify to a set of subgoals, one of which includes the original goal.

If ACL2 were to adopt the new set of subgoals, it would loop indefinitely. Therefore, it checks whether the input goal is a member of the output subgoals. If so, it announces that the simplification is ``specious'' and pretends that no simplification occurred.

``Maximally simplified'' formulas that produce specious simplifications are maximally simplified in a very technical sense: were ACL2 to apply every applicable rule to them, no progress would be made. Since ACL2 can only apply every applicable rule, it cannot make further progress with the formula. But the informed user can perhaps identify some rule that should not be applied and make it inapplicable by disabling it, allowing the simplifier to apply all the others and thus make progress.

When specious simplifications are a problem it might be helpful to disable rules involved in forcing (including case-splits; see force
and see case-split). For the example above we see the following
output; and in fact, a hint to disable

Splitter note (see :DOC splitter) for Goal (0 subgoals). case-split: ((:REWRITE BAD))A more drastic possibility is to disable all forcing (including case-splits) and resubmit the formula to observe whether forcing is involved in the loop or not. The commands

ACL2 !>:disable-forcing and ACL2 !>:enable-forcing

disable and enable the pragmatic effects of both `force`d hypothesis. By disabling that rule, at least for the subgoal in
question, you may allow the simplifier to make progress on the subgoal.