logo

Demonstrations for the theory of proveit.logic.sets.unification

In [1]:
import proveit
from proveit import a, b, c, d, e, f, m, x, A, B, C, D, InstantiationFailure
from proveit.logic import Forall, And, Or, Equals, InSet, NotInSet, Set, Union
from proveit.core_expr_types import A_1_to_m
from proveit.logic.sets import x_in_any_A, x_notin_all_A
from proveit.numbers import (zero, one, two, three, four, five, six, seven,
                             Add, Integer, NaturalPos)
%begin demonstrations
In [2]:
Or(InSet(x, A), InSet(x, B), InSet(x,C)).prove(assumptions=[InSet(x,Union(A,B,C))])
 ⊢  
In [3]:
InSet(x,Union(A,B,C)).prove(assumptions=[Or(InSet(x, A), InSet(x, B), InSet(x,C))])
 ⊢  
In [4]:
NotInSet(x, Union(A,B,C,D)).definition()
 ⊢  
In [5]:
NotInSet(x, Union(A,B,C)).prove(assumptions=[And(NotInSet(x,A), NotInSet(x,B),NotInSet(x,C))])
 ⊢  
In [ ]:

Miscellaneous Testing

The material below was developed to test various unification-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 [6]:
# define some enumerated Sets for use in testing, containing numeric literals
set_123, set_45, set_12345, set_1357, set_246 = (
        Set(one, two , three),
        Set(four, five),
        Set(one, two, three, four, five),
        Set(one, three, five, seven),
        Set(two, four, six))
set_123:
set_45:
set_12345:
set_1357:
set_246:
In [7]:
# define some enumerated Sets for use in testing, containing variables
set_abc, set_abcde, set_de = (
        Set(a, b, c),
        Set(a, b, c, d, e),
        Set(d, e))
set_abc:
set_abcde:
set_de:

Testing the UnionMembership class methods

The UnionMembership class has the following class methods:

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

A few UnionMembership objects for convenience:

In [8]:
# a UnionMembership object that is clearly True
union_mem_01 = Union(set_abc, set_de).membership_object(d)
union_mem_01.expr
In [9]:
# a UnionMembership object that is clearly False
union_mem_02 = Union(set_123, set_45).membership_object(six)
union_mem_02.expr
In [10]:
# a UnionMembership object that is not clearly True or False
union_mem_03 = Union(set_123, set_abc).membership_object(d)
union_mem_03.expr
In [11]:
# a UnionMembership object that is not clearly True or False
union_mem_04 = Union(set_abc, Set(two, Add(one, three), five)).membership_object(d)
union_mem_04.expr

UnionMembership.definition()

From self $= [x \in (A \cup B \cup \ldots)]$, deduce and return something of the form $[x \in (A \cup B \cup \ldots)] = [(x \in A) \lor (x \in B) \lor \ldots$.

In [12]:
union_mem_01.expr
In [13]:
union_mem_01.definition()
 ⊢  
In [14]:
union_mem_02.expr
In [15]:
# notice the definition is returned even for False membership claims
union_mem_02.definition()
 ⊢  
In [16]:
union_mem_03.expr
In [17]:
# notice the definition is returned even for membership claims
# with unknown verity
union_mem_03.definition()
 ⊢  
In [18]:
union_mem_04.expr
In [19]:
# notice the definition is returned even for membership claims
# with unknown verity
union_mem_04.definition()
 ⊢  

UnionMembership.unfold()

From a self proven or assumed of the form $[x \in (A \cup B \cup \ldots)]$, derive and return $[(x \in A) \lor (x \in B) \lor \ldots]$.

In [20]:
union_mem_01.expr
In [21]:
union_mem_01.unfold(assumptions=[union_mem_01.expr])
 ⊢  
In [22]:
union_mem_02.expr
In [23]:
# This should fail, since 6 is not in the union
try:
    union_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_{m in NaturalPos} [forall_{x, A_{1}, A_{2}, ..., A_{m} | x in (A_{1} union  A_{2} union  ... union  A_{m})} ((x in A_{1}) or  (x in A_{2}) or  ... or  (x in A_{m}))] with {m: 2, x: 6, A: ({1, 2, 3}, {4, 5})}:
Unsatisfied condition: 6 in ({1, 2, 3} union {4, 5}). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.
In [24]:
Union(set_123, set_45).membership_object(two).expr
In [25]:
# Notice here we don't need any explicit assumptions
Union(set_123, set_45).membership_object(two).unfold()
 ⊢  
In [26]:
# Consider a union of sets with some reducible elements:
Union(Set(two, Add(two, three)), Set(one, Add(one, two))).membership_object(three).expr
In [27]:
# We are still ok unfolding the membership, without any extra assumptions
Union(Set(two, Add(two, three)), Set(one, Add(one, two))).membership_object(three).unfold()
 ⊢  

UnionMembership.conclude()

Called on self $= [x \in (A \cup B \;\cup\; ...)]$, and knowing or assuming $[[x \in A] \lor [x \in B] \;\lor\; ...]$, derive and return self.

In [28]:
union_mem_01.expr
In [29]:
# conclude() requires no extra assumptions for this one
union_mem_01.conclude()
 ⊢  
In [30]:
# Recall the False UnionMembership object:
union_mem_02.expr
In [31]:
# We should not be able to conclude() such a False IntersectMembership object:
try:
    union_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}) or  (x in A_{2}) or  ... or  (x in A_{m})} (x in (A_{1} union  A_{2} union  ... union  A_{m}))] with {m: 2, x: 6, A: ({1, 2, 3}, {4, 5})}:
Unsatisfied condition: (6 in {1, 2, 3}) or (6 in {4, 5}). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.
In [32]:
# Recall this IntersectMembership object of unknown verity (where 'c' is an unassigned variable):
union_mem_03.expr
In [33]:
# We should not be able to conclude() such an DifferenceMembership object:
try:
    union_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}) or  (x in A_{2}) or  ... or  (x in A_{m})} (x in (A_{1} union  A_{2} union  ... union  A_{m}))] with {m: 2, x: d, A: ({1, 2, 3}, {a, b, c})}:
Unsatisfied condition: (d in {1, 2, 3}) or (d in {a, b, c}). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.
In [34]:
# But if we supply some extra information about 'c', we can conclude:
union_mem_03.conclude(assumptions=[Equals(d, a)])
 ⊢  
In [35]:
# Consider a more general UnionMembership object
Union(Set(b, e), Set(b, c, d)).membership_object(a).expr
In [36]:
# We should not be able to conclude() such a UnionMembership object,
# without knowing the value of a:
try:
    Union(Set(b, 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_{m in NaturalPos} [forall_{x, A_{1}, A_{2}, ..., A_{m} | (x in A_{1}) or  (x in A_{2}) or  ... or  (x in A_{m})} (x in (A_{1} union  A_{2} union  ... union  A_{m}))] with {m: 2, x: a, A: ({b, e}, {b, c, d})}:
Unsatisfied condition: (a in {b, e}) or (a in {b, c, d}). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.
In [37]:
# define a Union with some unsimplified elements:
Union(Set(one, Add(one, one), Add(two, one)), Set(Add(one, one), three)).membership_object(c).expr
In [38]:
Union(Set(one, Add(one, one), Add(two, one)), Set(Add(one, one), three)).membership_object(c).conclude(
        assumptions=[Equals(c, two)])
 ⊢  
In [39]:
# a UnionMembership object involving general sets
Union(Integer, NaturalPos).membership_object(x).expr
In [40]:
# a conclude() on that general set UnionMembership
Union(Integer, NaturalPos).membership_object(x).conclude(
        assumptions=[Equals(x, zero)])
 ⊢  

Testing the UnionNonmembership class methods

The UnionNonmembership class has the following class methods:

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

A few UnionNonmembership objects for convenience:

In [41]:
# a UnionMembership object that is clearly True
union_nonmem_01 = Union(set_123, set_45).nonmembership_object(six)
union_nonmem_01.expr
In [42]:
# a UnionNonmembership object that is clearly False
union_nonmem_02 = Union(set_abc, set_de).nonmembership_object(d)
union_nonmem_02.expr
In [43]:
# a UnionNonmembership object that is not clearly True or False
union_nonmem_03 = Union(set_123, set_abc).nonmembership_object(d)
union_nonmem_03.expr
In [44]:
# a UnionMembership object that is not clearly True or False
union_nonmem_04 = Union(set_abc, Set(two, Add(one, three), Add(two, three))).nonmembership_object(d)
union_nonmem_04.expr

UnionNonmembership.definition()

From self $= [x \notin (A \cup B \cup \ldots)]$, deduce and return something of the form $[x \notin (A \cup B \cup \ldots)] = [(x \notin A) \land (x \notin B) \land \ldots]$.

In [45]:
union_nonmem_01.expr
In [46]:
union_nonmem_01.definition()
 ⊢  
In [47]:
union_nonmem_02.expr
In [48]:
# notice the definition is returned even for False membership claims
union_nonmem_02.definition()
 ⊢  
In [49]:
union_nonmem_03.expr
In [50]:
# notice the definition is returned even for membership claims
# with unknown verity
union_nonmem_03.definition()
 ⊢  
In [51]:
union_nonmem_04.expr
In [52]:
# notice the definition is returned even for membership claims
# with unknown verity
union_nonmem_04.definition()
 ⊢  

UnionNonmembership.conclude()

Called on self $= [x \notin (A \cup B \;\cup\; ...)]$, and knowing or assuming $[[x \notin A] \land [x \notin B] \;\land\; ...]$, derive and return self.

In [53]:
union_nonmem_01.expr
In [54]:
# conclude() requires no extra assumptions for this one
union_nonmem_01.conclude()
 ⊢  
In [55]:
# Recall the False UnionNonmembership object:
union_nonmem_02.expr
In [56]:
# We should not be able to conclude() such a False UnionNonmembership object:
try:
    union_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}), (x not-in A_{2}), ..., (x not-in A_{m})} (x not-in (A_{1} union  A_{2} union  ... union  A_{m}))] with {m: 2, x: d, A: ({a, b, c}, {d, e})}:
Unsatisfied condition: d not-in {a, b, c}. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.
In [57]:
# Recall this UnionNonmembership object of unknown verity (where 'd' is an unassigned variable):
union_nonmem_03.expr
In [58]:
# We should not be able to conclude() such a UnionNonmembership object:
try:
    union_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}), (x not-in A_{2}), ..., (x not-in A_{m})} (x not-in (A_{1} union  A_{2} union  ... union  A_{m}))] with {m: 2, x: d, A: ({1, 2, 3}, {a, b, c})}:
Unsatisfied condition: d not-in {1, 2, 3}. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.
In [59]:
# But if we supply some extra information about 'd', we can conclude:
union_nonmem_03.conclude(assumptions=[Equals(d, four), NotInSet(d, Set(a, b, c))],
                         simplify_with_known_evaluations=True)
,  ⊢  
In [60]:
# Consider a more general UnionNonmembership object
Union(Set(b, e), Set(b, c, d)).nonmembership_object(a).expr
In [61]:
# We should not be able to conclude() such a UnionNonmembership object,
# without knowing the value of a:
try:
    Union(Set(b, e), Set(b, c, d)).nonmembership_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_{m in NaturalPos} [forall_{x, A_{1}, A_{2}, ..., A_{m} | (x not-in A_{1}), (x not-in A_{2}), ..., (x not-in A_{m})} (x not-in (A_{1} union  A_{2} union  ... union  A_{m}))] with {m: 2, x: a, A: ({b, e}, {b, c, d})}:
Unsatisfied condition: a not-in {b, e}. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.
In [62]:
# define a Union with some unsimplified elements:
Union(Set(one, Add(one, one), Add(two, one)), Set(Add(one, one), three)).membership_object(c).expr
In [63]:
Union(Set(one, Add(one, one), Add(two, one)), Set(Add(one, one), three)).nonmembership_object(c).conclude(
        assumptions=[Equals(c, zero)],
        simplify_with_known_evaluations=True)
 ⊢  
In [64]:
# a UnionNonmembership object involving general sets
Union(Integer, NaturalPos).nonmembership_object(x).expr
In [65]:
# a conclude() on that general set UnionNonmembership
Union(Integer, NaturalPos).nonmembership_object(x).conclude(
        assumptions=[NotInSet(x, Integer)])
 ⊢  
In [66]:
%end demonstrations