Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
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
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
(defun name (v1 ... vn) body)If the event is accepted, a definitional axiom is added to the world,
)=body, stored as a special kind of unconditional rewrite rule. However, the
defunevent 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
defunevent, coded as part of the
declarationthat 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
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 ``system'' 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 ;But for a complete list of system books, see books .
(+ 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
(include-book "arithmetic-5/top" :dir :system)
See certify-book to certify a file of events for reuse later.
See defconst to define a new constant, allowing you to write a
*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
(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 primiarily with the
defthm event, though
defun and other events may introduce rules.
To prove formula and generate, say a
:rewrite rule and a
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
:rewriterule you could provide a
:corollarymodifier to the
(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.,
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
: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,
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
:linearrules 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
(rev x) is the identity function and
commutative, for example.
(set-equal (rev x) x)You can make ACL2 use these two theorems as
(set-equal (append x y) (append y x))
:rewriterules to replace instances of
(APPEND x y)by
set-equalterms, even though the results are not actually
EQUAL. This is possible provided the target occurs in a context admitting
set-equalas a congruence relation. For example, the
(implies (set-equal a b) (iff (member e a) (member e b)))gives the rewriter permission to use the above
set-equalrules as rewrite rules in the second argument of any
memberexpression 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
(CDR X) by replacing
(CONS A B), you can make it
eliminate other destructors. For example, the system book
"arithmetic-5/top" provides an
elim rule that eliminates
(floor x y)
(mod x y) by replacing
(+ r (* y q)), so that the
floor expression becomes
q and the
mod expression becomes
When introducing your own
elim rules you will probably also need to into
generalize rules (see below) so that the new variables are
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 insure 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.