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

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

Intersection $\cap$

Introduction

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:

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:

Intersect(A, B).membership_object(x).expr

Intersect(A, B).nonmembership_object(y).expr

Demonstrations

A number of basic identities and relationships can be automatically proven.

SubsetEq(S, Intersect(S, S)).conclude()

 ⊢  

SubsetEq(S, Intersect(S, S)).prove()

 ⊢  

Forall(S, SubsetEq(S, Intersect(S, S))).prove()

 ⊢  

And(InSet(x, A), InSet(x, B), InSet(x,C)).prove(assumptions=[InSet(x,Intersect(A,B,C))])

 ⊢  

InSet(x,Intersect(A,B,C)).prove(assumptions=[And(InSet(x, A), InSet(x, B), InSet(x,C))])

 ⊢  

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

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

set_123:

set_12345:

set_1234567:

# 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 Intersect class methods

The Intersect class currently has just the following two class methods:

membership_object(self, element)
nonmembership_object(self, element)

</font>

Define a few example Intersect and IntersectMembership objects

Intersect(set_abc, set_abcde).membership_object(b).expr

Intersect(set_abc, set_abcde).nonmembership_object(d).expr

Intersect(A,B,C,D).nonmembership_object(x).definition()

 ⊢  

Intersect(A,B,C).nonmembership_object(x).conclude(
        assumptions=[Or(NotInSet(x,A), NotInSet(x,B),NotInSet(x,C))])

 ⊢  

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

A few IntersectMembership objects for convenience:

# an IntersectMembership object that is clearly True
intersect_mem_01 = Intersect(set_abc, set_abcde).membership_object(b)
intersect_mem_01.expr

# an IntersectMembership object that is clearly False
intersect_mem_02 = Intersect(set_123, set_12345).membership_object(four)
intersect_mem_02.expr

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

# definition() returns an equality defining the intersection membership
intersect_mem_01.definition()

 ⊢  

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

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

intersect_mem_01.expr

intersect_mem_01.conclude(assumptions=[InSet(b, set_abc), InSet(b, set_abcde)])

 ⊢  

# Recall the False IntersectMembership object:
intersect_mem_02.expr

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

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

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

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

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

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

 ⊢  

Testing the IntersectNonmembership class methods

The IntersectNonmembership class currently has the following class methods:

definition(self, **defaults_config)
conclude(self, **defaults_config)

</font>

A few IntersectNonmembership objects for convenience:

# an IntersectNonmembership object that is True
intersect_nonmem_00 = Intersect(set_123, set_12345).nonmembership_object(four)
intersect_nonmem_00.expr

# an IntersectNonmembership object that is (possibly) true
intersect_nonmem_01 = Intersect(set_abc, set_abcde).nonmembership_object(f)
intersect_nonmem_01.expr

# an IntersectMembership object that is clearly False
intersect_nonmem_02 = Intersect(set_123, set_12345).nonmembership_object(two)
intersect_nonmem_02.expr

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

# definition() returns an equality defining the intersection membership
intersect_nonmem_00.definition()

 ⊢  

# definition() returns an equality defining the intersection membership
intersect_nonmem_01.definition()

 ⊢  

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

# Recall our true nonmembership object
intersect_nonmem_00.expr

# we do not need explicit assumptions to conclude:
intersect_nonmem_00.conclude()

 ⊢  

# Recall our (potentially) true nonmembership object
intersect_nonmem_01.expr

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

 ⊢  

# Recall the False IntersectNonmembership object:
intersect_nonmem_02.expr

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

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}) or  (x not-in A_{2}) or  ... or  (x not-in A_{m})} (x not-in (A_{1} intersect  A_{2} intersect  ... intersect  A_{m}))] with {m: 2, x: 2, A: ({1, 2, 3}, {1, 2, 3, 4, 5})}:
Unsatisfied condition: (2 not-in {1, 2, 3}) or (2 not-in {1, 2, 3, 4, 5}). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

# Recall this IntersectNonmembership object of unknown verity (where 'c' is an unassigned variable):
intersect_nonmem_03.expr

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

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}) or  (x not-in A_{2}) or  ... or  (x not-in A_{m})} (x not-in (A_{1} intersect  A_{2} intersect  ... intersect  A_{m}))] with {m: 2, x: c, A: ({1, 2, 3}, {1, 2, 3, 4, 5})}:
Unsatisfied condition: (c not-in {1, 2, 3}) or (c not-in {1, 2, 3, 4, 5}). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

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

 ⊢  

%end demonstrations