Major Section: MISCELLANEOUS

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 forcing.

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 rules
conflict and undermine each other. For example, under suitable
hypotheses, `(length x)`

might be rewritten to `(+ 1 (length (cdr x)))`

by the `:`

`definition`

of `length`

and then a `:`

`rewrite`

rule might be used
to ``fold'' that back to `(length x)`

. Generally speaking the
presence of such ``looping'' rewrite rules causes ACL2's simplifier
either to stop gracefully because of heuristics such as that
described in the documentation for `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 `foo`

to be a function of one
argument returning one result:

(defstub foo (x) t)Add the following

`:`

`type-prescription`

rule about `foo`

:
(defaxiom forcer (implies (force (not (true-listp x))) (equal (foo x) t)) :rule-classes :type-prescription)Note that we could define a

`foo`

with this property; `defstub`

and
`defaxiom`

are only used here to get to the gist of the problem
immediately. Consider the proof attempt for the following formula.
(thm (implies (and (consp x) ; hyp 1 (true-listp (cdr x)) ; hyp 2 (true-listp x)) ; hyp 3 (foo x))) ; conclWhen we simplify this goal,

`hyp 1`

cannot be simplified. `Hyp 2`

simplifies to `t`

, because `x`

is known to be a non-`nil`

true list so its
`cdr`

is a true list by type reasoning; because true hypotheses are
dropped, `hyp 2`

simply disappears. `Hyp 3`

simplifies to
`(true-listp (cdr x))`

by opening up the `:`

`definition`

of
`true-listp`

. Note that `hyp 3`

has simplified to the old `hyp 2`

.
So at this point, the ``current (intermediate) goal'' is
(implies (and (consp x) ; rewritten hyp 1 (true-listp (cdr x))) ; rewritten hyp 3 (foo x)) ; unrewritten concland we are working on

`(foo x)`

. But the `:`

`type-prescription`

rule
above tells us that `(foo x)`

is `t`

if the hypothesis of the rule is
true. Thus, in the case that the hypothesis of the rule is true, we
are done. It remains to prove the current intermediate goal under
the assumption that the hypothesis of the rule is false. This is
done by adding the negation of the `:`

`type-prescription`

rule's
hypothesis to the current intermediate goal. This is what `force`

does in this situation. The negation of the hypothesis is
`(true-listp x)`

. Adding it to the current goal produces the subgoal
(implies (and (consp x) ; rewritten hyp 1 (true-listp (cdr x)) ; rewritten hyp 3 (true-listp x)) ; FORCEd hyp (foo x)). ; unrewritten conclObserve that this is just our original goal. Despite all 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 all forcing (including case-splits) and resubmit the formula to observe whether forcing is involved in the loop or not. See force. The commands

ACL2 !>:disable-forcing and ACL2 !>:enable-forcingdisable and enable the pragmatic effects of both

`force`

and `case-split`

. If the loop is broken when forcing is
disabled, then it is very likely some forced hypothesis of
some rule is ``undoing'' a prior simplification. The most common
cause of this is when we force a hypothesis that is actually
false but whose falsity is somehow temporarily hidden (more below).
To find the offending rule, compare the specious simplification with
its non-specious counterpart and look for rules that were speciously
applied that are not applied in the non-specious case. Most likely
you will find at least one such rule and it will have a `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.
To illustrate what we mean by the claim that specious
simplifications often arise because the system forces a false
hypothesis, reconsider the example above. At the time we used the
`:`

`type-prescription`

rule, the known assumptions were `(consp x)`

and
`(true-listp (cdr x))`

. Observe that this tells us that `x`

is a true
list. But the hypothesis forced to be true was
`(not (true-listp x))`

. Why was the falsity of this hypothesis
missed? The most immediate reason is that the encoding of the two
assumptions above does not produce a context (``type-alist'') in
which `x`

is recorded to be a true-list. When we look up
`(not (true-listp x))`

in that context, we are not told that it is
false. More broadly, the problem stems from the fact that when we
force a hypothesis we do not bring to bear on it all of the
resources of the theorem prover. Thus it could be -- as here --
that the hypothesis could be proved false in the current context but
is not obviously so. No matter how sophisticated we made the
forcing mechanism, the unavoidable incompleteness of the theorem
prover would still permit the occasional specious simplification.
While that does not excuse us from trying to avoid specious
simplifications when we can -- and we may well strengthen the type
mechanism to deal with the problem illustrated here -- specious
simplifications will probably remain a problem deserving of the
user's attention.