Refinement-failure
what to do when a rewrite rule fails the refinement check
One reason a :rewrite rule may fail to fire is that
its equivalence relation fails to be a known refinement of the generated
equivalence relation (or ``geneqv'') governing the current target of the
rewriter. In the following discussion we assume you are familiar with the
notion of the generated equivalence relation. If not, please see geneqv for the necessary background and details.
Is a Rule Not Firing Because of a Refinement Failure?
To determine whether refinement failure is the cause of a rule's failure
to fire, enable break-rewrite with (brr t) and install a monitor with :rf set to t on the rule, e.g., (monitor rune
'(:rf t)), where rune evaluates to the rune of the rule in
question. You might also specify a :condition so that a break occurs
only if the target is the translated term, tterm, you expected the rule
to hit,
(monitor rune '(:condition (equal (brr@ :target) 'tterm) :rf t)).
Then try the proof again. (Note: if the rule being monitored is a simple abbreviation rule, be sure to supply the hint :DO-NOT
'(PREPROCESS) as discussed in monitor.) If a monitored rule fails
to fire (under the monitored condition) because its equivalence relation is
not known to refine the geneqv derived for that occurrence of the target, an
interactive break will occur. The break header will name the rule, print the
target, show the rule's equivalence relation, and show the geneqv. The
header tells you the equivalence relation is not a refinement of the geneqv.
You might wish to use the break-rewrite command :path or :path+ to
print the path down to the target from the top-level goal. That will show
the geneqv derived for each active call of the rewriter and will help you
understand why the current geneqv is what it is. While looking at the path
make sure that the current occurrence of the target is the one you expected
the rule to hit. If it is not, proceed to the next break with :ok.
When you find the target you're looking for, focus your attention on the
equivalence relation and geneqv. To fix the problem you need the former to
be a refinement of the latter. When you understand how to make that happen,
abort the failing proof attempt with :a! and try to fix the problem.
How to Fix a Refinement Failure
There are two basic ways to ``fix'' a refinement failure:
- (a) prove a refinement rule that establishes that the
equivalence relation used in the rule indeed refines one of the equivalence
relations displayed in the geneqv, or
- (b) prove a congruence rule that will extend the geneqv
derived for the current occurrence of the target.
We illustrate these approaches below. But first you must keep in mind
that the equivalence relation in the rule may not refine any possible geneqv
derivable along the path. You may have to find a different proof or, at
least, you may have to define some additional equivalence relations,
refinement rules, and congruence rules, and prove a version of your lemma
that uses a new relation. After all, this is a theorem proving problem and
not all fixes are trivial!
How Geneqvs Are Displayed
As illustrated in the discussion of geneqv, a generated equivalence
is essentially a set of equivalence relations. ACL2 prints geneqvs in three
different ways depending on the utility doing the printing.
When reporting that an equivalence relation is not a refinement of a
geneqv, the geneqv is printed simply as a list of equivalence relation names,
e.g., (EQV1 EQV2). Order is unimportant as this list represents a
set.
When reporting the path the rewriter took to the current target and the
geneqvs for each active call of the rewriter along that path, each geneqv is
printed as a list of doublets, where the first component of the doublet is
the name of an equivalence relation and the second component is the name of
the congruence rule responsible for adding that relation to the
geneqv, e.g.,
((EQV1 EQV1-IFF-CONGRUENCE-FOR-F)
(EQV2 EQV2-IFF-CONGRUENCE-FOR-F))
This is just another presentation of (eqv1 eqv2) but we believe
the congruence rule names may help you recall how equivalence relations get
into the set.
Finally, in trace$, or the value returned by (brr@ :geneqv) or any
other system utility that displays the actual internal representation of a
geneqv you will see something like this:
((5603 EQV1 . (:congruence EQV1-IFF-CONGRUENCE-FOR-F))
(4957 EQV2 . (:congruence EQV2-IFF-CONGRUENCE-FOR-F)))
where the equivalence relation names are paired with the runes (not just the names)
of the responsible congruence rules and the numbers are unique session-dependent indices
for those runes allowing quick determination of the enabled status of the rules.
You will see the first two print conventions in the examples below.
Some Generic Examples
In the following discussion we introduce some functions that will allow us
to explore refinement failures. The experiments reported below are carried
out in the community book books/demos/refinement-failure-test-book.lisp
whose input/output log may be found in
books/demos/refinement-failure-test-log.txt.
We're going to attempt to prove (P (F (G A (BETA B)))) by rewriting
the occurrence of (BETA B) to (GAMMA B) and appealing to a rule
that establishes (P (F (G A (GAMMA B)))). But at every subterm level in
the conjecture different equivalence relations are involved. Thus, many
equivalence and congruence relations are involved and that makes this example
hard to follow. Assume that PEQ, FEQ, G2EQ1, G2EQ2, and
G2EQ1! are known equivalence relations.
Possibly Distracting Aside: In this section of this documentation we use
names that follow a certain convention. These conventions help the authors
keep the names straight! Perhaps they'll help you too. Names containing
``EQ'' are equivalence relations; they will serve as ``inside''
equivalences for the function symbol indicated by the first character in the
name, ``P'', ``F'' or ``G''; if that first character is
followed by ``2'' it means they apply to the second argument of the function,
otherwise they apply to the first (and only) argument; and if there is more
than one such inside equivalence relation for that function the name is
suffixed with ``1'' or ``2''. The exclamation mark at the end of
``G2EQ1!'' is to remind us that the function is a refinement of G2EQ1.
Thus PEQ is the inside equivalence for the first (only) argument of
P-terms and G2EQ1 is the inside equivalence for the second argument
of G-terms and is one of two such relations.
Imagine that we've proved two rewrite rules:
Clearly, our strategy to prove (P (F (G A (BETA B)))) is to use
RULE to replace the (BETA B) by (GAMMA B), and then use
DONE to reduce the conjecture to T.
However, the problem is that RULE uses the equivalence relation
G2EQ1!. So the rewriter, which starts by maintaining IFF on the
top-level P term, will have to evolve a geneqv so that by the time it
reaches the occurrence of (BETA B) the geneqv at that target admits
G2EQ1! as a refinement. To do so we'll provide the following congruence rules. As you read them, remember that the term we'll be working
on is (P (F (G A (BETA B)))), i.e., our conjecture is a call of P,
in which the 1st (and only) argument is a call of F, in which the 1st
(and only) argument is a call of G, in which the 2nd argument is call of
BETA.
- IFF is maintained on a call of P provided PEQ is maintained on
the 1st argument of P:
- event: (DEFCONG PEQ IFF (P X) 1)
- name: PEQ-IMPLIES-IFF-P-1
- PEQ is maintained on a call of F provided FEQ is maintained on
the 1st argument of F:
- event: (DEFCONG FEQ PEQ (F X) 1)
- name: FEQ-IMPLIES-PEQ-F-1
- FEQ is maintained on a call of G provided G2EQ1 is maintained on
the 2nd argument of G:
- event: (DEFCONG G2EQ1 FEQ (G X Y) 2)
- name: G2EQ1-IMPLIES-FEQ-G-2
- FEQ is also maintained on a call of G provided G2EQ2 is maintained on
the 2nd argument of G:
- event: (DEFCONG G2EQ2 FEQ (G X Y) 2)
- name: G2EQ2-IMPLIES-FEQ-G-2
Note that there are two ways to maintain FEQ on a call of G:
maintain either G2EQ1 or G2EQ2 on the second argument of G.
But neither of those equivalence relations is used in our rewrite RULE.
Our RULE uses G2EQ1!, so assume we've proved:
Having arranged all of the above, imagine issuing the commands
(brr T)
(monitor '(:REWRITE RULE)
'(:condition (and (equal (brr@ :target) '(BETA B))
'(:path+ :go))
:rf t))
(thm (P (F (G A (BETA B))))
:hints (("Goal" :do-not '(preprocess))))
Note: The :condition value above will cause a break only if the
:target is (BETA B), but when the break occurs it will issue the
command :PATH+ to print the path and then issue the command :GO to
proceed from the break. Because we've just monitored a simple
abbreviation rule, we include in the thm command the hint to avoid
preprocessing, as advised in the documentation for monitor.
Because we've done the equivalence, congruence, and refinement setup
perfectly, our RULE will fire and we will get a break like this:
(1 Breaking (:REWRITE RULE) on (BETA B):
1 ACL2 >
The subsequent :PATH+ command will show how the rewriter descended to
here from the top-level goal and will display the geneqvs derived for each
rewrite.
1 ACL2 >:path+
1. Simplifying the clause
((P (F (G A (BETA B)))))
2. Rewriting (to simplify) the atom of the first literal,
(P (F (G A (BETA B)))),
Geneqv: (IFF)
3. Rewriting (to simplify) the first argument,
(F (G A (BETA B))),
Geneqv: ((PEQ PEQ-IMPLIES-IFF-P-1))
4. Rewriting (to simplify) the first argument,
(G A (BETA B)),
Geneqv: ((FEQ FEQ-IMPLIES-PEQ-F-1))
5. Rewriting (to simplify) the second argument,
(BETA B),
Geneqv: ((G2EQ2 G2EQ2-IMPLIES-FEQ-G-2)
(G2EQ1 G2EQ1-IMPLIES-FEQ-G-2))
6. Attempting to apply (:REWRITE RULE) to
(BETA B)
Preserving: G2EQ1!
Geneqv: ((G2EQ2 G2EQ2-IMPLIES-FEQ-G-2)
(G2EQ1 G2EQ1-IMPLIES-FEQ-G-2))
1 ACL2 >
Recall, from the discussion above, that sometimes geneqvs are printed
merely as a list of equivalence relations, e.g., (G2EQ2 G2EQ1), and
other times, as above, are printed so as to include the name of the
congruence relation responsible for each equivalence.
Notice that in frame 4, where the rewriter is working on (G A (BETA
B)) it is to maintain the FEQ equivalence relation (which was
justified from frame 3 by the rule FEQ-IMPLIES-PEQ-F-1 where the
rewriter was to maintain PEQ). But when the rewriter stepped from frame
4 to the second argument of (G A (BETA B)) in frame 5, it used both
G2EQ1-IMPLIES-FEQ-G-2 and G2EQ2-IMPLIES-FEQ-G-2 to derive the
geneqv (G2EQ2 G2EQ1). Then, when it attempted to apply RULE, whose
equivalence relation is G2EQ1!, it passed the refinement test because
G2EQ1! refines G2EQ1, which is one of the equivalences listed in
the geneqv.
When we proceed from the break, the proof completes successfully.
But now imagine that we had failed to prove (DEFREFINEMENT G2EQ1!
G2EQ1). The thm command above would have caused this break:
(1 Breaking (:REWRITE RULE) on (BETA B):
The equivalence relation, G2EQ1!, of this rule is not a refinement
of the current geneqv, (G2EQ2 G2EQ1). Use :path or :path+ to see how
the geneqv evolved. See :DOC refinement-failure for advice about how
to deal with this kind of problem.
1 ACL2 >
The break header explains the problem: the rewriter does not know that
G2EQ1! refines G2EQ1 or G2EQ2. Of course, we do know
that and the fix is simply to prove the ``forgotten'' defrefinement.
On the other hand, suppose we had proved the defrefinement but had
forgotten to prove that FEQ is maintained on a call of G when
G2EQ1 is maintained on the 2nd argument of G, i.e., (DEFCONG
G2EQ1 FEQ (G X Y) 2), aka G2EQ1-IMPLIES-FEQ-G-2. Then the thm
command would produce the following break.
(1 Breaking (:REWRITE RULE) on (BETA B):
The equivalence relation, G2EQ1!, of this rule is not a refinement
of the current geneqv, (G2EQ2). Use :path or :path+ to see how the
geneqv evolved. See :DOC refinement-failure for advice about how to
deal with this kind of problem.
Note that the geneqv is printed in its simplest form, as a list of
equivalence relation names; in this case only one name is included:
G2EQ2. Of course, if we believed G2EQ1! does refine G2EQ2, it
would suffice to prove the corresponding refinement rule. But let's suppose
we know G2EQ1! doesn't refine G2EQ2. Instead, we know G2EQ1!
refines G2EQ1, which is not in the geneqv. Our problem then is to
arrange for G2EQ1 to be in the geneqv. Look at the path that got us
here.
1 ACL2 >:path+
1. Simplifying the clause
((P (F (G A (BETA B)))))
2. Rewriting (to simplify) the atom of the first literal,
(P (F (G A (BETA B)))),
Geneqv: (IFF)
3. Rewriting (to simplify) the first argument,
(F (G A (BETA B))),
Geneqv: ((PEQ PEQ-IMPLIES-IFF-P-1))
4. Rewriting (to simplify) the first argument,
(G A (BETA B)),
Geneqv: ((FEQ FEQ-IMPLIES-PEQ-F-1))
5. Rewriting (to simplify) the second argument,
(BETA B),
Geneqv: ((G2EQ2 G2EQ2-IMPLIES-FEQ-G-2))
6. Attempting to apply (:REWRITE RULE) to
(BETA B)
Preserving: G2EQ1!
Geneqv: ((G2EQ2 G2EQ2-IMPLIES-FEQ-G-2))
1 ACL2 >
In frame 4 we are to maintain FEQ on a call of G. In frame 5 we
are rewriting the second argument of G and used
G2EQ2-IMPLIES-FEQ-G-2 to derive the new geneqv containing G2EQ2.
We could get G2EQ1 into that new geneqv is only we had a congruence rule
that says FEQ is maintained on G when rewriting the second argument
of G maintaining G2EQ1. That's just the ``forgotten'' (DEFCONG
G2EQ1 FEQ (G X Y) 2). Of course we could alternatively have chosen to
prove (DEFCONG G2EQ1! FEQ (G X Y) 2), but it is generally better to
prove the strongest congruence rules we know.
Finally, as documented in refinement and congruence,
refinement and congruence rules are not (always) tracked and usually do
not show up in the summary printed at the end of proof attempts.
The decision not to track every use of these rules was made to improve
prover efficiency.
