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
(include-book "clause-processors/autohide" :dir :system) (local (autohide member-equal subsep-equal)) (defthm my-thm1 ...) (defthm my-thm2 ...)
Advice: always localize
(local (autohide member-equal)) (local (autohide subsetp-equal)) (defthm my-thm1 ...) (defthm my-thm2 ...)
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.