From 7f5210a3b6174ae49c09ba2717403a870210d3d2 Mon Sep 17 00:00:00 2001 From: Wayne Witzel Date: Fri, 5 Apr 2024 20:12:14 -0600 Subject: [PATCH] Prove class (or set) membership from the element side as well as the domain side via 'readily_provable_membership', if the element has this attribute, and 'deduce_membership'. This is the addendum for Issue #320. --- .../proveit/logic/classes/membership/in_class.py | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/packages/proveit/logic/classes/membership/in_class.py b/packages/proveit/logic/classes/membership/in_class.py index 4fc2292ecbf2..8b4c6683627c 100644 --- a/packages/proveit/logic/classes/membership/in_class.py +++ b/packages/proveit/logic/classes/membership/in_class.py @@ -174,11 +174,16 @@ def _readily_provable(self, check_directly_known_elem_equality=True): however. ''' from proveit.logic import Equals, is_irreducible_value + # check if this is readily provable from the domain side if hasattr(self, 'membership_object'): if self.membership_object._readily_provable(): return True element = self.element domain = self.domain + # check if this is readily provable from the element side + if hasattr(element, 'readily_provable_membership'): + if element.readily_provable_membership(domain): + return True # Try a known evaluation. if not is_irreducible_value(element): @@ -218,16 +223,23 @@ def conclude(self, **defaults_config): ''' from proveit.logic import Equals, is_irreducible_value + # check if this is readily provable from the domain side 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 + + # check if this is readily provable from the element side; + # if so, call 'deduce_membership' on the element. + if hasattr(element, 'readily_provable_membership'): + if element.readily_provable_membership(domain): + return element.deduce_membership(domain) + + # Try a known evaluation of the element. if not is_irreducible_value(element): try: evaluation = Equals.get_known_evaluation(element)