Rewrite a term
Rewrite$ is a macro that provides a convenient and flexible
interface to the ACL2 rewriter, which can be called programmatically.
The documentation below is divided into the following sections.
- An introductory example
- Return values
- General Form
- Basic options
- Hint options, each with default nil
- Advanced options
- Summary of algorithm
- Related tools
An introductory example
We begin with the following example of a call of rewrite$. The
keyword option :translate t is used because the first argument is not a
translated term, due to the call of the macro, append. We see
that the call of rewrite$ produces a 2-element list consisting of the
result, X, of rewriting the input term, together with a list of runes justifying that rewrite.
ACL2 !>(rewrite$ '(car (append (cons x y) z)) :translate t)
(X ((:DEFINITION BINARY-APPEND)
Notice the ``fake rune'' that is returned. Fake runes are easy to remove;
see for example the constant *fake-rune-alist* in the ACL2 sources or
function drop-fake-runes defined in community book
Other simple examples may be found in community book
A call (rewrite$ term ...) returns an error-triple, (mv erp
val state). Erp is non-nil when an error has occurred. Otherwise
val is of the form (rewritten-term runes . pairs) where pairs
is typically nil (as discussed further below) and:
- rewritten-term is the result of rewriting term as directed by
the other inputs; and
- runes is a list containing the runes that participated in the
rewriting of term to rewritten-term.
Because of forcing (see force), rewriting of the input term may
generate goals to be proved later, based on the forced hypotheses encountered
during rewriting that were not relieved at that time. We call these ``forced
assumptions''. If there are forced assumptions, then they are conjoined into
a single goal, which by default is the target of a separate call to the
prover, much like a call of thm. The return value pairs,
mentioned above, is nil exactly when there are no forced assumptions. We
say no more here about pairs, as it will suffice for most users to view
them solely as an indicator of forced assumptions. (Technical note for
advanced users: these are the pairs returned by ACL2 source function
There are many keyword arguments that control the rewriting process. One
of particular importance semantically is :alist. When this argument is
nil then the resulting rewritten term is provably equivalent (with
respect to the current ACL2 world) to the input term. Otherwise the
rewritten term is provably equivalent to the result of substituting the
specified alist into the input term. Another important keyword argument is
:hyps, which provides hypotheses under which the given term is to be
rewritten. The hypotheses themselves may be rewritten, using keyword argument
:rewrite-hyps. All keywords are documented below.
All arguments of rewrite$ except the first are keyword arguments,
hence are optional, with appropriate defaults. All are evaluated.
; Basic options (in alphabetical order):
:alist ; default nil
:ctx ; default 'rewrite$
:default-hints-p ; default t
:equiv ; default nil
:geneqv ; default nil
:hyps ; default nil
:must-rewrite ; default nil
:prove-forced-assumptions ; default t
:repeat ; default 1
:translate ; default nil
:untranslate ; default nil
; Hint options (in alphabetical order), each with default nil:
:backchain-limit-rw :expand :hands-off :in-theory
:no-thanks :nonlinearp :restrict :rw-cache-state
; Advanced options (in alphabetical order):
:obj ; default '?
:rrec ; default nil
:wrld ; default (w state)
Term should evaluate to a translated or untranslated term (see term) according to whether the value of :translate is nil or
non-nil, respectively. If :translate is nil (the default),
term should already be in translated form; otherwise term will be
IMPORTANT: The keyword options, discussed below according to the groups
above, are all evaluated. So for example:
(rewrite$ '(cons a (cdr x)) :alist '((a . (car x))) :hyps '((consp x)))
(rewrite$ '(cons a (cdr x)) :alist ((a . (car x))) :hyps ((consp x)))
- :alist (default nil)
is an association list mapping variables to terms, where each term is already
translated or else is untranslated according to whether the value of
:translate is nil or non-nil, respectively.
- :ctx (default 'rewrite$)
is a ``context'', such as the ctx argument of er.
- :default-hints-p (default t)
is non-nil when the
construction of hints for the rewriter call is to take into account the default-hints in the current world.
- :equiv and :geneqv (both with default nil)
specify the equivalence relation(s) to be preserved by (congruence-based) rewriting. It is illegal to specify a non-nil value
for more than one of these. Most users will prefer to use :equiv, which
should be a function symbol that is a known (to ACL2) equivalence relation.
The keyword option :geneqv is really only for those who know how
generated equivalence relations are represented in the ACL2 system.
- :hyps (default nil)
is a non-empty list of hypotheses under which rewriting takes place. Each
hypothesis is already translated or is untranslated according to whether the
value of :translate is nil or non-nil, respectively.
- :must-rewrite (default nil)
indicates, when its value is
non-nil, that the rewritten term must not be equal to the input term. It
is illegal to supply non-nil values for both :alist and
:must-rewrite, since it's usually not a sensible combination since at the
least, the alist will be substituted into the term.
- :prove-forced-assumptions (default t)
affects the proof of
the forced assumptions. It has the following legal values.
- t: prove the forced assumptions as mentioned above: a single prover
call to prove their conjunction.
- :same-hints: same as t, except generate the same :hints for
the prover call as are generated for the rewriting (from the eight hint
options discussed below).
- nil: do not attempt a proof of the forced assumptions, instead
returning a non-nil `pairs' value as discussed above.
- :none-forced: cause an error if there are any forced
- Otherwise, the value of :prove-forced-assumptions should be of the
form expected for the value of :hints supplied to defthm. For
example, the following might follow :prove-forced-assumptions in a call
of rewrite$: '(("Goal" :in-theory (enable reverse))).
- :repeat (default 1)
indicates how many times to call the rewriter. The value should be a positive
integer. If the value of :repeat is greater than 1, then the term
resulting from the first call is the input term for the second call, whose
result (if the value of :repeat is greater than 2) is the input term for
the third call, and so on. Note that the value of :alist is nil for
all calls after the first.
- :translate (default nil)
indicates whether or not terms in the input are to be translated or not (see
term for a discussed of ``translate''). If the value is nil then
translation will not take place, so the given terms — not only the input
term, but also terms in the cdr positions of the :alist and terms in
the :hyps — should already be in translated form. But if the value
is not nil, then all of these will be translated.
- :untranslate (default nil)
indicates whether the rewritten term will be given in translated or
untranslated form. It also specifies, when not nil, that certain error
messages display terms in untranslated form.
Hint options, each with default nil
The eight hint options displayed above are the same as discussed in the
documentation topic, hints. These are the only legal hint keywords for
The ``advanced options'' :obj, :wrld, and :rrec can
generally be ignored, so we say little about them here. :Obj is the
``obj'' argument of the rewriter, typically the symbol `?' but t
when backchaining. See rewrite$-hyps and its use in community book
books/kestrel/apt/simplify-defun-impl.lisp for how :rrec can avoid
repeating some computations. :Wrld should probably be left as its
default, which is the current ACL2 logical world.
Summary of algorithm
Here we provide a brief summary of the algorithm used by rewrite$.
Most users can probably skip this section.
Not surprisingly, the primary simplification technique used by
rewrite$ is rewriting. However, forward-chaining and linear-arithmetic are also used, as follows.
Initially, a function called rewrite$-setup is invoked on the given
:hyps to produce data structures that record facts from forward-chaining
— a so-called fc-pair-lst data structure — and linear
arithmetic — a so-called pot-lst data structure. (Exception: this
step is skipped if :rrec is supplied, since the value of that option
already contains such information.) Then we loop through :repeat
iterations, where each iteration proceeds according the the following
pseudocode. Note that the initial alist is given by :alist, but
subsequent alists are all nil.
Replace term with its rewrite with respect to the alist, hyps, fc-pair-lst,
If the alist is empty and the term didn't change, exit the loop.
See rewrite$-hyps for a tool that rewrites a list of hypotheses.
That tool does more than just apply rewriting directly to each hypothesis: it
also uses forward-chaining and linear-arithmetic derived from
the hypotheses. A related tool rewrite$-context, is similar but takes
an ``rrec'' input that already contains any forward-chaining and
For related tools see expander and easy-simplify-term. In
particular, code from the expander function tool2-fn served as a guide to
the coding of rewrite$; see community-book