Congruence
The relations to maintain while simplifying arguments
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 rule of class :congruence might be built,
assuming that set-equal is a known equivalence relation, is:
Example:
(defthm set-equal-implies-iff-memb-2
(implies (set-equal x y)
(iff (memb e x) (memb e y)))
:rule-classes :congruence)
Also see defcong and see equivalence.
NOTE: This topic discusses so-called ``classic'' congruence rules. A more
general class of rules, so-called ``patterned'' congruence rules, is
supported. We discuss only classic congruence rules below; for a discussion
of patterned congruence rules, first read the present topic and then see patterned-congruence.
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 other than if, 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. See geneqv for a discussion of how generated equivalence
relations are derived using congruence rules and how generated equivalence
relations are represented.
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.
NOTE however that unlike other rules, the tracking of congruence
rules is incomplete. Specifically: when congruence rules are used by the
rewriter as it descends through terms, to maintain the generated equivalence
relation used for rewriting, ACL2 does not track the congruence rules that are
used, even though it is relevant that they are all enabled. Congruence
rules that are used only in this way will therefore not appear in the summary.
Remark on Replacing IFF by EQUAL. You may encounter a warning
suggesting that a congruence rule ``can be strengthened by replacing the
second equivalence relation, IFF, by EQUAL.'' Suppose for example that this
warning occurs when you submit the following rule:
(defcong equiv1 iff (fn x y) 2)
which is shorthand for the following:
(defthm equiv1-implies-iff-fn-2
(implies (equiv1 y y-equiv)
(iff (fn x y) (fn x y-equiv)))
:rule-classes (:congruence))
The warning is telling you that ACL2 was able to deduce that fn always
returns a Boolean, and hence a trivial but useful consequence is obtained by
replacing iff by equal —
(defcong equiv1 equal (fn x y) 2)
— which is shorthand for the following:
(defthm equiv1-implies-equal-fn-2
(implies (equiv1 y y-equiv)
(equal (fn x y) (fn x y-equiv)))
:rule-classes (:congruence))
If you have difficulty proving the latter directly, you can derive it from
the former by giving a suitable hint, minimally as follows.
(defcong equiv1 equal (fn x y) 2
:hints (("Goal"
:use equiv1-implies-iff-fn-2
:in-theory
(union-theories '((:type-prescription fn))
(theory 'minimal-theory)))))
By heeding this warning, you may avoid unnecessary double-rewrite
warnings later. We now explain why, but see double-rewrite for
relevant background material.
For example, suppose you have proved the ``iff'' version of the
congruence rule above, and later you submit the following rewrite rule.
(defthm equal-list-perm
(implies (equiv1 x y)
(fn x y)))
Since fn is known to return a Boolean, ACL2 performs an optimization
that stores this rule as though it were the following.
(defthm equal-list-perm
(implies (equiv1 x y)
(equal (fn x y) t)))
Thus, if ACL2's rewriter sees a term (fn a b) in a context where the
equivalence relation iff is not being maintained, then it cannot use
rule equiv1-implies-iff-fn-2, so it rewrites argument a without the
benefit of knowing that it suffices to maintain equiv1; and then it
caches the result. When ACL2 subsequently attempts to relieve the hypothesis
(equiv1 x y), it will rewrite x simply by returning the rewritten
value of a from the result cache. This is unfortunate if a could
have been rewritten more completely under maintenance of the equivalence
relation equiv1 — which is legal in the hypothesis since a is
an argument of equiv1, which is an equivalence relation. The user
who observes the warning from rule equiv1-implies-iff-fn-2, and replaces
it with equiv1-implies-equal-fn-2, will avoid this unfortunate
case.
