Removing restrictions on classic congruence rules

This topic assumes familiarity with the basics of congruence rules; see congruence. Some aspects of congruence rules carry over to patterned congruence rules; in particular, they may be disabled, but they are not tracked for reporting in the summary.

We begin our discussion by showing some patterned congruence rules and using them to illustrate some terminology.

Example forms: ; ``Shallow'' patterned congruence rule: (implies (e1 y1 y2) (e2 (f1 3 y1 (cons x x)) (f1 3 y2 (cons x x)))) ; ``Deep'' patterned congruence rule: (implies (e1 y1 y2) (e2 (mv-nth 1 (foo x y1 z)) (mv-nth 1 (foo x y2 z)))) ; ``Deep'' patterned congruence rule: (implies (e1 y1 y2) (e2 (mv-nth 1 (foo x (g y1) z)) (mv-nth 1 (foo x (g y2) z))))

In the example forms above,

We invite you to browse the community book
`demos/patterned-congruences.lisp`, which provides several examples of
patterned congruence rules and their use, as well as several examples of
formulas that are illegal as patterned congruence rules for various
reasons.

We now define the class of patterned congruence rules. The general form of a patterned congruence rule is

(implies (equiv1 x y) (equiv2 lhs rhs)),

where the rule is not classic (see congruence) and the following
conditions hold. `lambda`.

Patterned congruence rules are used, much like classic congruence rules, by
the ACL2 rewriter to determine which equivalence relations to maintain as it
dives into a term. Recall (see congruence) that if it suffices for the
rewriter to maintain

(defun e1 (x y) (equal x y)) (defequiv e1) (defun f10 (x) (list 3 x x)) (defun f11 (x y) (declare (ignore y)) x) (defthm e1-implies-iff-f11-cong-2 (implies (e1 y1 y2) (iff (f11 (f10 x) y1) (f11 (f10 x) y2))) :rule-classes (:congruence)) (in-theory (disable f11 (:t f11) e1))

The following proof fails, because the indicated call of

(thm (implies (e1 b1 b2) (iff (f11 (f10 a) b1) (f11 (f10 a) ; expands before b2 is rewritten b2))))

On the other hand, the following succeeds because the rewrite discussed
above does indeed take place when the indicated call of

(thm (implies (e1 b1 b2) (iff (f11 (f10 a) b1) (f11 (f10 a) ; does not expand b2))) :hints (("Goal" :in-theory (disable f10))))

This inherent sequentiality of matching is important for soundness, as is
illustrated by examples using the function `demos/patterned-congruences.lisp`.

The example above illustrates the following point: as the rewriter dives into a term, then when matching is attempted using a patterned congruence rule, rewriting has already taken place to the left of the current subterm. By contrast, note that this pass through the rewriter will not yet have completed rewriting of terms to the right of the current subterm when matching a patterned congruence rule.

Patterned congruence rules are used primarily during the process of
*rewriting*. In particular, unlike classic congruence rules, they are
*not* used to do equality substitution at the goal level or in proof-builder commands such as

(defstub foo (x y z) t) (thm (implies (equal u (* a b)) (foo u u b)))

The theorem fails, of course, but what is interesting is that ACL2
simplifies it by replacing the variable

(FOO (* A B) (* A B) B)

This sort of substitution can also be made when

The discussion above is intended to suffice for effective use of patterned
congruence rules. If you are interested in their *implementation*, we
invite you to read the long comment entitled ``Essay on Patterned Congruences
and Equivalences'' in ACL2 source file `rewrite.lisp`.