# Demonstrations for the theory of proveit.logic.sets.intersection¶

In [1]:
import proveit
from proveit import a, b, c, d, e, f, A, B, C, D, S, m, x, y, InstantiationFailure, ProofFailure
from proveit.logic import And, Equals, Forall, InSet, Intersect, NotInSet, Or, Set, SubsetEq
from proveit.core_expr_types import A_1_to_m
from proveit.logic.sets import x_in_every_A, x_notin_some_A
%begin demonstrations


# Intersection $\cap$¶

## Introduction ¶

The intersection of sets $A$ and $B$, denoted in the usual way by $A \cap B$, is represented in Prove-It with the Intersect class:

In [2]:
Intersect(A, B)


and membership (or non-membership) in such an intersection is captured with the IntersectMembership (or IntersectNonmembership) class, typically created using the membership_object() or nonmembership_object() methods in the Intersect class:

In [3]:
Intersect(A, B).membership_object(x).expr

In [4]:
Intersect(A, B).nonmembership_object(y).expr


## Demonstrations ¶

A number of basic identities and relationships can be automatically proven.

In [5]:
SubsetEq(S, Intersect(S, S)).conclude()

In [6]:
SubsetEq(S, Intersect(S, S)).prove()

In [7]:
Forall(S, SubsetEq(S, Intersect(S, S))).prove()

In [8]:
And(InSet(x, A), InSet(x, B), InSet(x,C)).prove(assumptions=[InSet(x,Intersect(A,B,C))])

In [9]:
InSet(x,Intersect(A,B,C)).prove(assumptions=[And(InSet(x, A), InSet(x, B), InSet(x,C))])


## Miscellaneous Testing¶

The material below was developed to test various intersection-related methods. Some of this material could be integrated into the _demonstrations_ page eventually and/or deleted as development continues.

### Some Example Sets For Testing¶

In [10]:
from proveit.numbers import one, two, three, four, five, six, seven
# define some enumerated Sets for use in testing, containing literals
set_123, set_12345, set_1234567 = (
Set(one, two , three),
Set(one, two , three, four, five),
Set(one, two , three, four, five, six, seven))

set_123:
set_12345:
set_1234567:
In [11]:
# define some enumerated Sets for use in testing, containing variables
set_abc, set_abcde = (
Set(a, b, c),
Set(a, b, c, d, e))

set_abc:
set_abcde:

### Testing the Intersect class methods¶

The Intersect class currently has just the following two class methods:

membership_object(self, element)
nonmembership_object(self, element)
</font>

Define a few example Intersect and IntersectMembership objects

In [12]:
Intersect(set_abc, set_abcde).membership_object(b).expr

In [13]:
Intersect(set_abc, set_abcde).nonmembership_object(d).expr

In [14]:
Intersect(A,B,C,D).nonmembership_object(x).definition()

In [15]:
Intersect(A,B,C).nonmembership_object(x).conclude(
assumptions=[Or(NotInSet(x,A), NotInSet(x,B),NotInSet(x,C))])


### Testing the IntersectMembership class methods¶

The IntersectMembership class currently has the following class methods:

definition(self, **defaults_config)
unfold(self, **defaults_config)
conclude(self, **defaults_config)
</font>

A few IntersectMembership objects for convenience:

In [16]:
# an IntersectMembership object that is clearly True
intersect_mem_01 = Intersect(set_abc, set_abcde).membership_object(b)
intersect_mem_01.expr

In [17]:
# an IntersectMembership object that is clearly False
intersect_mem_02 = Intersect(set_123, set_12345).membership_object(four)
intersect_mem_02.expr

In [18]:
# an IntersectMembership object that is not clearly True or False
intersect_mem_03 = Intersect(set_123, set_12345).membership_object(c)
intersect_mem_03.expr


### IntersectMembership.definition()¶

In [19]:
# definition() returns an equality defining the intersection membership
intersect_mem_01.definition()

In [20]:
# notice the definition() returns an equality, regardless of the truth
# of the underlying membership claim --- 4 is clearly not in the intersection
intersect_mem_02.definition()


### IntersectMembership.unfold()¶

In [21]:
# Here the unfold() is able to derive that the IntersectMembership object
# is in fact True, so no assumptions are needed:
display(intersect_mem_01.expr)
intersect_mem_01.unfold()

In [22]:
# In the case of the False intersect_mem_02, we must
# include the IntersectMembership as an assumption to produce the unfolding:
intersect_mem_02.unfold(assumptions=[intersect_mem_02.expr])

In [23]:
# In the case of the intersect_mem_03 of unknown verity, we must
# include some ssumptions to produce the unfolding:
intersect_mem_03.unfold(assumptions=[intersect_mem_03.expr])

In [24]:
# In the case of the intersect_mem_03 of unknown verity, we must
# include some assumptions to produce the unfolding:
intersect_mem_03.unfold(assumptions=[Equals(c, two)])


### IntersectMembership.conclude()¶

In [25]:
intersect_mem_01.expr

In [26]:
intersect_mem_01.conclude(assumptions=[InSet(b, set_abc), InSet(b, set_abcde)])

In [27]:
# Recall the False IntersectMembership object:
intersect_mem_02.expr

In [28]:
# We should not be able to conclude() such a False IntersectMembership object:
try:
intersect_mem_02.conclude()
assert False, "Expecting a ProofFailure (InstantiationFailure); should not get this far!"
except InstantiationFailure as the_error:
print("ProofFailure (InstantiationFailure): {}".format(the_error))

ProofFailure (InstantiationFailure): Proof step failed:
Attempting to instantiate |- forall_{m in NaturalPos} [forall_{x, A_{1}, A_{2}, ..., A_{m} | (x in A_{1}), (x in A_{2}), ..., (x in A_{m})} (x in (A_{1} intersect  A_{2} intersect  ... intersect  A_{m}))] with {m: 2, x: 4, A: ({1, 2, 3}, {1, 2, 3, 4, 5})}:
Unsatisfied condition: 4 in {1, 2, 3}. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

In [29]:
# Recall this IntersectMembership object of unknown verity (where 'c' is an unassigned variable):
intersect_mem_03.expr

In [30]:
# We should not be able to conclude() such an IntersectMembership object:
try:
intersect_mem_03.conclude()
assert False, "Expecting a ProofFailure (InstantiationFailure); should not get this far!"
except InstantiationFailure as the_error:
print("ProofFailure (InstantiationFailure): {}".format(the_error))

ProofFailure (InstantiationFailure): Proof step failed:
Attempting to instantiate |- forall_{m in NaturalPos} [forall_{x, A_{1}, A_{2}, ..., A_{m} | (x in A_{1}), (x in A_{2}), ..., (x in A_{m})} (x in (A_{1} intersect  A_{2} intersect  ... intersect  A_{m}))] with {m: 2, x: c, A: ({1, 2, 3}, {1, 2, 3, 4, 5})}:
Unsatisfied condition: c in {1, 2, 3}. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

In [31]:
# But if we supply some extra information about 'c', we can conclude:
intersect_mem_03.conclude(assumptions=[Equals(c, three)])


### Testing the IntersectNonmembership class methods¶

The IntersectNonmembership class currently has the following class methods:

definition(self, **defaults_config)
conclude(self, **defaults_config)
</font>

A few IntersectNonmembership objects for convenience:

In [32]:
# an IntersectNonmembership object that is True
intersect_nonmem_00 = Intersect(set_123, set_12345).nonmembership_object(four)
intersect_nonmem_00.expr

In [33]:
# an IntersectNonmembership object that is (possibly) true
intersect_nonmem_01 = Intersect(set_abc, set_abcde).nonmembership_object(f)
intersect_nonmem_01.expr

In [34]:
# an IntersectMembership object that is clearly False
intersect_nonmem_02 = Intersect(set_123, set_12345).nonmembership_object(two)
intersect_nonmem_02.expr

In [35]:
# an IntersectMembership object that is not clearly True or False
intersect_nonmem_03 = Intersect(set_123, set_12345).nonmembership_object(c)
intersect_nonmem_03.expr


### IntersectMembership.definition()¶

In [36]:
# definition() returns an equality defining the intersection membership
intersect_nonmem_00.definition()

In [37]:
# definition() returns an equality defining the intersection membership
intersect_nonmem_01.definition()

In [38]:
# notice the definition() returns an equality, regardless of the truth
# of the underlying membership claim --- 2 is clearly in the intersection
intersect_nonmem_02.definition()


### IntersectNonmembership.conclude()¶

In [39]:
# Recall our true nonmembership object
intersect_nonmem_00.expr

In [40]:
# we do not need explicit assumptions to conclude:
intersect_nonmem_00.conclude()

In [41]:
# Recall our (potentially) true nonmembership object
intersect_nonmem_01.expr

In [42]:
# because the nonmembership claim is ambiguous, we need some assumptions to conclude:
intersect_nonmem_01.conclude(assumptions=[Or(NotInSet(f, set_abc), NotInSet(f, set_abcde))])

In [43]:
# Recall the False IntersectNonmembership object:
intersect_nonmem_02.expr

In [44]:
# We should not be able to conclude() such a False IntersectNonmembership object:
try:
intersect_nonmem_02.conclude()
assert False, "Expecting a ProofFailure (InstantiationFailure); should not get this far!"
except InstantiationFailure as the_error:
print("ProofFailure (InstantiationFailure): {}".format(the_error))

ProofFailure (InstantiationFailure): Proof step failed:
Attempting to instantiate |- forall_{m in NaturalPos} [forall_{x, A_{1}, A_{2}, ..., A_{m} | (x not-in A_{1}) or  (x not-in A_{2}) or  ... or  (x not-in A_{m})} (x not-in (A_{1} intersect  A_{2} intersect  ... intersect  A_{m}))] with {m: 2, x: 2, A: ({1, 2, 3}, {1, 2, 3, 4, 5})}:
Unsatisfied condition: (2 not-in {1, 2, 3}) or (2 not-in {1, 2, 3, 4, 5}). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

In [45]:
# Recall this IntersectNonmembership object of unknown verity (where 'c' is an unassigned variable):
intersect_nonmem_03.expr

In [46]:
# We should not be able to conclude() such an IntersectNonmembership object:
try:
intersect_nonmem_03.conclude()
assert False, "Expecting a ProofFailure (InstantiationFailure); should not get this far!"
except InstantiationFailure as the_error:
print("ProofFailure (InstantiationFailure): {}".format(the_error))

ProofFailure (InstantiationFailure): Proof step failed:
Attempting to instantiate |- forall_{m in NaturalPos} [forall_{x, A_{1}, A_{2}, ..., A_{m} | (x not-in A_{1}) or  (x not-in A_{2}) or  ... or  (x not-in A_{m})} (x not-in (A_{1} intersect  A_{2} intersect  ... intersect  A_{m}))] with {m: 2, x: c, A: ({1, 2, 3}, {1, 2, 3, 4, 5})}:
Unsatisfied condition: (c not-in {1, 2, 3}) or (c not-in {1, 2, 3, 4, 5}). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

In [47]:
# But if we supply some extra information about 'c', we can conclude:
intersect_nonmem_03.expr.prove(assumptions=[Equals(c, four)],
simplify_with_known_evaluations=True)

In [48]:
%end demonstrations