NOTE-2-7-PROOFS

Major Section:  NOTE-2-7

An improvement in the linear arithmetic heuristics has been provided by Robert Krug. For information about this change, search for the comment in add-linear-lemma (file rewrite.lisp) that begins as follows.

; Previous to Version_2.7, we just went ahead and used the result of

The non-linear-arithmetic addition (see non-linear-arithmetic) led to several small changes in the linear-arithmetic decision procedure (see linear-arithmetic). Two of these changes could affect existing proofs.

First, when we are setting up the initial arithmetic data-base (which we call the ``pot-lst''), we have always scanned it to see if there were any pairs of inequalities from which we could derive a previously unknown equality. In some cases we added this equality to the clause and in others we used it to rewrite the clause, substituting one side of the equality for the other throughout the clause. Previously, the heuristics that we used to determine whether we performed the substitution differed from those used in several other places in the code. This has now been regularized, and similar heuristics are now used throughout the code.

The second change to the linear-arithmetic decision procedure is that we now explicitly add inequalities derived from type reasoning to the pot-lst. Previously, we performed cancellations against these inequalities without adding them to the pot-lst. This change results in there being more inequalities in the pot-lst than before, and so more chances for there to be a pair of inequalities from which an equality can be derived. In effect, certain simple consequences of the current goal (see type-set) may now be added as hypotheses of the goal or used to peform equality substitutions.

A slight improvement has been made to the way certain rewrite rules are stored. It was already the case that a rewrite rule rule whose conclusion C is not a call of a known equivalence relation (or eq, eql, or =) is stored as (iff C t), except that if ACL2 can determine (using its type-set mechanism) that C is Boolean, then the rule is stored as (equal C t). The iprovement is that if C and C' are Boolean, then a rule stated as (iff C C') is stored as (equal C C'). Thanks to Pete Manolios for providing an example that led us to consider this improvement.

The heuristic use of equalities (fertilization) has been modified. Previously, ACL2 would sometimes substitute using an equality but keep the equality, and then undo the substitution by using the equality again. Now, when ACL2 keeps an equality after using it, it puts the equality inside a call of hide. Descendents of that goal that are unchanged by simplification will have this call of hide removed so that the equality can once again contribute to the proof. This change can cause some proofs to succeed that otherwise would fail. In the unlikely event that a proof fails that formerly succeeded, the following hint on "Goal" may fix the problem (see hints):

:expand ((:free (x) (hide x)))

We have refined the heuristics employed when an IF form is assumed true or false. Our previous attempt (see note-2-6-proofs for the original announcement) was not as general as we had believed. We have also improved some low-level code responsible for rewriting IF expressions. In earlier versions of ACL2, it was possible to have the truth or falsity of an IF expression explicitly recorded in the type-alist, and yet not use this information during rewriting. This problem has been corrected. Thanks to Robert Krug for noticing this problem and implementing the fix.

We have sped up the rewriter in some cases where there are large collections of mutually-recursive functions (see mutual-recursion). (Implementation notes: technically, we have modified the way function being-openedp operates on the fnstack, and we have modified *current-acl2-world-key-ordering* as described in the essay above its definition.)

Forward-chaining is now done in the preprocessing phase of proof attempts (see the discussion of :DO-NOT -- see hints). This is part of a technical change, made in support of translation of type declarations to guards (see note-2-7-guards). Previously, whenever ACL2 checked for built-in-clauses, it then looked for a contradiction using type-set reasoning if it did not find a suitable built-in clause. The change is to perform forward-chaining in such cases (i.e., when a built-in clause is not found).

A couple of changes have been made in the generation of goals for forcing-rounds. Thanks to Eric Smith for bringing issues to our attention that led to these changes. For one, guards are no longer relevant in such goal generation. Formerly, the addition of a guard could make a proof fail that otherwise succeeded. Secondly, contextual information is now always kept when it involves a constrained constant, i.e., a zero-ary function introduced in the signature of an encapsulate.