from proveit import (Literal, defaults, USE_DEFAULTS, ProofFailure,
UnusableProof, single_or_composite_expression,
prover, equality_prover, relation_prover)
from proveit.relation import Relation
from proveit.logic.classes import InClass, ClassMembership
[docs]class InSet(InClass):
'''
Set membership is a special case of class membership, so we'll
derive from InClass for code re-use. The operators are distinct
(though the formatting is the same).
'''
# operator of the InSet operation
_operator_ = Literal(string_format='in', latex_format=r'\in',
theory=__file__)
# map (element, domain) pairs to corresponding InSet expressions
inset_expressions = dict()
def __init__(self, element, domain, *, styles=None):
element = single_or_composite_expression(element)
domain = single_or_composite_expression(domain)
InSet.inset_expressions[(element, domain)] = self
InClass.__init__(self, element, domain, operator=InSet._operator_,
styles=styles)
def negated(self):
'''
Return the negated membership expression,
element not in domain.
'''
from .not_in_set import NotInSet
return NotInSet(self.element, self.domain)
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 or there is a
known as-strong membership (with known equal elements and the
domain a subset of the desired domain).
'''
if InClass._readily_provable(
self, check_directly_known_elem_equality=(
check_directly_known_elem_equality)):
return True
if self.as_strong_known_membership() is not None:
return True
return False
[docs] @prover
def conclude(self, **defaults_config):
'''
Attempt to conclude that the element is in the domain. First
see if there is an equivalent known membership to use
(same domain). If not, see if there is a membership object
that is readily provable and conclude via that object if so.
Then check for a membership that is at least as strong with
a possibly different domain to use. Finally, defer to
InClass.conclude which defers to InRelation.conclude and
attempts simplifications.
'''
# See if the element, or something known to be equal to
# the element, is known to be a member of the domain or a subset
# of the domain.
as_strong_membership = self.as_strong_known_membership(
include_canonical_forms=False)
if as_strong_membership is not None:
if as_strong_membership.domain == self.domain:
try:
# Use an equivalent known membership.
return self.conclude_from_as_strong_membership(
as_strong_membership)
except UnusableProof:
pass
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()
as_strong_membership = self.as_strong_known_membership(
include_canonical_forms=True)
if as_strong_membership is not None:
# Use a known membership that is at least as strong.
return self.conclude_from_as_strong_membership(
as_strong_membership)
return InClass.conclude(self)
@prover
def conclude_from_as_strong_membership(self, as_strong_membership,
**defaults_config):
'''
Conclude from a membership with an equal element and a domain
that is a subset of the desired domain.
'''
from proveit.logic import Equals, SubsetEq
elem_sub = as_strong_membership.element
if as_strong_membership.domain == self.domain:
elem_sub_in_domain = as_strong_membership
else:
eq_rel = Equals(as_strong_membership.domain, self.domain)
if eq_rel.readily_provable():
# domains are equal -- just substitute the domain.
elem_sub_in_domain = eq_rel.sub_right_side_into(
as_strong_membership.inner_expr().domain)
else:
# S is a superset of R, so now we can prove x in S.
sub_rel = SubsetEq(as_strong_membership.domain, self.domain)
try:
sub_rel.prove()
except ProofFailure:
# May have been blocked to avoid infinite
# recursion.
return InClass.conclude(self)
elem_sub_in_domain = sub_rel.derive_superset_membership(
elem_sub)
if elem_sub == self.element:
return elem_sub_in_domain # done
# Just need to sub in the element for _elem_sub.
return elem_sub_in_domain.inner_expr().element.substitute(
self.element)
def as_strong_known_membership(self, include_canonical_forms=True):
'''
If there is a known membership that is as strong as this one,
where the element is known to be equal this one's element
and the domain is a subset of this one's domain, return this
as-strong known membership. Otherwise, return None.
'''
from proveit.logic import Equals, SubsetEq
known_memberships = list(
InClass.yield_known_memberships(
self.element,
include_canonical_forms=include_canonical_forms))
# First see of there is a known membership with the same domain.
for known_membership in known_memberships:
if known_membership.domain == self.domain:
# this is the best to use; we are done
return known_membership
# Next see of there is a known membership with a domain
# readily provable to be equal to this domain.
for known_membership in known_memberships:
eq_rel = Equals(known_membership.domain, self.domain)
if eq_rel.readily_provable():
return known_membership
# Finaly see of there is a known membership with a domain
# readily provable to be a subset of to this domain.
for known_membership in known_memberships:
sub_rel = SubsetEq(known_membership.domain, self.domain)
if sub_rel.readily_provable():
return known_membership
return None # No match found.
[docs]class SetMembership(ClassMembership):
def __init__(self, element, domain):
'''
Base class for any 'membership object' returned by a domain's
'membership_object' method.
'''
# The expression represented by this Membership.
if (element, domain) in InSet.inset_expressions:
expr = InSet.inset_expressions[(element, domain)]
else:
expr = InSet(element, domain)
ClassMembership.__init__(self, element, domain, expr=expr)