the rewriter's generated equivalence relation

As the rewriter descends through a term, rewriting the subterms, it uses congruence rules to determine which equivalences may be used to rewrite one subterm to another while ensuring that each rewrite maintains a given equivalence. Generally speaking multiple equivalences may be used to rewrite subterms. A ``generated equivalence'' or ``geneqv'' (pronounced ``genequiv'') is the way we encode which equivalences may be used by the rewriter at any given subterm position.

The outline of this discussion is as follows.

- Basic Support for Equivalence Relations: a review of equivalence relations, refinement, and congruence
- Salient Facts about the ACL2 Rewriter: a review of how the rewriter works
- Using Congruence Rules to Generate Acceptable Equivalences for Subterms: an illustration of how congruence rules are used to determine the equivalences the rewriter is permitted to use
- Debugging Tools: How to see what equivalences are permitted while rewriting the current target and how to see how the set evolved as the rewriter descended from the top-level goal.

If you do not know what the following ACL2 macro forms do, you should see their documentation.

; prove and store that eqv is an equivalence relation: (defequiv eqv) ; prove and store that the equivalence relation eqv1 ; refines the equivalence relation eqv2 (defrefinement eqv1 eqv2) ; prove and store that the equivalence relation eqv1 is a congruence relation ; for the kth argument of the function f, preserving the equivalence relation ; eqv2. (defcong eqv1 eqv2 (f x1 ... xn) k)

An example of the last form is

(defcong set-equal iff (member e x) 2)

which essentially expands to

(defthm set-equal-implies-iff-member-2 (implies (set-equal x y) (iff (member e x) (member e y))) :rule-classes (:congruence))

(ACL2 actually generates a different variable name in place of

Helpful documentation topics include equivalence, refinement, congruence, `defequiv`, `defrefinement`, and
`defcong`.

- Goals, which are represented as clauses, are simplified by rewriting each literal in turn, assuming the other literals false.
- When a term is rewritten (under some assumptions) the rewriter is given an equivalence relation to maintain, i.e., the output of the rewriter must be equivalent in that sense to the input, under the assumptions.
- The initial equivalence relation to be maintained while rewriting a
literal is
`iff`. - Each
: `rewrite`rule in ACL2 effectively concludes with a term of the form(@('eqv lhs rhs) , whereeqv is an equivalence relation. Such a rule may be used to replace instances oflhs by the corresponding instance ofrhs , and maintains the equivalence relationeqv . But the rule is only applicable ifeqv *refines*the equivalence relation to be maintained by rewrite. See refinement. - If the term to be rewritten is a function call,
(fn a1 ... ak) , the rewriter rewrites eachai to, say,ai' , before applying rules to(fn a1' ... ak '). To be more precise, when the ACL2 rewriter is asked to rewrite(fn a1 ... an) maintaining some equivalenceeqv , it first rewrites eachai , maintaining an equivalence generated from the congruence rules about how to rewrite thei th argument offn maintainingeqv . Suppose eachai is thus rewritten to some other termai' . That is,(fn a1 ... an) is transformed to(fn a1' ... an ') which is known to beeqv -equivalent to(fn a1 ... an) . Then the rewriter applies all theeqv rules it knows to(fn b1 ... bn) . - How the rewriter uses the known congruence rules to determine
the equivalence relation to be maintained while rewriting each
ai is illustrated below. Equal refines all equivalence relations.Equal maintains all equivalence relations across all argument positions of all functions.

In this section show how ACL2 generates the equivalence relation it will
maintain when diving into subterms. We do so by discussing a couple of
contrived examples. The actual script for these examples is in

Our examples use the following functions.

Len is an ACL2 primitive that determines the number of elements in a list.(perm x y) determines whetherx is a permutation ofy , i.e., whether each element that occurs in eitherx ory occurs in both the same number of times. For example(perm '(A B A C) '(C B A A)) is true, but(perm '(A B A C) '(A B B C)) is false.(pairwise-iff x y) determines whether corresponding elements ofx andy are propositionally equivalent (i.e.,IFF -equivalent). For example,(pairwise-iff '(T NIL T) '(1 NIL A)) is true (since both1 andA are non-NIL and thus propositionally equivalent toT ), but(pairwise-iff '(T NIL T) '(1 NIL NIL)) is false.- Both
perm andpairwise-iff can be proved to be equivalence relations. - Both
perm andpairwise-iff are congruence relations for the first argument oflen that maintainequal ity oflen .(defthm perm-implies-equal-len-1 (implies (perm x y) (equal (len x) (len y))) :rule-classes (:congruence)) (defthm pairwise-iff-implies-equal-len-1 (implies (pairwise-iff x y) (equal (len x) (len y))) :rule-classes (:congruence))

Now consider proving

(defthm example-thm-1 (equal (len (isort (norml x))) (len x)) :rule-classes nil)

Before we start you should understand that there are many ways to prove
this little theorem. The most straightforward is just to prove that

If you run the

The rewriter then dives into the first argument of the

Thus, when rewriting

The geneqv just derived is represented internally as

((5658 PAIRWISE-IFF :CONGRUENCE PAIRWISE-IFF-IMPLIES-EQUAL-LEN-1) (5651 PERM :CONGRUENCE PERM-IMPLIES-EQUAL-LEN-1))

Ignoring the two numbers, we see two pairs, each naming an equivalence
relation and the rune that justifies its use here. The numbers are
session-specific indices uniquely associated with the two runes that allow
ACL2 to determine quickly if the runes are enabled. Note that we do not
include an entry for

Debugging tools in ACL2 typically display the geneqv above as

((PAIRWISE-IFF PAIRWISE-IFF-IMPLIES-EQUAL-LEN-1) (PERM PERM-IMPLIES-EQUAL-LEN-1))

or even

(PAIRWISE-IFF PERM).

We discuss debugging tools that display geneqvs below.

But what does this geneqv buy us during this proof? Recall where we were
in the proof discussed above. We're rewriting

(defthm perm-isort ; isort perserves perm (perm (isort X) X)) (defthm pairwise-iff-norml ; norml preserves pairwise-iff (pairwise-iff (norml x) x))

then the rewriter would replace

Thus,

The Community Book

Generated equivalence relations are never mentioned or displayed in the
prover output. But of course they are crucial since they determine which
rewrite rules can be used. If a rule was expected to be used in a proof or
proof attempt but was not used it might be because the rule's equivalence
relation failed to be a refinement of the geneqv in effect when the intended
target was encountered. If `brr` is enabled and a `monitor`ed
rule is tried by the rewriter but does not fire because it failed the
refinement test, a break-rewrite interactive break occur. See refinement-failure for some advice for how you might respond to such a
failure.

From within a break-rewrite break the `brr-commands` `linear-arithmetic` procedure) that orchestrate other calls to the rewriter.
As of Version 8.6, each frame of the

In addition, from within such a break the brr-command