		Search-engine friendly clone of the ACL2 documentation.

Rule-classes

Patterned-congruence

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, e1 and e2 are known equivalence relations, which (as for classic congruence rules) we call the ``inner'' and ``outer'' equivalences. The examples above are not classic, because the ``function symbol'' of the rule — f1 in the first example, mv-nth in the second and third examples — is not being applied to distinct variables. The first example is called ``shallow'' because the ``variable'' of the rule, y1, is a top-level argument of the ``lhs'' of the rule, which is the first call of f1; the others do not have this property, as y1 is buried under further function calls.

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. Equiv1 and equiv2 are known equivalence relations, which (as in the classic case) we call the ``inner'' and ``outer'' equivalences, respectively. The terms lhs and rhs are function calls, and we call these the lhs and rhs of the rule, respectively. The variable x occurs in lhs and the variable y occurs in rhs. These must be the only occurrences of x and y in either lhs or rhs, and rhs must be the result of substituting y for x in lhs. None of the following may occur as a function symbol of lhs (or, equivalently, rhs): if, implies, equal, or a 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 e2 when rewriting a term, then it suffices to maintain e1 when rewriting an argument of that term provided there is an applicable congruence rule with outer equivalence e2 and inner equivalence e1. An analogous principle holds for patterned congruence rules, which by the way consider refinements of the outer equivalence just as is done by classic congruence rules. But there is a new wrinkle because the lhs of a patterned congruence rule is a function call that can have non-variable arguments. Consider the following events.

(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 f10 expands before the rewriter is applied to b2 — otherwise b2 would rewrite to b1 because (e1 b1 b2) is known in that context and by the rule above, it suffices to maintain e1 when rewriting b2.

(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 f10 does not expand.

(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 some-consp in the aforementioned community book, 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 = and equiv. The simplest way to understand this point may be with the following trivial example.

(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 u by the term (* a b) throughout the goal and then dropping the equality, to produce the following goal.

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

This sort of substitution can also be made when equal is replaced by a known equivalence relation, if a classic congruence rule for foo justifies the substitution. But that is not the case for our implementation of patterned congruence rules.

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.