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.