• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
    • Gl
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Fgl
    • Removable-runes
    • Efficiency
    • Rewrite-bounds
    • Bash
    • Def-dag-measure
    • Bdd
    • Remove-hyps
    • Contextual-rewriting
    • Simp
    • Rewrite$-hyps
    • Bash-term-to-dnf
    • Use-trivial-ancestors-check
    • Minimal-runes
    • Clause-processor-tools
    • Fn-is-body
    • Without-subsumption
    • Rewrite-equiv-hint
    • Def-bounds
    • Rewrite$-context
    • Try-gl-concls
    • Hint-utils
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Proof-automation

Rewrite$

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)
     (:REWRITE CDR-CONS)
     (:REWRITE CAR-CONS)
     (:FAKE-RUNE-FOR-TYPE-SET NIL)))
ACL2 !>

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 kestrel/utilities/runes.lisp.

Other simple examples may be found in community book books/demos/rewrite-dollar-input.lsp.

Return values

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 extract-and-clausify-assumptions.)

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.

General Form

All arguments of rewrite$ except the first are keyword arguments, hence are optional, with appropriate defaults. All are evaluated.

 (rewrite$ term

; 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 translated.

IMPORTANT: The keyword options, discussed below according to the groups above, are all evaluated. So for example:

; Correct
(rewrite$ '(cons a (cdr x)) :alist '((a . (car x))) :hyps '((consp x)))

; WRONG!
(rewrite$ '(cons a (cdr x)) :alist ((a . (car x))) :hyps ((consp x)))

Basic options

• :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 assumptions.
  • 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 rewrite$.

Advanced options

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,
  and pot-lst.
If the alist is empty and the term didn't change, exit the loop.

Related tools

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 linear-arithmetic information.

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 books/misc/expander.lisp.