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 resulting conjecture is often simpler and hence more amenable to proof.

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))The application of such a rule is entirely analogous to the application of the rule

`car-cdr-elim`

discussed above. We discuss such rules and their
application more carefully below.

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

`equiv`

is a known equivalence relation (see defequiv); `x`

is a variable symbol; and `lhs`

contains one or more terms (called
``destructor terms'') of the form `(fn v1 ... vn)`

, where `fn`

is
a function symbol and the `vi`

are distinct variable symbols,
`v1`

, ..., `vn`

include all the variable symbols in the formula,
no `fn`

occurs in `lhs`

in more than one destructor term, and all
occurrences of `x`

in `lhs`

are inside destructor terms.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.