## CONGRUENCE

the relations to maintain while simplifying arguments
```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.