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.

To determine whether refinement failure is the cause of a rule's failure
to fire, enable break-rewrite with `monitor` with `rune` of the rule in
question. You might also specify a

(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 `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

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

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!

As illustrated in the discusson 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.,

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

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.

In the following discussion we introduce some functions that will allow us
to explore refinement failures. The experiements reported below are carried
out in the community book

We're going to attempt to prove

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
``

Imagine that we've proved two rewrite rules:

(DEFTHM RULE (G2EQ1! (BETA X) (GAMMA X))) (DEFTHM DONE (P (F (G X (GAMMA Y))))) which is actually stored as

(DEFTHM DONE (IFF (P (F (G X (GAMMA Y)))) T)) .

Clearly, our strategy to prove

However, the problem is that `congruence` rules. As you read them, remember that the term we'll be working
on is

IFF is maintained on a call ofP providedPEQ is maintained on the 1st argument ofP :*event*:(DEFCONG PEQ IFF (P X) 1) *name*:PEQ-IMPLIES-IFF-P-1

PEQ is maintained on a call ofF providedFEQ is maintained on the 1st argument ofF :*event*:(DEFCONG FEQ PEQ (F X) 1) *name*:FEQ-IMPLIES-PEQ-F-1

FEQ is maintained on a call ofG providedG2EQ1 is maintained on the 2nd argument ofG :FEQ is*also*maintained on a call ofG providedG2EQ2 is maintained on the 2nd argument ofG :

Note that there are two ways to maintain

G2EQ1! refinesG2EQ1 :*event*:(DEFREFINEMENT G2EQ1! G2EQ1) *name*:G2EQ1!-REFINES-G2EQ1

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 `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

(1 Breaking (:REWRITE RULE) on (BETA B): 1 ACL2 >

The subsequent

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.,

Notice that in frame 4, where the rewriter is working on

When we proceed from the break, the proof completes successfully.

But now imagine that we had failed to prove

(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
*we* do know
that and the fix is simply to prove the ``forgotten'' `defrefinement`.

On the other hand, suppose we had proved the

(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:

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

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.