Encapsulate
Hide some events and/or constrain some functions
Encapsulate provides a way to execute a sequence of events and then hide some of the resulting effects. There are two kinds of
encapsulations: ``trivial'' and ``non-trivial''. We discuss these briefly
before providing detailed documentation.
A trivial encapsulation is an event of the following form.
(encapsulate
() ; nil here indicates "trivial"
<event-1>
...
<event-k>)
We use the term ``sub-events'' to refer to <event-1> through
<event-k>. Each sub-event <event-i> may be ``local'', that
is, of the form (local <event-i'>); the other sub-events are called
``non-local''. When this encapsulate form is submitted to ACL2, it is
processed in two passes. On the first pass, each sub-event is printed (by
default) and processed in sequence; admission of the encapsulate fails if
any <event-i> fails to be admitted. Then a second pass is made after
rolling back the logical world to what it was just before executing the
encapsulate form. In the second pass, only the non-local forms
<event-i> are evaluated, again in order, and proofs are skipped.
For example, the following trivial encapsulation exports a single event,
member-equal-reverse. The lemma member-revappend is used (as a
rewrite rule) to prove member-equal-reverse on the first pass, but
since member-revappend is local, it is ignored on the second
(final) pass.
(encapsulate
()
(local
(defthm member-revappend
(iff (member-equal a (revappend x y))
(or (member-equal a x)
(member-equal a y)))
:hints (("Goal" :induct (revappend x y)))))
(defthm member-equal-reverse
(iff (member-equal a (reverse x))
(member-equal a x))))
Of course, one might prefer to prove these events at the top level,
rather than within an encapsulation; but the point here is to illustrate that
you can have local events that do not become part of the logical
world. (Such a capability is also provided at the level of books; in particular, see include-book.)
Note that trivial encapsulates must introduce at least one sub-event, or
else they are treated as no-ops, with no effect on the logical world.
Consider the following example.
ACL2 !>(encapsulate nil (local (defun f (x) x)))
To verify that the encapsulated event correctly extends the current
theory we will evaluate it. The theory thus constructed is only ephemeral.
Encapsulated Event:
ACL2 !>>(LOCAL (DEFUN F (X) X))
Since F is non-recursive, its admission is trivial. We observe that
the type of F is described by the theorem (EQUAL (F X) X).
Summary
Form: ( DEFUN F ...)
Rules: NIL
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
F
End of Encapsulated Event.
ACL2 Observation in ( ENCAPSULATE NIL (LOCAL ...) ...): The submitted
encapsulate event has created no new ACL2 events, and thus is leaving
the ACL2 logical world unchanged. See :DOC encapsulate.
Summary
Form: ( ENCAPSULATE NIL (LOCAL ...) ...)
Rules: NIL
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:EMPTY-ENCAPSULATE
ACL2 !>
After the above evaluation, we are left in the world with which we
began. For example, if you evaluate the above form in the initial ACL2 world,
you can see the following both before and after that evaluation.
ACL2 !>:pbt 0
0:x(EXIT-BOOT-STRAP-MODE)
ACL2 !>
On the other hand, non-trivial encapsulations provide a way to introduce
axioms about new function symbols, without introducing inconsistency and
without introducing complete definitions. The following example illustrates
how that works.
(encapsulate
; The following list has a single signature, introducing a function foo of
; one argument that returns one value. (The list is non-empty, so we call
; this a "non-trivial" encapsulation.)
( ((foo *) => *) )
; Introduce a ``witness'' (example) for foo, marked as local so that
; it is not exported:
(local (defun foo (x) x))
; Introduce a non-local property to be exported:
(defthm foo-preserves-consp
(implies (consp x)
(consp (foo x))))
)
The form above introduces a new function symbol, foo, with the
indicated property and no definition. In fact, the output from ACL2 concludes
as follows.
The following constraint is associated with the function FOO:
(IMPLIES (CONSP X) (CONSP (FOO X)))
To understand this example, we consider how non-trivial encapsulations are
processed. The same two passes are made as for trivial encapsulations, and
the (local) definition of foo is ignored on the second pass, and
hence does not appear in the resulting ACL2 logical world. But before
the second pass, each signature is stored in the world. Thus,
when the theorem foo-preserves-consp is encountered in the second pass,
foo is a known function symbol with the indicated signature.
If any event fails while evaluating a call of encapsulate, the entire
encapsulate call is deemed to have failed, and the logical world
is rolled back to what it was immediately before the encapsulate
call.
We now provide detailed documentation. But discussion of redundancy for
encapsulate events may be found elsewhere; see redundant-encapsulate.
Other Examples:
(encapsulate (((an-element *) => *))
; The list of signatures above could also be written
; ((an-element (lst) t))
(local (defun an-element (lst)
(if (consp lst) (car lst) nil)))
(local (defthm member-equal-car
(implies (and lst (true-listp lst))
(member-equal (car lst) lst))))
(defthm thm1
(implies (null lst) (null (an-element lst))))
(defthm thm2
(implies (and (true-listp lst)
(not (null lst)))
(member-equal (an-element lst) lst))))
(encapsulate
() ; empty signature: no constrained functions indicated
(local (defthm hack
(implies (and (syntaxp (quotep x))
(syntaxp (quotep y)))
(equal (+ x y z)
(+ (+ x y) z)))))
(defthm nthcdr-add1-conditional
(implies (not (zp (1+ n)))
(equal (nthcdr (1+ n) x)
(nthcdr n (cdr x))))))
General Form:
(encapsulate (signature ... signature)
ev1
...
evn)
where each signature is a well-formed signature, each
signature describes a different function symbol, and each evi is an
embedded event form (see embedded-event-form). Also see signature, in particular for a discussion of how a signature can assign a
guard to a function symbol. There must be at least one evi. The
evi inside local special forms are called ``local'' events
below. Events that are not local are sometimes said to be
``exported'' by the encapsulation. We make the further restriction that no
defaxiom event may be introduced in the scope of an encapsulate
(not even by encapsulate or include-book events that are among
the evi). Furthermore, no non-local include-book event
is permitted in the scope of any encapsulate with a non-empty list of
signatures.
To be well-formed, an encapsulate event must have the properties that
each event in the body (including the local ones) can be successfully
executed in sequence and that in the resulting theory, each function mentioned
among the signatures was introduced via a local event and has
the signature listed. (A utility is provided to assist in debugging
failures of such execution; see redo-flat.) In addition, the body may
contain no ``local incompatibilities'' which, roughly stated, means that the
events that are not local must not syntactically require
symbols defined by local events, except for the functions
listed in the signatures. See local-incompatibility. Finally,
no non-local recursive definition in the body may involve in its
suggested induction scheme any function symbol listed among the signatures. See subversive-recursions.
Observe that if the signatures list is empty, the resulting
``trivial'' encapsulate may still be useful for deriving theorems to be
exported whose proofs require lemmas you prefer to hide (i.e., made local). Whether trivial or not (i.e., whether the signature is empty or
not), encapsulate exports the results of evaluating its non-local
events, but its local events are ignored for the
resulting logical world.
The result of a non-trivial encapsulate event is an extension of the
logic in which, roughly speaking, the functions listed in the signatures are constrained to have the signatures listed and to
satisfy the non-local theorems proved about them. In fact, other
functions introduced in the encapsulate event may be considered to have
``constraints'' as well. (See constraint for details, which are
only relevant to functional instantiation.) Since the constraints were
all theorems in the ``ephemeral'' or ``local'' theory, we are assured that the
extension produced by encapsulate is sound. In essence, the local definitions of the constrained functions are just ``witness functions''
that establish the consistency of the constraints. Because those
definitions are local, they are not present in the theory produced by
encapsulation. After a non-trivial encapsulate event is admitted,
theorems about the constrained function symbols may then be proved —
theorems whose proofs necessarily employ only the constraints. Thus,
those theorems may be later functionally instantiated, as with the
:functional-instance lemma instance (see lemma-instance), to
derive analogous theorems about different functions, provided the constraints
(see constraint) can be proved about the new functions.
The default-defun-mode for the first event in an encapsulation is
the default defun-mode ``outside'' the encapsulation. But since events changing the defun-mode are permitted within the body of an
encapsulate, the default defun-mode may be changed. However,
defun-mode changes occurring within the body of the encapsulate
are not exported. In particular, the ACL2-defaults-table after an
encapsulate is always the same as it was before the encapsulate,
even though the encapsulate body might contain defun-mode changing
events, :program and :logic. See defun-mode. More generally, after execution of an encapsulate event,
the value of ACL2-defaults-table is restored to what it was
immediately before that event was executed. See ACL2-defaults-table.
We make some remarks on guards and evaluation. Calls of functions
introduced in the signatures list cannot be evaluated in the ACL2
read-eval-print loop. See defattach for a way to overcome this
limitation. Moreover, any :guard supplied in the signature is
automatically associated in the world with its corresponding function
symbol, with no requirement beyond what is required for a legal signature other than that all of the guard's function symbols are in
:logic mode with their guards verified. In particular,
there need not be any relationship between a guard in a signature and the
guard in a local witness function. Finally, note that for functions
introduced non-locally inside a non-trivial encapsulate event,
guard verification is illegal unless ACL2 determines that the proof
obligations hold outside the encapsulate event as well.
(encapsulate
((f (x) t))
(local (defun f (x) (declare (xargs :guard t)) (consp x)))
;; ERROR!
(defun g (x)
(declare (xargs :guard (f x)))
(car x)))
The order of the events in the vicinity of an encapsulate is
confusing. We discuss it in some detail here because when logical names are
being used with theory functions to compute sets of rules, it is sometimes
important to know the order in which events were executed. (See logical-name and see theory-functions.) What, for example, is the set
of function names extant in the middle of an encapsulation?
If the most recent event is previous and then you execute an
encapsulate constraining an-element with two non-local events in its body, thm1 and thm2, then the order of the events after the encapsulation is (reading chronologically forward):
previous, thm1, thm2, an-element (the encapsulate
itself). Actually, between previous and thm1 certain extensions
were made to the world by the superior encapsulate, to permit
an-element to be used as a function symbol in thm1.
Remark on return value. As with all events, a call of
encapsulate returns an error-triple, (mv erp val state),
where erp is nil when the event is redundant or is successfully
admitted. When erp is nil, the value val, which is typically
printed after a space, is determined as follows.
- If the encapsulate event is redundant, then val is
:redundant.
- Otherwise, if no new events are introduced, then val is
:empty-encapsulate.
- Otherwise, if the last sub-event in the final pass of the encapsulate
form evaluates to (mv nil '(:return-value x)) for some x, val
is x. Note that this can be accomplished by placing the form
(value-triple '(:return-value x) :on-skip-proofs t) as the final form in
the encapsulate, but since proofs are skipped during that pass, the
argument :on-skip-proofs t is necessary for val to be x.
- Otherwise, if the list of signatures is nil then val is
t.
- Otherwise, if there is a single signature introducing the function symbol,
fn, then val is fn.
- Otherwise, val is the list of function symbols introduced in the list
of signatures.
Remark on implicit constraints (unknown-constraints). See partial-encapsulate for a related utility that allows some of the constraints
to be unspecified. This is an advanced capability that is useful when one
installs special-purpose code, possibly in raw Lisp, using a trust tag (see
defttag).
Remark for ACL2(r) (see real). For ACL2(r), encapsulate can
be used to introduce classical and non-classical functions, as determined by
the signatures; see signature. Those marked as classical (respectively
non-classical) must have classical (respectively, non-classical) local
witness functions. A related requirement applies to functional instantiation;
see lemma-instance.
Subtopics
- Signature
- How to specify the arity of a constrained function
- Constraint
- Restrictions on certain functions introduced in encapsulate events
- Partial-encapsulate
- Introduce functions with some constraints unspecified
- Redundant-encapsulate
- Redundancy of encapsulate events
- Infected-constraints
- Events affecting constraints of encapsulates
- Functional-instantiation
- An analogue in ACL2 of higher-order logical reasoning. Functional
instantiation allows you to prove theorems ``by analogy'' with previous
theorems. See hints and see lemma-instance.
