# Defcong

Prove congruence rule

Defcong is used to prove that one equivalence relation
preserves another in a given argument position of a given function.

Example:
(defcong set-equal iff (memb x y) 2)
is an abbreviation for
(defthm set-equal-implies-iff-memb-2
(implies (set-equal y y-equiv)
(iff (memb x y) (memb x y-equiv)))
:rule-classes (:congruence))

See congruence and also see equivalence.

General Form:
(defcong equiv1 equiv2 term k
:package package
:event-name event-name
:rule-classes rule-classes
:instructions instructions
:hints hints
:otf-flg otf-flg)

where equiv1 and equiv2 are known equivalence relations;
term is a call of a function fn, other than if, on the correct
number of distinct variable arguments, (fn x1 ... xn); k is a
positive integer less than or equal to the arity of fn; package, if
supplied, is one of :current, :equiv1, :equiv2, :function
or :legacy; event-name, if supplied, is a symbol; and other
arguments are as specified in the documentation for `defthm`. The
defcong macro expands into a call of `defthm`. The name of the
`defthm` event is equiv1-implies-equiv2-fn-k, unless an
:event-name keyword argument is supplied, in which case event-name
is used. The package of symbols generated, such as variables and `defthm` names, is determined by the package argument: if it is not
supplied or its value is :current, then the `current-package` is
used; if its value is :equiv1 or :legacy, then the package of
:equiv1 is used; if its value is :equiv2, then the package of
:equiv2 is used; and if its value is :function, then the package of
fn is used. The term of the theorem is

(implies (equiv1 xk yk)
(equiv2 (fn x1... xk ...xn)
(fn x1... yk ...xn))).

The rule-class :`congruence` is added to the `rule-classes` specified, if it is not already there. All other arguments to
the generated `defthm` form are as specified by the keyword arguments
above.

NOTE: In normal usage, defcong can only create classic congruence rules, not patterned-congruence rules. However, if fn
is a macro, it's possible for a patterned congruence rule to be generated,
depending on what term expands to.

For example, the following produces a shallow patterned congruence
rule:

(defun f (x y) (and x y))
(defmacro g (x) `(f ,x t))
(defcong iff equal (g x) 1)