Set

class proveit.logic.Set(*elems, styles=None)

Bases: proveit.Function

Defines an enumerated set (i.e. a set with explicitly-listed elements). For example, one could use Set(one, two, three) to produce the enumerated set {1, 2, 3} or Set(a, b, a) to produce the enumerated set {a, b, a}. Although repeated elements can be specified and will appear in output expressions, the Set is interpreted as a set and not a multiset — thus, e.g., we have {a, b, a} = {a, b} and the cardinality of an enumerated Set such as {a, b, a} should be the cardinality of the underlying support {a, b}.

Methods Summary

deduce_enum_proper_subset(self[, …])	Deduce that this Set expression has as a proper subset the set specified by either (a) the indices in the subset_indices list OR (b) the Set specified by subset (but not both). For example, both {a, b, c, d}.deduce_enum_proper_subset(subset_indices=[1, 3]) and {a, b, c, d}.deduce_enum_proper_subset(subset=Set(b, d)) return |– {b, d} subset {a, b, c, d} (assuming the appropriate knowledge about either a or c (or both) not being elements of the subset {b, d}). This process is complicated by the fact that the Set class allows for multiplicity of elements without actually representing a multi-set (thus, for example, {a, a} = {a}). Recall that the subset_eq and superset_eq notations are style- variants of each other, so we are simply calling the deduce_as_proper_superset_of() method then using the with_styles() method to reverse the order of the relation.
deduce_enum_subset_eq(self[, …])	Deduce that this Set expression has as an improper subset the set specified by either the indices in subset_indices list or the Set() specified by subset (but not both). For example, both {a, b, c, d}.deduce_enum_subset_eq(subset_indices=[1, 3]) and {a, b, c, d}.deduce_enum_subset_eq(subset=Set(b, d)) return |– {b, d} subset_eq {a, b, c, d}. This process is complicated by the fact that the Set class allows for multiplicity of elements without actually representing a multi-set (thus, for example, {a, a} = {a}). Recall that the subset_eq and superset_eq notations are style- variants of each other, so we are simply calling the deduce_as_superset_eq_of() method then using the with_styles() method to reverse the order of the relation.
elem_substitution(self[, elem, sub_elem])	Deduce that this enum Set expression is equal to the Set obtained when every instance of elem in self is replaced by the sub_elem. The deduction depends on the sub_elem being equal to the elem it is replacing. Examples: Let S = Set(a, b, a, b, a, c). Then S.elem_substitution() gives ERROR; S.elem_substitution(elem=d, sub_elem=two, assumptions=[Equals(d, two)] gives ERROR; S.elem_substitution(elem=b, sub_elem=four, assumptions=[Equals(b, four)]) gives |- S = {a, 4, a, 4, a, c}; S.single_elem_substitution(elem=a, sub_elem=two, assumptions=[Equals(a, two)]) gives |- S = {2, b, 2, b, 2, c}; S.single_elem_substitution(elem=c, sub_elem=d, assumptions=[Equals(c, d)]) gives |- S = {a, b, a, b, a, d};.
latex(self, \*\*kwargs)	Return a latex-formatted representation of the Expression.
membership_object(self, element)
moved(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘permutation_move’.
nonmembership_object(self, element)
permutation(self[, new_order, cycles])	Deduce that this Set expression is equal to a Set in which the elements at indices 0, 1, …, n-1 have been reordered as specified EITHER by the new_order list OR by the cycles list parameter. For example, {a, b, c, d}.permutation_general(new_order=[0, 2, 3, 1]) and {a, b, c, d}.permutation_general(cycles=[(1, 2, 3)]) would both return |- {a, b, c, d} = {a, c, d, b}.
permutation_move(self[, init_idx, final_idx])	Deduce that this Set expression is equal to a Set in which the element at index init_idx has been moved to final_idx.
permutation_swap(self[, idx01, idx02])	Deduce that this Set expression is equal to a Set in which the elements at indices idx01 and idx02 have swapped locations. For example, {a, b, c, d, e}.permutation_swap(2, 4) would return |– {a, b, c, d, e} = {a, b, e, d, c}.
permuted(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘permutation’.
prove_by_cases(self, forall_stmt, …)	For the enumerated set S = {x1, x2, …, xn} (i.e.
reduced(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘reduction’.
reduction(self, \*\*defaults_config)	Deduce that this enum Set expression is equal to the Set’s support – i.e. equal to a Set with all multiplicities reduced to 1.
single_elem_substitution(self[, elem, idx, …])	Deduce that this enum Set expression is equal to a Set in which the element specified either by elem or by the position idx has been replaced with sub_elem. The deduction depends on the sub_elem being equal to the replace elem. If elem specified in the form elem=’elem’, method attempts to substitute for the 1st occurrence of elem; if elem=[‘elem’,n], method attempts to substitute for the nth occurrence of elem. If both elem and idx are specified, the elem arg is ignored. Examples: Let S = Set(a, b, a, b, a, c). Then S.single_elem_substitution() gives error; S.single_elem_substitution(elem=b, sub_elem=four, assumptions=[Equals(b, four)]) gives |- S = {a, 4, a, b, a, c}; S.single_elem_substitution(elem=[b, 2], sub_elem=four, assumptions=[Equals(b, four)]) gives |- S = {a, b, a, 4, a, c}; S.single_elem_substitution(idx=3, sub_elem=four, assumptions=[Equals(b, four)]) gives |- S = {a, b, a, 4, a, c};.
string(self, \*\*kwargs)	Return a string representation of the Expression.
swapped(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘permutation_swap’.

Methods Documentation

deduce_enum_proper_subset(self, subset_indices=None, subset=None, \*\*defaults_config)

Deduce that this Set expression has as a proper subset the set specified by either (a) the indices in the subset_indices list OR (b) the Set specified by subset (but not both). For example, both {a, b, c, d}.deduce_enum_proper_subset(subset_indices=[1, 3]) and {a, b, c, d}.deduce_enum_proper_subset(subset=Set(b, d)) return |– {b, d} subset {a, b, c, d} (assuming the appropriate knowledge about either a or c (or both) not being elements of the subset {b, d}). This process is complicated by the fact that the Set class allows for multiplicity of elements without actually representing a multi-set (thus, for example, {a, a} = {a}). Recall that the subset_eq and superset_eq notations are style- variants of each other, so we are simply calling the deduce_as_proper_superset_of() method then using the with_styles() method to reverse the order of the relation.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_enum_subset_eq(self, subset_indices=None, subset=None, \*\*defaults_config)

Deduce that this Set expression has as an improper subset the set specified by either the indices in subset_indices list or the Set() specified by subset (but not both). For example, both {a, b, c, d}.deduce_enum_subset_eq(subset_indices=[1, 3]) and {a, b, c, d}.deduce_enum_subset_eq(subset=Set(b, d)) return |– {b, d} subset_eq {a, b, c, d}. This process is complicated by the fact that the Set class allows for multiplicity of elements without actually representing a multi-set (thus, for example, {a, a} = {a}). Recall that the subset_eq and superset_eq notations are style- variants of each other, so we are simply calling the deduce_as_superset_eq_of() method then using the with_styles() method to reverse the order of the relation.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

elem_substitution(self, elem=None, sub_elem=None, \*\*defaults_config)

Deduce that this enum Set expression is equal to the Set obtained when every instance of elem in self is replaced by the sub_elem. The deduction depends on the sub_elem being equal to the elem it is replacing. Examples: Let S = Set(a, b, a, b, a, c). Then S.elem_substitution() gives ERROR; S.elem_substitution(elem=d, sub_elem=two,

assumptions=[Equals(d, two)] gives ERROR;

S.elem_substitution(elem=b, sub_elem=four,

assumptions=[Equals(b, four)])

gives |- S = {a, 4, a, 4, a, c};

S.single_elem_substitution(elem=a, sub_elem=two,

assumptions=[Equals(a, two)])

gives |- S = {2, b, 2, b, 2, c};

S.single_elem_substitution(elem=c, sub_elem=d,

assumptions=[Equals(c, d)])

gives |- S = {a, b, a, b, a, d};

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘elem_substituted’ returns the right-hand side of ‘elem_substitution’. ‘elem_substitute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘elem_substitution’ for the inner expression.

latex(self, \*\*kwargs)

Return a latex-formatted representation of the Expression. The kwargs can contain formatting directives (such as ‘fence’ used to indicate when a sub-expression should be wrapped in parentheses if there can be ambiguity in the order of operations).

membership_object(self, element)

moved(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘permutation_move’.

nonmembership_object(self, element)

permutation(self, new_order=None, cycles=None, \*\*defaults_config)

Deduce that this Set expression is equal to a Set in which the elements at indices 0, 1, …, n-1 have been reordered as specified EITHER by the new_order list OR by the cycles list parameter. For example,

{a, b, c, d}.permutation_general(new_order=[0, 2, 3, 1])

and

{a, b, c, d}.permutation_general(cycles=[(1, 2, 3)])

would both return |- {a, b, c, d} = {a, c, d, b}.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘permuted’ returns the right-hand side of ‘permutation’. ‘permute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘permutation’ for the inner expression.

permutation_move(self, init_idx=None, final_idx=None, \*\*defaults_config)

Deduce that this Set expression is equal to a Set in which the element at index init_idx has been moved to final_idx. For example, {a, b, c, d} = {a, c, b, d} via init_idx = 1 (i.e. ‘b’) and final_idx = -2. In traditional cycle notation, this corresponds to an index-based cycle (init_idx, init_idx+1, …, final_idx) where 0 ≤ init_idx ≤ final_idx ≤ n - 1 for a set of size n.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘moved’ returns the right-hand side of ‘permutation_move’. ‘move’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘permutation_move’ for the inner expression.

permutation_swap(self, idx01=None, idx02=None, \*\*defaults_config)

Deduce that this Set expression is equal to a Set in which the elements at indices idx01 and idx02 have swapped locations. For example, {a, b, c, d, e}.permutation_swap(2, 4) would return |– {a, b, c, d, e} = {a, b, e, d, c}

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘swapped’ returns the right-hand side of ‘permutation_swap’. ‘swap’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘permutation_swap’ for the inner expression.

permuted(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘permutation’.

prove_by_cases(self, forall_stmt, \*\*defaults_config)

For the enumerated set S = {x1, x2, …, xn} (i.e. self), and given a universal quantification over the set S of the form Forall_{x in S} P(x), conclude and return the Forall expression knowing/assuming [P(x1) and P(x2) and … P(xn)]. This also addresses the case where we have Forall_{x in S | Q(x) ^ Q(x) => P(x)} P(x).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

reduced(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘reduction’.

reduction(self, \*\*defaults_config)

Deduce that this enum Set expression is equal to the Set’s support – i.e. equal to a Set with all multiplicities reduced to 1. For example, the Set(a, a, b, b, c, d)={a, a, b, b, c, d} is equal to its support {a, b, c, d}. The deduction is achieved by successively applying the element-by-element elem_multiplicity_reduction() method until no further reduction is possible.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘reduced’ returns the right-hand side of ‘reduction’. ‘reduce’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘reduction’ for the inner expression.

single_elem_substitution(self, elem=None, idx=None, sub_elem=None, \*\*defaults_config)

Deduce that this enum Set expression is equal to a Set in which the element specified either by elem or by the position idx has been replaced with sub_elem. The deduction depends on the sub_elem being equal to the replace elem. If elem specified in the form elem=’elem’, method attempts to substitute for the 1st occurrence of elem; if elem=[‘elem’,n], method attempts to substitute for the nth occurrence of elem. If both elem and idx are specified, the elem arg is ignored. Examples: Let S = Set(a, b, a, b, a, c). Then S.single_elem_substitution() gives error; S.single_elem_substitution(elem=b, sub_elem=four,

assumptions=[Equals(b, four)])

gives |- S = {a, 4, a, b, a, c};

S.single_elem_substitution(elem=[b, 2], sub_elem=four,

assumptions=[Equals(b, four)])

gives |- S = {a, b, a, 4, a, c};

S.single_elem_substitution(idx=3, sub_elem=four,

assumptions=[Equals(b, four)])

gives |- S = {a, b, a, 4, a, c};

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘single_elem_substituted’ returns the right-hand side of ‘single_elem_substitution’. ‘single_elem_substitute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘single_elem_substitution’ for the inner expression.

string(self, \*\*kwargs)

Return a string representation of the Expression. The kwargs can contain formatting directives (such as ‘fence’ used to indicate when a sub-expression should be wrapped in parentheses if there can be ambiguity in the order of operations).

swapped(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘permutation_swap’.