Source code for proveit.logic.sets.equivalence.set_equiv

from proveit import (as_expression, defaults, USE_DEFAULTS, UnusableProof,
                     ProofFailure, equality_prover, prover, relation_prover)
from proveit import Literal
from proveit.relation import EquivRelation, TransitivityException
from proveit.util import OrderedSet
from proveit.logic.irreducible_value import (
        IrreducibleValue, is_irreducible_value)
from proveit import A, B, C, P, f, x, y, z


[docs]class SetEquiv(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. ''' # operator for the SetEquiv relation _operator_ = Literal(string_format='equiv', latex_format=r'\cong', theory=__file__) # map Expressions to sets of Judgments of set equivalences that # involve the Expression on the left hand or right hand side. # known_equalities = dict() known_equivalences = dict() # Record the SetEquiv objects being initialized (to avoid infinite # recursion while automatically deducing an equality is in the # Boolean set). initializing = set() def __init__(self, a, b, *, styles=None): EquivRelation.__init__(self, SetEquiv._operator_, a, b, styles=styles) if self not in SetEquiv.initializing: SetEquiv.initializing.add(self) try: # proactively prove (a equiv b) in Boolean. self.deduce_in_bool() except BaseException: # may fail before the relevent _axioms_ have # been generated pass # and that's okay SetEquiv.initializing.remove(self)
[docs] def side_effects(self, judgment): ''' Derive the revised form, unfold, and derive, as universal quantifications, left/right membership conditioned on right/left membership. ''' from proveit.logic.booleans import TRUE, FALSE if (self.lhs != self.rhs): # e.g. if we don't have SetEquiv(A, A) # automatically derive the reversed form which is equivalent yield self.derive_reversed yield self.unfold yield self.derive_left_membership_via_right yield self.derive_right_membership_via_left
# STILL CHECKING ON THE RELEVANCE OF THE FOLLOWING # if hasattr(self.lhs, 'equality_side_effects'): # for side_effect in self.lhs.equality_side_effects(judgment): # yield side_effect
[docs] def negation_side_effects(self, judgment): ''' Side-effect derivations to attempt automatically for a negated equivalence. IN PROGRESS ''' yield self.deduce_not_equiv # A not_equiv B from not(A equiv B)
def _readily_provable(self, check_transitive_pair=True): from proveit import safe_dummy_var from proveit.logic import Equals, Forall, InSet lhs, rhs = self.lhs, self.rhs if Equals(lhs, rhs).readily_provable(): return True if EquivRelation._readily_provable( self, check_transitive_pair=check_transitive_pair): return True # No worry about conflicts with assumptions because the # variable will be bound by a quantifier: _x = safe_dummy_var(self, avoid_default_assumption_conflicts=False) if Forall(_x, InSet(_x, lhs), domain=rhs).proven() and ( Forall(_x, InSet(_x, rhs), domain=lhs).proven()): return True return False
[docs] @prover def 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 ''' from proveit.logic import Equals if Equals(self.lhs, self.rhs).readily_provable(): try: return self.conclude_via_reflexivity() except UnusableProof: pass try: return self.conclude_as_folded() except ProofFailure: raise ProofFailure(self, defaults.assumptions, "Unable to automatically conclude by " "standard means. To try to prove this via " "transitive implication relations, try " "'conclude_via_transitivity'.") # if self.lhs or self.rhs in (TRUE, FALSE): # try: # # Try to conclude as TRUE or FALSE. # return self.conclude_boolean_equality(assumptions) # except ProofFailure: # pass # if is_irreducible_value(self.rhs): # try: # evaluation = self.lhs.evaluation(assumptions) # if evaluation.rhs != self.rhs: # raise ProofFailure(self, assumptions, "Does not match with evaluation: %s"%str(evaluation)) # return evaluation # except SimplificationError as e: # raise ProofFailure(self, assumptions, "Evaluation error: %s"%e.message) # elif is_irreducible_value(self.lhs): # try: # evaluation = self.rhs.evaluation(assumptions) # if evaluation.rhs != self.lhs: # raise ProofFailure(self, assumptions, "Does not match with evaluation: %s"%str(evaluation)) # return evaluation.derive_reversed() # except SimplificationError as e: # raise ProofFailure(self, assumptions, "Evaluation error: %s"%e.message) # try: # Implies(self.lhs, self.rhs).prove(assumptions, automation=False) # Implies(self.rhs, self.lhs).prove(assumptions, automation=False) # # lhs => rhs and rhs => lhs, so attempt to prove lhs = rhs via lhs <=> rhs # # which works when they can both be proven to be Boolean. # try: # return Iff(self.lhs, self.rhs).derive_equality(assumptions) # except: # from proveit.logic.booleans.implication import eq_from_mutual_impl # return eq_from_mutual_impl.instantiate({A:self.lhs, B:self.rhs}, assumptions=assumptions) # except ProofFailure: # pass # """ # # Use conclude_equality if available # if hasattr(self.lhs, 'conclude_equality'): # return self.lhs.conclude_equality(assumptions) # if hasattr(self.rhs, 'conclude_equality'): # return self.rhs.conclude_equality(assumptions) # """ # Use a breadth-first search approach to find the shortest # path to get from one end-point to the other. return EquivRelation.conclude(self)
@staticmethod def WeakRelationClass(): return SetEquiv # SetEquiv is the strong and weak form @staticmethod def StrongRelationClass(): return SetEquiv # SetEquiv is the strong and weak form
[docs] @prover def conclude_via_reflexivity(self, **defaults_config): ''' Prove and return self of the form A equiv A. ''' from . import set_equiv_reflexivity, set_equiv_reflection if self.lhs == self.rhs: return set_equiv_reflexivity.instantiate({A: self.lhs}) return set_equiv_reflection.instantiate({A:self.lhs, B:self.rhs})
[docs] @prover def conclude_as_folded(self, **defaults_config): ''' From forall_{x} (x in A) = (x in B), conclude A set_equiv B. ''' from . import set_equiv_fold return set_equiv_fold.instantiate({A: self.lhs, B: self.rhs})
[docs] @prover def 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})] ''' from . import set_equiv_unfold return set_equiv_unfold.instantiate({A: self.lhs, B: self.rhs})
@prover def derive_left_membership_via_right(self, **defaults_config): ''' From A ≅ B, derive that forall_{x in B} x in A. ''' from . import left_membership_via_right return left_membership_via_right.instantiate( {A:self.lhs, B:self.rhs}) @prover def derive_right_membership_via_left(self, **defaults_config): ''' From A ≅ B, derive that forall_{x in A} x in B. ''' from . import right_membership_via_left return right_membership_via_left.instantiate( {A:self.lhs, B:self.rhs})
[docs] @prover def derive_reversed(self, **defaults_config): ''' From A set_equiv B derive B set_equiv A. This derivation is an automatic side-effect. ''' from . import set_equiv_reversal return set_equiv_reversal.instantiate({A: self.lhs, B: self.rhs})
@equality_prover("reversed", "reverse") def symmetrization(self, **defaults_config): ''' Prove (A ≅ B) = (B ≅ A). ''' from . import set_equiv_symmetry return set_equiv_symmetry.instantiate({B:self.lhs, A:self.rhs})
[docs] @prover def deduce_not_equiv(self, **defaults_config): ''' Deduce A not_equiv B assuming not(A equiv B), where self is (A equiv B). ''' from .set_not_equiv import SetNotEquiv return SetNotEquiv(self.lhs, self.rhs).conclude_as_folded()
[docs] @prover def 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. ''' from . import set_equiv_transitivity other = as_expression(other) if not isinstance(other, SetEquiv): # If the other relation is not "SetEquiv", # call from the "other" side. return other.apply_transitivity(self) other_set_equiv = other # We can assume that B set_equiv A will be a Judgment if # A set_equiv B is a Judgment because it is derived as a # side-effect. if self.rhs == other_set_equiv.lhs: return set_equiv_transitivity.instantiate( {A: self.lhs, B: self.rhs, C: other_set_equiv.rhs}, preserve_all=True) elif self.rhs == other_set_equiv.rhs: return set_equiv_transitivity.instantiate( {A: self.lhs, B: self.rhs, C: other_set_equiv.lhs}, preserve_all=True) elif self.lhs == other_set_equiv.lhs: return set_equiv_transitivity.instantiate( {A: self.rhs, B: self.lhs, C: other_set_equiv.rhs}, preserve_all=True) elif self.lhs == other_set_equiv.rhs: return set_equiv_transitivity.instantiate( {A: self.rhs, B: self.lhs, C: other_set_equiv.lhs}, preserve_all=True) else: raise TransitivityException( self, defaults.assumptions, 'Transitivity cannot be applied unless there is ' 'something in common in the set equivalences: ' '%s vs %s' % (str(self), str(other)))
[docs] @prover def 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. ''' from . import sub_left_side_into from proveit.logic import Equals Plambda = Equals._lambda_expr(lambda_map, self.rhs) return sub_left_side_into.instantiate( {A: self.lhs, B: self.rhs, P: Plambda})
[docs] @prover def 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. ''' from . import sub_right_side_into from proveit.logic import Equals Plambda = Equals._lambda_expr(lambda_map, self.lhs) return sub_right_side_into.instantiate( {A: self.lhs, B: self.rhs, P: Plambda})
def readily_in_bool(self): ''' Set equivalence is readily provable to be a Boolean if the set_equiv_is_bool theorem is usable. ''' from . import set_equiv_is_bool return set_equiv_is_bool.is_usable()
[docs] @relation_prover def deduce_in_bool(self, **defaults_config): ''' Deduce and return that this SetEquiv claim is in the Boolean set. ''' from . import set_equiv_is_bool return set_equiv_is_bool.instantiate({A: self.lhs, B: self.rhs})