Major Section: RULE-CLASSES
See rule-classes for a general discussion of rule classes, including how they are used to build rules from formulas and a discussion of the various keywords in a rule class description.
Examples:
(defthm p-and-r-forward ; When (p a) appears in a formula to be
(implies (and (p x) (r x)) ; simplified, try to establish (p a) and
(q (f x))) ; (r a) and, if successful, add (q (f a))
:rule-classes :forward-chaining) ; to the known assumptions.
(defthm p-and-r-forward ; as above with most defaults filled in
(implies (and (p x) (r x))
(q (f x)))
:rule-classes ((:forward-chaining :trigger-terms ((p x))
:corollary (implies (and (p x) (r x))
(q (f x)))
:match-free :all)))
To specify the triggering terms provide a non-empty list of terms
as the value of the :trigger-terms field of the rule class object.
General Form: Any theorem, provided an acceptable triggering term exists.The structure of this documentation is as follows. First we give a brief overview of forward chaining and contrast it to backchaining (rewriting). Then we lay out the syntactic restrictions on
:forward-chaining rules.
Then we give more details about the process and point to a tool to assist
you in debugging your :forward-chaining rules.Overview and When to Use Forward Chaining
Forward chaining is performed as part of the simplification process: before
the goal is rewritten a context is established. The context tells the
theorem prover what may be assumed during rewriting, in particular, to
establish hypotheses of rewrite rules. Forward chaining is used to extend
the context before rewriting begins. For example, the :forward-chaining
rule (implies (p x) (p1 x)) would add (p1 A) to the context, where
A is some term, if (p A) is already in the context.
Forward chaining and backchaining are duals. If a rewrite rule requires that
(p1 A) be established and (p A) is known, it could be done either by
making (implies (p x) (p1 x)) a :forward-chaining rule or a
:rewrite rule. Which should you choose?
As a rule of thumb, if a conclusion like (p1 A) is expected to be
widely needed, it is better to derive it via forward chaining because then
it is available ``for free'' during the rewriting after paying the one-time
cost of forward chaining. Alternatively, if (p1 A) is a rather
special hypothesis of key importance to only a few rewrite rules, it is
best to derive it only when needed. Thus forward chaining is pro-active
and backward chaining (rewriting) is reactive.
Syntactic Restrictions
Forward chaining rules are generated from the corollary term
(see rule-classes) as follows. First, every let expression is
expanded away (hence, so is every let* and lambda expression), as
is every call of a so-called ``guard holder,'' mv-list or
return-last (the latter resulting from macroexpansion of calls of
prog2$, must-be-equal or mbe), ec-call, and a few
others), or `the'. If the resulting term has the form
(implies hyp concl), then concl is treated as a conjunction, with one
forward chaining rule with hypothesis hyp created for each conjunct. In
the other case, where the corollary term is not an implies, we process
it as we process the conclusion in the first case.
Note that unlike rewrite rules, a nested implication is not folded into a single implication. Consider for example the following term.
(implies (p1 x)
(implies (p2 x)
(p3 x)))
Although this term is parsed for a rewrite rule as
(implies (and (p1 x) (p2 x)) (p3 x)), that is not the case when this term
is parsed for a forward-chaining rule, in which case (p1 x) is treated as
the hypothesis and (implies (p2 x) (p3 x)) is treated as the conclusion.The :trigger-terms field of a :forward-chaining rule class object
should be a non-empty list of terms, if provided, and should have certain
properties described below. If the :trigger-terms field is not provided,
it defaults to the singleton list containing the ``atom'' of the first
hypothesis of the formula. (The atom of (not x) is x; the atom of
any other term is the term itself.) If there are no hypotheses and no
:trigger-terms were provided, an error is caused.
A triggering term is acceptable if it is not a variable, a quoted constant, a
lambda application, a let- (or let*-) expression, or a
not-expression, and every variable symbol in the conclusion of the
theorem either occurs in the hypotheses or occurs in the trigger.
More Details about Forward Chaining
:Forward-chaining rules are used by the simplifier before it begins
to rewrite the literals of the goal. (Forward chaining is thus carried out
from scratch for each goal.) If any term in the goal is an instance of a
trigger of some forward chaining rule, we try to establish the hypotheses of
that forward chaining theorem (from the negation of the goal). To relieve a
hypothesis we only use type reasoning, evaluation of ground terms, and
presence among our known assumptions. We do not use rewriting. So-called
free variables in hypotheses are treated specially; see free-variables. If
all hypotheses are relieved, and certain heuristics approve of the newly
derived conclusion, we add the instantiated conclusion to our known
assumptions. Since this might introduce new terms into the assumptions,
forward chaining is repeated. Heuristic approval of each new addition is
necessary to avoid infinite looping as would happen with the rule
(implies (p x) (p (f x))), which might otherwise forward chain from
(p A) to (p (f A)) to (p (f (f A))), etc.
Caution. Forward chaining does not actually add terms to the goals
displayed during proof attempts. Instead, it extends an associated
context, called ``assumptions'' in the preceding paragraph, that ACL2
builds from the goal currently being proved. (For insiders: forward chaining
extends the type-alist.) The context starts out with ``obvious''
consequences of the negation of the goal. For example, if the goal is
(implies (and (p A) (q (f A)))
(c A))
then the context notes that (p A) and (q (f A)) are non-nil and
(c A) is nil. Forward chaining is then used to expand the context.
For example, if a forward chaining rule has (f x) as a trigger term and
has body (implies (p x) (r (f x))), then the context is extended by
binding (r (f A)) to non-nil, provided the heuristics approve of this
extension. Note however that since (r (f A)) is put into the context,
not the goal, you will not see it in the goal formula. Furthermore, the
assumption added to the context is just the instantiation of the conclusion
of the rule, with no simplification or rewriting applied. Thus, for example,
if it contains an enabled non-recursive function symbol it is unlikely ever
to match a (rewritten) term arising during subsequent simplification of the
goal.However, forward-chaining does support the linear arithmetic reasoning
package. For example, suppose that forward-chaining puts (< (f x) (g x))
into the context. Then this inequality also goes into the linear arithmetic
database, together with suitable instances of linear lemmas whose trigger
term is a call of g. See linear.
Debugging :forward-chaining rules can be difficult since their effects
are not directly visible on the goal being simplified. Tools are available
to help you discover what forward chaining has occurred
see forward-chaining-reports.
