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
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
(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:
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
- 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
(defun all (set-for-all-reduction)
(declare (xargs :guard (setp set-for-all-reduction)))
(if (empty set-for-all-reduction)
(and (predicate (head set-for-all-reduction))
(all (tail set-for-all-reduction)))))
(implies (in arbitrary-element (all-set))
(implies (all-hyps) (all (all-set))))