Hide
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. 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.
Another common case, described below, is when hide is added by the
simplifier because an attempted execution of the term failed. In this case,
an :expand hint as described above will have no effect because the
execution will just fail again; the hide will be re-inserted; and the
hapless user will find themselves questioning their own sanity.
Hide terms are generally ignored not only by the rewriter but by other
ACL2 procedures, including the induction heuristics and (by default) removal
of guard-holders.
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 1 2 3) arises in a proof. Since the
arguments are all constants, ACL2 may 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.
Often that expression will use a call of comment, where (comment x
y) is logically just y, to tell you the problematic constrained
function, in this case by rewriting the original expression to the following;
see comment. (Near the end of this topic we discuss how to avoid the
call of comment.)
(hide (comment "Failed attempt to call constrained function CONSTRAINED-FN"
(another-fn 1 2 3)))
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 f
of no arguments in terms of a constrained function g, you may
often see (f) rewrite to:
(hide (comment "Failed attempt to call constrained function G"
(f))).
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 (comment ".." (another-fn 1 2
3))) mentioned above. Suppose that you can show that (another-fn 1 2
3) is (constrained-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 (comment "Failed attempt to call constrained function CONSTRAINED-FN"
(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 a hint to :expand that term.
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 (comment "Failed attempt to call constrained function CONSTRAINED-FN"
(another-fn 1 2 3)))
(constrained-fn 1 2 3))
:hints
(("Goal" :expand
(hide (comment "Failed attempt to call constrained function CONSTRAINED-FN"
(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.
Finally, note that you can avoid the generation of comment calls
inside the generated call of hide, as was the case through ACL2 Version
8.2, as follows.
(defattach-system ; generates (local (defattach ...))
hide-with-comment-p
constant-nil-function-arity-0)
After evaluation of this event, our running example (another-fn 1 2 3)
would generate (hide (another-fn 1 2 3)) rather than a term of the
form (hide (comment "..." (another-fn 1 2 3))).
In some cases such backward compatibility might also be achieved as
follows; also see guard-holders.
(defattach-system ; generates (local (defattach ...))
remove-guard-holders-blocked-by-hide-p
constant-nil-function-arity-0)
Function: hide
(defun hide (x)
(declare (xargs :guard t))
x)Subtopics
- Comment
- Variant of prog2$ to help debug evaluation failures during
proofs
- Autohide
- Tell ACL2 to automatically hide some terms.
