SetEquiv

class proveit.logic.SetEquiv(a, b, *, styles=None)

Bases: proveit.relation.equiv_relation.EquivRelation

Class to capture the membership equivalence of 2 sets A and B. SetEquiv(A, B) is a claim that all elements of A are also elements of B and vice-versa. The SetEquiv relation uses the congruence symbol to distinguish the SetEquiv claim from the stronger claim that A = B.

Attributes Summary

initializing
known_equivalences

Methods Summary

apply_transitivity(self, other, …)	From A set_equiv B (self) and B set_equiv C (other) derive and return A set_equiv C.
conclude(self, \*\*defaults_config)	Attempt to conclude the equivalence in various ways: simple reflexivity (A equiv A), via an evaluation (if one side is an irreducible), or via transitivity.
conclude_as_folded(self, \*\*defaults_config)	From forall_{x} (x in A) = (x in B), conclude A set_equiv B.
conclude_via_reflexivity(self, …)	Prove and return self of the form A equiv A.
deduce_in_bool(self, \*\*defaults_config)	Deduce and return that this SetEquiv claim is in the Boolean set.
deduce_not_equiv(self, \*\*defaults_config)	Deduce A not_equiv B assuming not(A equiv B), where self is (A equiv B).
derive_reversed(self, \*\*defaults_config)	From A set_equiv B derive B set_equiv A.
negation_side_effects(self, judgment)	Side-effect derivations to attempt automatically for a negated equivalence.
side_effects(self, judgment)	Derive the revised form, unfold, and derive, as universal quantifications, left/right membership conditioned on right/left membership.
sub_left_side_into(self, lambda_map, …)	From A equiv B, and given P(B), derive P(A) assuming P(B).
sub_right_side_into(self, lambda_map, …)	From A equiv B, and given P(A), derive P(B) assuming P(A).
unfold(self, \*\*defaults_config)	From A set_equiv B derive forall_{x} [(x in A) = (x in B)]. A set_equiv B must be known, provable, or assumed to be True. For example, SetEquiv(Set(1, 2, 3), Set(a, b, c)).unfold( assumptions=[SetEquiv(Set(1, 2, 3), Set(a, b, c))]) returns: SetEquiv({1, 2, 3}, {a, b, c}) |- forall_{x} [(x in {1, 2, 3}) = (x in {a, b, c})].

Attributes Documentation

initializing = {}

known_equivalences = {}

Methods Documentation

apply_transitivity(self, other, \*\*defaults_config)

From A set_equiv B (self) and B set_equiv C (other) derive and return A set_equiv C. If “other” is not a SetEquiv, reverse roles and call ‘apply_transitivity’ from the “other” side. This method initially based on the apply_transitivity method from Equals class.

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

conclude(self, \*\*defaults_config)

Attempt to conclude the equivalence in various ways: simple reflexivity (A equiv A), via an evaluation (if one side is an irreducible), or via transitivity. IN PROGRESS

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

conclude_as_folded(self, \*\*defaults_config)

From forall_{x} (x in A) = (x in B), conclude A set_equiv B.

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

conclude_via_reflexivity(self, \*\*defaults_config)

Prove and return self of the form A equiv A.

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

deduce_in_bool(self, \*\*defaults_config)

Deduce and return that this SetEquiv claim is in the Boolean set.

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

deduce_not_equiv(self, \*\*defaults_config)

Deduce A not_equiv B assuming not(A equiv B), where self is (A equiv B).

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

derive_reversed(self, \*\*defaults_config)

From A set_equiv B derive B set_equiv A. This derivation is an automatic side-effect.

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

negation_side_effects(self, judgment)

Side-effect derivations to attempt automatically for a negated equivalence. IN PROGRESS

side_effects(self, judgment)

Derive the revised form, unfold, and derive, as universal quantifications, left/right membership conditioned on right/left membership.

sub_left_side_into(self, lambda_map, \*\*defaults_config)

From A equiv B, and given P(B), derive P(A) assuming P(B). UNDER CONSTRUCTION, adapted from Equals class. P(x) is provided via lambda_map as a Lambda expression or an object that returns a Lambda expression when calling lambda_map() (see proveit.lambda_map, proveit.lambda_map.SubExprRepl in particular), or, if neither of those, an expression upon which to perform a global replacement of self.rhs.

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

sub_right_side_into(self, lambda_map, \*\*defaults_config)

From A equiv B, and given P(A), derive P(B) assuming P(A). UNDER CONSTRUCTION, adapted from Equals class. P(x) is provided via lambda_map as a Lambda expression or an object that returns a Lambda expression when calling lambda_map() (see proveit.lambda_map, proveit.lambda_map.SubExprRepl in particular), or, if neither of those, an expression upon which to perform a global replacement of self.lhs.

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

unfold(self, \*\*defaults_config)

From A set_equiv B derive forall_{x} [(x in A) = (x in B)]. A set_equiv B must be known, provable, or assumed to be True. For example,

SetEquiv(Set(1, 2, 3), Set(a, b, c)).unfold(

assumptions=[SetEquiv(Set(1, 2, 3), Set(a, b, c))])

returns:

SetEquiv({1, 2, 3}, {a, b, c}) |- forall_{x} [(x in {1, 2, 3}) = (x in {a, b, c})]

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