Major Section: NOTE-2-6
Certain optimizations are performed when converting terms to clausal
form. For example, (< 0 1) is known to be t,
(HARD-ERROR ctx str alist) is known to be nil, and
(INTEGERP n) is known to imply (RATIONALP n).
In earlier versions of ACL2, the conversion of a term to clausal
form expanded LAMBDA applications. That may no longer occur.
Some proofs may slow down (or fail) because your
LAMBDA-expressions are not expanded away when you ``expected''
them to be.
Robert Krug found a soundness bug in our linear arithmetic package. The bug was caused by the derivation of an equation from two inequalities without taking adequate precautions to ensure that both sides of the inequalities were numeric. Robert also kindly provided a fix which we adopted. Thanks Robert!
We fixed a bug that could prevent the application of a metatheorem.
A bug has been fixed that had caused bogus forcing rounds (see forcing-round). The bug could occur when the hypothesis of a rule was forced (see force) before the prover decided to start over and prove the original goal by induction. Thanks to Rob Sumners for drawing our attention to this problem.
Some low-level fixes have been made that prevent certain infinite loops, based on reports by users. We thank Yunja Choi, Matt Wilding, and Pete Manolios for reporting such problems.
An obscure potential soundness hole has been fixed by redoing the way evaluation takes place in the ACL2 loop and during theorem proving. We expect that users will see no difference based on this change. (Those interested in the details can see the long comment ``Essay on Evaluation in ACL2'' in source file interface-raw.lisp.)
A small change was made in computation for a heuristic that controls backchaining. This will speed up proofs dramatically in a very few cases but should have a very small impact in general.
The simplifier has been modified to avoid eliminating hypotheses of goals that can be established by contextual (specifically, type-set) reasoning alone. We believe that this change will generally strengthen ACL2's reasoning engine, although on rare occasions a lemma that formerly was provable may require user assistance. Thanks to Robert Krug for suggesting this change and providing its implementation.
Case splits are now limited, by default. This may allow some proof attempts to provide output where previously the prover would appear to ``go out to lunch.'' For a more complete discussion, including instructions for how users can control case splitting, see set-case-split-limitations.
A bug has been fixed in the handling of :type-prescription rules by
the bdd package. Thanks to Rob Sumners for discovering this bug
and supplying a helpful example.
ACL2 may now use the built-in induction scheme for a function symbol
even if that function symbol is disabled. Formerly, if a function
symbol was disabled then its induction scheme was only considered if
an explicit induction hint was supplied, other than :induct t.
We eliminated the rule-class linear-alias. This rule class was seldom
used and complicated the linear arithmetic decision procedure in ways that
made it difficult to extend to handle some non-linear special cases.
The only use of the rule-class that we know of was in our own nqthm
books, which were an attempt to provide an embedding of the Nqthm logic
and theorem prover into ACL2. But that facility was also practically
never used, as far as we know. So both linear-alias rules and the
nqthm books have been eliminated.
In earlier versions of ACL2, when the IF-form of (AND p q) was
assumed true -- as when rewriting the alpha expression in
(IF (AND p q) alpha beta) -- the assumption mechanism did not deduce
that p and q are true, only that their conjunction, in its
IF-form, is true. This has long been known as a deficiency in
both ACL2 and the earlier Nqthm but it was tedious to do better when
one considered the full range of IF-forms one might encounter in the
test of another IF. Rather than code all the cases, we just waited
until clausification got rid of them. Robert Krug developed a pretty
nice treatment of the general case and we added it in this version.
This also involved a surprising number of changes elsewhere in the system
because the improved handling of assumptions caused the theorem prover
often to ``erase'' hypotheses provided by :use hints because it could
simplify them to t. Thank you Robert!
In response to a suggestion from Robert Krug, we added mfc-ap so
that extended metafunctions can take advantage of linear arithmetic.
See extended-metafunctions.
There is less delay in printing goals. In previous versions, a goal was not printed until its subgoals were created (or the goal was proved). Now, the goal is printed essentially as soon as it is created.
A small technical change has been made in the function term-order,
to give priority on the function symbol count over the weighting of
constants. So for example, while previously the term (f) preceded
the constant 2, that is no longer the case. If this change is noticed
at all, it will probably be noticed in how so-called permutative
rewrite rules are applied; see loop-stopper. Thanks to Robert Krug
for suggesting this improvement and providing part of the
implemtation.
