''. If you are reading this topic as part of the tutorial on
the theorem prover, do not follow these links upon your first reading. Just
take note of the existence of the facilities and ideas mentioned.Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
In the following paragraphs we give some links to advanced topics, marked
with ``''. If you are reading this topic as part of the tutorial on
the theorem prover, do not follow these links upon your first reading. Just
take note of the existence of the facilities and ideas mentioned.
Arithmetic: If your goal theorem involves even trivial arithmetic,
such as adding or subtracting 1, we recommend that you do
(include-book "arithmetic/top-with-meta" :dir :system)which loads into ACL2 all the rules in one of the so-called ACL2 ``community books''. (Books are certified files of definitions, lemmas, etc., usually prepared by other ACL2 users and explicitly shared with the community. The ACL2 installation instructions suggest downloading the community books.) The book "top-with-meta" is the most elementary and most widely used arithmetic book. Other community books include "arithmetic-5/top" and various hardware and floating-point arithmetic books.
Rules Concluding with Arithmetic Inequalities: If you are tempted to create a rewrite rule with an arithmetic inequality as its conclusion or left-hand side, think again. Inequalities such as
(<= (len (delete e x)) (len x))make poor left-hand sides for rewrite rules. For example, the inequality above does not match the target
(<= (LEN (DELETE E X)) (+ 1 (LEN X)))even though it is sufficient to prove the target (given some simple arithmetic). We recommend that if you have a theorem that establishes an arithmetic inequality, you make it a linear rule. See linear
.Rearranging Formulas Before Making Rules: It is possible to rearrange
the propositional structure of a proved formula before processing it as a
rule. This allows you to state a theorem one way ``for publication'' and
rearrange it to be stored as a more effective rule.
See introduction-to-the-database (a tutorial topic you'll come to later) and
its discussion of the concept of corollary. Also, see the discussion of
corollary in rule-classes .
Rewriting with New Equivalence Relations:
You may introduce new equivalence relations, like ``set-equal'' or
``is-a-permutation'' and cause the rewriter to replace equivalents by
equivalents in suitable contexts, where you use congruence rules to
inform ACL2 of where these more relaxed notions of equivalence may be used;
see equivalence and see congruence .
Pragmatic Advice to Control Rules: You may attach various pragmas
to a rule that allow you rather fine heuristic control over whether and how the
rule is applied. For example, you may mark a hypothesis to be
forced (see force ) meaning that the rule is to be applied even if that
hypothesis is not relieved -- but if the proof is successful the system will
turn its attention to all forced subgoals. You may similarly mark a
hypothesis so as to cause a case split, allowing the relief of the
hypothesis on one branch and spawning another branch explicitly denying the
hypothesis; see case-split . You may add a bogus hypothesis that looks at
the intended application of the rule and decides whether to apply the rule
or not, performing an arbitrary computation on the syntactic context of the
application; see syntaxp . By providing a :match-free modifier to the
:rewrite rule declaration in your rule-classes, you may tell ACL2 to try all
or only the first free variable value it guesses (see rule-classes
). You may provide a bogus hypothesis that computes from the
syntactic environment the values to guess for the free variables in a rule;
see bind-free . You may mark a term so that the rewriter does not
dive into it; see hide .
Programming Your Own Rewriter:
If you cannot find a way to use rewrite rules to make the transformations
you desire, you might investigate the use of metafunctions. A
metafunction is just a little theorem prover of your own design. It takes
as input a list structure representing a term and returns a list structure
representing a term. If you can prove that the meaning of the input and
output terms are equivalent, you can extend the ACL2 simplifier to call your
metafunction. See meta .
The Order in which Targets are Rewritten:
The rewriter sweeps through terms ``inside-out'' otherwise known as
``left-most innermost first''. Thus, before trying to apply rewrite
rules to (f a1 ... an), rules are applied to the ai.
This has the good effect of normalizing the ai.
This fact might help you understand why sometimes your rules ``don't
seem to fire.'' For example, suppose you have a rule for rewriting
(len (rev x)) to (len x) and suppose you wish to prove a theorem
about (LEN (REV (CONS A B))). Suppose rev is defined in terms of
append, as shown in programming-knowledge-taken-for-granted. Then
you might see a checkpoint in which the (LEN (REV ...)) above has been
simplified to (LEN (APPEND (REV B) (LIST A))) instead of to
(LEN (CONS A B)). Why wasn't your rule about (len (rev x)) applied?
The reason is that (REV (CONS A B)) rewrote to (APPEND (REV B) (LIST A))
before rules were applied to (LEN (REV ...)). You need a rule about
(len (append x y)), as you will see from the checkpoint.
The Order in which Rules are Tried: The rewriter tries the most
recently proved rules first. For example, suppose f, g, and h
are functions defined so that the following two theorems are provable and
suppose you executed the following two events in the order shown:
(defthm rule1 (equal (f (g x)) (h 1 x))) (defthm rule2 (equal (f (g x)) (h 2 X)))Then if rewrite rules are applied to
(F (G A)), the result
will be (H 2 A), because the latter rule, rule2, is applied
first. It is generally best not to have conflicting rules or, at least,
to understand how such conflicts are resolved. The system will warn you
when you propose a rule that conflicts with an existing one.If you were reading this topic as part of the tutorial introduction to the theorem prover, use your browser's Back Button now to return to introduction-to-rewrite-rules-part-2.
