ACL2-pc::fancy-use
(macro)
Use one or more previously-proved theorems efficiently.
Examples:
(fancy-use (:instance my-thm (x a) (y b))
(disable h))
(fancy-use (foo (:instance bar (x a))))
Example of typical usage:
(defun f2 (x)
(declare
(xargs :hints
(("Goal"
:instructions
((fancy-use ((:instance my-thm (x a) (y b)))
(disable h)))))))
(f2-body x))
General Forms:
(fancy-use lmi+)
(fancy-use lmi+ thy)
(fancy-use lmi+ thy alt-thy)
(fancy-use lmi+ thy alt-thy verbose)
where lmi+ is a lemma-instance or a true list of
lemma-instances, that is, an object that can be supplied as a :use hint
(see hints); and thy and alt-thy, when supplied and
non-nil, are theory expressions.
This proof-builder macro attempts to prove a theorem by applying the
:use hint constructed from lmi+ in a carefully controlled, efficient
manner. This proof is attempted in the theory, thy, if supplied and
non-nil, else in the current-theory. If that proof fails, then a
single, ordinary prover call is made with that :use hint and in the
following theory: alt-thy if supplied and non-nil, else thy if
supplied and non-nil, else the current-theory. If the proof has
not yet succeeded and the original theory is not nil or
(current-theory :here), then a final proof is attempted in the same
careful manner as the first proof attempt.
Output is inhibited by default. However, if verbose is t then
output is as specified by the enclosing environment; and if verbose is
any other non-nil value, then output is mostly inhibited for that attempt
by use of the proof-builder command, :quiet.
For a few small examples, see community book
kestrel/utilities/proof-builder-macros-tests.lisp.
For convenient shortcuts in the case of using guard or termination
theorems, see ACL2-pc::prove-guard and ACL2-pc::prove-termination, respectively.
Hacker tip: Invoke (trace$ acl2::pc-fancy-use-fn) to see the
proof-builder instruction created when invoking fancy-use.
