INTRODUCTION-TO-THE-DATABASE

how to update the database 
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 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 primiarily 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 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.