Giving `apply$` permission to handle a user-defined function in proofs

The word ``warrant'' is defined in the Merriam-Webster dictionary as ``a commission or document giving authority to do something....''

The discussion below mentions the concept of `badge`s, which are
easily confused with warrants. See the discussion of **Badges versus
Warrants** at the top of `defbadge`. But roughly put, badges extend
the ACL2 syntax and warrants extend the proof theory. You'll need a badge
for

In the ACL2 proof theory, the functions `badge` and `apply$`
are undefined on user-defined function symbols. To be precise, when
presented with a user-defined function symbol, `defwarrant`.

In the ACL2 evaluation theory — a consistent extension of the proof
theory — all warrants issued by `badge`. However, for a `defwarrant`. This topic discusses warrants *per se*, their names, their
logical meaning, when they must be explicitly added as hypotheses to
conjectures, and their consistency.

If *fn* has a warrant, then the warrant is the term
`(apply$-warrant-`*fn*`)`, i.e., a call of the 0-ary
warrant function named, `apply$-warrant-`*fn*. That warrant
function name is admitted to the logic when

The warrant function for `defun-sk` because the warrant must specify the values
returned by `(apply$ 'fn args)` *for all possible* `badge` and `apply$` defer to two undefined
functions,

It is easiest to understand the above paragraph by looking at the
generated warrant function for `apply$` and whose badge is

(defun-sk apply$-warrant-foldr () (forall (args) (implies (tamep-functionp (cadr args)) (and (equal (badge-userfn 'FOLDR) '(APPLY$-BADGE 3 1 NIL :FN NIL)) (equal (apply$-userfn 'FOLDR args) (foldr (car args) (cadr args) (caddr args)))))) :constrain t)

Notice also that the tameness hypothesis involves the universally
quantified variable

(equal (badge-userfn 'FOLDR) '(APPLY$-BADGE 3 1 NIL :FN NIL))

and

(forall (args) (implies (tamep-functionp (cadr args)) (equal (apply$-userfn 'FOLDR args) (foldr (car args) (cadr args) (caddr args)))))

The first specifies the value of the undefined function used by `'FOLDR` and requires that the second element of

Finally, notice that the warrant function for

Now consider a function symbol that returns more than one result. Suppose
the badge of

(defun-sk apply$-warrant-add-and-subtract () (forall (args) (and (equal (badge-userfn 'add-and-subtract) '(APPLY$-BADGE 2 2 . T)) (equal (apply$ 'add-and-subtract args) (mv-list 2 (add-and-subtract (car args) (cadr args)))))))

Once *fn* it
proves two rewrite rules, conjoined under the name `apply$-`*fn*,
that ``lifts'' the warrant from the level of the two undefined functions to
the level of

(defthm apply$-foldr (and (implies (force (apply$-warrant-foldr)) (equal (badge 'FOLDR) '(APPLY$-BADGE 3 1 NIL :FN NIL))) (implies (and (force (apply$-warrant-foldr)) (tamep-functionp (car (cdr args)))) (equal (apply$ 'FOLDR args) (foldr (car args) (car (cdr args)) (car (cdr (cdr args))))))))

Observe that these rules say that if `force`d in both rules.

The effect of these rules is if either

If no warrant has been issued for

*There is no easy way to determine the warrants you'll need to make a
formula a theorem.* At first this seems to be a problem that could be solved
with a few rules of thumb and indeed, there are a few useful rules. But they
don't guarantee success.

*Rule 1.* One way to determine sufficient warrants for a formula to
be a theorem is to attempt to prove the formula without warrants and see the
checkpoints. This may have to be repeated to collect sufficient warrants and
can be frustrating. Furthermore, as illustrated further below, it can lead
to unnecessary warrants.

Most users attempt to anticipate what warrants are needed.

*Rule 2.* You will probably need a warrant hypothesis for every
user-defined function symbol mentioned in the fully translated term occupying
any slot of ilk `lambda$` expressions. In the latter case, you must consider every
user-defined function symbol in the *fully translated* body of the
`lambda$` expression. (If you've ignored our recommendations to use

But Rule 2 says ``probably need a warrant'' because whether you do or not depends on what you're proving. In the examples below, suppose we have carried out these events.

(include-book "projects/apply/top" :dir :system) (defun$ sq (x) (* x x))

and recall that `loop$` scion logically defined
as

(defun$ collect$ (fn lst) (if (endp lst) nil (cons (apply$ fn (list (car lst))) (collect$ fn (cdr lst)))))

No warrant is *really* needed to prove

(thm (equal (collect$ 'sq (append a b)) (append (collect$ 'sq a) (collect$ 'sq b))))

because it *could* be proved by appealing to the more general

(thm (equal (collect$ fn (append a b)) (append (collect$ fn a) (collect$ fn b))))

which makes clear that the properties of

But if you followed Rule 1 and just submitted

(thm (equal (collect$ 'sq (append a b)) (append (collect$ 'sq a) (collect$ 'sq b))))

the proof would fail with a checkpoint indicating that you need the
warrant for

To further dim our hopes for a simple way to identify warrants, consider

(defun$ square (i) (apply$ 'sq (list i)))

and then the proof of

(thm (equal (square i) (* i i)))

This theorem requires the warrant for

*Rule 3.* You may need warrants for any symbols used in

And then of course there is usual reason you need forgotten hypotheses: some lemma critical to your proof has that hypothesis.

For example, one could imagine proving

(defthm lemma (implies (apply$-warrant-sq) (equal (square x) (sq x))))

and then try to prove

(thm (equal (square x) (* x x)) :hints (("Goal" :in-theory (disable square))))

hoping the lemma would reduce

Returning to the first thing we said in this section, there is no easy sure-fire way to determine the warrants you'll need. It just depends on the functions you're manipulating, the cases explored in the proof, the hypotheses of crucial lemmas, etc. However, our experience is that it's not nearly so hard as we're suggesting here!

Basically you'll need a warrant for

There is another piece of good news perhaps best explained by example.

Imagine that you've defined and warranted your own versions of the
familiar list concatenation and list reverse functions under the names

(defun$ ap (x y) (if (endp x) y (cons (car x) (ap (cdr x) y)))) (defun$ rv (x) (if (endp x) nil (ap (rv (cdr x)) (list (car x)))))

What warrant(s) do you need to prove

(implies (true-listp x) (equal (apply$ 'rv (list (apply$ 'rv (list x)))) x))?

You clearly need the warrant for *all
evaluation* is carried out by

(defun$ rv1 (x) (if (endp x) nil (apply$ 'ap (list (rv1 (cdr x)) (list (car x))))))

and then tried to prove

(implies (true-listp x) (equal (apply$ 'rv1 (list (apply$ 'rv1 (list x)))) x))

we would indeed need warrants for both

But the warrant for the original

Because ```APPLY$-WARRANT-`*fn*'' is hard to remember, we
provide a macro for referring to the conjunction of warrant terms for a list
of functions.

General Form: (warrant fn1 fn2 ... fnk)

where each

(AND (FORCE (APPLY$-WARRANT-fn1)) (FORCE (APPLY$-WARRANT-fn2)) ... (FORCE (APPLY$-WARRANT-fnk)))

Because there are over 800 ACL2 primitives built into `lambda$` term, and
list all and only the function names that need warrants. For example, if the
body of the

The `force`s the warrants
because (a) we assume the only use of the macro is to add warrant hypotheses
to conjectures and (b) by forcing warrants agressively the prover ``almost
completes'' more proofs and enters a forcing round that highlights the need
to assume those warrants. When a rewrite rule, for example, is conditioned
on a warrant that is not forced (as would happen if you added the hyps

Adding warrants to formulas certainly restricts (weakens) the resulting
theorem since it is only applicable when the warrant is assumed. But an
important question to ponder is whether adding warrants can actually make a
formula vacuously valid? That is, can a set of warrants simply be
unsatisfiable so that any formula having that set of warrants among its
hypotheses is a theorem? Put another way, is there a model for the set of
all warrants introduced by `defwarrant`?

The answer is yes. This is discussed in ``Limited
Second-Order Functionality in a First-Order Setting'' by Matt Kaufmann
and J Strother Moore. For any set of functions warranted by *define*, under the standard ACL2 definitional
principle, versions of those functions (together with `defwarrant` and tameness. See the paper for a sketch of the proof and see the comment
titled `Essay on Admitting a Model for Apply$ and the Functions that Use
It` in the ACL2 source file