Source code for proveit.logic.classes.membership.in_class

from proveit import (Expression, Judgment, Literal, defaults, USE_DEFAULTS,
                     prover, equality_prover, relation_prover,
                     ProofFailure, UnsatisfiedPrerequisites)
from proveit.relation import Relation
from proveit.util import OrderedSet

[docs]class InClass(Relation): ''' Class membership denotes a collection of mathmematical objects that satisfy a certain common property. It is distinct from set membership, however. In particular, subsets of sets may be defined via subset comprehension, but there is no such analogue for classes. In this manner, classes can be more inclusive than sets without worrying about Russel's paradox. A class that is not a set is called a proper class. Note: Expressions objects that represent proper classes should have an attribute called 'is_proper_class' that is True. This will ensure that when such an object is used as a domain, it will automatically make an InClass condition instead of InSet. ''' # operator of the InClass operation. # The formatting is the same as InSet, but the operation is # distinct. _operator_ = Literal( string_format='in_c', latex_format=r'\underset{{\scriptscriptstyle c}}{\in}', theory=__file__) # maps elements to their known InClass Judgments. known_memberships = dict() # maps canonical forms of elements to InClass Judgments. # For example, map x to (1*x in S) if (1*x in S) is a Judgment. known_memberships_by_canonical_form = dict() # map (element, domain) pairs to corresponding InClass expressions inclass_expressions = dict() def __init__(self, element, domain, *, operator=None, styles=None): ''' Create a class membership relation indicating that the given 'element' is in the given 'domain'. If an 'operator' is provide, use this as the operator instead of InClass._operator_ (e.g., for InSet which derives from InClass but uses a distinct operator). ''' if operator is None: operator = InClass._operator_ Relation.__init__(self, operator, element, domain, styles=styles) self.element = self.operands[0] self.domain = self.operands[1] InClass.inclass_expressions[(self.element, self.domain)] = self if hasattr(self.domain, 'membership_object'): self.membership_object = self.domain.membership_object(element) if not isinstance(self.membership_object, ClassMembership): raise TypeError( "The 'membership_object' of %s is a %s which " "is not derived from %s as it should be." % (self.domain, self.membership_object.__class__, ClassMembership)) def __dir__(self): ''' If the domain has a 'membership_object' method, include methods from the object it generates. ''' if 'membership_object' in self.__dict__: return sorted(set(list(self.__dict__.keys()) + dir(self.membership_object))) else: return sorted(self.__dict__.keys()) def __getattr__(self, attr): ''' If the domain has a 'membership_object' method, include methods from the object it generates. ''' if attr in ('lhs', 'rhs'): return Relation.__getattr__(self, attr) if 'membership_object' in self.__dict__: return getattr(self.membership_object, attr) raise AttributeError
[docs] @staticmethod def reversed_operator_str(formatType): ''' Reversing \in gives \ni. Reversing "in" gives "contains". ''' if formatType=='latex': return '\ni_{C}' else: return 'contains_C'
def _record_as_proven(self, judgment): ''' Store the proven membership in known_memberships, and store the membership with the element in its canonical form in known_canonical_memberships. ''' Relation._record_as_proven(self, judgment) InClass.known_memberships.setdefault( self.element, OrderedSet()).add(judgment) InClass.known_memberships_by_canonical_form.setdefault( self.element.canonical_form(), OrderedSet()).add(judgment)
[docs] def side_effects(self, judgment): ''' If the domain has a 'membership_object' method, side effects will also be generated from the 'side_effects' object that it generates. ''' if hasattr(self, 'membership_object'): for side_effect in self.membership_object.side_effects(judgment): yield side_effect
[docs] def negation_side_effects(self, judgment): ''' Fold Not(x in S) as (x not-in S) as an automatic side-effect. ''' yield self.deduce_not_in
[docs] def negated(self): ''' Return the negated membership expression, element not in domain. ''' from .not_in_class import NotInClass return NotInClass(self.element, self.domain)
[docs] @prover def deduce_not_in(self, **defaults_config): r''' Deduce x not in C assuming not(A in C), where self = (x in C). ''' return self.negated().prove()
def _build_canonical_form(self): ''' The canonical form of this membership is based upon 'as_defined' which defines what the membership means. ''' if hasattr(self, 'membership_object'): return self.membership_object._build_canonical_form() else: return Relation._build_canonical_form(self) def _readily_provable(self, check_directly_known_elem_equality=True): ''' This membership is readily provable if the membership object indicates that it is readily provable. If check_directly_known_elem_equality is True and all else fails, we will check the first expression directly known to be equal to the element to see if its membership in the daomin is readily provable. This helps, for example, when there is an obvious definition to use. Don't apply this recursively, however. ''' from proveit.logic import Equals, is_irreducible_value if hasattr(self, 'membership_object'): if self.membership_object._readily_provable(): return True element = self.element domain = self.domain # Try a known evaluation. if not is_irreducible_value(element): try: elem_eval = Equals.get_known_evaluation(element).rhs except UnsatisfiedPrerequisites: return None return type(self)(elem_eval, self.domain).readily_provable() if check_directly_known_elem_equality: # Check the first directly known equality of the element to # see if this equal expression's membership is readily # provable. for eq_expr in Equals.yield_directly_known_eq_exprs( element, include_canonical_forms=False): if type(self)(eq_expr, domain).readily_provable( check_directly_known_elem_equality=False): return True return False return False def _readily_disprovable(self): ''' This membership is readily disprovable if the corresponding nonmembership is readily provable. ''' return self.negated().readily_provable()
[docs] @prover def conclude(self, **defaults_config): ''' Attempt to conclude that the element is in the domain. Try standard relation strategies (evaluate or somplify both sides). If that doesn't work, try using the domain-specific 'conclude' method of the membership object. ''' from proveit.logic import Equals, is_irreducible_value if hasattr(self, 'membership_object') and ( self.membership_object._readily_provable()): # Don't bother with a fancy, indirect approach if # we can readily conclude membership via the membership # object. return self.membership_object.conclude() # Try a known evaluation of the element. element = self.element domain = self.domain if not is_irreducible_value(element): try: evaluation = Equals.get_known_evaluation(element) except UnsatisfiedPrerequisites: evaluation = None if evaluation is not None: membership = type(self)(evaluation.rhs, domain) if membership.readily_provable(): membership = membership.prove() return membership.inner_expr().element.substitute( element) # Check the first directly known expression equal to the element # to see if we can prove it's membership. for eq_expr in Equals.yield_directly_known_eq_exprs( element, include_canonical_forms=False): membership_of_eq_expr = type(self)(eq_expr, domain) # Avoid applying this check recursively. if membership_of_eq_expr.readily_provable( check_directly_known_elem_equality=False): membership_of_eq_expr = membership_of_eq_expr.prove() return membership_of_eq_expr.inner_expr().element.substitute( element) break # only try the first known equal expression # Try the standard Relation strategies -- evaluate or # simplify both sides. try: return Relation.conclude(self) except ProofFailure: # Both sides are already irreducible or simplified # or we were unable to simplify either side. pass # Unable to simplify the element. Try to conclude via # the 'membership_object' if there is one. if hasattr(self, 'membership_object'): return self.membership_object.conclude() raise ProofFailure(self, defaults.assumptions, "Unable to conclude automatically; " "the domain, %s, has no 'membership_object' " "method with a strategy for proving " "membership." % self.domain)
@prover def conclude_negation(self, **defaults_config): ''' Attempt to conclude that the element is not in the domain via proving nonmembership. ''' nonmembership = self.negated() return nonmembership.prove().unfold_not_in()
[docs] @staticmethod def yield_known_memberships(element, *, include_canonical_forms=True, assumptions=USE_DEFAULTS): ''' Yield the known memberships of the given element applicable under the given assumptions. In 'include_canonical_forms' is True, then we can treat elements of the same canonical form as the same for this purpose. ''' from proveit._core_.proof import Assumption known_memberships = ( InClass.known_memberships_by_canonical_form if include_canonical_forms else InClass.known_memberships) with defaults.temporary() as tmp_defaults: if assumptions is not USE_DEFAULTS: tmp_defaults.assumptions = assumptions # Make sure we derive assumption side-effects first. Assumption.make_assumptions() if include_canonical_forms: key = element.canonical_form() else: key = element if key in known_memberships: for known_membership in known_memberships[key]: if known_membership.is_applicable(): yield known_membership
[docs] @equality_prover('shallow_simplified', 'shallow_simplify') def shallow_simplification(self, *, must_evaluate=False, **defaults_config): ''' Attempt to evaluate whether some x ∊ S is TRUE or FALSE using the 'definition' method of the domain's 'membership_object' if there is one. ''' from proveit.logic import TRUE, EvaluationError if not must_evaluate: # Don't oversimplify! # Unless 'must_evaluate' is true, we'll forgo the # treatment below. return Relation.shallow_simplification( self, must_evaluate=must_evaluate) # try a 'definition' method (via the membership object) if not hasattr(self, 'membership_object'): # Don't know what to do otherwise. return Relation.shallow_simplification( self, must_evaluate=must_evaluate) try: definition = self.membership_object.definition() except NotImplementedError: # Don't know what to do otherwise. return Relation.shallow_simplification( self, must_evaluate=must_evaluate) try: rhs_eval = definition.rhs.evaluation(automation=must_evaluate) except EvaluationError as e: if must_evaluate: raise e return Relation.shallow_simplification(self) evaluation = definition.apply_transitivity(rhs_eval) # Try also to evaluate this by deducing membership # or non-membership in case it generates a shorter proof. try: if evaluation.rhs == TRUE: self.membership_object.conclude() else: not_in_domain = self.negated() if hasattr(not_in_domain, 'nonmembership_object'): not_in_domain.nonmembership_object.conclude() except BaseException: pass return evaluation
def _deduce_canonically_equal(self, rhs): ''' Call _deduce_canonically_equal on the membership obect if there is one. ''' if hasattr(self, 'membership_object'): try: return self.membership_object._deduce_canonically_equal(rhs) except NotImplementedError: pass return Relation._deduce_canonically_equal(self, rhs)
[docs] @staticmethod def check_proven_class_membership(membership, element, class_of_class): if (not isinstance(membership, Judgment) or not isinstance(membership.expr, InClass) or membership.element != element or not isinstance(membership.domain, class_of_class)): raise ValueError( "Failed to meet expectation: %s is supposed to be a " "proven Judgment that %s is a member of a class " "represented by an Expression of type %s" %(membership, element, class_of_class))
[docs]class ClassMembership: def __init__(self, element, domain, *, expr=None): ''' Base class for any 'membership object' returned by a domain's 'membership_object' method. ''' self.element = element self.domain = domain # The expression represented by this Membership. if expr is not None: self.expr = expr if (self.element, self.domain) in InClass.inclass_expressions: self.expr = InClass.inclass_expressions[(self.element, self.domain)] else: self.expr = InClass(self.element, self.domain)
[docs] def side_effects(self, judgment): raise NotImplementedError( "Membership object, %s, has no 'side_effects' method implemented" % str( self.__class__))
def _build_canonical_form(self): ''' The canonical form of this membership is based upon 'as_defined' which defines what the membership means. ''' try: return self.as_defined().canonical_form() except NotImplementedError: # If 'as_defined' is not implemented, use the default # method of building the canonical form. return Relation._build_canonical_form(self.expr) def _readily_provable(self): ''' By default, we will determine if this membership is readily provable if its "as_defined()" expression is readily provable. ''' try: return self.as_defined().readily_provable() except NotImplementedError: # If 'as_defined' is not implemented, this default # method for determining provability can never be true. return False def _readily_disprovable(self): ''' By default, we will determine if this membership is readily disprovable if its "as_defined()" expression is readily disprovable. ''' try: return self.as_defined().readily_disprovable() except NotImplementedError: # If 'as_defined' is not implemented, this default # method for determining provability can never be true. return False
[docs] @prover def conclude(self, **defaults_config): raise NotImplementedError( "Membership object, %s, has no 'conclude' method implemented" % str( self.__class__))
[docs] @equality_prover('defined', 'define') def definition(self, **defaults_config): ''' Prove the membership equal to an expression that defines the membership. ''' raise NotImplementedError( "Membership object, %s, has no 'definition' method implemented" % str( self.__class__))
def as_defined(self): ''' Returns the expression that defines the membership. ''' raise NotImplementedError( "Membership object, %s, has no 'as_defined' method implemented" % str( self.__class__)) def _deduce_canonically_equal(self, rhs): ''' Equate 'self' to the 'rhs' via the definition. Raises NotImplementedError if 'definition' is not implemented. ''' definition = self.definition() def_eq_rhs = definition.deduce_canonically_equal(rhs) return definition.apply_transitivity(def_eq_rhs) def readily_in_bool(self, **defaults_config): ''' Unless this is overridden, we won't presume that the membership is readily provable to be boolean. ''' return False
[docs] @relation_prover def deduce_in_bool(self, **defaults_config): raise NotImplementedError( "Membership object, %s, has no 'deduce_in_bool' method implemented" % str( self.__class__))