		Search-engine friendly clone of the ACL2 documentation.

Note-2-8

Note-2-8-proofs

ACL2 Version 2.8 Notes on Changes in Proof Engine

ACL2 now prevents certain rewriting loops; see rewrite-stack-limit.

During the computation of constraints for functional instantiation, (prog2$ term1 term2) and (the type term2) are now treated as term2.

A change has been made in heuristics for controlling rewriting during proofs by induction. Formerly, during induction proofs, ACL2 suppressed rewriting of certain ``induction hypothesis'' terms, and forced expansion of certain ``induction conclusion'' terms, until rewriting had stabilized. This meddling with the rewriter is still turned off when rewriting has stabilized, but it is now turned off earlier once an ancestor has been through the rewriter and the current goal is free of ``induction conclusion'' terms. Thanks to Dave Greve and Matt Wilding for providing an example and associated analysis that led us to look for a heuristic modification.

A change has been made in the heuristics for handling certain ``weak'' compound-recognizer rules when building contexts. Those who want to dig deeply into this change are welcome to look at the code following the call of most-recent-enabled-recog-tuple in the code for function assume-true-false in the ACL2 sources.

The handling of free variables in a hypothesis of a rewrite rule (see free-variables) has been improved in the case that the hypothesis is of the form (equiv x y), where equiv is a known equivalence relation (see equivalence). Previously, if the rewriter was attempting to rewrite the hypothesis (equiv x y) of a rewrite rule, in a context where x' is an instance of x, then the rewriter could fail to notice a term (equiv x' y') true in the current context where y' is an instance of y, in the case that x' precedes y' in the term-order. This has been remedied. This improvement applies regardless of whether x, y, or (we believe) both are already fully instantiated in the present context. Thanks to Joe Hendrix for bringing up an example and to Vernon Austel for providing another, simple example.

A very minor change has been made to the rewriter in the case that an equality appears on the left-hand side of a :rewrite rule. Formerly, when such an equality (equal x y) was commuted to (equal y x) in order for the rule to match the current term, then all equalities on the instantiated right-hand side of the rule were commuted, except for those occurring inside another equality. The instantiated right-hand side is no longer modified. It seems very unlikely that this change will cause proofs to fail, though we cannot completely rule out that possibility.

We have modified how the ACL2 simplifier handles the application of a defined function symbol to constant arguments in certain cases, which we now describe. As before, ACL2 attempts to simplify such a function application by evaluation, provided the :executable-counterpart of the function is enabled. And as before, if that evaluation fails due to a subroutine call of a constrained function (introduced by encapsulate), ACL2 may wrap a call of hide around this function application. (See hide.) But now, ACL2 attempts to apply definitions and rewrite rules in the case that this evaluation fails, and only if the resulting term is unchanged does ACL2 wrap hide around this function application. Thanks to Matt Wilding for bringing up the idea of this modification.

The generation of "Goal" for recursive (and mutually-recursive) definitions now uses the subsumption/replacement limitation (default 500). See case-split-limitations.

Default hints now apply to hints given in definitions, not just theorems. See default-hints.

Thanks to Robert Krug for implementing the following two improvements involving linear arithmetic reasoning: linear arithmetic now uses the conclusions of forward-chaining rules, and type-set now uses a small amount of linear reasoning when deciding inequalities.