Introduction-to-the-database
How to update the database
We assume you've read introduction-to-rewrite-rules-part-1
and introduction-to-key-checkpoints.
The theorem prover's heuristics are influenced by the database of rules and
the enabled/disabled status of the rules. You can think of the database as a
global hint, potentially affecting all parts of a proof attempt.
However, in addition to the ``global hint,'' it is possible to give
local hints that affect the theorem prover's behavior on specific
subgoals. We discuss the database here and discuss local hints later in the
tutorial.
The theorem prover's ``database'' is called the ACL2 world. You
change the world by issuing commands called events. The most common
events are defun for defining new functions (and predicates) and
defthm for proving new theorems. Both add rules to the database. Here
are some commonly used events.
We recommend that upon the first reading of this tutorial you do not follow
the links shown below! The links take you into the hypertext reference
manual, where it is easy to get lost unless you're looking for detail about
one specific feature.
See defun to define a new function or predicate symbol.
Definitional axioms are just a kind of rewrite rule, but defun may
also add rules affecting the determination of the type of a term and rules
affecting the induction analysis. When you issue a defun command you
will always supply the name of the function or predicate, the list of
formal parameters, v1,...vn, and the body:
(defun name (v1 ... vn)
body)
If the event is accepted, a definitional axiom is added to the
world, (name v1...vn)=body, stored as a special
kind of unconditional rewrite rule. However, the defun event may require
theorems to be proved. Specifically, measure theorems must be proved
to establish that recursively defined functions always terminate, by proving
that an ordinal measure of the formal parameters decreases in a
well-founded way in every recursive call. In addition, if
guards are being used to declare the expected domain of the
newly defined function, guard theorems might be proved to establish
that all functions stay within their expected domains. In any case, you may
provide additional information to the defun event, coded as part of the
declaration that Common Lisp allows:
(defun name (v1 ... vn)
(declare (xargs ...))
body)
The xargs (``extra arguments to defun'') entry may specify, among
other things, the measure to use in the termination proof, hints for use by
the prover during the termination proof, the guard of the new function, and
hints for use by the prover during the guard verification step.
See defthm to prove a theorem and to add it as a rule of one
or more specified rule-classes. When you issue a defthm command you
always specify a name for the theorem you're trying to prove and a
formula stating the theorem. You may optionally supply some local
hints as we describe later in the tutorial. You may also optionally supply
some rule classes indicating how you want your formula stored as a
rule, after it is proved. We discuss the defthm rule classes
below.
See in-theory to enable or disable rules. Rules have names
derived from the names you give to functions and theorems, e.g., (:REWRITE
LEFT-IDENTITY-OF-FOO . 2) for the second rewrite rule you created from the
theorem named LEFT-IDENTITY-OF-FOO. Rule names are called runes.
A theory is just a set (list) of runes. The current theory is
the list of enabled runes and the in-theory event can add runes to or
delete runes from the current theory.
See include-book to change the world by loading a
certified file of other events. The most common use of include-book is
to load ``community books'' — books written by other ACL2 users who have
released them for distribution to the community. The most common books loaded
are probably the arithmetic books:
; * for the most elementary arithmetic, needed for any problem
; that involves even simple addition and multiplication like
; (+ x (* 2 y) -3):
(include-book "arithmetic/top-with-meta" :dir :system)
; * for more complicated arithmetic involving non-linear terms like
; (* x y), (expt x (+ i j)), and floor and mod
(include-book "arithmetic-5/top" :dir :system)
But for a complete list of system books, see books .
See certify-book to
certify a file of events for reuse later.
See defconst to define a new constant, allowing you to write a
symbol, e.g., *weekdays* in place of some object, e.g., '(MON TUE WED
THU FRI) in formulas.
See defmacro to define a new syntactic abbreviation. The macro
facility in Lisp is quite powerful, allowing you to compute the form to
which some type-in expands. For example, the primitive macro COND is
defined so that (COND ((P X) 1)((Q X) 2)(T 3)) expands to (IF (P X)
1 (IF (Q X) 2 3)).
See defstobj to introduce a single-threaded object that
your functions may modify ``destructively'' provided they follow strict
syntactic rules.
See events for a complete list of the ACL2 events. There are
events to allow mutually recursive definitions, to introduce some new function
symbols constrained to satisfy given axioms, to allow the temporary
introduction of a ``local'' event to help prove some goal theorem and then
disappear, to provide the power of first-order quantification and a choice
operator, and many other features.
There are also commands that allow you to inspect the world, e.g., to print
the command that introduced a given name, to show all the commands back to a
certain one, undo the last command or more generally roll-back to an earlier
command. See history .
The Defthm Rule-Classes
We've already discussed the key role that rules play in controlling the
behavior of the system. New rules are introduced primarily with the
defthm event, though defun and other events may introduce rules.
To prove formula and generate, say a :rewrite rule and a
:generalize rule from it, you would write
(defthm name
formula
:rule-classes (:rewrite :generalize))
If you wanted to rearrange the shape of the formula before generating the
:rewrite rule you could provide a :corollary modifier to the
:rewrite rule class:
(defthm name
formula
:rule-classes ((:rewrite :corollary ...)
:generalize)).
There are many classes of rules, affecting different parts of the system.
Each class is denoted by a keyword, e.g., :REWRITE, :LINEAR, etc.
You are responsible for specifying the class(es) of rules to be generated from
a given formula and several different rules (possibly of different classes)
may be derived from a single formula. Each class admits optional modifiers
that allow you finer control over each rule. Each class admits the
:corollary modifier with which you can rearrange the formula before a
rule of that class is generated. This allows you to state a theorem in its
most elegant form for publication purposes but store it as a rule with the
most appropriate hypotheses and conclusion. Other modifiers tend to be
specific to certain rule classes, but for example, :rewrite rule
modifiers include an optional limit on the depth of backchaining and options
for handling free variables.
We give some links below to other classes of rules. However, we recommend
that you not follow these links upon your first reading of this tutorial!
See rewrite for a description of how to create a rewrite
rule.
See linear for a description of how to store theorems
concluding with arithmetic inequalities. The trouble with storing
(<= (len (delete e x)) (len x))
as a rewrite rule is that it only matches instances of that inequality and
thus fails to match
(<= (LEN (DELETE E X)) (+ 1 (LEN X)))
ACL2 contains an extensible linear arithmetic decision procedure and by
storing inequalities as :linear rules you can make that decision
procedure aware of the basic inequalities between non-primitive numerically
valued terms.
See equivalence , see congruence ,
and see refinement to learn how to introduce a new equivalence
relation to the rewriter. For example, suppose you define set-equal so
that it returns t precisely if its two arguments are lists containing the same
elements, regardless of order or number of occurrences. Note that under this
sense of ``equivalence'', (rev x) is the identity function and
append is commutative, for example.
(set-equal (rev x) x)
(set-equal (append x y) (append y x))
You can make ACL2 use these two theorems as :rewrite rules to replace
instances of (REV x) and (APPEND x y) by set-equal terms, even
though the results are not actually EQUAL. This is possible provided the
target occurs in a context admitting set-equal as a congruence relation.
For example, the congruence rule:
(implies (set-equal a b)
(iff (member e a)
(member e b)))
gives the rewriter permission to use the above set-equal rules as
rewrite rules in the second argument of any member expression being used
in a propositional way.
See elim for a description of how to make the system adopt a
``change of variable'' tactic that can trade in destructor functions
for constructor functions. In analogy with how ACL2 eliminates (CAR
X) and (CDR X) by replacing X with (CONS A B), you can make
it eliminate other destructors. For example, the community book
"arithmetic-5/top" provides an elim rule that eliminates (floor
x y) and (mod x y) by replacing x by (+ r (* y q)), so that
the floor expression becomes q and the mod expression becomes
r. When introducing your own elim rules you will probably also need
to introduce generalize rules (see below) so that the new variables are
appropriately constrained.
See generalize for a description of how you can make ACL2 restrict
the new variables it introduces when generalizing. ACL2 will sometimes
replace a term by a new variable and with generalize rules you can ensure
that the new variable symbol has certain properties of the term it
replaces.
See induction for a description of how to tailor the inductions
suggested by a term. Most of the time when ACL2 chooses the ``wrong''
induction, the easiest fix is with a local :induct hint (see below). But
if the same problem arises repeatedly in several theorems, you might want to
``educate'' ACL2's induction heuristic.
For a complete list of rule-classes, See rule-classes .
If you are reading this as part of the tutorial introduction to the theorem
prover, use your browser's Back Button now to return to introduction-to-the-theorem-prover.
