ACL2-pc::prove-guard
(macro)
Verify guards efficiently by using a previous guard theorem.
Example:
(prove-guard f1 (disable h))
Example of typical usage:
(defun f2 (x)
(declare
(xargs :guard
(g x)
:guard-hints
(("Goal"
:instructions
((prove-guard f1
(disable h)))))))
(f2-body x))
General Forms:
(prove-guard fn)
(prove-guard fn thy)
(prove-guard fn thy alt-thy)
(prove-guard fn thy alt-thy verbose)
where fn is a known function symbol and thy and alt-thy,
when supplied and non-nil, are theory expressions.
This proof-builder macro attempts to prove a theorem, typically a
guard proof obligation, by applying the hint :guard-theorem fn in
a carefully controlled, efficient manner (using the :fancy-use proof-builder macro). 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. In all of those
non-nil cases for the verbose input, a little message will be
started at the beginning of the second and third proof attempts, if any.
For a few small examples, see community book
kestrel/utilities/proof-builder-macros-tests.lisp.
For a way to use lemma instances other than guard theorems, see ACL2-pc::fancy-use.
Hacker tip: Invoke (trace$ acl2::pc-fancy-use-fn) to see the
proof-builder instruction created when invoking prove-guard.
