Acl2 Version 1.5 Notes
Acl2 now allows ``complex rationals,'' which are complex numbers
whose real parts are rationals and whose imaginary parts are non-zero
rationals. See complex.
A new way of handling forced hypotheses has been implemented.
Rather than cause a case split at the time the force occurs, we
complete the main proof and then embark on one or more ``forcing rounds'' in
which we try to prove the forced hypotheses. See forcing-round.
To allow us to compare the new handling of force with the old, Version
1.5 implements both and uses a flag in state to determine which method
should be used. Do (assign old-style-forcing t) if you want force to be handled as it was in Version 1.4. However, we expect to
eliminate the old-style forcing eventually because we think the new style is
more effective. To see the difference between the two approaches to forcing,
try proving the associativity of append under both settings of
old-style-forcing. To get the new behavior invoke:
(thm (implies (and (true-listp a) (true-listp b))
(equal (append (append a b) c)
(append a (append b c)))))
Then (assign old-style-forcing t) and invoke the thm command above again.
A new :cases hints allows proof by cases. See hints.
Include-book and encapsulate now restore the ACL2-defaults-table when they complete. See include-book and see
The guards on many Acl2 primitives defined in axioms.lisp have
been weakened to permit them to be used in accordance with lisp custom and
It is possible to attach heuristic filters to :rewrite rules
to limit their applicability. See syntaxp.
A tutorial has been added (but as of Version_3.6.1 it has become
Events now print the Summary paragraph listing runes used,
time, etc., whether they succeed or fail. The format of the ``failure
banner'' has been changed but still has multiple asterisks in it. Thm
also prints a Summary, whether it succeeds or fails; but thm is not an
A new event form skip-proofs has been added; see skip-proofs.
A user-specific customization facility has been added in the form of a book
that is automatically included, if it exists on the current directory. See
A facility for conditional metalemmas has been implemented; see meta.
The acceptable values for ld-skip-proofsp have changed. In the old
version (Version 1.4), a value of t meant that proofs and local
events are to be skipped. In Version 1.5, a value of t means
proofs (but not local events) are to be skipped. A value of
'include-book means proofs and local events are to
be skipped. There are two other, more obscure, acceptable values. See ld-skip-proofsp.
In order to turn off the forcing of assumptions, one should now disable the :executable-counterpart of force (rather
than the :definition of force, as in the previous
release); see force.
The macros enable-forcing and disable-forcing make it
convenient to enable or disable forcing. See enable-forcing and see disable-forcing.
The new commands :pr and :pr! print the rules
created by an event or command. See pr and see pr!.
The new history commands :puff and :puff* will replace a compound command such as an encapsulate
or include-book by the sequence of events in it. That is, they
``puff up'' or ``lift'' the subevents of a command to the command level, eliminating the formerly superior command and
lengthening the history. This is useful if you want to ``partially
undo'' an encapsulate or book or other compound command so you
can experiment. See puff and see puff*.
Theory expressions now are allowed to use the free variable world
and prohibited from using the free variable state. See theories, although it is essentially the same as before except it mentions
world instead of state. See world for a discussion of
the Acl2 logical world. Allowing in-theory events to be
state-sensitive violated an important invariant about how books
Table keys and values now are allowed to use the free variable
world and prohibited from using the free variable state. See
the note above about theory expressions for some explanation.
The macro for minus, -, used to expand (- x 3) to (+ x
-3) and now expands it to (+ -3 x) instead. The old macro, if used in
the left-hand sides of rewrite rules, produced inapplicable rules because the
constant occurs in the second argument of the +, but potential target
terms generally had the constant in the first argument position because of the
effect of commutativity-of-+.
A new class of rule, :linear-alias rules, allows one to implement the
nqthm package and similar hacks in which a disabled function is to be
known equivalent to an arithmetic function.
A new class of rule, :built-in-clause rules, allows one to extend the
set of clauses proved silently by defun during measure and guard processing. See built-in-clause.
The new command pcb! is like pcb but sketches the command and then prints its subsidiary events in full. See pcb!.
:Rewrite class rules may now specify the :loop-stopper field. See rule-classes and see loop-stopper.
The rules for how loop-stoppers control permutative rewrite rules
have been changed. One effect of this change is that now when the built-in
commutativity rules for + are used, the terms a and (- a)
are permuted into adjacency. For example, (+ a b (- a)) is now
normalized by the commutativity rules to (+ a (- a) b); in Version 1.4,
b was considered syntactically smaller than (- a) and so (+ a b
(- a)) is considered to be in normal form. Now it is possible to arrange
for unary functions be be considered ``invisible'' when they are used in
certain contexts. By default, unary-- is considered invisible when
its application appears in the argument list of binary-+. See loop-stopper and see :DOC set-invisible-fns-table.
Extensive documentation has been provided on the topic of Acl2's ``term
ordering.'' See term-order.
Calls of ld now default ld-error-action to :return
rather than to the current setting.
The command descriptor :x has been introduced and is synonymous
with :max, the most recently executed command. History commands such as :pbt print a :x beside the
most recent command, simply to indicate that it is the most
The command descriptor :x-23 is synonymous with (:x -23).
More generally, every symbol in the keyword package whose first character is
#\x and whose remaining characters parse as a negative integer is
appropriately understood. This allows :pbt :x-10 where
:pbt (:max -10) or :pbt (:here -10) were
previously used. The old forms are still legal.
The order of the arguments to defcong has been changed.
The simplifier now reports the use of unspecified built-in type information
about the primitives with the phrase ``primitive type reasoning.'' This
phrase may sometimes occur in situations where ``propositional calculus'' was
formerly credited with the proof.
The function pairlis has been replaced in the code by a new
function pairlis$, because Common Lisp does not adequately specify its
Some new Common Lisp functions have been added, including logtest,
logcount, integer-length, make-list, remove-duplicates, string, and concatenate. The source file
/slocal/src/acl2/axioms.lisp is the ultimate reference regarding Common
Lisp functions in Acl2.
The functions defuns and theory-invariant have been
documented. See defuns and see theory-invariant.
A few symbols have been added to the list *acl2-exports*.
A new key has been implemented for the ACL2-defaults-table,
:irrelevant-formals-ok. See set-irrelevant-formals-ok.
The connected book directory, cbd, must be nonempty and begin and
end with a slash. It is set (and displayed) automatically upon your first
entry to lp. You may change the setting with set-cbd. See
:oops will undo the last :ubt. See oops.
Documentation has been written about the ordinals. See :DOC
e0-ordinalp and see :DOC e0-ord-<. [Note added later: Starting with
Version_2.8, instead see o-p and see o<.
The color events — (red), (pink), (blue), and (gold) —
may no longer be enclosed inside calls of local, for soundness
reasons. In fact, neither may any event that sets the ACL2-defaults-table. See embedded-event-form.
See ld-keyword-aliases for an example of how to change the exit
keyword from :q to something else.
The attempt to install a monitor on :rewrite rules
stored as simple abbreviations now causes an error because the application of
abbreviations is not tracked.
A new message is sometimes printed by the theorem prover, indicating that a
given simplification is ``specious'' because the subgoals it produces include
the input goal. In Version 1.4 this was detected but not reported, causing
behavior some users found bizarre. See specious-simplification.
:Definition rules are no longer always required to specify the
:clique and :controller-alist fields; those fields can be defaulted
to system-determined values in many common instances. See definition.
A warning is printed if a macro form with keyword arguments is given
duplicate keyword values. Execute (thm t :doc nil :doc "ignored") and
read the warning printed.
A new restriction has been placed on encapsulate. Non-local recursive definitions inside the encapsulate may not use, in
their tests and recursive calls, the constrained functions introduced by the
encapsulate. See subversive-recursions. (Note added in
Version 2.3: Subversive recursions were first recognized by us here in Version
1.5, but our code for recognizing them was faulty and the bug was not fixed
until Version 2.3.)
The events defequiv, defcong, defrefinement,
and defevaluator have been reimplemented so that they are just macros
that expand into appropriate defthm or encapsulate events; they are no longer primitive events. See the documentation of each affected event.
The defcor event, which was a shorthand for a defthm that
established a corollary of a named, previously proved event, has been
eliminated because its implementation relied on a technique we have decided to
ban from our code. If you want the effect of a defcor in Version 1.5 you
must submit the corresponding defthm with a :by hint naming the
previously proved event.
Error reporting has been improved for inappropriate in-theory hints and events, and for syntax errors in rule classes, and for
non-existent filename arguments to ld.
Technical Note: We now maintain the Third Invariant on type-alists, as
described in the Essay on the Invariants on Type-alists, and Canonicality.
This change will affect some proofs, for example, by causing a to rewrite more
quickly to c when (equiv a b) and (equiv b c) are both known
and c is the canonical representative of the three.