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

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

The macro form `defthm` of rule-class `defcong` macro automatically
generates the general formula shown above. See defcong.

The `iff` and the inside
equivalence for the second argument is `if` (but not, for example, as an argument to `cons`), we
can rewrite its second argument maintaining `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 a' b')`
provided

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')` if `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.

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

(defthm equal-list-perm (implies (equiv1 x y) (fn x y)))

Since

(defthm equal-list-perm (implies (equiv1 x y) (equal (fn x y) t)))

Thus, if ACL2's rewriter sees a term `iff` is not being maintained, then it cannot use
rule