REDUNDANT-ENCAPSULATE

redundancy of encapsulate events 
Major Section:  ENCAPSULATE

For this documentation topic we assume familiarity with encapsulate events and the notion of redundancy for events; see encapsulate and see redundant-events.

The typical way for an encapsulate event to be redundant is when a syntactically identical encapsulate has already been executed under the same default-defun-mode, default-ruler-extenders, and default-verify-guards-eagerness. But more generally, the encapsulate events need not be syntactically identical; for example, it suffices that they agree when the contents of local sub-events are ignored. The precise criterion for redundancy is given below, but let us first look at a consequence of the point just made about ignoring the contents of local sub-events. Consider the following sequence of two events. 

(encapsulate
 ()
 (defun f (x) x)
 (local (defthm f-identity
          (equal (f x) x))))

(encapsulate
 ()
 (defun f (x) x)
 (local (defthm false-claim
          (equal (f x) (not x)))))
You might be surprised to learn that the second is actually redundant, even though false-claim is clearly not a theorem; indeed, its negation is a theorem! The following two points may soften the blow. First, this behavior is as specified above (and is specified more precisely below): the contents of local events are ignored when checking redundancy of encapsulate events. Second, this behavior is sound, because the logical meaning of an encapsulate event is taken from the events that it exports, which do not include events that are local to the encapsulate event.

Some users, however, want to use encapsulate events for testing in a way that is thwarted by this ignoring of local sub-events. Consider the following sort of example. 

(encapsulate ()
             (local (defthm test1 ...)))

(encapsulate ()
             (local (defthm test2 ...)))
Since the contents of local events are ignored when checking redundancy of an encapsulate event, the second form just above is indeed redundant, presumably not as expected by whomever wrote these two tests. A solution is to add distinct non-local forms, for example as follows. 
(encapsulate ()
             (value-triple "test1")
             (local (defthm test1 ...)))

(encapsulate ()
             (value-triple "test2")
             (local (defthm test2 ...)))
A different solution is to use make-event for testing, as follows. 
(make-event (er-progn (defthm test1 ...)
                      (value '(value-triple nil))))
(make-event (er-progn (defthm test2 ...)
                      (value '(value-triple nil))))
Also see community books misc/eval.lisp, make-event/eval-check.lisp, and make-event/eval-tests.lisp for more ways to test in books.

The precise criterion for redundancy of encapsulate events is that the existing and proposed encapsulate events contain the same signatures and the same number of top-level events -- let k be that number -- and for each i < k, the ith top-level events E1 and E2 from the earlier and current encapsulates have one of the following properties.

o E1 and E2 are equal; or

o E1 is of the form (record-expansion E2 ...); or else

o E1 and E2 are equal after replacing each local sub-event by (local (value-triple :elided)), where a sub-event of an event E is either E itself, or a sub-event of a constituent event of E in the case that E is a call of with-output, with-prover-time-limit, with-prover-step-limit, record-expansion, time$, progn, progn!, or encapsulate itself.