logo

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