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

import proveit
from proveit import ExprRange, InstantiationFailure, ProofFailure, used_vars, free_vars
from proveit import a, b, c, d, e, i, l, m, n, x, y
from proveit import A, B, C, D, E
from proveit.logic import Boolean, TRUE, FALSE
from proveit.logic import (Equals, Forall, InSet, NotEquals, NotInSet,
                           Or, ProperSubset, Set, SubsetEq)
from proveit.numbers import zero, one, two, three, four, five, six, seven, Add
%begin demonstrations

Enumerated Sets $\{a, b, \ldots, n\}$

Introduction
Simple Expressions involving the enumerated Set class
Common Attributes of an enumerated Set
Axioms
Theorems & Conjectures
Further Demonstrations

1. Deducing Set memberships such as $\vdash b\in\{a, b, c\}$, $\vdash 1\in\{1, 2, 3\}$, and $\vdash \{a, b\}\in\{\{\}, \{a\}, \{b\}, \{a, b\}\}$
2. Deducing Set non-memberships such as $\vdash 4\notin\{1, 2, 3\}$ and $\vdash d\notin\{a, b, c\}$
3. Deducing subset relationships between enumerated Sets: $\vdash\{2, 4, 6\}\subseteq\{1, 2, 3, 4, 5, 6, 7\}$ and $\vdash\{1, 3, 5, 1, 5\}\subseteq\{1, 2, 3, 4, 5, 6, 7\}$
4. Instantiating the proper_subset_of_superset conjecture to deduce $\{1, 2, 3\}\subset\{1, 2, 3, 4, 5, 6\}$
5. Deducing that $\{2, 4, 6\}\subset\{1, 2, 3, 4, 5, 6\}$ and $\{c, b, a\} \subset \{a, b, c, d, e\}$
6. Deducing that $\{1, a, 1\}\subset\{1, a, 1, b, 2, a\}$ when $a = 1$

Miscellaneous Testing

Introduction

Finite, explicitly enumerated sets (i.e., sets defined by an explicit listing of elements) are ubiquitous in logic and mathematics, and regularly arise in theorems and proofs. For example, one might need to consider elements in the Boolean set: $\mathbb{B}=\{\mathtt{TRUE}, \mathtt{FALSE}\} = \{\top, \bot\}$ or the integer equivalents $\{1, 0\}$, or perhaps a set of variables $\{a, b, c\}$ or that set's power set $\{\{\}, \{a\}, \{b\}, \{c\}, \{a, b\}, \{b, c\}, \{a, c\}, \{a, b, c\} \}$. Often, one needs to consider a finite but unspecified-size set such as $\{a, b, \ldots, n\}$.

In Prove-It, we construct such finite enumerated sets with the Set class, which takes an arbitrary number of Prove-It expressions as arguments (including zero arguments for an empty set), like this: $\mathtt{Set}(e_1, e_2, \ldots, e_n)$. The result is a set of the elements $e_1$, $e_2$, $\ldots$, $e_n$, where the initial order specified is preserved for display purposes but the order itself has no inherent meaning.

Interestingly, you can also create redundantly populated sets such as $\{a, b, a\}$, which as we'll see below, are not considered multi-sets but instead are simply alternative representations of the reduced “support set” without the multiplicities — e.g., $\{a, b, a\} = \{a, b\}$. Until one actively requests that a set such as $\{a, b, a\}$ be reduced to its support, Prove-It will continue to encode and display the set with the seeming multiplicities.

Simple Expressions Involving Enumerated Sets

Enumerated sets are easy to construct using the Set class, and such Sets are easily incorporated into other expressions. Various Set construction examples are shown below, including small Sets of literals and variables, a Set of Sets (including an empty set), and a finite Set of unspecified length:

# A 3-element set of (literal) integers:
set_123 = Set(one, two, three)

set_123:

# A 3-element set of variables:
set_abc = Set(a, b, c)

set_abc:

# A 6-element set of combining literals and variables:
set_123_abc = Set(one, two, three, a, b, c)

set_123_abc:

# A 4-element set of enumerated sets, including an empty set:
power_set_ab = Set(Set(), Set(a), Set(b), Set(a, b))

power_set_ab:

# a set of the first n positive integers
# set_1_to_n = Set(Iter(i, i, one, n))
set_1_to_n = Set(ExprRange(i, i, one, n))

set_1_to_n:

# Claim that x is a member of the set {a, b, c}
InSet(x, set_123)

# A more elaborate claim about what it means for x to be a member
# of the set {1, 2, 3}. Notice the set appears as a domain specification:
Forall(x, Or(Equals(x, one), Equals(x, two), Equals(x, three)), domain=set_123)

Common Attributes of enumerated Set expressions

Let's look at some simple examples of enumerated sets and their common attributes.

# Recall some enumerated sets defined earlier:
display(set_123)
display(set_abc)
display(power_set_ab)

We can look at the construction of such expressions by calling expr_info() to see the table version of the expression's underlying directed acyclic graph (DAG) representation:

# See how an enumerated set expression is constructed:
set_123.expr_info()

	core type	sub-expressions	expression
0	Operation	operator: 1 operands: 2
1	Literal
2	ExprTuple	3, 4, 5
3	Literal
4	Literal
5	Literal

We can access the elements of an enumerated Set as operands of the Set class or somewhat more intuitively as elements of the Set, either of which return a tuple of the elements:

# the elements of the enumerated, as a tuple of elements
set_123.operands

# or more intuitively, using the elements attribute:
set_123.elements

Of course, we can also access each of the elements individually:

# and we can grab any single element:
e1, e2, e3 = set_123.elements[0], set_123.elements[1], set_123.elements[2]

e1:

e2:

e3:

And we can grab a slice of the elements:

# grab a slice of the elements:
set_123.operands[1:3]

We can get the set of all variables appearing in a Set, which returns an empty set if there no variables, and returns a reduced set if there are multiple instances of any variables:

# the set of variables used in the enumerated set
# (in this case an empty set because the set contains only literals)
used_vars(set_123)

# the set of variables used in the enumerated set
used_vars(set_abc)

# define a set with two instances of the same variable
set_aba = Set(a, b, a)

set_aba:

# notice that the operands include multiplicities
set_aba_operands = set_aba.operands

set_aba_operands:

# and the elements attribute includes multiplicities
set_aba_elements = set_aba.elements

set_aba_elements:

# but the tuple of variables used is just (a, b)
# and the order of appearance is not guaranteed
set_aba_vars = used_vars(set_aba)

set_aba_vars:

We can also dig into a Set in terms of its sub-expressions:

# grab subexpressions from the Set construction
subexpr0, subexpr_1, subexpr_11 = (
        set_abc.sub_expr(0),
        set_abc.sub_expr(1),
        set_abc.sub_expr(1).sub_expr(1))

subexpr0:

subexpr_1:

subexpr_11:

Axioms

Right now we have a single axiom in the logic.sets/enumeration theory, defining what it means to be a member of an enumerated set. If $x\in\{y_1,y_2, \ldots,y_n\}$, then $x=y_1 \lor x=y_2 \lor \ldots \lor x=y_n$:

from proveit.logic.sets.enumeration  import enum_set_def
enum_set_def

 ⊢  

As an exercise, we could, for example, manually instantiate that axiom for the case of $x\in\mathbb{B}$, by first instantiating for $x\in\{\top, \bot\}$:

enum_set_def_spec = enum_set_def.instantiate(
        {n:two, x:x, y:(TRUE, FALSE)})

enum_set_def_spec:  ⊢  

… and then bring in our axiomatic definition of the Boolean as $\mathbb{B}=\{\top, \bot\}$ and perform the appropriate substitution:

from proveit.logic.booleans  import bools_def
bools_def

 ⊢  

bools_def.sub_left_side_into(enum_set_def_spec)

 ⊢  

Theorems & Conjectures

The logic.sets/enumeration theory already has a substantial number of related theorems and conjectures established, most of which would typically be used implicitly behind-the-scenes when utilizing the various related Set class methods instead of being used directly and explicitly in theorem form. Some illustrative examples of the theorems are shown below, and the remainder can be found in the enumeration theorems Jupyter Python notebook.

from proveit.logic.sets.enumeration import (
        fold, fold_singleton, leftward_permutation,
        reduction_right, subset_eq_of_superset)

# If x=y1 or x=y2 or … or x=yn, then x is in the
# set containing all those options
fold

 ⊢  

# if x=y, then x is in the set {y}
fold_singleton

 ⊢  

# An enumerated set is equal to a version of itself in which
# an element is moved to the left in the "list" of elements.
# Notice the set element 'c' below:
leftward_permutation

 ⊢  

# An enumerated set is equal to a version of itself in which a 2nd
# occurrence of an element is removed. Notice the element(s) x in
# the set below:
reduction_right

 ⊢  

# An enumerated set is always an improper subset of
# any set containing the original enumerated set
subset_eq_of_superset

 ⊢  

Demonstrations

1. Deducing Set memberships such as $\vdash b\in\{a, b, c\}$, $\vdash 1\in\{1, 2, 3\}$, and $\vdash \{a, b\}\in\{\{\}, \{a\}, \{b\}, \{a, b\}\}$.

Many simple enumerated set membership claims can be deduced automatically or relatively easily.
Let's start with a few claims about set membership:

# Some (as yet) unproven claims
b_in_set_abc, three_in_set_123, set_ab_in_its_power_set = (
        InSet(b, set_abc), InSet(three, set_123), InSet(Set(a, b), power_set_ab))

b_in_set_abc:

three_in_set_123:

set_ab_in_its_power_set:

Prove-It can prove each of these claims automatically, without any extra nudging from us:

# prove the claim that b is an elem of {a, b, c}
b_in_set_abc.prove()

 ⊢  

# prove the claim that 3 is an elem of {1, 2, 3}
three_in_set_123.prove()

 ⊢  

# prove the claim that {a,b} is an elem of its own power set
set_ab_in_its_power_set.prove()

 ⊢  

The proofs generated by Prove-It for those three judgments established above (click on the turnstile in an expression to go to the proof page), are somewhat complicated and opaque, relying on the very basic fold theorem each time for how membership is defined for an enumerated set. As an alternative, consider a manual application of the in_enumerated_set theorem:

from proveit.logic.sets.enumeration import in_enumerated_set
in_enumerated_set

 ⊢  

# Instantiate the theorem for the case of {a,b} being in its own power set:
set_ab_in_its_power_set_kt = in_enumerated_set.instantiate(
    {m:three, n:zero, a:(Set(), Set(a), Set(b)), b:Set(a,b), c:()})

set_ab_in_its_power_set_kt:  ⊢  

Now the proof of such a claim is relatively straightforward, and we will have moved much of the heavy-lifting of the previous proofs to a single underlying proof of the in_enumerated_set theorem itself:

set_ab_in_its_power_set_kt.proof()

	step type	requirements	statement
0	instantiation	1, 2, 3, 4, 5	⊢
	: , : , : , : , :
1	conjecture		⊢
	proveit.logic.sets.enumeration.in_enumerated_set
2	conjecture		⊢
	proveit.numbers.numerals.decimals.nat3
3	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
4	instantiation	6	⊢
	: , : , :
5	conjecture		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
6	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq

2. Deducing Set non-memberships such as $\vdash 4\notin\{1, 2, 3\}$ and $\vdash d\notin\{a, b, c\}$.

Many simple enumerated set non-membership claims can be deduced automatically or relatively easily.
First, recall a some enumerated Sets defined earlier:

display(set_123)
display(set_abc)

Prove-It can automatically prove some simple non-membership claims:

NotInSet(four, set_123).prove()

 ⊢  

If the sets involve variables with unassigned values, however, things are more complicated. For example, Prove-It will rightly refuse to automatically deduce that $d\notin \{a, b, c\}$, because we don't know what the variables might be equal to:

try:
    NotInSet(d, set_abc).prove()
    assert False, "Should not make it to this point."
except ProofFailure as e:
    print("Proof Failure: {}".format(e))

Proof Failure: 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: d, y: (a, b, c)}:
Unsatisfied condition: d != a. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

If we can provide Prove-It with the appropriate assumptions, however, we're OK:

NotInSet(d, set_abc).prove(assumptions=[NotEquals(a,d), NotEquals(b,d), NotEquals(c,d)])

, ,  ⊢  

In real-life operations, somewhere along the way we might have already proven that set of inequalities $a\ne d$, $b\ne d$, $c\ne d$, and Prove-It would then be able to automatically prove that $d\notin\{a, b, c\}$.

3. Deducing subset relationships between enumerated Sets: $\vdash\{2, 4, 6\}\subseteq\{1, 2, 3, 4, 5, 6, 7\}$ and $\vdash\{1, 3, 5, 1, 5\}\subseteq\{1, 2, 3, 4, 5, 6, 7\}$.

Although Prove-It might not be able to automatically prove that any arbitrary enumerated Set is a subset of another, the enumerated Set class has some machinery to help us out.

Consider the following sets, which include the set $\{1, 3, 5, 1, 5\}$ with redundant elements (recall that the enumerated Set class allows us to create a set that appears to hold multiple copies of the same element, but the set is not actually a multi-set):

# define some enumerated sets
set_1234567, set_evens, set_odds = (
        Set(one, two, three, four, five, six, seven),
        Set(two, four, six),
        Set(one, three, five, one, five))

set_1234567:

set_evens:

set_odds:

Prove-It can automatically prove that $\{2, 4, 6\}\subseteq\{1, 2, 3, 4, 5, 6, 7\}$:

SubsetEq(set_evens, set_1234567).prove()

 ⊢  

This can produce an odd-looking result, because an enumerated Set might look like a multi-set but is in fact equal to its underlying support. For example, because $\{1, 3, 5, 1, 5\} = \{1, 3, 5\}$, we have the following result, even though the subset appears to have multiple copies of elements $1$ and $5$:

SubsetEq(set_odds, set_1234567).prove()

 ⊢  

4. Instantiating the proper_subset_of_superset conjecture to deduce $\{1, 3, 5\}\subset\{1, 2, 3, 4, 5, 6\}$.

The enumerated Set class has machinery to help automate the deduction of proper subset relationships such as $\{1, 3, 5\}\subset\{1, 2, 3, 4, 5, 6\}$ between enumerated Sets. To gain some insight into how such machinery works, however, it can be useful to derive such a relationship by manually enacting the same steps as the automation would.

So, consider the enumerated Sets $\{1, 3, 5\}$ and $\{1, 2, 3, 4, 5, 6\}$ defined below:

set_135, set_123456 = (
        Set(one, three, five),
        Set(one, two, three, four, five, six))

set_135:

set_123456:

ProperSubset(set_135, set_123456).prove()

 ⊢  

But we have an established theorem (really a conjecture) in the enumeration theory that we can use to deduce the subset relationship:

from proveit.logic.sets.enumeration import proper_subset_of_superset
proper_subset_of_superset

 ⊢  

Our goal here is to instantiate the proper_subset_of_superset theorem with the details of our desired case, where we will take:

• $m=3$ to be the size of our subset Set $\{1, 3, 5\}$;
• $n=2$ to be the size of $c_1, \ldots, c_n$ portion of our superset Set $\{1, 2, 3, 4, 5, 6\}$;
• $\{a_1, \ldots, a_m\}$ to be our subset $\{1, 3, 5\}$;
• and $\{a_1, \ldots, a_m, b, c_1, \ldots, c_n\}$ to be our superset $\{1, 2, 3, 4, 5, 6\}$ after being suitably permuted to something like $\{1, 3, 5, 2, 4, 6\}$, which then requires $b$ to be the element $2$ and $\{c_1, \ldots, c_n\}$ to be the set $\{4, 6\}$.

We begin the process by deducing an equivalence between our original superset and the permuted version of that set required for the theorem application:

superset_permuted_kt = set_123456.permutation(new_order=[0, 2, 4, 1, 3, 5])

superset_permuted_kt:  ⊢  

Notice that we eventually want to replace $b$ with our superset element $2$ (although we could have chosen any superset element that isn't in the subset and chosen a different permutation as necessary), and so we'll want to know that $2\notin\{1, 3, 5\}$. The instantiation machinery might handle that part for us automatically, but for this example we'll ask Prove-It to first do it for us explicitly:

NotInSet(two, set_135).prove()

 ⊢  

Now we should be ready to instantiate the proper_subset_of_superset theorem as shown below:

proper_subset_of_superset_spec = proper_subset_of_superset.instantiate(
        {m:three, n:two, a:set_135.elements, b:two, c:(four, six)})

proper_subset_of_superset_spec:  ⊢  

And finally we use our earlier-derived permutation equivalence to back substitute and get the desired subset relationship:

superset_permuted_kt.sub_left_side_into(proper_subset_of_superset_spec)

 ⊢  

5. Deducing that $\{2, 4, 6\}\subset\{1, 2, 3, 4, 5, 6\}$ and $\{c, b, a\}\subset\{a, b, c, d, e\}$.

The enumerated Set class has machinery to help automate the deduction of proper subset relationships such as $\{1, 3, 5\}\subset\{1, 2, 3, 4, 5, 6\}$ derived manually in the previous demonstration. That process of set reduction, permutation, theorem application, and back substitution, has been encapsulated in the Set.deduce_enum_proper_subset() method. For example, we can derive that $\{2, 4, 6\}\subset\{1, 2, 3, 4, 5, 6\}$ in a single step:

# define the subset {2, 4, 6}
set_246 = Set(two, four, six)

set_246:

# deduce that {2, 4, 6} is a proper subset of {1, 2, 3, 4, 5, 6}
proper_subset_jdgmt = set_123456.deduce_enum_proper_subset(subset=set_246)

proper_subset_jdgmt:  ⊢  

That process works without any special assumptions included in the call of the deduce_enum_proper_subset() method because Prove-It recognizes the elements $1, 2, \ldots, 6$ as distinct literals and thus that (e.g.) $1\notin\{2, 4, 6\}$ (which allows Prove-It to recognize that the set $\{1, 2, 3, 4, 5, 6\}$ not only contains the set $\{2, 4, 6\}$ but also has elements not in that subset).
If we are dealing with variables, though, the process is not so clear-cut. Consider, for example, the claim that $\{c, b, a\}\subset\{a, b, c, d, e\}$. If one interprets the letter elements as literals, then it's clear that $d\notin\{c, b, a\}$ and we can easily understand that $\{c, b, a\}$ is a proper subset of $\{a, b, c, d, e\}$. But if $a, b, \ldots, e$ are variables, it's not at all clear that $d\ne a$ and thus it's not clear that $d\notin\{c, b, a\}$.
Thus, without some additional information or additional assumptions, the deduce_enum_proper_subset() method will fail to deduce the desired relationship:

from proveit import e
set_abcde, set_cba = Set(a, b, c, d, e), Set(c, b, a)
try:
    set_abcde.deduce_enum_proper_subset(subset=set_cba)
    assert False, "Should not make it to this point."
except ValueError as e:
    print("Proof Failure: {}".format(e))

Proof Failure: Failed to prove that the supposed Self superset {a, b, c, d, e} has any elements not already contained in the supposed proper subset {c, b, a}. Notice that this might be because the sets have unassigned variables

If we supply the additional assumptions, however, that $d\ne a$, $d\ne b$, and $d\ne c$, the derivation works fine:

set_abcde.deduce_enum_proper_subset(subset=set_cba,
        assumptions=[NotEquals(d, a), NotEquals(d, b), NotEquals(d, c)])

, ,  ⊢  

Alternatively we could have supplied the equivalent assumption that $d\notin \{c, b, a\}$:

set_abcde.deduce_enum_proper_subset(subset=set_cba,
        assumptions=[NotInSet(d, Set(c, b, a))])

 ⊢  

6. Deducing that $\{1, a, 1\}\subset\{1, a, 1, b, 2, a\}$ when $a=1$.

Variables and multiplicities can combine to produce some tricky cases when trying to establish subset relationships between enumerated Sets. Notice that when considering the possibility that $\{1, a, 1\}\subset\{1, a, 1, b, 2, a\}$, if it turns out that $a=b=2$, then the proper subset relation does not hold. Prove-It will not deduce the proper subset relationship without more information. Using the enumerated Set.deduce_enum_proper_subset() method, we get an error:

set_1a1 = Set(one, a, one)
set_1a1b2a = Set(one, a, one, b, two, a)
print("set_1a1 =")
display(set_1a1)
print("set_1a1b2a =")
display(set_1a1b2a)
try:
    set_1a1b2a.deduce_enum_proper_subset(subset=set_1a1)
    assert False, "Should not get to this point."
except ValueError as the_error:
    print("Proof Failure (ValueError): {}".format(the_error))

set_1a1 =

set_1a1b2a =

Proof Failure (ValueError): Failed to prove that the supposed Self superset {1, a, 1, b, 2, a} has any elements not already contained in the supposed proper subset {1, a}. Notice that this might be because the sets have unassigned variables

If we provide a little more information, however, specifying how to interpret the variable 'a', Prove-It is able to proceed (in part because now it can be proven that 2 is in the superset but not in the subset):

set_1a1b2a.deduce_enum_proper_subset(subset=set_1a1, assumptions=[Equals(a, one)])

 ⊢  

Miscellaneous Testing

The material below was developed to test various enumerated Set and Set-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

# some standard enumerated sets
from proveit import e
set_12345, set_abcde, set_1a2b3c, set_a2c13b, set_3c1ab2, power_set_of_ab, empty_set = (
    Set(one, two, three, four, five),
    Set(a, b, c, d, e),
    Set(one, a, two, b, three, c),
    Set(a, two, c, one, three, b),
    Set(three, c, one, a, b, two),
    Set(Set(), Set(a), Set(b), Set(a,b)),
    Set())

set_12345:

set_abcde:

set_1a2b3c:

set_a2c13b:

set_3c1ab2:

power_set_of_ab:

empty_set:

# some non-standard enumerated sets pretending to be multi-sets (but not!)
set_12131, set_1a1b2a = (
    Set(one, two, one, three, one),
    Set(one, a, one, b, two, a))

set_12131:

set_1a1b2a:

Testing the permutation_move() method

The permutation_move() method has the following format:

permutation_move(self, init_idx=None, final_idx=None, assumptions=USE_DEFAULTS):

and moves the element at index init_idx to position final_idx (a “pluck and insert” process).

# permuting an element in a Set of literals
Set(one, two, three, four, five).permutation_move(0, 1)

 ⊢  

# permuting an element in a Set of variables
Set(a, b, c, d, e).permutation_move(1, 3)

 ⊢  

# permuting an element in a heterogeneous Set
Set(one, a, two, b, three, c).permutation_move(3, 1)

 ⊢  

# permuting an element in a Set of Sets
power_set_of_ab.permutation_move(0, 3)

 ⊢  

# permuting an element FROM a non-existent location
# in the Set should not work
try:
    set_1a2b3c.permutation_move(6, 3)
except IndexError as the_error:
    print("Index Error: {}".format(the_error))

Index Error: 'init_idx' = 6 is out of range. Should have 0 ≤ init_idx ≤ 5.

# permuting an element TO a non-existent location
# in the Set should not work
try:
    set_1a2b3c.permutation_move(4, 6)
except IndexError as the_error:
    print("Index Error: {}".format(the_error))

Index Error: 'final_idx' = 6 is out of range. Should have 0 ≤ final_idx ≤ 5.

Testing the permutation_swap() method

The permutation_swap() method has the following format:

permutation_swap(self, idx01=None, idx02=None, assumptions=USE_DEFAULTS):

and attempts to deduce that the Set expression is equal to a Set in which the elements at index locations idx01 and idx02 have swapped locations.

# basic swap permutation
set_1a2b3c.permutation_swap(1, 4)

 ⊢  

# basic swap with irrelevant assumptions
set_1a2b3c.permutation_swap(1, 4, assumptions=[Equals(a, one)])

 ⊢  

# if idx01 > idx02
set_123.permutation_swap(1, 0)

 ⊢  

# empty swap: idx01 = idx02
set_123.permutation_swap(2, 2)

 ⊢  

# if indices not valid:
try:
    set_12345.permutation_swap(2, 6)
    assert False, "Should not make it to this point."
except IndexError as the_error:
    print("Index Error: {}".format(the_error))

Index Error: Index or indices out of bounds: {6}. Subset indices should be elements of {0, 1, 2, 3, 4}.

Testing the permutation() method

The permutation() method has the following format:

permutation(self, new_order=None, cycles=None, assumptions=USE_DEFAULTS)

where new_order is a list of the indices in the desired order, and cycles is a list of tuples designating index-based cycles, either of which derive an equivalence to a permuted version of the Set. A new_order designation must include all indices; a cycles designation need only specify the indices involved in a cycle.

# permuting an element in a Set of literals
set_12345.permutation(new_order=[1, 2, 3, 4, 0])

 ⊢  

# permuting an element in a Set of variables
set_abcde.permutation(new_order=[4, 3, 1, 0, 2])

 ⊢  

# permuting an element in a heterogeneous Set
# using cycle notation
set_1a2b3c.permutation(cycles=[(0,1),(2, 3)])

 ⊢  

# permuting an element in a Set of Sets
# using cycle notation
power_set_of_ab.permutation(cycles=[(0,2,3)])

 ⊢  

# supplying incorrect (out-of-bound) indices for the new_order
# should give an informative error
try:
    set_1a2b3c.permutation(new_order=[2, 3, 1, 5, 4, 6])
except IndexError as the_error:
    print("Index Error: {}".format(the_error))

Index Error: Index or indices out of bounds: {6}. new_order should be a list of indices i such that 0 ≤ i ≤ 5.

# supplying incomplete indices for the new_order
# should give an informative error
try:
    set_1a2b3c.permutation(new_order=[2, 0, 5, 4])
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: new_order specification is missing indices: {1, 3}.

# supplying incorrect (out-of-bound) indices for cycles
# should give an informative error
try:
    set_1a2b3c.permutation(cycles=[(1, 3, 2),(0, 6)])
    assert False, "Should not get to this line!"
except IndexError as the_error:
    print("Index Error: {}".format(the_error))

Index Error: Index or indices out of bounds: {6}. cycles should only contain indices i such that 0 ≤ i ≤ 5.

# supplying indices more than once in cycles
# notation should give an informative an error
try:
    set_1a2b3c.permutation(cycles=[(1, 3, 2),(3, 4)])
    assert False, "Should not get to this line!"
except IndexError as the_error:
    print("Index Error: {}".format(the_error))

Index Error: Index or indices duplicated in cycles specification. cycles should contain only a single instance of any specific index value.

# supplying both new_order and cycles args
# should give an informative an error
try:
    set_1a2b3c.permutation(new_order=[5,4,3,2,1,0], cycles=[(1, 3, 2)])
    assert False, "Should not get to this line!"
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: Need to specify EITHER new_order OR cycles, but not both.

Automatically proving sets are equal via permutation

Equals(set_1a2b3c, set_a2c13b).prove()

 ⊢  

Equals(set_1a2b3c, set_3c1ab2).prove()

 ⊢  

Equals(set_a2c13b, set_3c1ab2).prove()

 ⊢  

Testing the deduce_as_superset_eq_of() method

The deduce_as_superset_eq_of() method has the following format:

deduce_as_superset_eq_of(self, subset_indices=None, subset=None, **defaults_config)

where one supplies either the subset_indices OR a subset, but not both. subset_indices is a list of indices of desired subset elements of the original Set, and subset provides the desired subset as an actual enumerated Set. In using subset_indices or subset, either one, the proffered order of subset elements is preserved in the derived subset relationship.

# some non-standard enumerated sets pretending to be multi-sets (but not!)
set_12131, set_1a1b2a = (
    Set(one, two, one, three, one),
    Set(one, a, one, b, two, a))

set_12131:

set_1a1b2a:

# deducing as a superset_eq of a set of literals
set_12345.deduce_as_superset_eq_of(subset_indices=[1, 4, 3])

 ⊢  

# deducing a subset of a heterogeneous Set using subset notation
set_1a2b3c.deduce_as_superset_eq_of(subset=Set(a, two, c))

 ⊢  

Testing the deduce_enum_subset_eq() method

The deduce_enum_subset_eq() method has the following format:

deduce_enum_subset_eq(self, subset_indices=None, subset=None, assumptions=USE_DEFAULTS)

where one supplies either the subset_indices OR a subset, but not both. subset_indices is a list of indices of desired subset elements of the original Set, and subset provides the desired subset as an actual enumerated Set. In using subset_indices or subset, either one, the proffered order of subset elements is preserved in the derived subset relationship.

# deducing a subset of a Set of literals
set_12345.deduce_enum_subset_eq(subset_indices=[1, 4, 3])

 ⊢  

# deducing a subset of a Set of variables
set_abcde.deduce_enum_subset_eq(subset_indices=[2, 1, 0])

 ⊢  

# deducing a subset of a heterogeneous Set
# using subset notation
set_1a2b3c.deduce_enum_subset_eq(subset=Set(a, two, c))

 ⊢  

# deducing a subset of a Set of Sets
# using subset notation
power_set_of_ab.deduce_enum_subset_eq(subset=Set(Set(a), Set(b)))

 ⊢  

# deducing a subset of a Set
# with redundant subset elements specified
set_1a1b2a.deduce_enum_subset_eq(subset_indices=[0, 1, 2])

 ⊢  

# what if we have a variable in the supposed subset and the variable
# is equal to a value in the supposed superset?
set_12a = Set(one, two, a)
set_12345.deduce_enum_subset_eq(subset=Set(one, two, a), assumptions=[Equals(a, one)])

 ⊢  

# Works when subset = empty set
set_12131.deduce_enum_subset_eq(subset=empty_set)

 ⊢  

# Work when subset = superset = empty set
empty_set.deduce_enum_subset_eq(subset=empty_set)

 ⊢  

# supplying incorrect (out-of-bound) indices for subset
# should give an informative error
try:
    set_1a2b3c.deduce_enum_subset_eq(subset_indices=[2, 6, 0])
except IndexError as the_error:
    print("Index Error: {}".format(the_error))

Index Error: Index or indices out of bounds: {6}. Subset indices should be elements of {0, 1, 2, 3, 4, 5}.

# supplying incorrect elements for subset
# should give an informative error
try:
    set_1a2b3c.deduce_enum_subset_eq(subset=Set(a, B, two, d))
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: Specified subset {a, B, 2, d} does not appear to be a subset of the original set {1, a, 2, b, 3, c}. The following elements appear in the requested subset Set but not in the original Set: {B, d}.

Testing the deduce_enum_proper_subset() method

The deduce_enum_proper_subset() method has the following format:

deduce_enum_proper_subset(self, subset_indices=None, subset=None, assumptions=USE_DEFAULTS)

where one supplies either the subset_indices OR a subset, but not both. subset_indices is a list of indices of desired subset elements of the original Set, and subset provides the desired subset as an actual enumerated Set. In using subset_indices or subset, either one, the proffered order of subset elements is preserved in the derived subset relationship.

# deducing a subset of a Set of literals
set_12345.deduce_enum_proper_subset(subset_indices=[1, 4, 3])

 ⊢  

# deducing a subset of a Set of variables
set_abcde.deduce_enum_proper_subset(
        subset_indices=[2, 1, 0],
        assumptions=[NotEquals(d,a), NotEquals(d,b), NotEquals(d,c)])

, ,  ⊢  

# deducing a proper subset of a Set of variables
# with no additional information about the variables
try:
    set_abcde.deduce_enum_proper_subset(subset_indices=[2, 1, 0])
    assert False, "Should not make it to this point."
except ValueError as the_error:
    print("Proof Failure: {}".format(the_error))

Proof Failure: Failed to prove that the supposed Self superset {a, b, c, d, e} has any elements not already contained in the supposed proper subset {c, b, a}. Notice that this might be because the sets have unassigned variables

# deducing a proper subset of a heterogeneous Set
# Will often need more info, depending on the arrangement specified:
try:
    set_1a2b3c.deduce_enum_proper_subset(subset=Set(a, two, c))
    assert False, "Should not make it to this point."
except ValueError as the_error:
    print("Proof Failure: {}".format(the_error))

Proof Failure: Failed to prove that the supposed Self superset {1, a, 2, b, 3, c} has any elements not already contained in the supposed proper subset {a, 2, c}. Notice that this might be because the sets have unassigned variables

# but we can supply enough info to help:
set_1a2b3c.deduce_enum_proper_subset(
    subset=Set(a, two, c), assumptions=[NotInSet(one, Set(a, two, c))])

 ⊢  

# deducing a subset of a Set with redundant subset elements specified
# the variables will initially be a problem
try:
    set_1a1b2a.deduce_enum_proper_subset(subset_indices=[0, 1, 2])
    assert False, "Should not get to this point."
except ValueError as the_error:
    print("Proof Failure: {}".format(the_error))

Proof Failure: Failed to prove that the supposed Self superset {1, a, 1, b, 2, a} has any elements not already contained in the supposed proper subset {1, a}. Notice that this might be because the sets have unassigned variables

# but if we supply a single foothold, it will work; notice here that
# we supplied the info in terms of the unreduced set, but could also
# supply the info in terms of the reduced set (see next cell)
set_1a1b2a.deduce_enum_proper_subset(
    subset_indices=[0, 1, 2], assumptions=[NotInSet(b, Set(one, a, one))])

 ⊢  

# Compare to previous cell. If we supply a single foothold, it will work;
# notice here that we supplied the info in terms of the reduced set, but could also
# supply the info in terms of the un-reduced set (see previous cell)
set_1a1b2a.deduce_enum_proper_subset(
    subset_indices=[0, 1, 2], assumptions=[NotInSet(b, Set(one, a))])

 ⊢  

# Here we have a variable in the supposed proper subset and the variable
# is equal to a value in the supposed superset:
set_12345.deduce_enum_proper_subset(subset=Set(one, two, a), assumptions=[Equals(a, one)])

 ⊢  

# If we have the same variable appearing in both the subset and superset,
# even if we then assume the variable has a specific value, we can
# run into difficulties. The following works correctly though:
set_1a1b2a.deduce_enum_proper_subset(
        subset_indices=[0, 1, 2], assumptions=[Equals(a, one)])

 ⊢  

NotEquals(six, a).prove(assumptions=[Equals(a, one)])

 ⊢  

example_deduction = NotInSet(five, Set(a, two)).prove(assumptions=[Equals(a, one)])

example_deduction:  ⊢  

set_1a1b2a.deduce_enum_proper_subset(
            subset_indices=[0, 1, 2], assumptions=[NotEquals(a, two)])

 ⊢  

# Related: note that Prove-It will automatically deduce various
# non-membership claims:
NotInSet(two, Set(one, a, one)).prove(assumptions=[NotInSet(two, Set(one, a))])

 ⊢  

# Related: note that Prove-It will automatically deduce various
# non-membership claims:
NotInSet(two, Set(one, a)).prove(
        assumptions=[NotInSet(two, Set(one, a, one))])

 ⊢  

# deducing a proper subset of a Set with redundant subset elements specified
set_12131.deduce_enum_proper_subset(subset=Set(one, two, two))

 ⊢  

# Also works when the subset is the empty set
set_12131.deduce_enum_proper_subset(subset=empty_set)

 ⊢  

# Although the empty set {} is an improper subset of itself
# and the empty set is a proper subset of any non-empty set,
# the empty set is not a proper subset of itself
try:
    empty_set.deduce_enum_proper_subset(subset=empty_set)
    assert False, "Should not make it to the point."
except ValueError as the_error:
    print("Proof Failure: {}".format(the_error))

Proof Failure: Specified subset {} does not appear to be a proper subset of the original set {}. All of the superset elements appear in the specified subset.

# supplying incorrect (out-of-bound) indices for subset
# should give an informative error
try:
    set_1a2b3c.deduce_enum_proper_subset(subset_indices=[2, 6, 0])
except IndexError as the_error:
    print("Index Error: {}".format(the_error))

Index Error: Index or indices out of bounds: {6}. Subset indices should be elements of {0, 1, 2, 3, 4, 5}.

# supplying incorrect elements for subset
# should give an informative error
try:
    set_1a2b3c.deduce_enum_proper_subset(subset=Set(a, B, two, d))
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: Specified subset {a, B, 2, d} does not appear to be a subset of the original set {1, a, 2, b, 3, c}. The following elements appear in the requested subset Set but not in the original Set: {B, d}.

# Switching the subset and superset should give an error
try:
    set_123.deduce_enum_proper_subset(subset=set_123456)
    assert False, "Should not make it to this point!"
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: Specified subset {1, 2, 3, 4, 5, 6} does not appear to be a subset of the original set {1, 2, 3}. The following elements appear in the requested subset Set but not in the original Set: {5, 4, 6}.

Testing the elem_multiplicity_reduction() method

The Set.elem_multiplicity_reduction() method has the following format:

elem_multiplicity_reduction(self, elem=None, idx=None, **defaults_config)

and attempts to deduce that the Set expression is equal to the same Set in which the multiply-occurring set element specified by elem or by the 0-based position idx has been removed from the set. If elem specified, method attempts to delete the 2nd occurrence of elem from the set. If neither elem nor idx specified, method attempts to delete the first repeated element of the Set. If both elem and idx are specified, the elem param is ignored.

# A reminder of some Sets with (apparent) multiplicities
display(Set(one, two, one, three, one))
display(Set(one, a, one, b, two, a))

# remove the 2nd occurrence of the element 1
Set(one, two, one, three, one).elem_multiplicity_reduction(elem=one)

 ⊢  

# remove the element 1 occurring at 0-based index position 4
Set(one, two, one, three, one).elem_multiplicity_reduction(idx=4)

 ⊢  

# remove the element '1' occurring at 0-based index position 4
# ignoring the elem argument referring to element '3'
Set(one, two, one, three, one, three).elem_multiplicity_reduction(elem=three, idx=4)

 ⊢  

# remove the 1st occurrence of the multiply-occurring element 'a'
Set(one, a, one, b, two, a).elem_multiplicity_reduction(idx=1)

 ⊢  

# remove the 1st repetition of an element (using default args)
Set(one, a, one, b, two, a).elem_multiplicity_reduction()

 ⊢  

# reduce set by removing a non-trivially-defined multiply-occurring element
Set(one, Add(one, one), one, Add(one, one)).elem_multiplicity_reduction(elem=Add(one, one))

 ⊢  

# try reducing with default args a set with no multiplicities
try:
    Set(one, two, three).elem_multiplicity_reduction()
    assert False, "Should not make it to this point!"
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: {1, 2, 3} appears to already be in reduced form.

# try reducing a specific element with no multiplicities
try:
    Set(one, a, one, b, two, a).elem_multiplicity_reduction(elem=b)
    assert False, "Should not make it to this point!"
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: Specified element 'b' appears just 1 time in the enum Set and thus cannot be eliminated.

# try reducing a specific element that does not appear in the set
try:
    Set(one, a, one, b, two, a).elem_multiplicity_reduction(elem=c)
    assert False, "Should not make it to this point!"
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: Specified element 'c' appears zero times in the enum Set and thus cannot be eliminated.

# try reducing an element by idx when the elem occurs only once
try:
    Set(one, a, one, b, two, a).elem_multiplicity_reduction(idx=3)
    assert False, "Should not make it to this point!"
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: The element 'b' specified at index idx=3 occurs just once in the enum Set and thus cannot be eliminated.

Testing the reduction() method

The Set.reduction() method has the following format:

reduction(self, assumptions=USE_DEFAULTS)

and attempts to deduce that the Set expression is equal to the Set's support -- i.e. equal to a Set with all multiplicities reduced to 1. The resulting support Set maintains the original order of all 1st-appearing elements in the Set.

# A reminder of some Sets with (apparent) multiplicities
display(Set(one, two, one, three, one))
display(Set(one, a, one, b, two, a))

Set(one, two, one, three, one).reduction()

 ⊢  

Set(one, a, one, b, two, a).reduction()

 ⊢  

Set(one, two, three).reduction()

 ⊢  

Set().reduction()

 ⊢  

Set(one, Add(one, one), one).elem_multiplicity_reduction(idx=0)

 ⊢  

Testing the shallow_simplification() method

Currently, shallow_simplification eliminates multiplicities (see reduction) and also, if all of the elements are literal integers, puts them into a sorted order.

unsimplified_set = Set(five, two, two, six, three, one, four, five)

unsimplified_set:

unsimplified_set.simplification()

 ⊢  

Either of these may be disabled via changing the Set simplification directives.

Set.change_simplification_directives(eliminate_duplicates=False)

unsimplified_set.simplification()

 ⊢  

Set.change_simplification_directives(
    eliminate_duplicates=True, sort_if_literal_integers=False)

unsimplified_set.simplification()

 ⊢  

Testing the single_elem_substitution() method

The Set.single_elem_substitution() method has the following format:

single_elem_substitution(self, elem=None, idx=None, sub_elem=None, assumptions=USE_DEFAULTS)

and attempts to deduce that the Set expression is equal to the Set obtained when the element specified by elem or idx is replaced by sub_elem, which requires that elem = sub_elem.

# |– Replace the 1st 'a' (elem at index 1) in {1, a, 1, b, 2, a} with 2
# using idx arg
set_1a1b2a.single_elem_substitution(idx=1, sub_elem=two, assumptions=[Equals(a, two)])

 ⊢  

# |– Replace the 1st 'a' (elem at index 1) in {1, a, 1, b, 2, a} with 2
# using elem arg
set_1a1b2a.single_elem_substitution(elem=a, sub_elem=two, assumptions=[Equals(a, two)])

 ⊢  

# |– Replace the 2nd 'a' (elem at index 5) in {1, a, 1, b, 2, a} with 2
# using compound elem arg
set_1a1b2a.single_elem_substitution(elem=[a, 2], sub_elem=two, assumptions=[Equals(a, two)])

 ⊢  

# |– Replace the 1st 'e' (elem at index 4) in {a, b, c, d, e} with 4
# using idx arg
from proveit import e
set_abcde.single_elem_substitution(idx=4, sub_elem=four, assumptions=[Equals(e, four)])

 ⊢  

# We can go the other way as well, replacing a literal by a variable. Yay!
Set(one, two, three, four, five).single_elem_substitution(elem=three, sub_elem=c, assumptions=[Equals(c, three)])

 ⊢  

# And we can replace a variable with a variable. Yay!
from proveit import e
set_abcde.single_elem_substitution(elem=c, sub_elem=e, assumptions=[Equals(c, e)])

 ⊢  

# should get meaningful error message when trying to substitute for an
# element but picking a multiplicity that doesn't exist. Here there is no 2nd 'b':
try:
    set_1a1b2a.single_elem_substitution(elem=[b, 2], sub_elem=two, assumptions=[Equals(a, two)])
    assert False, "Should not make it to this point."
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: single_elem_substitution() method looked for 2 instance(s) of the elem 'b' in the set (1, a, 1, b, 2, a) but found only 1 instance(s). The elem 'b' does not appear to exist in the original set with sufficient multiplicity.

# should get meaningful error message when trying to substitute for an
# element but picking a multiplicity that doesn't make sense:
try:
    set_1a1b2a.single_elem_substitution(elem=[b, 0], sub_elem=two, assumptions=[Equals(a, two)])
    assert False, "Should not make it to this point."
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: In specifying the elem to be replaced in the call to Set.single_elem_substitution(), it doesn't appear to make sense to specify instance #0 of the element b in the set of elements (1, a, 1, b, 2, a).

# should get a meaningful error message when omitting the sub_elem argument
try:
    set_1a1b2a.single_elem_substitution(idx=1, assumptions=[Equals(a, two)])
    assert False, "Should not make it to this point."
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: single_elem_substitution() method missing sub_elem argument. Must specify the replacement value using argument 'sub_elem='.

# should get meaningful error message when trying to substitute for an
# element that doesn't exist in the original set:
try:
    set_1a1b2a.single_elem_substitution(elem=c, sub_elem=two, assumptions=[Equals(c, two)])
    assert False, "Should not make it to this point."
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: single_elem_substitution() method looked for 1 instance(s) of the elem 'c' in the set (1, a, 1, b, 2, a) but found only 0 instance(s). The elem 'c' does not appear to exist in the original set with sufficient multiplicity.

Testing the elem_substitution() method

The Set.elem_substitution() method has the following format:

elem_substitution(self, elem=None, sub_elem=None, assumptions=USE_DEFAULTS)

and attempts to deduce that the Set expression is equal to the Set obtained when all instances of the element specified by elem are replaced by sub_elem, which requires that elem = sub_elem.

# |– Replace all instances of 'a' in {1, a, 1, b, 2, a} with 2
set_1a1b2a.elem_substitution(elem=a, sub_elem=two, assumptions=[Equals(a, two)])

 ⊢  

# |– Replace all instances of 'b' in {1, a, 1, b, 2, a} with 3
set_1a1b2a.elem_substitution(elem=b, sub_elem=three, assumptions=[Equals(b, three)])

 ⊢  

Set(a, b, a, b, a).elem_substitution(elem=a, sub_elem=two, assumptions=[Equals(a, two)])

 ⊢  

# |– Replace all instances of 'e' in {a, b, c, d, e} with 4
from proveit import e
set_abcde.elem_substitution(elem=e, sub_elem=four, assumptions=[Equals(e, four)])

 ⊢  

# We can go the other way as well, replacing all instances of a literal by a variable. Yay!
# Here we replace all instances of 3 with the variable c
Set(one, two, three, four, five).elem_substitution(elem=three, sub_elem=c, assumptions=[Equals(c, three)])

 ⊢  

# And we can replace a variable with a variable. Yay!
# Here we replace all instances of c with the variable e
from proveit import e
set_abcde.elem_substitution(elem=c, sub_elem=e, assumptions=[Equals(c, e)])

 ⊢  

# What if we do a sequence of these, and then call deduce_enum_subset_eq? Is it possible to 
# get back to where we began?
# Here we show that {a, b, c, d, e} \subset_eq {1, 2, 3, d, e} when a=2, b=2, c=3.
temp_assumptions = [Equals(a, two), Equals(b, two), Equals(c, three)]
elems_to_replace = [a, b, c]
elems_sub = [two, two, three]
num_elems_to_replace = len(elems_to_replace)
from proveit import TransRelUpdater
expr = set_abcde
eq = TransRelUpdater(expr, temp_assumptions)
for i in range(0, len(elems_to_replace)):
    expr = eq.update(expr.elem_substitution(
            elem=elems_to_replace[i], sub_elem=elems_sub[i],
            assumptions=temp_assumptions, preserve_all=True))
temp_subset_eq_kt = Set(one, two, three, d, e).deduce_enum_subset_eq(subset = expr)
eq.relation.sub_left_side_into(temp_subset_eq_kt)

, ,  ⊢  

# Should get meaningful error message when trying to substitute for an
# element that doesn't exist in the original set:
try:
    set_1a1b2a.elem_substitution(elem=c, sub_elem=two, assumptions=[Equals(c, two)])
    assert False, "Should not make it to this point."
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: In calling the Set.elem_substitution() method, the element 'c' to be replaced does not appear to exist in the original set {1, a, 1, b, 2, a}.

# Should get meaningful error message when omitting the elem argument
try:
    set_1a1b2a.elem_substitution(sub_elem=two, assumptions=[Equals(c, two)])
    assert False, "Should not make it to this point."
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: Set.elem_substitution() method requires the specification of the element to be replaced and the requested substitution value, but found elem=None and sub_elem=2.

# Should get meaningful error message when omitting the sub_elem argument
try:
    set_1a1b2a.elem_substitution(elem=a, assumptions=[Equals(a, two)])
    assert False, "Should not make it to this point."
except ValueError as the_error:
    print("Value Error: {}".format(the_error))

Value Error: Set.elem_substitution() method requires the specification of the element to be replaced and the requested substitution value, but found elem=a and sub_elem=None.

Testing the membership_object() method

The Set.membership_object() method has the following format:

membership_object(self, element)

and produces an EnumMembership object of the form (element $\in$ self), which then has a number of related methods such as side_effects(), definition(), etc.

example_membership_obj_01 = Set(B,C,D).membership_object(C)

example_membership_obj_01:

# to see the explicit membership object, use the expr attribute
example_membership_obj_01.expr

example_membership_obj_02 = Set(B,C,D).membership_object(E)

example_membership_obj_02:

example_membership_obj_02.expr

membership_object().definition()

# With variables
Set(B,C,D).membership_object(C).definition()

 ⊢  

Set(B,C,D).membership_object(E).definition()

 ⊢  

# Works easily with literals
Set(one, two, three).membership_object(three).definition()

 ⊢  

# Works easily with literals
Set(one, two, three).membership_object(four).definition()

 ⊢  

# Also appears to work OK with single-element sets
Set(one).membership_object(four).definition()

 ⊢  

# Also works with single-element sets
Set(y).membership_object(x).definition()

 ⊢  

membership_object().conclude()

Set(B,C,D).membership_object(C).conclude()

 ⊢  

# Will fail to conclude without suffient info. In particular, needs to
# know the element in question is equal to one of the set elements
try:
    Set(B,C,D).membership_object(A).conclude()
    assert False, "Should not make it to this point."
except InstantiationFailure as the_error:
    print("InstantiationFailure: {}".format(the_error))

InstantiationFailure: 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: A, y: (B, C, D)}:
Unsatisfied condition: (A = B) or (A = C) or (A = D). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

# Works easily with literals
Set(one, two, three).membership_object(three).conclude()

 ⊢  

# Will fail as it should when trying to conclude a false membership claim
try:
    Set(one, two, three).membership_object(four).conclude()
    assert False, "Should not make it to this point."
except InstantiationFailure as the_error:
    print("InstantiationFailure: {}".format(the_error))

InstantiationFailure: 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.

# Notice that the conclude() method will not automatically
# simplify expressions within the list:
temp_test_set = Set(one, Add(one, one), three)
temp_test_mem = temp_test_set.membership_object(three).expr

temp_test_mem:

temp_test_mem.conclude()

 ⊢  

# Notice that the conclude() method will not automatically
# simplify expressions within the list, but can still check for equality
# (Here, 2 = 1+1, and thus the value 2 is indeed in the list)
temp_test_set_02 = Set(one, Add(one, one), three)
temp_test_mem_02 = temp_test_set.membership_object(two).expr

temp_test_mem_02:

temp_test_mem_02.conclude()

 ⊢  

membership_object().unfold()

Set(B,C,D).membership_object(C).unfold()

 ⊢  

Set(one, two, three).membership_object(three).unfold()

 ⊢  

# The unfolding will only work if the membership_object is true:
try:
    Set(one, two, three).membership_object(four).unfold()
    assert False, "Should not get to this point."
except InstantiationFailure as the_error:
    print("InstantiationFailure: {}".format(the_error))

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

membership_object().derive_in_singleton()

# The purpose of the derive_in_singleton() method is very mysterious.
Set(one, two, three).membership_object(three).derive_in_singleton(Equals(InSet(two, Set(two)), TRUE))

 ⊢  

Set(y).membership_object(x).derive_in_singleton(Equals(InSet(x, Set(y)), FALSE), assumptions=[NotEquals(x,y)])

 ⊢  

# Notice that the derived singleton membership claim can be
# completely independent of the original membership_object
Set(one, two, three).membership_object(three).derive_in_singleton(
    Equals(InSet(two, Set(two)), TRUE))

 ⊢  

membership_object().deduce_in_bool()

Set(A, B, C).membership_object(B).deduce_in_bool()

 ⊢  

Set(one, two, three).membership_object(three).deduce_in_bool()

 ⊢  

# And of course a false membership claim is also Boolean
Set(one, two, three).membership_object(four).deduce_in_bool()

 ⊢  

Testing the nonmembership_object() method

The Set.nonmembership_object() method has the following format:

nonmembership_object(self, element)

and produces an EnumNonmmembership object of the form (element $\notin$ self), along with a number of related methods such as side_effects(), equivalence(), etc.

example_nonmembership_object_01 = Set(B,C,D).nonmembership_object(A)

example_nonmembership_object_01:

example_nonmembership_object_01.expr

nonmembership_object().definition()

Set(B,C,D).nonmembership_object(A).definition()

 ⊢  

set_123.nonmembership_object(four).definition()

 ⊢  

# notice the equivalence doesn't depend on the
# nonmembership_object being true
set_123.nonmembership_object(two).definition()

 ⊢  

Set(one, two).nonmembership_object(two).definition()

 ⊢  

# Works with singletons as well
Set(one,).nonmembership_object(two).definition()

 ⊢  

# Works with singletons as well
Set(y).nonmembership_object(x).definition()

 ⊢  

nonmembership_object().conclude()

# Will fail to conclude without suffient info. In particular,
# needs to know the element in question is not equal to 
# any of the set elements
try:
    Set(B,C,D).nonmembership_object(A).conclude()
    assert False, "Should not make it to this point."
except InstantiationFailure as the_error:
    print("Proof/Instantiation Failure: {}".format(the_error))

Proof/Instantiation Failure: 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: A, y: (B, C, D)}:
Unsatisfied condition: A != B. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

# But given sufficient information, conclude() method works just fine
Set(B,C,D).nonmembership_object(A).conclude(
        assumptions=[NotEquals(A, B), NotEquals(A, C), NotEquals(A, D)])

, ,  ⊢  

# Works easily with literals
Set(one, two, three).nonmembership_object(four).conclude()

 ⊢  

# A singleton example -- requires explicit assumptions
Set(y).nonmembership_object(x).conclude(assumptions=[NotEquals(x, y)])

 ⊢  

# The conclude does not automatically simplify the expressions in the list
Set(one, Add(one, one), three).nonmembership_object(four).conclude()

 ⊢  

# # The conclude does not automatically simplify the expressions in the list
# but can still check for equalities --- in this case, the nonmembership
# is false (since 2 = 1 + 1), and thus the conclude() should fail because
# the value 2 is in {1, 1+1, 3}
try:
    Set(one, Add(one, one), three).nonmembership_object(two).conclude()
    assert False, "Expecting a ProofFailure (InstantiationFailure); should not make it this far!"
except InstantiationFailure as the_error:
    print("InstantiationFailure: {}".format(the_error))

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, 1 + 1, 3)}:
Unsatisfied condition: 2 != (1 + 1). For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

nonmembership_object().unfold()

Set(B,C,D).nonmembership_object(A).unfold(assumptions=[NotInSet(A, Set(B, C, D))])

 ⊢  

Set(one, two).nonmembership_object(A).unfold(assumptions=[NotInSet(A, Set(one, two))])

 ⊢  

Set(one, two, three).nonmembership_object(four).unfold()

 ⊢  

# Will fail to conclude if non-membership is simply known to be False.
try:
    Set(one, two, three, four).nonmembership_object(four).unfold()
    assert False, "Should not make it to this point."
except InstantiationFailure as the_error:
    print("Proof/Instantiation Failure: {}".format(the_error))

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

# Will fail to conclude if non-membership is simply unknown to be True or not.
try:
    Set(A, B, C).nonmembership_object(D).unfold()
    assert False, "Should not make it to this point."
except InstantiationFailure as the_error:
    print("Proof/Instantiation Failure: {}".format(the_error))

Proof/Instantiation Failure: Proof step failed:
Attempting to instantiate |- forall_{n in Natural} [forall_{x, y_{1}, y_{2}, ..., y_{n} | x not-in {y_{1}, y_{2}, ..., y_{n}}} ((x != y_{1}) and  (x != y_{2}) and  ... and  (x != y_{n}))] with {n: 3, x: D, y: (A, B, C)}:
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.

nonmembership_object().deduce_in_bool()

Set(A, B, C).nonmembership_object(B).deduce_in_bool()

 ⊢  

Set(one, two, three).nonmembership_object(four).deduce_in_bool()

 ⊢  

Set(one, Add(one, one), three).nonmembership_object(four).deduce_in_bool()

 ⊢  

%end demonstrations