In [1]:

```
import proveit
from proveit import a, b, c, d, e, f, x, y, A, B, S, InstantiationFailure
from proveit.logic import Or, Equals, NotEquals, Set, InSet, NotInSet, Difference
from proveit.numbers import (one, two, three, four, five, six, seven, Add,
Integer, Natural, NaturalPos, Neg)
%begin demonstrations
```

In [2]:

```
InSet(x, Difference(A, B)).definition()
```

In [3]:

```
InSet(x, Difference(A, B)).prove(assumptions=[InSet(x, A), NotInSet(x, B)])
```

In [4]:

```
InSet(x, Difference(A, Set(y))).prove(assumptions=[InSet(x, A), NotEquals(x, y)])
```

In [5]:

```
InSet(x, A).prove(assumptions=[InSet(x, Difference(A, B))])
```

In [6]:

```
NotInSet(x, B).prove(assumptions=[InSet(x, Difference(A, B))])
```

In [7]:

```
NotEquals(x, y).prove(assumptions=[InSet(x, Difference(A, Set(y)))])
```

In [8]:

```
NotInSet(x, Difference(A, B)).definition()
```

In [9]:

```
NotInSet(x, Difference(A, B)).prove(assumptions=[Or(NotInSet(x, A), InSet(x, B))])
```

In [10]:

```
Or(NotInSet(x, A), InSet(x, B)).prove(assumptions=[NotInSet(x, Difference(A, B))])
```

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 [11]:

```
# define some enumerated Sets for use in testing, containing numeric 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 [12]:

```
# define some enumerated Sets for use in testing, containing variables
set_abc, set_abcde = (
Set(a, b, c),
Set(a, b, c, d, e))
```

`DifferenceMembership`

class methods¶

The `DifferenceMembership`

class currently has the following class methods:

conclude(self, **defaults_config)

conclude_as_folded(self, **defaults_config)

definition(self, **defaults_config)

unfold(self, **defaults_config)

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

definition(self, **defaults_config)

unfold(self, **defaults_config)

A few `DifferenceMembership`

objects for convenience:

In [13]:

```
# a DifferenceMembership object that is clearly True
diff_mem_01 = Difference(set_abcde, set_abc).membership_object(d)
diff_mem_01.expr
```

In [14]:

```
# a DifferenceMembership object that is clearly False
diff_mem_02 = Difference(set_12345, set_123).membership_object(two)
diff_mem_02.expr
```

In [15]:

```
# a DifferenceMembership object that is not clearly True or False
diff_mem_03 = Difference(set_12345, set_123).membership_object(c)
diff_mem_03.expr
```

`DifferenceMembership.conclude()`

¶In [16]:

```
diff_mem_01.expr
```

In [17]:

```
# using explicit assumptions about set membership and set non-membership
diff_mem_01.conclude(assumptions=[InSet(d, set_abcde), NotInSet(d, set_abc)])
```

In [18]:

```
# using less explicit assumptions about set membership/nonmembership
diff_mem_01.conclude(assumptions=[NotEquals(d, a), NotEquals(d, b), NotEquals(d, c)])
```

In [19]:

```
# Recall the False IntersectMembership object:
diff_mem_02.expr
```

In [20]:

```
# We should not be able to conclude() such a False IntersectMembership object:
try:
diff_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 [21]:

```
# Recall this IntersectMembership object of unknown verity (where 'c' is an unassigned variable):
diff_mem_03.expr
```

In [22]:

```
# We should not be able to conclude() such an DifferenceMembership object:
try:
diff_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 [23]:

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

In [24]:

```
# Consider a more general DifferenceMembership object
Difference(Set(a, b, c, d, e), Set(b, c, d)).membership_object(a).expr
```

In [25]:

```
# We should not be able to conclude() such an DifferenceMembership object,
# without knowing the value of a:
try:
Difference(Set(a, b, c, d, e), Set(b, c, d)).membership_object(a).conclude()
assert False, "Expecting a ProofFailure (InstantiationFailure); should not get this far!"
except InstantiationFailure as the_error:
print("ProofFailure (InstantiationFailure): {}".format(the_error))
```

In [26]:

```
# define a Difference with an unsimplified element (1+1)
diff_mem_04 = Difference(Set(one, two, three), Set(Add(one, one), three)).membership_object(c)
diff_mem_04.expr
```

In [27]:

```
diff_mem_04.conclude(assumptions=[Equals(c, one)],
simplify_with_known_evaluations=True)
```

In [28]:

```
# a DifferenceMembership object involving general sets
diff_mem_05 = Difference(Integer, Natural).membership_object(x)
diff_mem_05.expr
```

In [29]:

```
diff_mem_05.conclude(assumptions=[InSet(x, Integer), NotInSet(x, Natural)])
```

`DifferenceMembership.conclude_as_folded()`

¶Currently, DifferenceMembership.conclude() simply calls DifferenceMembership.conclude_as_folded(), so the examples that work for conclude() should all work for conclude_as_folded().

In [30]:

```
diff_mem_01.expr
```

In [31]:

```
# using explicit assumptions about set membership and set non-membership
diff_mem_01.conclude_as_folded(assumptions=[InSet(d, set_abcde), NotInSet(d, set_abc)])
```

In [32]:

```
# using less explicit assumptions about set membership/nonmembership
diff_mem_01.conclude_as_folded(assumptions=[NotEquals(d, a), NotEquals(d, b), NotEquals(d, c)])
```

In [33]:

```
# Recall the False IntersectMembership object:
diff_mem_02.expr
```

In [34]:

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

In [35]:

```
# Recall this IntersectMembership object of unknown verity (where 'c' is an unassigned variable):
diff_mem_03.expr
```

In [36]:

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

In [37]:

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

In [38]:

```
# define a Difference with an unsimplified element (1+1)
diff_mem_06 = Difference(Set(one, two, three), Set(two, Add(two, one))).membership_object(c)
diff_mem_06.expr
```

In [39]:

```
diff_mem_06.conclude_as_folded(assumptions=[Equals(c, one)],
simplify_with_known_evaluations=True)
```

In [40]:

```
# a DifferenceMembership object involving general sets
diff_mem_07 = Difference(Natural, NaturalPos).membership_object(x)
diff_mem_07.expr
```

In [41]:

```
diff_mem_07.conclude_as_folded(assumptions=[InSet(x, Natural), NotInSet(x, NaturalPos)])
```

`DifferenceMembership.definition()`

¶Deduce and return something of the form $[x \in (A - B)] = [(x \in A) \land (x \notin B)$.

In [42]:

```
diff_mem_01.expr
```

In [43]:

```
diff_mem_01.definition()
```

In [44]:

```
diff_mem_02.expr
```

In [45]:

```
diff_mem_02.definition()
```

In [46]:

```
diff_mem_03.expr
```

In [47]:

```
diff_mem_03.definition()
```

In [48]:

```
diff_mem_04.expr
```

In [49]:

```
diff_mem_04.definition()
```

`DifferenceMembership.unfold()`

¶From something proven or assumed of the form $[x \in (A - B)]$, derive and return $[(x \in A) \land (x \notin B)]$, or, for the special case of $x \in (S - {y})$, derive and return $[(x \in A) \land (x \notin y)]$ (if that theorem is usable).

In [50]:

```
diff_mem_01.expr
```

In [51]:

```
diff_mem_01.unfold(assumptions=[diff_mem_01.expr])
```

In [52]:

```
diff_mem_02.expr
```

In [53]:

```
# This should fail, since 2 has been subtracted out
try:
diff_mem_02.unfold()
assert False, "Expecting a ProofFailure (InstantiationFailure); should not get this far!"
except InstantiationFailure as the_error:
print("ProofFailure (InstantiationFailure): {}".format(the_error))
```

In [54]:

```
Difference(set_12345, Set(one, three)).membership_object(two).expr
```

In [55]:

```
# Notice here we don't need any explicit assumptions
Difference(set_12345, Set(one, three)).membership_object(two).unfold()
```

In [56]:

```
diff_mem_08 = Difference(set_12345, Set(one, Add(one, two))).membership_object(two)
diff_mem_08.expr
```

In [57]:

```
diff_mem_08.unfold()
```

`DifferenceNonmembership`

class methods¶

The `DifferenceNonmembership`

class includes the following class methods:

conclude(self, **defaults_config)

conclude_as_folded(self, **defaults_config)

definition(self, **defaults_config)

unfold(self, **defaults_config)

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

definition(self, **defaults_config)

unfold(self, **defaults_config)

A few `DifferenceNonmembership`

objects for convenience:

In [58]:

```
# a DifferenceMembership object that is clearly True
diff_nonmem_01 = Difference(set_abcde, set_abc).nonmembership_object(b)
diff_nonmem_01.expr
```

In [59]:

```
# a DifferenceNonmembership object that is clearly False
diff_nonmem_02 = Difference(set_12345, set_123).nonmembership_object(four)
diff_nonmem_02.expr
```

In [60]:

```
# a DifferenceMembership object that is not clearly True or False
diff_nonmem_03 = Difference(set_12345, set_123).nonmembership_object(c)
diff_nonmem_03.expr
```

`DifferenceNonmembership.conclude()`

¶Prove something of the form $x \notin (A - B)$ via $(x \notin A) \lor (x \in B)$. The special case of $x \notin (S - \{y\})$ may be concluded via $(x \notin S) \lor (x = y)$ as long as that theorem is usable.

In [61]:

```
diff_nonmem_01.expr
```

In [62]:

```
# At first, this seems a bit odd … what if we have something like b=d?
# But in such a case, the subtraction of {a, b, c} would have removed the
# value for d as well, so it seems to be correct.
diff_nonmem_01.conclude()
```

In [63]:

```
# Notice that it doesn't matter what b actually is …
# The conclusion is independent of the assumption(s) about the value of b
diff_nonmem_01.conclude(assumptions=[Equals(b, d)])
```

In [64]:

```
diff_nonmem_02.expr
```

In [65]:

```
# We should not be able to conclude() the False non-membership:
try:
diff_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 [66]:

```
# Interestingly, we can assume an obviously False premise and conclude():
diff_nonmem_02.conclude(assumptions=[NotInSet(four, set_12345)])
```

In [67]:

```
diff_nonmem_03.expr
```

In [68]:

```
# We should not be able to conclude() the non-membership of unknown verity:
try:
diff_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 [69]:

```
# but given some information about the value of c, we can conclude():
diff_nonmem_03.conclude(assumptions=[Equals(c, two)])
```

In [ ]:

```
```

`DifferenceNonmembership.conclude_as_folded()`

¶Because `DifferenceNonmembership.conclude()`

simply calls `DifferenceNonmembership.conclude_as_folded()`

, the work above for the `conclude()`

method also demonstrates the functionality of the `conclude_as_folded()`

method.

`DifferenceNonmembership.definition()`

¶Deduce and return something of the form $[x \notin (A - B)] = [(x \notin A) or (x \in B)]$.

In [70]:

```
diff_nonmem_01.expr
```

In [71]:

```
diff_nonmem_01.definition()
```

In [72]:

```
diff_nonmem_02.expr
```

In [73]:

```
# Notice the definition is returned even for False non-membership claims
diff_nonmem_02.definition()
```

In [74]:

```
diff_nonmem_03.expr
```

In [75]:

```
# Notice the definition is returned even non-membership claims of unknown verity
diff_nonmem_03.definition()
```

In [76]:

```
diff_nonmem_complicated = Difference(Set(one, Add(one, one), three, Add(two, two)), Set(Add(one, one), Add(two, one), four)).nonmembership_object(c)
diff_nonmem_complicated.expr
```

In [77]:

```
diff_nonmem_complicated.definition()
```

`DifferenceNonmembership.unfold()`

¶From something proven or assumed of the form $[x \notin (A - B)]$, derive and return $[(x \notin A) \lor (x \in B)]$, or, for the special case of $x \notin (S - {y})$, derive and return $[(x \notin A) \lor (x = y)]$ (if that theorem is usable).

In [78]:

```
diff_nonmem_01.expr
```

In [79]:

```
diff_nonmem_01.unfold()
```

In [80]:

```
diff_nonmem_02.expr
```

In [81]:

```
# This should fail, since 4 has not been subtracted out
try:
diff_nonmem_02.unfold()
assert False, "Expecting a ProofFailure (InstantiationFailure); should not get this far!"
except InstantiationFailure as the_error:
print("ProofFailure (InstantiationFailure): {}".format(the_error))
```

In [82]:

```
Difference(set_12345, Set(one, three)).nonmembership_object(three).expr
```

In [83]:

```
# Notice here we don't need any explicit assumptions
Difference(set_12345, Set(one, three)).nonmembership_object(three).unfold()
```

In [84]:

```
# Consider an interesting example involving literals and an addition element
Difference(set_12345, Set(one, Add(one, two))).nonmembership_object(three).expr
```

In [85]:

```
# We can unfold that with no extra assumptions (clearly the 2nd disjunct is True):
Difference(set_12345, Set(one, Add(one, two))).nonmembership_object(three).unfold()
```

In [86]:

```
%end demonstrations
```