ELIM

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.

The following example of an :elim rule is an important one, and is built into ACL2.

(defaxiom car-cdr-elim
  (implies (consp x)
           (equal (cons (car x) (cdr x)) x))
  :rule-classes :elim)

The class of :elim rules is fundamentally quite different from the more common class of :rewrite rules. Briefly put, a :rewrite rule replaces instances of its left-hand side with corresponding instances of its right-hand side. But an :elim rule, on the other hand, has the effect of generalizing so-called ``destructor'' function applications to variables. In essence, applicability of a :rewrite rule is based on matching its left-hand side, while applicability of an :elim rule is based on the presence of at least one destructor term.

For example, a conjecture about (car x) and (cdr x) can be replaced by a conjecture about new variables x1 and x2, as shown in the following example. (Run the command :mini-proveall and search for CAR-CDR-ELIM to see the full proof containing this excerpt.)

Subgoal *1/1'
(IMPLIES (AND (CONSP X)
              (TRUE-LISTP (REV (CDR X))))
         (TRUE-LISTP (APP (REV (CDR X)) (LIST (CAR X))))).

The destructor terms (CAR X) and (CDR X) can be eliminated by using
CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X)
by X2.  This produces the following goal.

Subgoal *1/1''
(IMPLIES (AND (CONSP (CONS X1 X2))
              (TRUE-LISTP (REV X2)))
         (TRUE-LISTP (APP (REV X2) (LIST X1)))).

This simplifies, using primitive type reasoning, to

Subgoal *1/1'''
(IMPLIES (TRUE-LISTP (REV X2))
         (TRUE-LISTP (APP (REV X2) (LIST X1)))).

The application of an :elim rule thus replaces a variable by a term that contains applications of so-called ``destructor'' functions to that variable. The example above is typical: the variable x is replaced by the term (cons (car x) (cdr x)), which applies a so-called ``constructor'' function, cons, to applications (car x) and (cdr x) of destructor functions car and cdr to that same variable, x. But that is only part of the story. ACL2 then generalizes the destructor applications (car x) and (cdr x) to new variables x1 and x2, respectively, and ultimately the result is a simpler conjecture.

More generally, the application of an :elim rule replaces a variable by a term containing applications of destructors; there need not be a clear-cut notion of ``constructor.'' But the situation described above is typical, and we will focus on it, giving full details when we introduce the ``General Form'' below.

Notice that the situation can be complicated a bit by a rule's hypotheses. For example, the replacement specified by the rule car-cdr-elim (shown near the beginning of this discussion) is only valid if the variable being replaced is a cons structure. Thus, when ACL2 applies car-cdr-elim to replace a variable v, it will split into two cases: one case in which (consp v) is true, in which v is replaced by (cons (car v) (cdr v)) and then (car v) and (cdr v) are generalized to new variables; and one case in which (consp v) is false. In practice, (consp v) is often provable, perhaps even literally present as a hypotheses; then of course there is no need to introduce the second case. That is why there is no such second case in the example above.

You might find :elim rules to be useful whenever you have in mind a data type that can be built up from its fields with a ``constructor'' function and whose fields can be accessed by corresponding ``destructor'' functions. So for example, if you have a ``house'' data structure that represents a house in terms of its address, price, and color, you might have a rule like the following.

Example:
(implies (house-p x)
         (equal (make-house (address x)
                            (price x)
                            (color x))
                x))

General Form:
(implies hyp (equiv lhs x))

To use an :elim rule, the theorem prover waits until a conjecture has been maximally simplified. It then searches for an instance of some destructor term (fn v1 ... vn) in the conjecture, where the instance for x is some variable symbol, vi, and every occurrence of vi outside the destructor terms is in an equiv-hittable position. If such an instance is found, then the theorem prover instantiates the :elim formula as indicated by the destructor term matched; splits the conjecture into two goals, according to whether the instantiated hypothesis, hyp, holds; and in the case that it does hold, generalizes all the instantiated destructor terms in the conjecture to new variables and then replaces vi in the conjecture by the generalized instantiated lhs. An occurrence of vi is ``equiv-hittable'' if sufficient congruence rules (see defcong) have been proved to establish that the propositional value of the clause is not altered by replacing that occurrence of vi by some equiv-equivalent term.

If an :elim rule is not applied when you think it should have been, and the rule uses an equivalence relation, equiv, other than equal, it is most likely that there is an occurrence of the variable that is not equiv-hittable. Easy occurrences to overlook are those in the governing hypotheses. If you see an unjustified occurrence of the variable, you must prove the appropriate congruence rule to allow the :elim to fire.

Further examples of how ACL2 :elim rules are used may be found in the corresponding discussion of ``Elimation of Destructors'' for Nqthm, in Section 10.4 of A Computational Logic Handbook.