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
```

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
```

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))])
```

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.

`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))
```

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))
```

`Intersect`

class methods¶

The `Intersect`

class currently has just the following two class methods:

membership_object(self, element)

nonmembership_object(self, element)

</font>
nonmembership_object(self, element)

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))])
```

`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>
unfold(self, **defaults_config)

conclude(self, **defaults_config)

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))
```

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))
```

In [31]:

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

`IntersectNonmembership`

class methods¶

The `IntersectNonmembership`

class currently has the following class methods:

definition(self, **defaults_config)

conclude(self, **defaults_config)

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

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))
```

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))
```

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
```