`encapsulate`

events
Major Section: MISCELLANEOUS

Suppose that a given theorem, `thm`

, is to be functionally instantiated
using a given functional substitution, `alist`

. (See lemma-instance, or
for an example, see functional-instantiation-example.) What is the set of
proof obligations generated? It is the set obtained by applying `alist`

to
all terms, `tm`

, such that (a) `tm`

mentions some function symbol in the
domain of `alist`

, and (b) either (i) `tm`

arises from the ``constraint''
on a function symbol ancestral in `thm`

or in some `defaxiom`

or (ii)
`tm`

is the body of a `defaxiom`

. Here, a function symbol is
``ancestral'' in `thm`

if either it occurs in `thm`

, or it occurs in the
definition of some function symbol that occurs in `thm`

, and so on.

The remainder of this note explains what we mean by ``constraint'' in the words above.

In a certain sense, function symbols are introduced in essentially two ways.
The most common way is to use `defun`

(or when there is mutual recursion,
`mutual-recursion`

or `defuns`

). There is also a mechanism for
introducing ``witness functions''; see defchoose. The documentation for
these events describes the axioms they introduce, which we will call
here their ``definitional axioms.'' These definitional axioms are generally
the constraints on the function symbols that these axioms introduce.

However, when a function symbol is introduced in the scope of an
`encapsulate`

event, its constraints may differ from the definitional
axioms introduced for it. For example, suppose that a function's definition
is `local`

to the `encapsulate`

; that is, suppose the function is
introduced in the signature of the `encapsulate`

. Then its
constraints include, at the least, those non-`local`

theorems and
definitions in the `encapsulate`

that mention the function symbol.

Actually, it will follow from the discussion below that if the
signature is empty for an `encapsulate`

, then the constraint on
each of its new function symbols is exactly the definitional axiom
introduced for it. Intuitively, we view such `encapsulates`

just
as we view `include-book`

events. But the general case, where the
signature is not empty, is more complicated.

In the discussion that follows we describe in detail exactly which
constraints are associated with which function symbols that are introduced in
the scope of an `encapsulate`

event. In order to simplify the exposition
we make two cuts at it. In the first cut we present an over-simplified
explanation that nevertheless captures the main ideas. In the second cut we
complete our explanation by explaining how we view certain events as
being ``lifted'' out of the `encapsulate`

, resulting in a possibly
smaller `encapsulate`

, which becomes the target of the algorithm
described in the first cut.

At the end of this note we present an example showing why a more naive approach is unsound.

Finally, before we start our ``first cut,'' we note that any information you
want ``exported'' outside an `encapsulate`

event must be there as an
explicit definition or theorem. For example, even if a function `foo`

has
output type `(mv t t)`

in its signature, the system will not know
`(true-listp (foo x))`

merely on account of this information. Thus, if you
are using functions like `foo`

(constrained `mv`

functions), then you
may find it useful to prove (inside the `encapsulate`

, to be exported) a
`:`

`type-prescription`

rule for the constrained function, for example,
the `:`

`type-prescription`

rule `(true-listp (foo x))`

.

*First cut at constraint-assigning algorithm.* Quite simply, the formulas
introduced in the scope of an `encapsulate`

are conjoined, and each
function symbol introduced by the `encapsulate`

is assigned that
conjunction as its constraint.

Clearly this is a rather severe algorithm. Let us consider two possible optimizations in an informal manner before presenting our second cut.

Consider the (rather artificial) event below. The function `before1`

does
not refer at all, even indirectly, to the locally-introduced function
`sig-fn`

, so it is unfortunate to saddle it with constraints about
`sig-fn`

.

(encapsulate (((sig-fn *) => *)) (defun before1 (x) (if (consp x) (before1 (cdr x)) x)) (local (defun sig-fn (x) (cons x x))) (defthm sig-fn-prop (consp (sig-fn x))) )We would like to imagine moving the definition of

`before1`

to just in
front of this `encapsulate`

, as follows.
(defun before1 (x) (if (consp x) (before1 (cdr x)) x)) (encapsulate (((sig-fn *) => *)) (local (defun sig-fn (x) (cons x x))) (defthm sig-fn-prop (consp (sig-fn x))) )Thus, we will only assign the constraint

`(consp (sig-fn x))`

, from the
theorem `sig-fn-prop`

, to the function `sig-fn`

, not to the function
`before1`

.More generally, suppose an event in an `encapsulate`

event does not
mention any function symbol in the signature of the `encapsulate`

,
nor any function symbol that mentions any such function symbol, and so on.
(We might say that no function symbol from the signature is an
``ancestor'' of any function symbol occurring in the event.) Then we imagine
moving the event, so that it appears in front of the `encapsulate`

. We
don't actually move it, but we pretend we do when it comes time to assign
constraints. Thus, such definitions only introduce definitional axioms as
the constraints on the function symbols being defined. In the example above,
the event `sig-fn-prop`

introduces no constraints on function `before1`

.

Once this first optimization is performed, we have in mind a set of
``constrained functions.'' These are the functions introduced in the
`encapsulate`

that would remain after moving some of them in front, as
indicated above. Consider the collection of all formulas introduced by the
`encapsulate`

, except the definitional axioms, that mention these
constrained functions. So for example, in the event below, no such formula
mentions the function symbol `after1`

.

(encapsulate (((sig-fn *) => *)) (local (defun sig-fn (x) (cons x x))) (defthm sig-fn-prop (consp (sig-fn x))) (defun after1 (x) (sig-fn x)) )We can see that there is really no harm in imagining that we move the definition of

`after1`

out of the `encapsulate`

, to just after the
`encapsulate`

.Many subtle aspects of this rearrangement process have been omitted. For
example, suppose the function `fn`

uses `sig-fn`

, the latter being a
function in the signature of the encapsulation. Suppose a formula about
`fn`

is proved in the encapsulation. Then from the discussion above `fn`

is among the constrained functions of the encapsulate: it cannot be moved
before the encapsulate and it cannot be moved after the encapsulation. But
why is `fn`

constrained? The reason is that the theorem proved about
`fn`

may impose or express constraints on `sig-fn`

. That is, the theorem
proved about `fn`

may depend upon properties of the witness used for
`sig-fn`

. Here is a simple example:

(encapsulate (((sig-fn *) => *)) (local (defun sig-fn (x) (declare (ignore x)) 0)) (defun fn (lst) (if (endp lst) t (and (integerp (sig-fn (car lst))) (fn (cdr lst))))) (defthm fn-always-true (fn lst)))In this example, there are no

`defthm`

events that mention `sig-fn`

explicitly. One might therefore conclude that it is completely
unconstrained. But the witness we chose for it always returns an integer.
The function `fn`

uses `sig-fn`

and we prove that `fn`

always returns
true. Of course, the proof of this theorem depends upon the properties of
the witness for `sig-fn`

, even though those properties were not explicitly
``called out'' in theorems proved about `sig-fn`

. It would be unsound to
move `fn-always-true`

after the encapsulate. It would also be unsound to
constrain `sig-fn`

to satisfy just `fn-always-true`

without including in
the constraint the relation between `sig-fn`

and `fn`

. Hence both
`sig-fn`

and `fn`

are constrained by this encapsulation and the
constraint imposed on each is the same and states the relation between the
two as characterized by the equation defining `fn`

as well as the property
that `fn`

always returns true. Suppose, later, one proved a theorem about
`sig-fn`

and wished to functionally instantiate it. Then one must also
functionally instantiate `fn`

, even if it is not involved in the theorem,
because it is only through `fn`

that `sig-fn`

inherits its constrained
properties.This is a pathological example that illustrate a trap into which one may
easily fall: rather than identify the key properties of the constrained
function the user has foreshadowed its intended application and constrained
those notions. Clearly, the user wishing to introduce the `sig-fn`

above
would be well-advised to use the following instead:

(encapsulate (((sig-fn *) => *)) (local (defun sig-fn (x) (declare (ignore x)) 0)) (defthm integerp-sig-fn (integerp (sig-fn x)))) (defun fn (lst) (if (endp lst) t (and (integerp (sig-fn (car lst))) (fn (cdr lst))))) (defthm fn-always-true (fn lst)))Note that

`sig-fn`

is constrained merely to be an integer. It is the only
constrained function. Now `fn`

is introduced after the encapsulation, as a
simple function that uses `sig-fn`

. We prove that `fn`

always returns
true, but this fact does not constrain `sig-fn`

. Future uses of `sig-fn`

do not have to consider `fn`

at all.Sometimes it is necessary to introduce a function such as `fn`

within the
`encapsulate`

merely to state the key properties of the undefined function
`sig-fn`

. But that is unusual and the user should understand that both
functions are being constrained.

Another subtle aspect of encapsulation that has been brushed over so far has
to do with exactly how functions defined within the encapsulation use the
signature functions. For example, above we say ``Consider the collection of
all formulas introduced by the encapsulate,
*except the definitional axioms*, that mention these constrained
functions.'' We seem to suggest that a definitional axiom which mentions a
constrained function can be moved out of the encapsulation and considered
part of the ``post-encapsulation'' extension of the logical world, if
the defined function is not used in any non-definitional formula proved in
the encapsulation. For example, in the encapsulation above that constrained
`sig-fn`

and introduced `fn`

within the encapsulation, `fn`

was
constrained because we proved the formula `fn-always-true`

within the
encapsulation. Had we not proved `fn-always-true`

within the
encapsulation, `fn`

could have been moved after the encapsulation. But
this suggests an unsound rule because whether such a function can be moved
after the encapsulate depend on whether its *admission* used properties of
the witnesses! In particular, we say a function is ``subversive'' if any of
its governing tests or the actuals in any recursive call involve a function
in which the signature functions are ancestral. See subversive-recursions.

(Aside: The definition of `fn`

in the first enapsulation above that defines
`fn`

, i.e., the encapsulation with `fn-always-true`

inside, is subversive
because the call of the macro `AND`

expands to a call of `IF`

that
governs a recursive call of `fn`

, in this case:

(defun fn (lst) (if (endp lst) t (if (integerp (sig-fn (car lst))) (fn (cdr lst)) nil))).If we switch the order of conjuncts in

`fn`

, then the definition of `fn`

is no longer subversive, but it still ``infects'' the constraint generated
for the encapsulation, hence for `sig-fn`

, because `fn-always-true`

blocks the definition of `fn`

from being moved back (to after the
encapsulation). If we both switch the order of conjuncts and drop
`fn-always-true`

from the encapsulation, then the definition of `fn`

is
in essence moved back to after the encapsulation, and the constraint for
`sig-fn`

no longer includes the definition of `fn`

. End of aside.)Another aspect we have not discussed is what happens to nested encapsulations
when each introduces constrained functions. We say an `encapsulate`

event
is ``trivial'' if it introduces no constrained functions, i.e., if its
signatures is `nil`

. Trivial encapsulations are just a way to wrap up a
collection of events into a single event.

From the foregoing discussion we see we are interested in exactly how we can ``rearrange'' the events in a non-trivial encapsulation -- moving some ``before'' the encapsulation and others ``after'' the encapsulation. We are also interested in which functions introduced by the encapsulation are ``constrained'' and what the ``constraints'' on each are. We may summarize the observations above as follows, after which we conclude with a more elaborate example.

*Second cut at constraint-assigning algorithm.* First, we focus only on
non-trivial encapsulations that neither contain nor are contained in
non-trivial encapsulations. (Nested non-trivial encapsulations are not
rearranged at all: do not put anything in such a nest unless you mean for it
to become part of the constraints generated.) Second, in what follows we
only consider the non-`local`

events of such an `encapsulate`

, assuming
that they satisfy the restriction of using no locally defined function
symbols other than the signature functions. Given such an `encapsulate`

event, move, to just in front of it and in the same order, all definitions
and theorems for which none of the signature functions is ancestral. Now
collect up all formulas (theorems) introduced in the `encapsulate`

other
than definitional axioms. Add to this set any of those definitional
equations that is either subversive or defines a function used in a formula
in the set. The conjunction of the resulting set of formulas is called the
``constraint'' and the set of all the signature functions of the
`encapsulate`

together with all function symbols defined in the
`encapsulate`

and mentioned in the constraint is called the ``constrained
functions.'' Assign the constraint to each of the constrained functions.
Move, to just after the `encapsulate`

, the definitions of all function
symbols defined in the `encapsulate`

that have been omitted from the
constraint.

Implementation note. In the implementation we do not actually move events, but we create constraints that pretend that we did.

Here is an example illustrating our constraint-assigning algorithm. It builds on the preceding examples.

(encapsulate (((sig-fn *) => *)) (defun before1 (x) (if (consp x) (before1 (cdr x)) x)) (local (defun sig-fn (x) (cons x x))) (defthm sig-fn-prop (consp (sig-fn x))) (defun during (x) (if (consp x) x (cons (car (sig-fn x)) 17))) (defun before2 (x) (before1 x)) (defthm before2-prop (atom (before2 x))) (defthm during-prop (implies (and (atom x) (before2 x)) (equal (car (during x)) (car (sig-fn x))))) (defun after1 (x) (sig-fn x)) (defchoose after2 (x) (u) (and (< u x) (during x))) )

Only the functions `sig-fn`

and `during`

receive extra constraints. The
functions `before1`

and `before2`

are viewed as moving in front of the
`encapsulate`

, as is the theorem `before2-prop`

. The functions
`after1`

and `after2`

are viewed as being moved past the
`encapsulate`

. The implementation reports the following.

In addition to SIG-FN, we export AFTER2, AFTER1, BEFORE2, DURING and BEFORE1. The following constraint is associated with both of the functions DURING and SIG-FN: (AND (EQUAL (DURING X) (IF (CONSP X) X (CONS (CAR (SIG-FN X)) 17))) (CONSP (SIG-FN X)) (IMPLIES (AND (ATOM X) (BEFORE2 X)) (EQUAL (CAR (DURING X)) (CAR (SIG-FN X)))))Notice that the formula

`(consp (during x))`

is not a conjunct of the
constraint. During the first pass of the `encapsulate`

, this formula is
stored as a `:`

`type-prescription`

rule deduced during the definition
of the function `during`

. However, the rule is not exported because of a
rather subtle soundness issue. (If you are interested in details, see the
comments in source function `putprop-type-prescription-lst`

.)We conclude by asking (and to a certain extent, answering) the following
question: Isn't there an approach to assigning constraints that avoids
over-constraining more simply than our ``second cut'' above? Perhaps it
seems that given an `encapsulate`

, we should simply assign to each
locally defined function the theorems exported about that function. If we
adopted that simple approach the events below would be admissible.

(encapsulate (((foo *) => *)) (local (defun foo (x) x)) (defun bar (x) (foo x)) (defthm bar-prop (equal (bar x) x) :rule-classes nil)) (defthm foo-id (equal (foo x) x) :hints (("Goal" :use bar-prop))) ; The following event is not admissible in ACL2. (defthm ouch! nil :rule-classes nil :hints (("Goal" :use ((:functional-instance foo-id (foo (lambda (x) (cons x x))))))))Under the simple approach we have in mind,

`bar`

is constrained to satisfy
both its definition and `bar-prop`

because `bar`

mentions a function
declared in the signature list of the encapsulation. In fact, `bar`

is
so-constrained in the ACL2 semantics of encapsulation and the first two
events above (the `encapsulate`

and the consequence that `foo`

must be
the identity function) are actually admissible. But under the simple
approach to assigning constraints, `foo`

is unconstrained because no
theorem about it is exported. Under that approach, `ouch!`

is provable
because `foo`

can be instantiated in `foo-id`

to a function other than
the identity function.It's tempting to think we can fix this by including definitions, not just
theorems, in constraints. But consider the following slightly more elaborate
example. The problem is that we need to include as a constraint on `foo`

not only the definition of `bar`

, which mentions `foo`

explicitly, but
also `abc`

, which has `foo`

as an ancestor.

(encapsulate (((foo *) => *)) (local (defun foo (x) x)) (local (defthm foo-prop (equal (foo x) x))) (defun bar (x) (foo x)) (defun abc (x) (bar x)) (defthm abc-prop (equal (abc x) x) :rule-classes nil)) (defthm foo-id (equal (foo x) x) :hints (("Goal" :use abc-prop))) ; The following event is not admissible in ACL2. (defthm ouch! nil :rule-classes nil :hints (("Goal" :use ((:functional-instance foo-id (foo (lambda (x) (cons x x))) (bar (lambda (x) (cons x x))))))))