Demonstrations for the theory of proveit.logic.sets.subtraction¶

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


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

set_123:
set_12345:
set_1234567:
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))

set_abc:
set_abcde:

Testing the 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>

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

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

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

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

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

ProofFailure (InstantiationFailure): Proof step failed:
Attempting to instantiate |- forall_{x, A, B | x in A, x not-in B} (x in (A - B)) with {x: a, A: {a, b, c, d, e}, B: {b, c, d}}:
Unsatisfied condition: a not-in {b, c, d}. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

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

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

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

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

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

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

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


Testing the 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>

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

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

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

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

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

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

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

# We can unfold that with no extra assumptions (clearly the 2nd disjunct is True):

%end demonstrations