		Search-engine friendly clone of the ACL2 documentation.

Std/osets

All-by-membership

A way to quantify over sets.

all-by-membership is a generic theorem that can be used to prove that a property holds of a set by showing that a related property holds of the set elements.

The most important role of all-by-membership is to allow for pick-a-point proofs of subset. That is, it allows us to show that (subset X Y) holds by showing that every element of X satisfies (in a Y).

More generally, we could show that a set satisfies a predicate like integer-setp because each of its elements satisfies integerp.

Pick-a-Point Proofs in ACL2

We begin by explaining how pick-a-point proofs of subset can be carried out. In traditional mathematics, subset is defined using quantification over members, e.g., as follows:

(equal (subset X Y)
       (forall a (implies (in a X) (in a Y))))

This definition is very useful for pick-a-point proofs that some set X is a subset of Y. Such a proof begins by picking an arbitrary point a that is a member of X. Then, if we can show that a must be a member of Y, we have established (subset X Y).

These kinds of arguments are extremely useful, and we would like to be able to carry them out in ACL2 about osets. But since ACL2 does not have explicit quantifiers, we cannot even write a theorem like this:

(implies (forall a (implies (in a X) (in a Y)))
         (subset X Y))

But consider the contrapositive of this theorem:

(implies (not (subset X Y))
         (exists a (and (in a X) (not (in a Y)))))

We can prove something like this, by writing an explicit function to search for an element of X that is not an element of Y. That is, we can prove:

(implies (not (subset X Y))
         (let ((a (find-witness X Y)))
           (and (in a X)
                (not (in a Y)))))

Once we prove the above, we still need to be able to "reduce" a proof of (subset X Y) to a proof of (implies (in a X) (in a Y)). While we can't do this with a direct rewrite rule, we can sort of fake it using functional instantiation. As groundwork:

Using encapsulate, we introduce functions sub and super with the constraint that
```
(implies (in a (sub))
         (in a (super)))
```
Using this constraint, we prove the generic theorem:
```
(subset (sub) (super))
```

Then, when we want to prove (subset X Y) for some particular X and Y, we can functionally instantiate the generic theorem with

sub   <-- (lambda () X)
super <-- (lambda () Y)

And this allows us to prove (subset X Y) as long as we can relieve the constraint, i.e., (implies (in a X) (in a Y)).

Generalizing Pick-a-Point Proofs

In earlier versions of the osets library, we used an explicit argument to reduce subset proofs to pick-a-point style membership arguments. But we later generalized the approach to arbitrary predicates instead.

First, notice that if you let the predicate (P a) be defined as (in a Y), then (subset X Y) is just

(forall a (implies (in a X) (P a)))

Our generalization basically lets you reduce a proof of (P-setp X) to a proof of (implies (in a X) (P a)), for an arbitrary predicate P. This can be used to prove subset by just chooisng P as described above, but it can also be used for many other ideas by just changing the meaning of P. For instance, if P is integerp, then we can show that X is an integer-setp or similar.

The mechanism is just an adaptation of that described in the previous section.

We begin by introducing a completely arbitrary predicate.
Based on predicate, we introduce a new function, all, which checks to see if every member in a set satisfies predicate.
We set up an encapsulate which allows us to assume that some hypotheses are true and that any member of some set satisfies predicate.

Finally, we prove all-by-membership, which shows that under these assumptions, the set satisfies all. This theorem can be functionally instantiated to reduce a proof of (all X) to a proof of

(implies (in a X) (P a))

Definitions and Theorems

Function: all

(defun all (set-for-all-reduction)
  (declare (xargs :guard (setp set-for-all-reduction)))
  (if (emptyp set-for-all-reduction)
      t
    (and (predicate (head set-for-all-reduction))
         (all (tail set-for-all-reduction)))))

Theorem: membership-constraint

(defthm membership-constraint
  (implies (all-hyps)
           (implies (in arbitrary-element (all-set))
                    (predicate arbitrary-element))))

Theorem: all-by-membership

(defthm all-by-membership
  (implies (all-hyps) (all (all-set))))