Note-1-3
Acl2 Version 1.3 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 maintenance 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)).
