hide a term from the rewriter

Hide is actually the identity function: (hide x) = x for all x. However, terms of the form (hide x) are ignored by the ACL2 rewriter, except when explicit :expand hints are given for such terms (see hints) or when rewrite rules explicitly about hide are available. Hide terms are also ignored by the induction heuristics.

Sometimes the ACL2 simplifier inserts hide terms into a proof attempt out of the blue, as it were. Why and what can you do about it? Suppose you have a constrained function, say constrained-fn, and you define another function, say another-fn, in terms of it, as in:

(defun another-fn (x y z)
  (if (big-hairy-test x y z)
      (constrained-fn x y z)
Suppose the term (another-fn 'a 'b 'c) arises in a proof. Since the arguments are all constants, ACL2 will try to reduce such a term to a constant by executing the definition of another-fn. However, after a possibly extensive computation (because of big-hairy-test) the execution fails because of the unevaluable call of constrained-fn. To avoid subsequent attempts to evaluate the term, ACL2 embeds it in a hide expression, i.e., rewrites it to (hide (another-fn 'a 'b 'c)).

You might think this rarely occurs since all the arguments of another-fn must be constants. You would be right except for one special case: if another-fn takes no arguments, i.e., is a constant function, then every call of it fits this case. Thus, if you define a function of no arguments in terms of a constrained function, you will often see (another-fn) rewrite to (hide (another-fn)).

We do not hide the term if the executable counterpart of the function is disabled -- because we do not try to evaluate it in the first place. Thus, to prevent the insertion of a hide term into the proof attempt, you can globally disable the executable counterpart of the offending defined function, e.g.,

(in-theory (disable (:executable-counterpart another-fn))).

It is conceivable that you cannot afford to do this: perhaps some calls of the offending function must be computed while others cannot be. One way to handle this situation is to leave the executable counterpart enabled, so that hide terms are introduced on the calls that cannot be computed, but prove explicit :rewrite rules for each of those hide terms. For example, suppose that in the proof of some theorem, thm, it is necessary to leave the executable counterpart of another-fn enabled but that the call (another-fn 1 2 3) arises in the proof and cannot be computed. Thus the proof attempt will introduce the term (hide (another-fn 1 2 3)). Suppose that you can show that (another-fn 1 2 3) is (contrained-fn 1 2 3) and that such a step is necessary to the proof. Unfortunately, proving the rewrite rule

(defthm thm-helper
  (equal (another-fn 1 2 3) (constrained-fn 1 2 3)))
would not help the proof of thm because the target term is hidden inside the hide. However,
(defthm thm-helper
  (equal (hide (another-fn 1 2 3)) (constrained-fn 1 2 3)))
would be applied in the proof of thm and is the rule you should prove.

Now to prove thm-helper you need to use the two ``tricks'' which have already been discussed. First, to eliminate the hide term in the proof of thm-helper you should include the hint :expand (hide (another-fn 1 2 3)). Second, to prevent the hide term from being reintroduced when the system tries and fails to evaluate (another-fn 1 2 3) you should include the hint :in-theory (disable (:executable-counterpart another-fn)). Thus, thm-helper will actually be:

(defthm thm-helper
  (equal (hide (another-fn 1 2 3)) (constrained-fn 1 2 3))
  (("Goal" :expand (hide (another-fn 1 2 3))
           :in-theory (disable (:executable-counterpart another-fn)))))

See eviscerate-hide-terms for how to affect the printing of hide terms.