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

import proveit
from proveit import ExprTuple, InstantiationFailure, ProofFailure, UnsatisfiedPrerequisites
from proveit.logic import (Forall, Equals, EvaluationError, InSet, Not, NotEquals,
                           NotInSet, EmptySet, Set)
from proveit import a, b, c, d, e, f, i, x, y, A, B, C, D, E, F, G, H, I, S, T
from proveit.numbers import zero, one, two, three, four, five, six, seven, eight, nine, num, Exp
from proveit.numbers import Add, Integer, Mult, Natural, NaturalPos, Real, RealNeg, RealPos
from proveit.numbers.number_sets.number_set import NumberSet
%begin demonstrations

Membership $\in$

UNDER CONSTRUCTION

Introduction
Simple Expressions involving Membership $(\in)$
Common Attributes of a Membership $(\in)$ Expression
Axioms
Further Demonstrations

1. $(x\in A)\wedge(A\subset B)\Rightarrow (x\in B)$
2. $\forall_{x\in A}(x\in B) \Rightarrow (A \subseteq B)$
3. $(x\in B)\wedge(A\supset B)\Rightarrow (x\in A)$

Introduction

Set membership (*e.g.*, $x \in S$) (along with the related concepts of subset $\subset, \subseteq$, and superset $\supset, \supseteq$), is often critical in proofs, either as a goal in itself or as a condition or assumption appearing in a proof. For example, one might need to define a variable $x$ to be a natural number, $x \in \mathbb{N}$, to be used in a particulat theory, or we might want to prove that a number resides (or doesn't reside) in a particular set, for example that $\sqrt{2} \not\in \mathbb{Q}$.
This ``_demonstrations_`` notebook explores such membership expressions and related methods. (Set containment expressions involving $\subset$, $\subseteq$, $\supset$, etc., are explored more thoroughly in their own ``_demonstrations_`` notebook in ``proveit.logic.sets.inclusion``)

Simple Expressions Involving Membership ($\in$, $\not\in$)

It is straightforward to construct membership expressions. Here are some basic examples of such expressions:

# set membership
InSet(x, S)

NotInSet(x, EmptySet)

InSet(two, Natural)

NotInSet(num(-4), NaturalPos)

Exponentiated sets are not currently needed. They will likely be resurrected later and moved to a more appropriate theory package.

#InSet(ExprTuple(), Exp(S, zero)).prove()

#InSet(ExprTuple(A),Exp(S,one)).prove([InSet(A,S)])

#InSet(ExprTuple(A,B),Exp(S,two)).prove([InSet(A,S), InSet(B,S)])

#InSet(ExprTuple(A,B,C),Exp(S,three)).prove([InSet(A,S), InSet(B,S),InSet(C,S)])

#InSet(ExprTuple(A,B,C, D),Exp(S,four)).prove([InSet(A,S), InSet(B,S),InSet(C,S), InSet(D,S)])

#InSet(ExprTuple(A,B,C, D, E),Exp(S,five)).prove([InSet(A,S), InSet(B,S),InSet(C,S), InSet(D,S), InSet(E,S)])

#InSet(ExprTuple(A,B,C, D, E, F),Exp(S,six)).prove([InSet(A,S), InSet(B,S),InSet(C,S), InSet(D,S), InSet(E,S), InSet(F,S)])

#InSet(ExprTuple(A,B,C, D, E, F, G),Exp(S,seven)).prove([InSet(A,S), InSet(B,S),InSet(C,S), InSet(D,S), InSet(E,S), InSet(F,S), InSet(G,S)])

#InSet(ExprTuple(A,B,C, D, E, F, G, H),Exp(S,eight)).prove([InSet(A,S), InSet(B,S),InSet(C,S), InSet(D,S), InSet(E,S), InSet(F,S), InSet(G,S), InSet(H,S)])

#InSet(ExprTuple(A,B,C, D, E, F, G, H, I),Exp(S,nine)).prove([InSet(A,S), InSet(B,S),InSet(C,S), InSet(D,S), InSet(E,S), InSet(F,S), InSet(G,S), InSet(H,S), InSet(I,S)])

Not(InSet(x,S)).prove(assumptions=[NotInSet(x,S)])

 ⊢  

NotInSet(x,S).prove(assumptions=[Not(InSet(x,S))])

 ⊢  

example_membership = InSet(a, Natural)

example_membership:

example_membership.element

example_membership.deduce_in_bool()

 ⊢  

Miscellaneous Testing

The material below was developed to test various membership-related methods. Some of this material could be integrated into the demonstrations page eventually and/or deleted as development continues.

Testing the InSet class methods

The InSet class currently has the following prover-related class methods:

deduce_not_in(self, **defaults_config)
deduce_in_bool(self, **defaults_config)
conclude(self, **defaults_config)
shallow_simlification(self, *, must_evaluate=False, **defaults_config)

</font>

InSet.deduce_not_in()

Deduce x not in S assuming not(A in S), where self = (x in S). This is a somewhat odd method called on a membership object to actually conclude the negation of the membership claim. Some examples appear below:

# Here is a simple, literal example. Notice that the 'self' on which the method
# is called is actually the opposite claim from the conclusion being drawn.
InSet(x, S).deduce_not_in(assumptions=[Not(InSet(x, S))])

 ⊢  

# Even though the deduction involves the negation of the 'self' membership object,
# the self membership object args must match the assumptions
try:
    InSet(y, T).deduce_not_in(assumptions=[Not(InSet(x, S))])
    assert False, "Expecting an InstantiationFailure; should not make it to this point!"
except InstantiationFailure as the_error:
    print("ProofFailure (InstantiationFailure):{}".format(the_error))

ProofFailure (InstantiationFailure):Proof step failed assuming {[not](x in S)}:
Attempting to instantiate |- forall_{x, S | [not](x in S)} (x not-in S) with {x: y, S: T}:
Unsatisfied condition: [not](y in T). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

# Notice that we can prove simple non-memberships automatically,
# without the deduce_not_in()
NotInSet(three, Set(one, two)).prove()

 ⊢  

# The deduce_not_in() is more about a folding of the assumption or
# judgment about the negation of a membership claim or the negation of
# element equalities
InSet(a, Set(b, c, d)).deduce_not_in(assumptions=[NotEquals(a, b), NotEquals(a, c), NotEquals(a, d)])

, ,  ⊢  

InSet.deduce_in_bool()

# Membership claims are Boolean values
InSet(two, Set(one, two, three)).deduce_in_bool()

 ⊢  

# False membership claims are Boolean values
InSet(four, Set(one, two, three)).deduce_in_bool()

 ⊢  

# Membership claims with unknown verity are also Boolean values
InSet(a, Set(one, two, three)).deduce_in_bool()

 ⊢  

# Membership claims with unknown verity are also Boolean values
InSet(b, Set(c, d, f)).deduce_in_bool()

 ⊢  

# Membership claims with unknown verity are also Boolean values
InSet(b, Set(c, d, f)).deduce_in_bool(assumptions=[Equals(b, d)])

 ⊢  

# Membership claims with unknown verity are also Boolean values
# Here we don't know the value of the variable b:
InSet(b, Set(one, Add(one, one), three)).deduce_in_bool()

 ⊢  

# Here is a Membership claim that is False, involving assumptions
# about the value of variable b; notice the assumption is irrelevant
InSet(b, Set(one, Add(one, one), three)).deduce_in_bool(assumptions=[Equals(b, zero)])

 ⊢  

InSet.conclude()

# A simple membership claim can be deduced using conclude()
InSet(two, Set(one, two, three)).conclude()

 ⊢  

# We should not be able to conclude a False membership claim
try:
    InSet(four, Set(one, two, three)).conclude()
    assert False, "Expecting a ProofFailure (TypeError); should not make it this far!"
except InstantiationFailure as the_error:
    print("Proof Failure (Type Error): {}".format(the_error))

Proof Failure (Type Error): Proof step failed:
Attempting to instantiate |- forall_{n in Natural} [forall_{x, y_{1}, y_{2}, ..., y_{n} | (x = y_{1}) or  (x = y_{2}) or  ... or  (x = y_{n})} (x in {y_{1}, y_{2}, ..., y_{n}})] with {n: 3, x: 4, y: (1, 2, 3)}:
Unsatisfied condition: (4 = 1) or (4 = 2) or (4 = 3). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

InSet(a, Set(one, two, three)).conclude(assumptions=[Equals(a, two)])

 ⊢  

InSet(a, Set(b, c, d)).conclude(assumptions=[Equals(a, d)])

 ⊢  

InSet(b, Set(one, two, three)).conclude(assumptions=[InSet(b, Set(two, three))])

 ⊢  

# But there are a number of standard set memberships that can be deduced
# based on subset memberships
InSet(a, Integer).conclude(assumptions=[InSet(a, Natural)])

 ⊢  

# Verify that the conclude() method is not automatically simplifying aspects of the
# of set elements
InSet(a, Set(one, Add(one, one), three)).conclude(assumptions=[Equals(a, three)])

 ⊢  

# Verify that the conclude() method is not automatically simplifying aspects of the
# of set elements, even when checking for equalities
InSet(a, Set(one, Mult(one, two), three)).conclude(assumptions=[Equals(a, two)])

 ⊢  

InSet.evaluation()

InSet(four, Set(one, four, three)).evaluation()

 ⊢  

# And we should be able to shallow_evaluate a False claim
InSet(two, Set(one, Add(one, three), three)).evaluation()

 ⊢  

InSet.shallow_simplification()

# A simple membership claim can be deduced using shallow_simplification
# Notice we can evaluate 1+3 to find it equals 4, but we leave the 1+3
# (Works with/without must_evaluate=True)
InSet(four, Set(one, Add(one, three), three)).shallow_simplification()

 ⊢  

# We should not be able to shallow_evaluate a claim of unknown verity
try:
    InSet(a, Set(one, Add(one, three), three)).shallow_simplification(must_evaluate=True)
    assert False, "Expecting an EvaluationError; should not make it this far!"
except EvaluationError as the_error:
    print("EvaluationError: {}".format(the_error))

EvaluationError: Evaluation of (a = 1) or (a = (1 + 3)) or (a = 3) under assumptions {} is not known

# But we should be able to shallow_evaluate with the appropriate assumption(s)
InSet(a, Set(one, Add(one, three), three)).shallow_simplification(must_evaluate=True,
                                                                  assumptions=[Equals(a, four)])

 ⊢  

# But we should be able to shallow_evaluate with the appropriate assumption(s)
InSet(a, Set(one, Add(one, three), three)).shallow_simplification(must_evaluate=True,
                                                                  assumptions=[Equals(a, two)])

 ⊢  

Testing the NotInSet class methods

The NotInSet class currently has the following prover-related class methods:

deduce_in_bool(self, **defaults_config)
unfold_not_in(self, **defaults_config)
conclude(self, **defaults_config)
conclude_as_folded(self, **defaults_config)
shallow_evaluation(self, **defaults_config)

</font>

NotInSet.deduce_in_bool()

# Membership claims are Boolean values
NotInSet(four, Set(one, two, three)).deduce_in_bool()

 ⊢  

# False membership claims are Boolean values
NotInSet(two, Set(one, two, three)).deduce_in_bool()

 ⊢  

# Membership claims with unknown verity are also Boolean values
NotInSet(a, Set(one, two, three)).deduce_in_bool()

 ⊢  

# Membership claims with unknown verity are also Boolean values
NotInSet(b, Set(c, d, f)).deduce_in_bool()

 ⊢  

# False Membership claims with assumption-based variable values are Boolean values
NotInSet(b, Set(c, d, f)).deduce_in_bool(assumptions=[Equals(b, d)])

 ⊢  

# Membership claims with unknown verity are also Boolean values
# Here we don't know the value of the variable b:
NotInSet(b, Set(one, Add(one, one), three)).deduce_in_bool()

 ⊢  

# Here is a Membership claim that is False, involving assumptions
# about the value of variable b; notice the assumption is irrelevant
NotInSet(b, Set(one, Add(one, one), three)).deduce_in_bool(assumptions=[Equals(b, two)])

 ⊢  

NotInSet.unfold_not_in()

From $(x \notin y)$, derive and return $\lnot(x \in y)$.

# Here is a simple, literal example. Notice that the 'self' on which the method
# is called is actually the opposite claim from the conclusion being drawn.
NotInSet(x, S).unfold_not_in(assumptions=[NotInSet(x, S)])

 ⊢  

# Notice that we can unfold simple non-memberships automatically,
# without invoking assumptions
NotInSet(three, Set(one, two)).unfold_not_in()

 ⊢  

# The unfold_not_in() is more about a folding of the assumption or
# judgment about the negation of a membership claim or the negation of
# element equalities
NotInSet(a, Set(b, c, d)).unfold_not_in(assumptions=[NotInSet(a, Set(b, c, d))])

 ⊢  

# The unfold_not_in() is more about a folding of the assumption or
# judgment about the negation of a membership claim or the negation of
# element equalities
NotInSet(a, Set(b, c, d)).unfold_not_in(assumptions=[NotEquals(a, b), NotEquals(a, c), NotEquals(a, d)])

, ,  ⊢  

NotInSet.conclude()

# A simple nonmembership claim can be deduced using conclude()
NotInSet(four, Set(one, two, three)).conclude()

 ⊢  

# We should not be able to conclude a False nonmembership claim
try:
    NotInSet(two, Set(one, two, three)).conclude()
    assert False, "Expecting a ProofFailure (TypeError); should not make it this far!"
except InstantiationFailure as the_error:
    print("Proof Failure (InstantiationFailure): {}".format(the_error))

Proof Failure (InstantiationFailure): Proof step failed:
Attempting to instantiate |- forall_{n in Natural} [forall_{x, y_{1}, y_{2}, ..., y_{n} | (x != y_{1}), (x != y_{2}), ..., (x != y_{n})} (x not-in {y_{1}, y_{2}, ..., y_{n}})] with {n: 3, x: 2, y: (1, 2, 3)}:
Unsatisfied condition: 2 != 2. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

NotInSet(a, Set(one, two, three)).conclude(assumptions=[Equals(a, four)],
                                           simplify_with_known_evaluations=True)

 ⊢  

NotInSet(a, Set(b, c, d)).conclude(assumptions=[NotEquals(a, b), NotEquals(a, c), NotEquals(a, d)])

, ,  ⊢  

NotInSet(a, Natural).conclude(assumptions=[NotInSet(a, Integer)])

 ⊢  

NotInSet(a, Set(one, Add(one, one), three)).conclude(assumptions=[Equals(a, four)])

 ⊢  

NotInSet(a, Set(one, Mult(one, two), three)).conclude(
    assumptions=[NotEquals(a, one), NotEquals(a, two), NotEquals(a, three)])

, ,  ⊢  

# So do this one -- finding that when a!=1, a!=2, a!=3, then a not in {1, 1+1, 3}.
NotInSet(a, Set(one, Add(one, one), three)).conclude(
        assumptions=[NotEquals(a, one), NotEquals(a, two), NotEquals(a, three)])

, ,  ⊢  

NotInSet(a, Set(one, Add(one, two), four)).conclude(
        assumptions=[NotEquals(a, one), NotEquals(a, three), NotEquals(a, four)])

, ,  ⊢  

NotInSet.conclude_as_folded()

Attempt to conclude x not in S via Not(x in S).

NotInSet(zero, Set(one, two, three)).conclude_as_folded()

 ⊢  

NotInSet(a, Set(b, c, d)).conclude_as_folded(assumptions=[Not(InSet(a, Set(b, c, d)))])

 ⊢  

# This is an interesting example
NotInSet(a, Set(d, c, f)).conclude_as_folded(assumptions=[NotEquals(a, c), NotEquals(a, d), NotEquals(a, f)])

, ,  ⊢  

NotInSet.shallow_simplification()

Attempt to evaluate whether some x ∉ S is TRUE or FALSE using the 'definition' method of the domain's 'nonmembership_object' if there is one.

# A simple nonmembership claim can be deduced using shallow_simplification
NotInSet(two, Set(one, four, three, five)).shallow_simplification(must_evaluate=True)

 ⊢  

# A simple nonmembership claim can be deduced using shallow_simplification
# Notice we can evaluate 1+3 to find 1+3 != 2, but we leave the 1+3
NotInSet(two, Set(one, Add(one, three), three)).shallow_simplification(must_evaluate=True)

 ⊢  

# And we should be able to shallow_evaluate a False claim
NotInSet(four, Set(one, Add(one, three), three)).shallow_simplification(must_evaluate=True)

 ⊢  

# We should not be able to shallow_evaluate a claim of unknown verity
try:
    NotInSet(a, Set(one, Add(one, three), three)).shallow_simplification(must_evaluate=True)
    assert False, "Expecting an EvaluationError; should not make it this far!"
except EvaluationError as the_error:
    print("EvaluationError: {}".format(the_error))

EvaluationError: Evaluation of (a != 1) and (a != (1 + 3)) and (a != 3) under assumptions {} is not known

# But we should be able to shallow_evaluate with the appropriate assumption(s)
NotInSet(a, Set(one, Add(one, three), three)).shallow_simplification(must_evaluate=True,
                                                                     assumptions=[Equals(a, five)])

 ⊢  

# But we should be able to shallow_evaluate with the appropriate assumption(s)
NotInSet(a, Set(one, Add(one, three), three)).shallow_simplification(must_evaluate=True,
                                                                     assumptions=[Equals(a, one)])

 ⊢  

%end demonstrations