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 `k`

th
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
`k`

th 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.

*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 maintainance 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.