Major Section: MISCELLANEOUS
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. An :expand hint that removes all
calls of hide is:
:expand ((:free (x) (hide x)))The above hint can be particularly useful when ACL2's equality heuristics apply
hide to an equality after substituting it into the rest of the
goal, if that goal (or a subgoal of it) fails to be proved.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)
t))
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))
:hints
(("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.
