make a rule to forward chain when a certain trigger arises
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.


(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.