Lemma-instance
An object denoting an instance of a theorem
Lemma instances are the objects one provides via :use and
:by hints to bring to the theorem prover's attention some
previously proved or easily provable fact. A typical use of the :use
hint is given below. The value specified is a list of five lemma
instances.
:use (reverse-reverse
(:type-prescription app)
(:instance assoc-of-app
(x a) (y b) (z c))
(:functional-instance p-f
(p consp) (f flatten))
(:instance (:theorem (equal x x))
(x (flatten a))))
Observe that an event name can be a lemma instance. The :use hint
allows a single lemma instance to be provided in lieu of a list, as in:
:use reverse-reverse
or
:use (:instance assoc-of-app (x a) (y b) (z c))
A lemma instance denotes a formula which is either known to be a theorem or
which must be proved to be a theorem before it can be used. To use a lemma
instance in a particular subgoal, the theorem prover adds the formula as a
hypothesis to the subgoal before the normal theorem proving heuristics are
applied.
A lemma instance, or lmi, is of one of the following forms:
(1) name, where name names a previously proved theorem, axiom, or
definition and denotes the formula (theorem) of that name.
(2) rune, where rune is a rune (see rune) denoting
the :corollary justifying the rule named by the rune.
(3) (:theorem term), where term is any term alleged to be a
theorem. Such a lemma instance denotes the formula term. But before
using such a lemma instance the system will undertake to prove term.
(4) (:instance lmi (v1 t1) ... (vn tn)), where lmi is recursively
a lemma instance, the vi's are distinct variables, and the ti's are
terms. Such a lemma instance denotes the formula obtained by instantiating
the formula F denoted by lmi, normally by replacing each vi by
ti in F and requiring that each vi must be bound in F.
There are two exceptions. If the keyword :extra-bindings-ok is inserted
immediately after the lemma instance in order to remove that requirement, as
follows, then that requirement is ignored: (:instance
lmi :extra-bindings-ok (v1 t1) ... (vn tn)). Otherwise there is the
following exception pertaining to packages: if one or more variables
vi do not occur in F, but for each such vi exactly one variable
v with the same symbol-name as vi occurs in F and no
other vj with the same symbol-name as v is bound in the
substitution, then the pair (vi ti) is replaced by the pair (v ti)
in the substitution.
(5) (:functional-instance lmi (f1 g1) ... (fn gn)), where lmi is
recursively a lemma instance and each fi is an ``instantiable'' function
symbol of arity ni and gi is a function symbol, a macro alias for a
function symbol gi' (see macro-aliases-table) in which case we
treat gi as gi', or a pseudo-lambda expression of arity ni. An
instantiable function symbol is any defined or constrained function symbol
except the primitives not, member, implies, and o<, and a few others, as listed by the constant
*non-instantiable-primitives*. These are built-in in such a way that we
cannot recover the constraints on them. (Special case: a function
introduced in the :partial-theory of a dependent clause-processor is not
instantiable; see define-trusted-clause-processor.) A pseudo-lambda
expression is an expression of the form (lambda (v1 ... vn) body) where
the vi are distinct variable symbols and body is any term. No a
priori relation is imposed between the vi and the variables of
body, i.e., body may ignore some vi's and may contain ``free''
variables. However, we do not permit v to occur freely in body if
the functional substitution is to be applied to any formula (lmi or the
constraints to be satisfied) in a way that inserts v into the
scope of a binding of v by let or mv-let (or, lambda). If you happen to violate this restriction, an informative error
message will be printed. That message will list for you the potentially
illegal choices for v in the context in which the functional substitution
is offered. A :functional-instance lemma instance denotes the formula
obtained by functionally instantiating the formula denoted by lmi,
replacing fi by gi. However, before such a lemma instance can be
used, the system will generate proof obligations arising from the replacement
of the fi's by the gi's in constraints that ``support'' the lemma to
be functionally instantiated; see constraint. One might expect that if
the same instantiated constraint were generated on behalf of several events,
then each of those instances would have to be proved. However, for the sake
of efficiency, ACL2 stores the fact that such an instantiated constraint has
been proved, unless the proof was done inside an encapsulate event
that either has a non-empty signature list or is ``empty'' (stores
no events), and then avoids re-proving that constraint in future events.
See functional-instantiation-example for an example of the use of
:functional-instance (so-called ``functional instantiation'').
Note that ACL2(r) (see real) imposes additional requirements for
functional instantiation. See functional-instantiation-in-ACL2r.
(6) (:termination-theorem name) or (:termination-theorem! name),
where name is a function symbol in logic mode. Such a lemma
instance denotes the termination theorem previously proved for name,
possibly modified as discussed in the next paragraph. If no such theorem
exists — for example, if the definition of name is not recursive
— then the lemma instance is illegal in the case of
:termination-theorem, but denotes T in the case of
:termination-theorem!. If name is defined as part of a
mutually-recursive clique of definitions (see mutual-recursion), then
the lemma instance refers to the termination theorem proved for the entire
clique. See termination-theorem-example and see tthm.
Consider the application of :termination-theorem f while attempting to
prove the termination theorem for a function, g. For now suppose that
neither f nor g is defined using mutual-recursion. Suppose
that f and g have the same number of formal parameters. Then every
call of f in the termination theorem for f will be replaced by a
call of g on the same arguments (except, recursively, f is also
replaced by g in those arguments). The analogous replacement also takes
place for mutually recursive definitions, as follows. In the case that f
was introduced with (mutual-recursion (defun f1 ...) ... (defun fk ...))
and similarly g is being introduced with (mutual-recursion (defun g1
...) ... (defun gk ...)), where for each i from 1 to k the
number of formal parameters is the same for fi and gi, then the
functional substitution ((f1 . g1) ... (fk . gk)) is applied to the
termination theorem for the fi. (Logical justification in a nutshell:
the termination proof for the fi took place before adding their
definitional equations to the current theory, where the fi were thus
stubs with no axioms.) Note that unlike normal functional-instantiation, here there is no proof obligation. However, the
restriction applies from (5) above that the functions fi are
instantiable; when that fails, then the replacement of each fi by gi
will not take place.
Finally, note that an optional second argument to :termination-theorem
specifies an explicit functional substitution ((f1 g1) ... (fn gn)),
which is to be applied to the termination theorem for f. If that
argument is supplied, then there will be no attempt to derive a functional
substitution automatically, as described in the preceding paragraph.
(7) (:guard-theorem name) or (:guard-theorem name simplify),
where name is a guard-verified function symbol (hence, in
particular, is in logic mode). Such a lemma instance denotes the guard
theorem previously proved for name, where by default simplify is
:limited, which enables certain simplifications as documented elsewhere;
see gthm. Otherwise simplify should be nil, to avoid all
such simplification. If name is defined as part of a mutually-recursive
clique of definitions (see mutual-recursion), then the lemma instance
refers to the guard theorem proved for the entire clique. See guard-theorem-example and see gthm.
Obscure case for definitions. If the lemma instance refers to a
:definition rune, then it refers to the corollary formula
of that rune, which can be a normalized (simplified) form of the definition
body; see normalize. However, if the hint is a :by hint and the
lemma instance is based on a name (i.e., a symbol), rather than a rune, then
the formula is the original formula of the event, as shown by :pe, rather than the normalized version, as shown by :pf. This
is as one would expect: If you supply the name of an event, you expect it to
refer to the original event. For :use hints we use the simplified (normalized) form instead, which is reasonable since one would expect
simplification during the proof that re-traces the normalization done at the
time the rule was created.
We conclude with remarks on (6) and (7). The termination theorem actually
used is an unsimplified version of what was originally proved for the
indicated function; the guard theorem is, by default, partially simplified.
That is: while in general, the termination theorem is simplified before being
given to the prover, nevertheless the unsimplified theorem is what is actually
used for :termination-theorem lemma instances; for :guard-theorem,
some simplification is done that is independent of the theory, by using a form
of ``subsumption'' to eliminate redundancy and by deleting tautologies as well
as instances of built-in-clause rules that come with ACL2. Also see
guard-formula-utilities and guard-simplification. Moreover, the
:measure-debug and :guard-debug keywords for xargs are ignored when generating the termination or guard theorem. You can
see the termination or guard theorem for an existing function symbol FN
by evaluating the form (termination-theorem 'FN (w state)) or
(guard-theorem 'FN simplify guard-debug (w state) state), respectively.
In the former case, failure is indicated by a result of the form (FAILED
. msg), where msg is a message suitable for fmt; see msg.
Also see make-termination-theorem.
Why do we avoid simplification for :termination-theorem, as described
in the preceding paragraph? The reason is that it could in principle
strengthen the theorem, which is sound when admitting the original function
but not for lemma instances. Future work might try to allow simplification at
lemma-instance time, by ensuring that simplification never strengthens the
theorem. Alternatively, simplification might be checked for each usage to be
equivalence-preserving by defining a suitable macro based on make-event. For now, by avoiding simplification we guarantee that the
theorem we are using is truly a theorem. The theorem being used might not be
exactly the theorem originally proved, for example because of the use of case-split-limitations, which depends on the current logical world;
but we expect the two theorems to be logically equivalent.
Subtopics
- Termination-theorem-example
- How to use a previously-proved measure theorem
- Guard-theorem-example
- How to use a previously-proved guard theorem
- Guard-theorem
- Use a previously-proved guard theorem
- Termination-theorem
- Use a (functional instance of a) previously-proved measure theorem
