Major Section: RULE-CLASSES
See rule-classes for a general discussion of rule classes and
how they are used to build rules from formulas. An example
:corollary formula from which a :congruence rule might be built is:
Example:
(implies (set-equal x y)
(iff (memb e x) (memb e y))).
Also see defcong and see equivalence.
General Form:
(implies (equiv1 xk xk-equiv)
(equiv2 (fn x1... xk ...xn)
(fn x1... xk-equiv ...xn)))
where equiv1 and equiv2 are known equivalence relations, fn is an
n-ary function symbol and the xi and xk-equiv are all distinct
variables. The effect of such a rule is to record that the
equiv2-equivalence of fn-expressions can be maintained if, while
rewriting the kth argument position, equiv1-equivalence is
maintained. See equivalence for a general discussion of the
issues. We say that equiv2, above, is the ``outside equivalence''
in the rule and equiv1 is the ``inside equivalence for the kth
argument''
The macro form (defcong equiv1 equiv2 (fn x1 ... x1) k) is an
abbreviation for a defthm of rule-class :congruence that attempts to
establish that equiv2 is maintained by maintaining equiv1 in fn's
kth argument. The defcong macro automatically generates the general
formula shown above. See defcong.
The memb example above tells us that (memb e x) is propositionally
equivalent to (memb e y), provided x and y are set-equal. The
outside equivalence is iff and the inside equivalence for the second
argument is set-equal. If we see a memb expression in a
propositional context, e.g., as a literal of a clause or test of an
if (but not, for example, as an argument to cons), we can rewrite
its second argument maintaining set-equality. For example, a rule
stating the commutativity of append (modulo set-equality) could be
applied in this context. Since equality is a refinement of all
equivalence relations, all equality rules are always available.
See refinement.
All known :congruence rules about a given outside equivalence and fn
can be used independently. That is, consider two :congruence rules
with the same outside equivalence, equiv, and about the same
function fn. Suppose one says that equiv1 is the inside equivalence
for the first argument and the other says equiv2 is the inside
equivalence for the second argument. Then (fn a b) is equiv
(fn a' b') provided a is equiv1 to a' and b is equiv2
to b'. This is an easy consequence of the transitivity of
equiv. It permits you to think independently about the inside
equivalences.
Furthermore, it is possible that more than one inside equivalence
for a given argument slot will maintain a given outside equivalence.
For example, (length a) is equal to (length a') if a and a' are
related either by list-equal or by string-equal. You may prove two
(or more) :congruence rules for the same slot of a function. The
result is that the system uses a new, ``generated'' equivalence
relation for that slot with the result that rules of both (or all)
kinds are available while rewriting.
:Congruence rules can be disabled. For example, if you have two
different inside equivalences for a given argument position and you
find that the :rewrite rules for one are unexpectedly preventing the
application of the desired rule, you can disable the rule that
introduced the unwanted inside equivalence.
More will be written about this as we develop the techniques.