Rule-classes-introduction
Selecting which kind of rule to create
Successful ACL2 users generally direct many of their proved
theorems to be stored as rules, which can be applied automatically in
subsequent proof attempts. See rule-classes for a detailed discussion
of the kinds of rules that can be created. Here, we give a brief introduction
to rule-classes that may suffice for most ACL2 users.
The workhorse for ACL2 proof attempts is generally the application of rewrite rules. When you prove a theorem stated with defthm, ACL2
stores it as a rewrite rule unless either the :rule-classes keyword is
supplied explicitly or an error occurs because the theorem is not in a form
that ACL2 knows how to store as a rewrite rule. See rewrite for an
introduction to rewrite rules in ACL2. That topic also has links to useful
introductory material as well as a notion of congruence, which allows
the rewriting of one term to another when the two are merely equivalent in
some suitable sense, but not necessarily equal.
Most successful ACL2 users make only sparing use of other kinds of rules
besides rewrite rules. When in doubt, the default is probably best: the
absence of any :rule-classes keyword in a defthm event, which
is equivalent to :rule-classes :rewrite. Below are some suggestions for
when other kinds of rules might be appropriate. Of course, you are welcome to
scan the community-books for examples. One can for example find many
examples (apparently more than 15,000) of :type-prescription rules by
standing in the books/ directory and issuing the following shell
command (Linux or MacOS):
time egrep -e ':rule-classes .*type-prescription' --include='*.l*sp' -ri .
Below, we sometimes speak of the ``conclusion'' of a formula. For many
rule classes, this is simply the formula itself unless the formula is of the
form (implies hyp concl), in which case it is recursively the conclusion
of concl. See the subtopics of rule-classes for detailed
documentation.
- If the conclusion is a call of a primitive recognizer or a compound
recognizer, or the negation of such — for example, (true-listp (f x
y)) — consider making a type-prescription rule. (For relevant
background on recognizers, see compound-recognizer, which also
describes how to make a rule that designates a function as a
compound-recognizer.) But note that hypotheses of such a rule are
proved (``relieved'') by ACL2 only using type-set reasoning. If you
want rewriting to be used for relieving the hypotheses, you can wrap them in
force or case-split.
- If the conclusion is an inequality or negated inequality, consider making
a linear rule, but generally only if you can identify a reasonable
maximal term, which very roughly is a syntactially largest term that binds all
the variables. For example, the formula (< (f x y) (g y z)) might not
make a good linear rule. For a more careful discussion of maximal terms, see
linear.
- If the formula is a term in normal form (not simplifiable by your rewrite
rules) that tends to be an explicit hypothesis in some of your theorems,
consider making it a forward-chaining rule. For example, if you are
reasoning about a finite state machine (such as an interpreter) and your
theorems tend to have the hypothesis (good-state-p st), and your formula
is (good-state-p (foo st)), then that formula is a good candidate for a
forward-chaining rule.
- If the rule looks like a recursive definition (equal (f x1 x2 ..)
(... (f ...) ...)), consider making a definition rule.
- When you want to control the simplifier rather than just turning rules
(especially rewrite rules) loose on your terms, consider using meta
rules or clause-processor rules.
There are other rule classes that can be useful. See rule-classes
for a complete list.
