Some basic facts about the ACL2 rewriter

The ACL2 rewriter is technically part of the simplifier, but in
this documentation we often conflate the two and say things like ``the
conclusion simplifies to

But to understand how `rewrite`, `rewrite-quoted-constant`, `linear`, `congruence`,

In ACL2, the goals you see printed in proof output are represented internally as clauses. See clause.

The job of the simplifier is to simplify a clause, returning a set of
clauses whose conjunction is propositionally equivalent to the input clause.
The most desirable output set is the empty set, because the conjunction over
the empty set is

Note that if you are trying to simplify the clause

The simplifier works by first generating several data structures, here
called the ``context,'' which codify governing assumptions available for the
rewriting of each literal. These data structures include the type-alist and linear-arithmetic data base. They are built using
various rules derived from previously proved lemmas, including `type-prescription`, `forward-chaining`, and `linear`
rules. It then calls the rewriter successively on each literal passing it
the appropriate context and stipulating that the result of the rewriting must
be propositionally equivalent to the input. The rewriter returns a suitable
term. If the result is the unchanged, the simplifier just moves on to the
next literal. If the result contains no

The job of the rewriter is to take a term, some context, and an equivalence relation, and return a ``simpler'' term that is equivalent to the input term under the assumptions in the context.

The rewriter works by exploring the term, possibly changing the context and the equivalence relation as appropriate for the subterms it rewrites.

- If the term is a variable, the rewriter just returns it (unless the
context tells it something interesting about that variable, such as that the
variable is equal to
nil ). Sometimes you might wish that the value of a bound variable be rewritten, usually because the value found on the alist was rewritten under a different equivalence relation than the variable is now being used. Seedouble-rewrite . - If the term is a quoted constant, the rewriter tries to apply
: `rewrite-quoted-constant`rules to that constant. - If the term is
(IF a b c) , it rewrites the test,a , under the equivalence relationIFF to get some (possibly) new term,a' . Ifa' isnil or is obviously different fromnil (likeT ), the rewriter replaces theIF -term byb orc , appropriately, and rewrites that. If on the other hand, the rewriter can't decide whethera' isnil or not, it rewritesb tob' in an extended context in whicha' is assumed non-nil and rewritesc toc' in an extended context in whicha' isnil . In rewriting both branches it preserves the outer equivalence relation -- the one to be maintained while rewriting theIF -term. Then the rewriter returns(IF a' b' c '). - If the term is a call of an arithmetic inequality, like
(< a b) , the rewriter rewritesa andb and then considers whether the context allows it deduce the truth or falsity of the inequality using a linear-arithmetic decision procedure. The decision procedure, which is complete for linear inequalities over the rationals, uses heuristics to decide many integer cases, to select the order in which inequalities are combined to eliminate variables, and to handle some non-linear-arithmetic problems. - If the term is a call of a function symbol,
fn , on some argument terms,a1 , ...,an , the rewriter rewrites each argument,ai toai' . For each argument the rewriter uses known: `congruence`rules to determine which equivalence relations can be used to rewrite terms in that argument position so as to maintain the outer equivalence. Then, having transformed(fn a1 ... an) to(fn a1' ... an ') the rewriter tries to apply: `rewrite`rules to that transformed term, called the ``target.''. - Among the rewrite rules generally available for
(fn a1' ... an ') is the definition offn itself. The rewriter considers ``expanding'' the call, i.e., replacing it by the body offn after substituting theai' for the formal variables, if the definition is enabled, and then rewriting that. But heuristics are used to prevent the indefinite expansion of recursive definitions.

For an elementary tutorial on the application of a

(implies (and hyp1 ... hypk) (equiv lhs rhs))

where

If the rule in question is enabled and its

**Matching**: Technically, ACL2 uses a restriction of ordinary
first-order unification -- the restriction being that only variables in the
pattern (here the

However, our pattern matcher knows some things about the structure of
quoted constants. For example, the pattern

ACL2 !>(one-way-unify '(cons x y) ''(A B C)) (T ((Y QUOTE (B C)) (X QUOTE A)))

Note the quote marks in our input. Since

((y . '(B C)) (x . 'A))

i.e.,

Below are some other examples, but we've re-displayed the substitutions.

ACL2 !>(one-way-unify '(coerce x 'string) ''"Hello!") (T ((x . (#H #e #l #l #o #!)))) ACL2 !>(one-way-unify '(intern-in-package-of-symbol x y) ''ACL2::TEMP) (T ((y . 'TEMP) (x . '"TEMP"))) ACL2 !>(one-way-unify '(binary-+ '3 x) ''7) (T ((X . '4))) ACL2 !>(one-way-unify '(unary-- x) ''-7) (T ((X QUOTE 7))) ACL2 !>(one-way-unify '(unary-- x) ''7) (NIL NIL) ACL2 !>(one-way-unify '(binary-* '2 y) ''8) (T ((Y QUOTE 4))) ACL2 !>(one-way-unify '(binary-* x y) ''8) (NIL NIL)

Note that the pattern matching algorithm is incomplete on quoted
constants! For example, it fails to match

**Relieving the Hypotheses**: The hypotheses of a rewrite rule are
relieved one at a time starting with the left-most one. The basic strategy
is just to rewrite each hypothesis, assuming the current context and if

- Free variables: It is possible that a hypothesis contains variables that
are not bound by the substitution generated by the match. We call these
``free variables'' and the system tries to bind them to make the instantiated
hypothesis appear among the contextual assumptions. New bindings are
accumulated as hypotheses are relieved. It is possible to find multiple
successful substitutions, some possibly filtered out by subsequent
hypotheses. See
free-variables and the documentation topics it cites. - Pragmas: It is possible to mark a hypothesis so that it is temporarily
assumed true so that the rewrite rule can be applied. This essentially
spawns another subgoal to prove the hypothesis and thus brings the full power
of the prover (not just the rewriter) to bear on the hypothesis. See
`force`and`case-split`. It is also possible to include hypotheses that are logically always true but which cause the attempt to apply the rule to fail if a certain user-specified compuation so indicates. This can be used to restrict the application of a rule to certain syntactic situations. Seesyntaxp .

**Replacement**: Before the target is replaced by the rewritten
`loop-stopper`. Otherwise, if the hypotheses are
relieved (or assumed), the rewriter rewrites `if`s'' (see too-many-ifs. The latter
check is used to prevent unmanageable case explosions. (In general, the
number of cases rises exponentially with the number of