Rewrite-quoted-constant
Make a rule to rewrite a quoted constant
See rule-classes for a general discussion of rule classes,
including how they are used to build rules from formulas and a discussion of
the various keywords in a rule class description.
Note: It is helpful to know some basic facts about the ACL2 rewriter; see
random-remarks-on-rewriting.
Example Forms:
(defthm lambda-id
(fn-equal '(lambda (x) x) 'identity)
:rule-classes :rewrite-quoted-constant)
(defthm set-normalizer
(set-equalp (drop-duplicates-and-sort x) x)
:rule-classes :rewrite-quoted-constant)
(defthm lambda-id-generalized
(implies (symbolp v)
(fn-equal (list 'lambda (list v) v)
'identity))
:rule-classes :rewrite-quoted-constant)
To be accepted with rule-class :rewrite-quoted-constant a conjecture
must have one of the following three
General Forms:
(IMPLIES hyps (equiv 'const1 'const2)) ; [1]
(IMPLIES hyps (equiv (fn var) var)) ; [2]
(IMPLIES hyps (equiv (constructor ...) rhs)) ; [3]
where
- hyps is a term (typically a conjunction) and may include force and syntaxp hypotheses with the usual semantics,
- equiv is a known equivalence relation and, in the case of
[1] and [2], equiv is not EQUAL,
- var, in form [2], is a variable symbol, and
- constructor, in form [3], is an explicit value ``constructor''
function symbol listed in *one-way-unify1-implicit-fns*. The list just
mentioned includes cons, which can be used to match non-empty list
constants, coerce, which can match string constants,
intern-in-package-of-symbol, which can match symbol constants, and
binary-+ and certain other arithmetic primitives which can match numeric
constants. See random-remarks-on-rewriting for some examples.
If a rule meets the criteria for both a form [2] rule and a form
[3] rule, then it is considered to be a form [2] rule.
The function, fn, in a form [2] rule is called the
``normalizer.'' We explain this terminology as we discuss how such rules are
used.
The :rewrite-quoted-constant rule-class is permitted to specify a
:corollary and/or a :loop-stopper, with the usual syntax and
meaning. See :rule-classes. Note that for forms [1] and
[2] above a :loop-stopper is probably irrelevant as the forms
do not usually contain multiple variable symbols.
Once a :rewrite-quoted-constant rule is proved and stored, the
rewriter behaves as follows. When a quoted constant is encountered as the
target term to be rewritten, the rewriter considers each enabled
:rewrite-quoted-constant rule (most-recent first), looking for those
whose equiv refines (see :refinement) the equivalence
relation being maintained by the rewriter for the given occurrence of the
target. The rewriter tries to apply each such rule in turn (as described
below) and replaces the target by the rewritten result of the first
applicable rule.
A rule applies if the ``pattern'' (see below) in the conclusion
``matches'' the quoted constant and the hyps can be relieved in the
usual sense, including the treatment of free variables, pragmatic directives
like force and syntaxp, and heuristics such as those
controlled by any :loop-stopper options in the rule-class or
:restrict hints. If these conditions are met, the quoted
constant is replaced by the ``result.'' But the exact meanings of
``pattern,'' ``match'' and ``result'', here, are a little different from their
meanings for ordinary :rewrite rules and depend on which of the three
forms is being applied.
- A form [1] rule, whose conclusion is (equiv 'const1 'const2),
has 'const1 as its pattern and that pattern matches the target constant
'const only when const1 is exactly const. The result is
'const2. Note that it is impossible to prove a form [1] rule whose
equivalence is equal unless the two constants are identical, so we
disallow that case.
- A form [2] rule, whose conclusion is (equiv (fn var) var), is
most easily understood by swapping the roles of left- and right-hand sides of
its conclusion. Its pattern is the right-hand side, var, and its result
is derived from the left-hand side, (fn var). The reason we use the
form shown here is so that the same conjecture might also be used as an
ordinary :rewrite rule without forcing the user to type a
:corollary with the sides swapped. Since form [2] rules have a
variable as the pattern they will match any quoted constant, 'const, by
binding var to 'const. The result is the quoted constant, if any,
obtained by rewriting (fn var) under that binding of var. If that
rewrite does not result in a constant, no replacement is made, i.e., it is as
though the rule did not match. Note that it is pointless to prove a form
[2] rule whose equivalence is equal because it would replace a
quoted constant by itself, so we disallow that equivalence.
Intuitively, fn is a function that normalizes every member of the
equiv equivalence class: given a constant that is a member of the class
it returns its ``normal'' form. That is why we call fn the
``normalizer'' for equiv. However, you do not have to prove anything
like normality or canonicality; you just have to prove that fn returns a
member of the class. Having several different normalizers is possible but it
is best if only one is enabled at a time.
When var is bound to a constant, the rewriter will first try to reduce
(fn var) to a constant by simple evaluation. If that fails, it tries
using lemmas. If the normalizer or one of its subfunctions is disabled or is
non-executable or has a disabled executable counterpart the attempt to simply
evaluate (fn var) (under the assignment of 'const to var) may
fail. That is why full-blown rewriting of (fn var) is tried instead.
It might happen that evaluation fails but lemmas produce a constant.
The fact that form [2] rules are used ``backwards,'' with the roles
of the left- and right-hand sides swapped, has some ramifications worth
noting. First, you can also classify the same formula as a :rewrite
rule (but of course as such it won't rewrite quoted constants); as a
:rewrite rule it rewrites instances of (fn var) to the
corresponding instance of var. Second, when a
:rewrite-quoted-constant rule is added, the new rule is compared to old
rules for subsumption and warning messages are generated; however form
[2] rules are omitted from this subsumption check because their patterns
match every constant (in the equivalence class). Third, if you inspect a
form [2] rule with pr, it reports the actual syntax typed, e.g.,
the ``Lhs'' is (fn var) and the ``Rhs'' is var. But, if
you :monitor a form [2] rule and then interact with the
resulting break-rewrite you will see that the brr-commands
:lhs and :rhs report the swapped results. That is, in the break,
:lhs will be var and :rhs will be (fn var). This is
different from the display by pr because pr reports the actual
syntax but interactive breaks report how the rule is being used. We think
the interactive user, out of long habit, will type :lhs to see the
pattern being matched and we did not think it wise to add a special command
just to see the pattern in a form [2] rule. Fourth, if a form [2]
rule is mentioned in the report by pl the ``New term'' is reported to
be (fn 'const), however replacement of 'const occurs only if (fn
'const) reduces to a quoted constant by rewriting.
- A form [3] rule, whose conclusion is (equiv (constructor ...)
rhs), matches the constant 'const provided 'const is an instance
of (constructor ...) under some variable substitution s. We
illustrate cases where quoted constants are instances of ``constructor''
terms below and in random-remarks-on-rewriting. Note that form
[3] rules allow the equivalence relation to be equal. Use of
equal here could cause looping rewrites if the rhs reduces to a
constant. But we allow it because, as noted below, such a rule will also
permit you to rewrite a quoted constant into an equivalent term that is not a
quoted constant.
It is important to realize that form [1] and form [3] rules only
apply to the top-level of a quoted constant. We discuss this at length
because it can cause some confusion. The examples below are drawn from the
community book books/demos/rewrite-quoted-constant-examples. That book
introduces set-equalp as an equivalence relation and proves various
:rewrite-quoted-constant rules to rearrange the quoted constants
occurring in set-equalp contexts. Assume all the quoted constants
mentioned below occur in set-equalp contexts.
The form [1] rule (set-equalp 77 nil) will not cause '(1 2 3
. 77) to rewrite to '(1 2 3). Because ACL2 applications frequently
involve huge quoted list constants, we believe that making the rewriter
explore them down to the tips would be prohibitively expensive.
However, form [2] rules, of the general form (implies
hyps (equiv (fn var) var)), allow the normalizer to be applied to every
quoted constant occuring in a suitable equiv context. The normalizer
can then do a root-and-branch exploration of the constant to compute its
replacement.
For example, the rewrite-quoted-constants-examples book cited above
defines the normalizer (drop-dups-and-sort var) to coerce its argument
to a true-listp, eliminate duplicate elements, and sort the remaining
elements. It then proves the form [2] rule
(set-equalp (drop-dups-and-sort var) var). Now consider how this rule
is used when the rewriter encounters '(3 1 1 2 . 77) in a
set-equalp context. First, var is bound to 'const. Then, the
rewriter tries to relieve the instantiated hypotheses of the rule, if any.
The example rule here has no hypotheses. But you can provide some and
perhaps use them to prevent calling the normalizer on this particular
constant. Since var is bound to the constant 'const such
hypotheses can usually just be computed. Supposing the hypotheses are
relieved, the rewriter then rewrites (drop-dups-and-sort 'const). Under
the most common circumstance, this just causes your normalizer function, here
drop-dups-and-sort, to execute on the given constant. (If you have
verified the guard of the normalizer and 'const satisfies the guard,
then the execution is in the underlying raw Common Lisp.) In the most common
circumstance, the function will return an explicit constant. If that
returned value is indeed a constant (and different from 'const), the
rewriter replaces this occurrence of 'const by the returned value.
Otherwise the rule does not apply.
As noted earlier, form [3] rules are only applied at the top-level of
a quoted constant. For example, the rule (set-equalp (cons x y) (my-cons
x y)) will not cause '(1 2 3) to rewrite to (my-cons 1 (my-cons
2 (my-cons 3 nil))) in set-equalp contexts. Instead, it would produce
(my-cons 1 '(2 3)).
But since the rewriter will eventually be called on that term, and since
that term contains another top-level quoted constant, namely '(2 3), you
might expect the rule to eventually be used to replace '(2 3) by
(my-cons 2 '(3)). Indeed, that is what happens -- if you have proved
that set-equalp is a congruence for the second argument of
my-cons, maintaining set-equalp. However, for technical reasons
explained in comments in the book rewrite-quoted-constant-examples, each
rewrite occurs in a separate simplification step. So turning '(1 2 3)
into (my-cons 1 (my-cons 2 (my-cons 3 nil))) requires three
simplification steps. If the rule in question were (set-equalp (cons x
y) (cons x (double-rewrite y))) it would happen in one simplification step.
See double-rewrite and the examples in the book
rewrite-quoted-constant-examples.
Subtopics
- Random-remarks-on-rewriting
- Some basic facts about the ACL2 rewriter
