Geneqv
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.
Basic Support for Equivalence Relations
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 y
above.)
Helpful documentation topics include equivalence, refinement, congruence, defequiv, defrefinement, and
defcong.
Salient Facts about the ACL2 Rewriter
- 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), where eqv is an equivalence relation.
Such a rule may be used to replace instances of lhs by the corresponding
instance of rhs, and maintains the equivalence relation eqv. But
the rule is only applicable if eqv 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 each ai 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 equivalence eqv,
it first rewrites each ai, maintaining an equivalence generated from the
congruence rules about how to rewrite the ith argument of fn
maintaining eqv. Suppose each ai is thus rewritten to some other
term ai'. That is, (fn a1 ... an) is transformed to (fn a1'
... an') which is known to be eqv-equivalent to (fn a1 ... an).
Then the rewriter applies all the eqv 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.
Using Congruence Rules to Generate Acceptable Equivalences for
Subterms
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
books/demos/geneqv.lisp.
Our examples use the following functions.
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
(len (isort x)) is (len x) and to prove (len (norml x)) is
(len x). In this case, where the functions involved are isort and
norml, those theorems are easy to prove. But for some functions in
those roles of a problem like this it is easier to appeal to the properties
of certain equivalence relations. That's what we'll do here.
If you run the defthm above, the prover (after preprocessing)
eventually calls the rewriter on the equal term, requiring it to
maintain iff. The rewriter then dives into the two arguments, rewriting
(len (isort (norml x))) first, maintaining equality.
The rewriter then dives into the first argument of the len term,
(isort (norml x)). The congruence rule perm-implies-equal-len-1
above tells it that equality of the len term is maintained if the
first argument is rewritten maintaining the perm equivalence. In
addition, the congruence rule pairwise-iff-implies-equal-len-1 tells it
that equality of the len term is also maintained if the first
argument is rewritten maintaining the pairwise-iff equivalence.
Thus, when rewriting (isort (norml x)) the rewriter can use any
rewrite rule that maintains perm, any rewrite rule that maintains
pairwise-iff, and, of course, any rewrite rule that maintains
equal. In addition, of course, it can use any rewrite rule that
maintains a refinement of any of these equivalence relations. This
``generated equivalence'' or ``geneqv'' is denoted by a set containing the
named equivalence relations and the justifying congruence rules.
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 EQUAL since it maintains every equivalence relation
in every argument position of every function. Indeed, if you see a geneqv of
NIL it means EQUAL is the only acceptable equivalence relation in
that context.
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 (isort (norml x))
maintaining (PAIRWISE-IFF PERM). If the user had proved the following
two rewrite rules
(defthm perm-isort ; isort preserves perm
(perm (isort X) X))
(defthm pairwise-iff-norml ; norml preserves pairwise-iff
(pairwise-iff (norml x) x))
then the rewriter would replace (isort (norml x)) by (norml
x) using the first rule, since perm is a refinement of the geneqv, and
then the rewriter would rewrite that and replace it by x using the
second rule, since pairwise-iff is also a refinement of the geneqv.
Note that neither of these replacements preserve equality, but they are
permitted because they preserve the equality of the lens.
Thus, (equal (len (isort (norml x))) (len x)) has been simplified to
(equal (len x) (len x)) which further simplifies to t and the proof
is done.
The Community Book "books/demos/geneqv-test-book.lisp" (which
executes the commands in books/demos/geneqv-test-input.lsp) contains this and
other examples.
Debugging Tools
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 monitored
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 :path will
print the ``path'' from the current top-level goal down to the call of the
rewriter on current :target term. Like a call stack, the path is
composed of ``frames,'' most of which describe calls of the rewriter but some
of which are calls of other system functions (like the linear-arithmetic procedure) that orchestrate other calls to the rewriter.
As of Version 8.6, each frame of the :path that describes the attempt to
apply a particular rewrite rule will display the name of the equivalence
relation used by the rule (unless that name is equal). Every frame
describing a call of the rewriter includes the geneqv to be maintained as the
target is rewritten (unless the geneqv is nil which denotes the
equality relation). The noted exceptions are intended to shorten the
output in the most common cases: rewriting with equal and maintaining
equality.
In addition, from within such a break the brr-command :geneqv will
print the geneqv for the current target.
