ACL2-pc::equiv
(primitive)
attempt an equality (or congruence-based) substitution
Examples:
(equiv (* x y) 3) -- replace (* x y) by 3 everywhere inside the
current subterm, if their equality is among the
top-level hypotheses or the governors
(equiv x t iff) -- replace x by t everywhere inside the current
subterm, where only propositional equivalence
needs to be maintained at each occurrence of x
General form:
(equiv old new &optional relation)
Substitute new for old everywhere inside the current subterm,
provided that either (relation old new) or (relation new old) is
among the top-level hypotheses or the governors (possibly by way of
backchaining and/or refinement; see below). If relation is nil or
is not supplied, then it defaults to equal. If relation is not
equal (either explicitly or by default), then substitution of new
for old will only take place at occurrences for which relation is
among the equivalence relations being maintained without the use of
patterned-congruences. Also see acl2-pc::= for a much more
flexible command. Note that the equiv command fails if no substitution
is actually made.
Remark: No substitution takes place inside explicit values. So for
example, the instruction (equiv 3 x) will cause 3 to be replaced by
x if the current subterm is, say, (* 3 y), but not if the current
subterm is (* 4 y) even though 4 = (1+ 3).
The following remarks are quite technical and mostly describe a certain
weak form of ``backchaining'' that has been implemented for equiv in
order to support the = command. In fact neither the term (relation
old new) nor the term (relation new old) needs to be explicitly
among the current ``assumptions'', i.e., the top-level hypothesis or the
governors. Rather, there need only be such an assumption that ``tells us''
(r old new) or (r new old), for some equivalence relation
r that refines relation. Here, ``tells us'' means that
either one of the indicated terms is among those assumptions, or else there is
an assumption that is an implication whose conclusion is one of the indicated
terms and whose hypotheses (gathered up by appropriately flattening the first
argument of the implies term) are all among the current
assumptions.
