ACL2-PC::=

(atomic macro) 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.

Notes: (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.