Infected-constraints
Events affecting constraints of encapsulates
Here we explain briefly the two kinds of "Infected" warnings that are sometimes printed near the end of the output from encapsulate events. Also see constraint for a more complete
discussion of constraints produced by encapsulate events, and see subversive-recursions for a more complete discussion of the second kind of
"Infected" warning mentioned below, in the last example.
An "Infected" warning indicates that an event introducing a function
symbol inside encapsulate event affects the constraint exported for the
function introduced in the signature list of that encapsulate.
That function is typically introduced with defun, but it could be
introduced in a signature list of a subsidiary encapsulate event or in a
defchoose event. Below we'll discuss the case of defun, but the
others are completely analogous for an "Infected" warning.
Let's compare the following three examples.
EXAMPLE 1.
(encapsulate
(((sig-fn *) => *))
(local (defun sig-fn (x) (cons x x)))
(defun foo (x)
(sig-fn x))
(defthm foo-prop
(consp (foo x))))
In Example 1 above, ACL2 warns us that the defun event is having an
effect on the constraint of another function (more on that below).
ACL2 Warning [Infected] in ( ENCAPSULATE (((SIG-FN * ...) ...) ...)
...): Note that the definitional equation for FOO infects the constraint
of this encapsulation....
Indeed, just above that warning we see that the definitional equation for
foo is part of the constraint not only on foo but also on
sig-fn.
The following constraint is associated with both of the functions FOO
and SIG-FN:
(AND (EQUAL (FOO X) (SIG-FN X)) (CONSP (FOO X)))
The warning message suggests the desirability of moving the definition out
of the encapsulate, if possible. That is not possible above: the
definition of foo cannot be moved before the encapsulate because it
depends syntactically on sig-fn, and it cannot be moved after the
encapsulate because it depends syntactically on foo-prop.
By contrast, in the next two examples the defun of foo can be
moved before, respectively after, the encapsulate. In these simple
cases, ACL2 in effect does that for us automatically, and the constraint for
sig-fn doesn't mention foo or vice-versa. In other cases, you might
want to think about how to move the relevant defun (for foo, in this
case) manually.
EXAMPLE 2 (moving the definition of foo before the
encapsulate).
(encapsulate
(((sig-fn *) => *))
(local (defun sig-fn (x) (cons x x)))
(defun foo (x)
x)
(defthm foo-prop
(equal (foo x) (car (sig-fn x)))))
EXAMPLE 3 (moving the definition of foo after the
encapsulate).
(encapsulate
(((sig-fn *) => *))
(local (defun sig-fn (x) (cons x x)))
(defun foo (x)
(sig-fn x))
(defthm foo-prop
(consp (sig-fn x)))
)
We now turn to a second kind of "Infected" warning for a defun
form inside an encapsulate form. This type of warning indicates that in
addition to the effect on constraints discussed above, ACL2 refuses to store
an induction scheme or a built-in type-prescription rule for the
defun. Consider the following example.
EXAMPLE 4.
(encapsulate
(((f *) => *))
(local (defun f (x) (cdr x)))
(defthm f-prop
(equal (f nil) nil))
(defun g (x)
(if (consp x)
(g (f x))
x)))
As in Example 1 above, the exported constraint is on both function symbols
that have been introduced, reported as follows by ACL2.
The following constraint is associated with both of the functions G
and F:
(AND (EQUAL (F NIL) NIL)
(EQUAL (G X) (IF (CONSP X) (G (F X)) X)))
But this time, in addition, no induction scheme is stored for g, nor
is any built-in type-prescription rule stored for g, as indicated
by a warning that begins as follows.
ACL2 Warning [Infected] in ( ENCAPSULATE (((F * ...) ...) ...) ...):
Note that G is ``subversive.'' See :DOC infected-constraints....
Note that if f and g had been similarly defined at the top level
instead of within an encapsulate, a type-prescription rule would be added
asserting that ``the type of G is described by the theorem (NOT (CONSP (G
X))).'' But there is no such rule introduced in this ``subversive'' case.
Indeed, this ``theorem'' is not actually a theorem after evaluating the
encapsulate, as it does not even follow from the stronger
axiom (stronger, that is, than the constraint displayed above) that both
f and g are the identity function.
See subversive-recursions for more details, including criteria for
when this ``subversive'' situation arises and what might be done to address
it. Also see constraint for a general discussion of constraints
introduced by an encapsulate event.
