Major Section: RELEASE-NOTES
This is the first version of ACL2 released under the copyright of the University of Texas (UT). Future releases of ACL2 will be made from UT rather than Computational Logic, Inc. (CLI). Version 2.0 is just Version 1.9 as released by CLI, with a few bugs fixed.
A bug causing an infinite loop was fixed in functional instantiation.
The bug manifested itself when two conditions occurred simultaneously:
First, the functional substitution replaces a function symbol, e.g., FOO,
with a LAMBDA expression containing a free variable (a variable not among
in the LAMBDA formals). And, second, in one of the constraints being
instantiated there is a call of the function symbol FOO within the scope
of another LAMBDA expression. Unless you used such a functional
substitution, this bug fix will not affect you.
Less important notes:
The implementation of PRINC$ was changed so that it was no longer
sensitive to the external setting of *print-base* and other Common Lisp
special variables.
Typographical errors were fixed in the documentation.
Major Section: RELEASE-NOTES
The identity function case-split has been added. It is similar
to force but causes an immediate split of the top-level goal on
whether the indicated hypothesis is true.
Less important notes:
Minor bugs in the documentation were fixed.
Major Section: RELEASE-NOTES
Important changes:
A bug was fixed in the compile command, :comp. The compiled code
produced by :comp in previous versions could be wildly incorrect
because of a confusion between the printer and the reader regarding
what was the current Lisp *package*. This bug could manifest itself
only if you used the :comp command to compile previously uncompiled
functions while the current package was different from "ACL2".
What happened in that situation depended upon what symbols were
imported into your current package. The most likely behavior is
that the compiler would break or complain or the resulting compiled
code would call functions that did not exist.
There have been no other important changes to the code.
However, this release contains some useful new books, notably those on
the books subdirectories cli-misc and ihs. Both have
README files. The ihs books provide support for integer
hardware specifications. These books were crucial to Bishop Brock's
successful modeling of the Motorola CAP. We thank Bishop for producing
them and we thank all those who worked so hard to get these books released.
We highly recommend the ihs books to those modeling ALUs and other
arithmetic components of microprocessors or programming languages.
In previous versions of ACL2, the arithmetic books, found on
books/arithmetic/, included the addition of several unproved axioms
stating properties of the rationals that we believed could be derived from
our ``official'' axioms but which we had not mechanically proved. The axioms
were found in the book rationals-with-axioms.lisp,
which was then used in the uppermost arithmetic books top.lisp and
top-with-meta.lisp. John Cowles has now provided us with ACL2 proofs
of those ``axioms'' and so in this release you will find both
rationals-with-axioms.lisp and rationals-with-axioms-proved.lisp.
The former is provided for compatibility's sake. The latter is identical
but contains defthms where the former contains defaxioms.
The top-most books have been rebuilt using ``-axioms-proved'' book.
Thanks John.
Less important notes:
Bishop Brock found a bug in translated-acl2-unwind-protectp4.
Jun Sawada reported a bug in linear arithmetic that caused us not to
prove certain trivial theorems concluding with (not (equal i j)).
We have fixed both.
We now prohibit definitions that call certain event commands
such as DEFTHM and TABLE because our Common Lisp implementations
of them differ from their ACL2 meanings (so that compiled books
can be loaded correctly and efficiently).
Minor bugs in the documentation were fixed.
Major Section: RELEASE-NOTES
Important changes:
Versions of ACL2 preceding this one contain a subtle soundness bug! We found a flaw in our detection of subversive-recursions. The bug allowed some subversive recursions to slip through undetected.
We believe it would have been difficult to have exploited this flaw
inadvertently. In particular, the following five conditions are
necessary.
(1) Introduce a constrained function, say f, via an encapsulate.
(2) In the same encapsulation, define a clique of mutually
recursive functions. This clique must be non-local and in
:logic mode.
(3) In that mutually recursive clique, use the constrained function
f (perhaps indirectly) so that the termination argument for the
clique depends on properties of the witness for f. Thus,
f or some other function dependent upon f, must be used in
an argument in a recursive call or in a term governing a recursive
call. Furthermore, the use of f must be such that the
termination proof cannot be done without exploiting properties of
the witness for f. Other uses of the constrained functions in
the clique are ok.
(4) Fail to include the exploited properties of f among the
constraints of the encapsulation.
(5) Later, outside the encapsulation, explicitly use a functional
instantiation in which f is replaced by a function not enjoying
the crucial properties.
See subversive-recursions for details.
Less important notes:
We have begun to write some introductory tutorial material for those
who wish to learn to program in ACL2. Most of this material is
HTML-based. See the Hyper-Card on the ACL2 home page.
The documentation of verify-guards was improved to explain why
one might wish to verify the ``guards'' of a defthm event. The
missing documentation was noticed by John Cowles.
A bug was fixed in cross fertilization. The bug caused the system to report that it had substituted one term for another when in fact no substitution occurred. The bug was noticed by Bill McCune.
Major Section: RELEASE-NOTES
The new features are extensively documented. The relevant topics are:
:doc or :more-doc's ``(cont'd)''
:more
keyword command is so handy for reading long documentation strings
that we recommend you start with :doc more if reading at the
terminal. Some documentation has been written for guards which
you might find interesting.
Major Section: RELEASE-NOTES
Hacker mode has been eliminated and programming mode has been added.
Programming mode is unsound but does syntax checking and permits
redefinitions of names. See :doc load-mode and :doc g-mode.
The arguments to ld have changed. Ld is now much more
sophisticated. See ld.
For those occasions on which you wish to look at a large list
structure that you are afraid to print, try (walkabout x state),
where x is an Acl2 expression that evaluates to the structure in
question. I am afraid there is no documentation yet, but it is
similar in spirit to the Interlisp structure editor. You are
standing on an object and commands move you around in it. E.g., 1
moves you to its first element, 2 to its second, etc.; 0 moves you
up to its parent; nx and bk move you to its next sibling and
previous sibling; pp prettyprints it; q exits returning nil; = exits
returning the thing you're standing on; (= symb) assigns the thing
you're standing on to the state global variable symb.
Several new hints have been implemented, including :by and :do-not.
The old :do-not-generalize has been scrapped in favor of such new
hints as :do-not (generalize elim). :By lets you say ``this goal is
subsumed by'' a given lemma instance. The :by hint also lets you
say ``this goal can't be proved yet but skip it and see how the rest
of the proof goes.'' See hints.
Major Section: RELEASE-NOTES
Programming mode has been eliminated. Instead, all functions have a
``color'' which indicates what can be done with the function. For
example, :red functions can be executed but have no axioms
describing them. Thus, :red functions can be introduced after
passing a simple syntactic check and they can be redefined without
undoing. But nothing of consequence can be proved about them. At
the other extreme are :gold functions which can be executed and
which also have passed both the termination and the guard
verification proofs. The color of a function can be specified with
the new xargs keyword, :color, which, if omitted defaults to the
global setting of ld-color. Ld-color replaces load-mode. Setting
ld-color to :red causes behavior similar to the old :g-mode.
Setting ld-color to :gold causes behavior similar to the old
:v-mode. It is possible to prototype your system in :red and then
convert :red functions to :blue individually by calling
verify-termination on them. They can then be converted to :gold
with verify-guards. This allows us to undertake to verify the
termination and guards of system functions. See :doc color for an
introduction to the use of colors.
Type prescription rules have been added. Recall that in Nqthm, some
rewrite rules were actually stored as ``type-prescriptions.'' Such
rules allow the user to inform Nqthm's primitive type mechanism as
to the kinds of shells returned by a function. Earlier versions of
Acl2 did not have an analogous kind of rule because Acl2's type
mechanism is complicated by guards. Version 1.3 supports
type-prescription rules. See type-prescription.
Three more new rule-classes implement congruence-based rewriting.
It is possible to identify a binary relation as an equivalence
relation (see equivalence), to show that one equivalence
relation refines another (see refinement) and to show that a
given equivalence relation is maintained when rewriting a given
function call, e.g., (fn ...xk...), by maintaining another
equivalence relation while rewriting the kth argument
(see congruence). If r has been shown to be an equivalence
relation and then (implies hyps (r (foo x) (bar x))) is proved as a
:rewrite rule, then instances of (foo x) will be replaced by
corresponding instances of (bar x) provided the instance occurs in a
slot where the maintainence of r-equivalence is known to be
sufficient and hyps can be established as usual.
In Version 1.2, rule-classes were simple keywords, e.g., :rewrite or
:elim. In Version 1.3, rule-classes have been elaborated to allow
you to specify how the theorem ought to be used as a rule. That is,
the new rule-classes allows you to separate the mathematical
statement of the formula from its interpretation as a rule.
See rule-classes.
Rules used to be named by symbols, e.g., car and car-cons were the
names of rules. Unfortunately, this was ambiguous because there are
three rules associated with function symbols: the symbolic
definition, the executable counterpart, and the type-prescription;
many different rules might be associated with theorems, depending on
the rule classes. In Version 1.3 rules are named by ``runes''
(which is just short hand for ``rule names''). Example runes are
(:definition car), (:executable-counterpart car), and
(:type-prescription car . 1). Every rule added by an event has a
different name and you can enable and disable them independently.
See rune and see theories.
The identity function force, of one argument, has been added and
given a special interpretation by the functions responsible for
establishing hypotheses in backchaining: When the system fails to
establish some hypothesis of the form (force term), it simply
assumes it is true and goes on, delaying until later the
establishment of term. In particular, pushes a new subgoal to prove
term in the current context. When that subgoal is attacked, all of
the resources of the theorem prover, not just rewriting, are brought
to bear. Thus, for example, if you wish to prove the rule
(implies (good-statep s) (equal (exec s n) s')) and it is your
expectation that every time exec appears its first argument is a
good-statep then you might write the rule as
(implies (force (good-statep s)) (equal (exec s n) s')). This
rule is essentially an unconditional rewrite of (exec s n) to
s' that spawns the new goal (good-statep s). See force.
Because you can now specify independently how a theorem is used as a
rule, you need not write the force in the actual theorem proved.
See rule-classes.
Version 1.3 supports a facility similar to Nqthm's break-lemma.
See break-rewrite. You can install ``monitors'' on runes that
will cause interactive breaks under certain conditions.
Acl2 also provides ``wormholes'' which allow you to write functions
that cause interaction with the user but which do not require that
you have access to state. See wormhole.
The rewriter now automatically backchains to stronger recognizers.
There is no user hook to this feature but it may simplify some
proofs with which older versions of Acl2 had trouble. For example,
if the rewriter is trying to prove (rationalp (foo a b c)) it is now
smart enough to try lemmas that match with (integerp (foo a b c)).
Major Section: RELEASE-NOTES
Once again ld only takes one required argument, as the bind-flg has
been deleted.
Three commands have been added in the spirit of :pe. :Pe! is
similar to :pe but it prints all events with the given name, rather
than just the most recent. The command :pf prints the corollary
formula corresponding to a name or rune. The command :pl (print
lemmas) prints rules whose top function symbol is the given name.
See pe!, see pf, and see pl.
Book naming conventions have been changed somewhat. The
once-required .lisp extension is now prohibited! Directories are
supported, including a notion of ``connected book directory''.
See book-name. Also, the second argument of certify-book is
now optional, defaulting to 0.
Compilation is now supported inside the Acl2 loop. See comp and see set-compile-fns.
The default color is now part of the Acl2 world;
see :doc default-color. Ld-color is no longer an ld special.
Instead, colors are events; see the documentation for red,
pink, blue, and gold.
A table exists for controlling whether Acl2 prints comments when it
forces hypotheses of rules; see :doc force-table. Also, it is now
possible to turn off the forcing of assumptions by disabling the
definition of force; see force.
The event defconstant is no longer supported, but a very similar
event, defconst, has been provided in its place. See defconst.
The event for defining congruence relations is now defcong
(formerly, defcon).
Patterns are now allowed in :expand hints. See the documentation
for :expand inside the documentation for hints.
We have improved the way we report rules used by the simplifier. All runes of the same type are reported together in the running commentary associated with each goal, so that for example, executable counterparts are listed separately from definitions, and rewrite rules are listed separately from linear rules. The preprocessor now mentions ``simple'' rules; see simple.
The mechanism for printing warning messages for new rewrite rules,
related to subsumption, now avoids worrying about nonrecursive
function symbols when those symbols are disabled. These messages
have also been eliminated for the case where the old rule is a
:definition rule.
Backquote has been modified so that it can usually provide predictable results when used on the left side of a rewrite rule.
Time statistics are now printed even when an event fails.
The Acl2 trace package has been modified so that it prints using the
values of the Lisp globals *print-level* and *print-length*
(respectively).
Table has been modified so that the :clear option lets you replace
the entire table with one that satisfies the val and key guards (if
any); see table.
We have relaxed the translation rules for :measure hints to defun,
so that the the same rules apply to these terms that apply to terms
in defthm events. In particular, in :measure hints mv is treated
just like list, and state receives no special handling.
The loop-stopper test has been relaxed. The old test required that every new argument be strictly less than the corresponding old argument in a certain term-order. The new test uses a lexicographic order on term lists instead. For example, consider the following rewrite rule.
(equal
(variable-update var1
val1 (variable-update var2 val2 vs))
(variable-update var2
val2 (variable-update var1 val1 vs)))
This rule is permutative. Now imagine that we want to apply this
rule to the term
(variable-update u y (variable-update u x vs)).Since the actual corresponding to both
var1 and var2 is u, which
is not strictly less than itself in the term-order, this rule would
fail to be applied in this situation when using the old test.
However, since the pair (u x) is lexicographically less than the
pair (u y) with respect to our term-order, the rule is in fact
applied using our new test.Messages about events now contain a space after certain left parentheses, in order to assist emacs users. For example, the event
(defthm abc (equal (+ (len x) 0) (len x)))leads to a summary containing the line
Form: ( DEFTHM ABC ...)and hence, if you search backwards for ``
(defthm abc'', you won't
stop at this message.
More tautology checking is done during a proof; in fact, no goal
printed to the screen, except for the results of applying :use and
:by hints or the top-level goals from an induction proof, are known
to Acl2 to be tautologies.
The ld-query-control-alist may now be used to suppress printing of
queries; see ld-query-control-alist.
Warning messages are printed with short summary strings, for example
the string ``Use'' in the following message.
Acl2 Warning [Use] in DEFTHM: It is unusual to :USE an enabled :REWRITE or :DEFINITION rule, so you may want to consider disabling FOO.At the end of the event, just before the time is printed, all such summary strings are printed out.
The keyword command :u has been introduced as an abbreviation for
:ubt :max. Printing of query messages is suppressed by :u.
The keyword :cheat is no longer supported by any event form.
Some irrelevant formals are detected; see irrelevant-formals.
A bug in the application of metafunctions was fixed: now if the output of a metafunction is equal to its input, the application of the metafunction is deemed unsuccessful and the next metafunction is tried.
An example has been added to the documentation for equivalence to suggest how to make use of equivalence relations in rewriting.
The following Common Lisp functions have been added to Acl2:
alpha-char-p, upper-case-p, lower-case-p, char-upcase,
char-downcase, string-downcase, string-upcase, and digit-charp-p.
A documentation section called proof-checker has been added for the
interactive facility, whose documentation has been slightly
improved. See in particular the documentation for
proof-checker, verify, and macro-command.
A number of events that had been inadvertently disallowed in books
are now permitted in books. These are: defcong, defcor, defequiv,
defrefinement, defstub, and verify-termination.
Major Section: RELEASE-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 encapsulate.
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 tradition.
It is possible to attach heuristic filters to :rewrite rules to
limit their applicability. See syntaxp.
A tutorial has been added; see acl2-tutorial.
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 event.
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 acl2-customization.
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
behaved.
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.
See linear-alias.
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-clauses.
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 set-invisible-fns-alist.
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 recent one.
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
pairlis function.
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 cbd.
:oops will undo the last :ubt. See oops.
Documentation has been written about the ordinals. See e0-ordinalp and see e0-ord-<.
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.