		Search-engine friendly clone of the ACL2 documentation.

Autohide

Tell ACL2 to automatically hide some terms.

Autohide is a computed hint (see computed-hints) that scans your proof goals for any uses of certain functions, and instructs ACL2 to wrap these calls in hide. This can be used as a way to tell ACL2 to ignore certain irrelevant terms so that proofs can be completed faster.

In particular, when I want to speed up a proof, I usually start by using accumulated-persistence to see if there are expensive rules that do not seem to be necessary. Often there are just a couple of expensive rules that can be disabled to achieve the bulk of the speedup.

But sometimes the list of rules to disable can get pretty long. Also, as the books you are relying upon are updated and extended with new rules, you might need to go back and additionally disable those rules to keep the proof fast. These are cases where autohide may be useful.

Instead of disabling specific rules, autohide tells ACL2 to wrap calls of certain functions in hide, effectively telling the prover to ignore those terms. If you know that, say, the member-equal terms you are going to encounter are really irrelevant to what you're trying to prove, then you might just autohide member-equal instead of trying to disable ten rules about it.

Basic Usage

(include-book "clause-processors/autohide" :dir :system)
(local (autohide member-equal subsep-equal))
(defthm my-thm1 ...)
(defthm my-thm2 ...)

The (autohide fn1 fn2 ...) macro expands to a table event and just records the names of the functions you want to autohide.

Advice: always localize autohide to avoid inadvertently hiding terms in other theorems.

Note that autohide is cumulative, so the above is equivalent to:

(local (autohide member-equal))
(local (autohide subsetp-equal))
(defthm my-thm1 ...)
(defthm my-thm2 ...)

Additional Functions

(autohide-summary) will tell you which functions are currently being automatically hidden;
(autohide-delete fn1 fn2) will remove specific functions from the autohide table.
(autohide-clear) will clear the table, basically turning off autohiding.

The autohide hint makes use of a verified clause-processor. If you need finer-grained control, e.g., you want to autohide certain functions only in specific subgoals, you may wish to disable the autohide hint and manually use the clause processor.