attempt an equality (or equivalence) substitution
Major Section: PROOF-CHECKER-COMMANDS
Examples:
= -- replace the current subterm by a term equated to it in
one of the hypotheses (if such a term exists)
(= x) -- replace the current subterm by x, assuming that the prover
can show that they are equal
(= (+ x y) z)
-- replace the term (+ x y) by the term z inside the current
subterm, assuming that the prover can prove
(equal (+ x y) z) from the current top-level hypotheses
or that this term or (equal z (+ x y)) is among the
current top-level hypotheses or the current governors
(= & z)
-- exactly the same as above, if (+ x y) is the current
subterm
(= (+ x y) z :hints :none)
-- same as (= (+ x y) z), except that a new subgoal is
created with the current goal's hypotheses and governors
as its top-level hypotheses and (equal (+ x y) z) as its
conclusion
(= (+ x y) z 0)
-- exactly the same as immediately above
(= (p x)
(p y)
:equiv iff
:otf-flg t
:hints (("Subgoal 2" :BY FOO) ("Subgoal 1" :use bar)))
-- same as (= (+ x y) z), except that the prover uses
the indicated values for otf-flg and hints, and only
propositional (iff) equivalence is used (however, it
must be that only propositional equivalence matters at
the current subterm)
General Form:
(= &optional x y &rest keyword-args)
If terms x and y are supplied, then replace x by y inside the
current subterm if they are ``known'' to be ``equal''. Here
``known'' means the following: the prover is called as in the prove
command (using keyword-args) to prove (equal x y), except that a
keyword argument :equiv is allowed, in which case (equiv x y) is
proved instead, where equiv is that argument. (See below for how
governors are handled.)Actually, keyword-args is either a single non-keyword or is a list
of the form ((kw-1 x-1) ... (kw-n x-n)), where each kw-i is one of
the keywords :equiv, :otf-flg, :hints. Here :equiv defaults to
equal if the argument is not supplied or is nil, and otherwise
should be the name of an ACL2 equivalence relation. :Otf-flg and
:hints give directives to the prover, as explained above and in the
documentation for the prove command; however, no prover call is made
if :hints is a non-nil atom or if keyword-args is a single
non-keyword (more on this below).
Remarks on defaults
(1) If there is only one argument, say a, then x defaults to the
current subterm, in the sense that x is taken to be the current
subterm and y is taken to be a.
(2) If there are at least two arguments, then x may be the symbol
&, which then represents the current subterm. Thus, (= a) is
equivalent to (= & a). (Obscure point: actually, & can be in any
package, except the keyword package.)
(3) If there are no arguments, then we look for a top-level
hypothesis or a governor of the form (equal c u) or (equal u c),
where c is the current subterm. In that case we replace the current
subterm by u.
As with the prove command, we allow goals to be given ``bye''s in
the proof, which may be generated by a :hints keyword argument in
keyword-args. These result in the creation of new subgoals.
A proof is attempted unless the :hints argument is a non-nil
atom other than :none, or unless there is one element of
keyword-args and it is not a keyword. In that case, if there are
any hypotheses in the current goal, then what is attempted is a
proof of the implication whose antecedent is the conjunction of the
current hypotheses and governors and whose conclusion is the
appropriate equal term.
Remarks: (1) It is allowed to use abbreviations in the hints.
(2) The keyword :none has the special role as a value of
:hints that is shown clearly in an example above. (3) If there
are governors, then the new subgoal has as additional hypotheses the
current governors.
