Source code for proveit.logic.sets.inclusion.subset_eq

from proveit import (as_expression, Literal, Operation, 
                     free_vars, safe_dummy_var,
                     Judgment, UnsatisfiedPrerequisites,
                     defaults, USE_DEFAULTS, prover, relation_prover)
from proveit import A, B, C, Q, x
from proveit import S
from .inclusion_relation import InclusionRelation


[docs]class SubsetEq(InclusionRelation): # operator of the SubsetEq operation _operator_ = Literal(string_format='subset_eq', latex_format=r'\subseteq', theory=__file__) # map left-hand-sides to SubsetEq Judgments # (populated in TransitivityRelation.derive_side_effects) known_left_sides = dict() # map right-hand-sides to SubsetEq Judgments # (populated in TransitivityRelation.derive_side_effects) known_right_sides = dict() def __init__(self, A, B, *, styles=None): ''' Create the expression for (A subset_eq B) ''' InclusionRelation.__init__(self, SubsetEq._operator_, A, B, styles=styles)
[docs] @staticmethod def reversed_operator_str(format_type): ''' Reversing subset_eq gives superset_eq. ''' return r'\supseteq' if format_type == 'latex' else 'superset_eq'
[docs] def remake_constructor(self): if self.is_reversed(): # Use the 'superset_eq' function if it is reversed. return 'superset_eq' # Use the default. return Operation.remake_constructor(self)
def _readily_provable(self, *, check_transitive_pair=False): ''' This SubsetEq relation is readily provable if the sets are provably equal or set equivalent, the corresponding Subset relation is provable, or ''' from proveit.logic import Forall, Equals, InSet, SetEquiv if hasattr(self.superset, 'readily_includes'): # If the superset has a 'readily_includes' method, we may # use it as a faster way to check if this is readily # provable. try: return self.superset.readily_includes(self.subset) except (NotImplementedError, UnsatisfiedPrerequisites): pass if Equals(self.subset, self.superset).readily_provable(): return True if SetEquiv(self.subset, self.superset).proven(): return True if InclusionRelation._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) # forall_{x in A} x in B => A subseteq B: univ_quant = Forall(_x, InSet(_x, self.superset), domain=self.subset) return univ_quant.proven()
[docs] @prover def conclude(self, **defaults_config): from proveit import ProofFailure from proveit.logic import Equals, SetOfAll, SetEquiv from . import subset_eq_via_equality # Equal sets include each other. if Equals(*self.operands.entries).readily_provable() and ( subset_eq_via_equality.is_usable()): return self.conclude_via_equality() # Equivalent sets include each other. # Using "proven" here on purpose. if SetEquiv(*self.operands.entries).proven(): return self.conclude_via_equivalence() # Check for special case of set comprehension # [{x | Q*(x)}_{x \in S}] \subseteq S if isinstance(self.subset, SetOfAll): from proveit.logic.sets.comprehension import ( comprehension_is_subset) set_of_all = self.subset if (len(set_of_all.all_instance_vars()) == 1 and set_of_all.instance_element == set_of_all.all_instance_vars()[0] and set_of_all.domain == self.superset): Q_op, Q_op_sub = ( Operation(Q, set_of_all.all_instance_vars()), set_of_all.conditions) concluded = comprehension_is_subset.instantiate( {S: set_of_all.domain, Q_op: Q_op_sub}, relabel_map={x: set_of_all.all_instance_vars()[0]}) return concluded _A, _B = self.operands.entries if hasattr(_A, 'deduce_superset_eq_relation'): return _A.deduce_superset_eq_relation(_B) if hasattr(_B, 'deduce_subset_eq_relation'): try: return _B.deduce_subset_eq_relation(_A) except (NotImplementedError, UnsatisfiedPrerequisites): pass try: # Attempt to conclude A subseteq B via # forall_{x in A} x in B. return self.conclude_as_folded() except ProofFailure as e: raise ProofFailure(self, defaults.assumptions, "Failed to conclude as folded: %s.\n" "To try to prove %s via transitive " "relations, try 'conclude_via_transitivity'." %(str(self), str(e)))
[docs] @prover def conclude_via_equality(self, **defaults_config): from . import subset_eq_via_equality return subset_eq_via_equality.instantiate( {A: self.subset, B: self.superset})
[docs] @prover def conclude_via_equivalence(self, **defaults_config): from . import subset_eq_via_equivalence return subset_eq_via_equivalence.instantiate( {A: self.subset, B: self.superset})
[docs] @prover def conclude_as_folded(self, **defaults_config): ''' Derive this folded version, A subseteq B, from the unfolded version, (forall_{x in A} x in B). ''' from . import fold_subset_eq # 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) return fold_subset_eq.instantiate( {A: self.subset, B: self.superset, x: _x})
[docs] @prover def unfold(self, elem_instance_var=None, **defaults_config): ''' From A subset_eq B, derive and return (forall_{x in A} x in B). x will be relabeled if an elem_instance_var is supplied. ''' from . import unfold_subset_eq if elem_instance_var is not None: temp_result = unfold_subset_eq.instantiate( {A: self.subset, B: self.superset}) return temp_result.instantiate( {x: elem_instance_var}, num_forall_eliminations=0) return unfold_subset_eq.instantiate( {A: self.subset, B: self.superset})
[docs] @prover def derive_superset_membership(self, element, **defaults_config): ''' From A subset_eq B and element x in A, derive x in B. ''' from . import unfold_subset_eq return unfold_subset_eq.instantiate( {A: self.subset, B: self.superset, x: element})
[docs] @prover def derive_subset_nonmembership(self, element, **defaults_config): ''' From A subset_eq B and element x not_in B, derive x not_in A. ''' from . import refined_nonmembership return refined_nonmembership.instantiate( {A: self.subset, B: self.superset, x: element})
[docs] @prover def apply_transitivity(self, other, **defaults_config): ''' Apply a transitivity rule to derive from this A subseteq B expression and something of the form B subseteq C, B subset C, or B=C to obtain A subset C or A subseteq C as appropriate. ''' from proveit.logic import Equals, SetEquiv, ProperSubset from . import (transitivity_subset_eq_subset, transitivity_subset_subset_eq, transitivity_subset_eq_subset_eq) other = as_expression(other) if isinstance(other, Equals) or isinstance(other, SetEquiv): return InclusionRelation.apply_transitivity(self, other) new_rel = None if other.subset == self.superset: if isinstance(other, ProperSubset): new_rel = transitivity_subset_eq_subset.instantiate( {A: self.subset, B: self.superset, C: other.superset}, preserve_all=True) elif isinstance(other, SubsetEq): new_rel = transitivity_subset_eq_subset_eq.instantiate( {A: self.subset, B: self.superset, C: other.superset}, preserve_all=True) elif other.superset == self.subset: if isinstance(other, ProperSubset): new_rel = transitivity_subset_subset_eq.instantiate( {A: other.subset, B: other.superset, C: self.superset}, preserve_all=True) elif isinstance(other, SubsetEq): new_rel = transitivity_subset_eq_subset_eq.instantiate( {A: other.subset, B: other.superset, C: self.superset}, preserve_all=True) if new_rel is None: raise ValueError( "Cannot perform transitivity with {0} and {1}!". format(self, other)) return new_rel.with_mimicked_style(self)
[docs] @relation_prover def deduce_in_bool(self, **defaults_config): ''' Deduce and return that this SubsetEq statement is in the Boolean set. ''' from . import subset_eq_is_bool is_bool_stmt = subset_eq_is_bool.instantiate( {A: self.normal_lhs, B: self.normal_rhs}) return is_bool_stmt.inner_expr().element.with_matching_style(self)
[docs]def superset_eq(A, B): ''' Return the expression representing (A superset_eq B), internally represented as (B subset_eq A) but with a style that reverses the direction. ''' return SubsetEq(B, A).with_styles(direction = 'reversed')