		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Further-information-on-rewriting

A grab bag of advice and information on rewriting

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; if including "arithmetic/top-with-meta" isn't sufficient, you could try (include-book "arithmetic-5/top" :dir :system).

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.