Elim
Make a destructor elimination rule
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.
An :elim rule is available for a given destructor function (in the
manner described below) when it is the most recently added enabled
:elim rule for that function.
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 ``Elimination of Destructors'' for Nqthm, in
Section 10.4 of A Computational Logic Handbook.
