Source code for proveit.numbers.functions.mon_dec_funcs

from proveit import (defaults, ExprRange, Function, Literal, Judgment,
                     UnsatisfiedPrerequisites, prover)
from proveit import n
from proveit.logic import InClass, ClassMembership, InSet, SubsetEq, SetMembership
from proveit.numbers import Interval, Real

[docs]class MonDecFuncs(Function): ''' MonDecFuncs denotes the set of monotonically-decreasing functions on some domain D and codomain C and is meant to capture and articulate properties of functions such as 1/x^2 on (0, infty). The initial development here is based on some analogous code and related concepts/structures in the VecSpaces() class, some pieces of which remain below despite their relevance still being questionable. This comment paragraph can eventually be deleted. We might eventually include a user-specifiable ordering for the domain, but assume for the time being that all orderings use the standard less than ordering < . ''' _operator_ = Literal( string_format=r'MonDecFuncs', latex_format=r'\textrm{MonDecFuncs}', theory=__file__) # A default domain may be set for convenience when determining # known memberships in MonDecFuncs. default_domain = None # Not clear this is still relevant, but might be useful. # Map functions to their known membership(s) within # MonDecFuncs(D) for some domain D. Such a membership relation # indicates that it is a monotonically-decreasing function # over the corresponding domain. known_mon_dec_funcs_memberships = dict() def __init__(self, domain, *, codomain=Real, styles=None, _operator=None): if _operator is None: _operator = MonDecFuncs._operator_ Function.__init__(self, _operator, domain, styles=styles) self.domain = domain self.codomain = codomain
[docs] def membership_object(self, element): return MonDecFuncsMembership(element, self)
@property def is_proper_class(self): ''' The collection of monotonically-decreasing functions over a domain D with codomain C consistitutes a set instead of a proper class. Thus we can use the standard InSet when considering the collection as a domain. ''' return False """ # keeping this temporarily while we evaluate its usefulness for # this MonDecFuncs context @staticmethod def get_domain(domain=None, *, may_be_none=False): ''' Return the given domain if one is provided (not None), or the default_domain if one was specified, or raise an exception. ''' if domain is not None: return domain if MonDecFuncs.default_domain is not None: return MonDecFuncs.default_domain if not may_be_none: raise ValueError("A domain for MonDecFuncs was not specified " "and MonDecFuncs.default_domain was not set.") # Not obviously relevant # @staticmethod # def yield_known_vec_spaces(vec, *, field=None): # ''' # Given a vector expression, vec, yield any vector spaces, # over the specified field, known to contain vec. # If the field is not specified, VecSpaces.default_field will # be used, and if a default has not been specified an exception # will be raised. # ''' # field = VecSpaces.get_field(field, may_be_none=True) # if vec not in InSet.known_memberships: # return # No known memberships to potentially yield. # for membership in InSet.known_memberships[vec]: # if not membership.is_applicable(): # # Skip it if it isn't usable under current default # # assumptions. # continue # # Check if the membership domain is a vector space over the # # specified field. # domain = membership.domain # vec_space = None # if (field is None and # domain in VecSpaces.known_vec_spaces_memberships): # vec_space = domain # elif (field is not None and # InClass(domain, VecSpaces(field)).proven()): # vec_space = domain # else: # try: # vec_space = including_vec_space(domain, field=field) # except NotImplementedError: # pass # if vec_space is None: # try: # vec_space_membership = deduce_as_vec_space(domain) # if vec_space_membership.domain.field == field: # vec_space = vec_space_membership.element # except NotImplementedError: # pass # if vec_space is not None: # # Match found: vec is a member of a domain # # that is a vector space over the specified field. # yield vec_space # @staticmethod # def yield_known_fields(vec_space): # ''' # Given a vector space, yield its known fields. # ''' # if vec_space in VecSpaces.known_vec_spaces_memberships: # judgments = VecSpaces.known_vec_spaces_memberships[vec_space] # for judgment in judgments: # yield judgment.expr.domain.field # THIS NEEDS WORK! NEEDS TESTING @staticmethod def yield_known_domain(mon_dec_fxn): ''' Given a monotonically-decreasing function, yield its known domain(s). ''' if mon_dec_fxn in MonDecFuncs.known_mon_dec_funcs_memberships: judgments = MonDecFuncs.known_mon_dec_funcs_memberships[mon_dec_fxn] for judgment in judgments: yield judgment.expr.domain.domain """
class MonDecFuncsMembership(SetMembership): ''' Defines methods that apply to membership in the set of monotonically-decreasing functions (MonDecFuncs), each element of which is characterized by its own domain and codomain. ''' def __init__(self, element, domain): # Realize here that the 'element' is a function (manifesting # as a Lambda map) and the 'domain' is MonDecFuncs, which # itself has a domain/codomain specification SetMembership.__init__(self, element, domain) if not isinstance(domain, MonDecFuncs): raise TypeError("domain expected to be MonDecFuncs, not %s" %domain.__class__) # analogous case for the following? # self.field = domain.field def side_effects(self, judgment): ''' Remember known MonDecFuncs memberships. ''' MonDecFuncs.known_mon_dec_funcs_memberships.setdefault( self.element, set()).add(judgment) return # generator yielding nothing yield def conclude(self): ''' Attempt to conclude this membership in a set of monotonically- decreasing functions. ''' # return deduce_as_vec_space(self.element, field=self.field) return deduce_as_mon_dec_func(self.element, domain=self.domain.domain) ## ======================== ## ## Utility Fxns ## ## Utility and details ## ## still being worked out ## ## ======================= ## # def containing_vec_space(vec, *, field): # ''' # Return a vector space over the given field which contains vec # as a member. Call the 'deduce_in_vec_space' class method on # 'vec' if there is one. Raise a NotImplementedError otherwise. # ''' # if hasattr(vec, 'deduce_in_vec_space'): # vec_in_space = vec.deduce_in_vec_space(field=field) # # Check that vec_in_space has the right form. # if (not isinstance(vec_in_space, Judgment) or # not isinstance(vec_in_space.expr, InSet)): # raise TypeError("'deduce_in_vec_space' expected to " # "return an InSet Judgment") # if vec_in_space.expr.element != vec: # raise ValueError("'deduce_in_vec_space' expected to " # "return an InSet Judgment with " # "the 'vec' as the 'element'") # vec_space = vec_in_space.domain # # Make sure we can prove vec_space is, in fact, a # # vector space. # deduce_as_vec_space(vec_space, field=field) # return vec_space # raise NotImplementedError( # "'containing_vec_space' is only implemented when " # "the element has a 'deduce_in_vec_space' method; %s " # "does not have such a method"%vec.__class__) def containing_mon_dec_func(fxn, *, domain): ''' Return a MonDecFunc over the given domain which contains 'fxn' as a member. Call the 'deduce_in_mon_dec_func' class method on 'fxn' if there is one. Raise a NotImplementedError otherwise. ''' if hasattr(vec, 'deduce_in_vec_space'): vec_in_space = vec.deduce_in_vec_space(field=field) # Check that vec_in_space has the right form. if (not isinstance(vec_in_space, Judgment) or not isinstance(vec_in_space.expr, InSet)): raise TypeError("'deduce_in_vec_space' expected to " "return an InSet Judgment") if vec_in_space.expr.element != vec: raise ValueError("'deduce_in_vec_space' expected to " "return an InSet Judgment with " "the 'vec' as the 'element'") vec_space = vec_in_space.domain # Make sure we can prove vec_space is, in fact, a # vector space. deduce_as_vec_space(vec_space, field=field) return vec_space raise NotImplementedError( "'containing_vec_space' is only implemented when " "the element has a 'deduce_in_vec_space' method; %s " "does not have such a method"%vec.__class__) # @prover # def deduce_as_vec_space(expr, *, field=None, **defaults_config): # ''' # Prove that the given expression is contained in the class of vector # spaces over some field. # ''' # from proveit.logic import CartExp # membership = None # if field is not None and InClass(expr, VecSpaces(field)).proven(): # # Already known as an appropriate vector space. # return InClass(expr, VecSpaces(field)).prove() # if isinstance(expr, CartExp): # ''' # For the Cartesian exponentiation of rational, real, or # complex numbers, we can deduce that it is a member of # the class of vector spaces over the corresponding field. # ''' # from proveit.numbers import Rational, Real, Complex # from . import ( # rational_vec_set_is_vec_space, real_vec_set_is_vec_space, # complex_vec_set_is_vec_space) # if expr.base == Rational: # membership = rational_vec_set_is_vec_space.instantiate( # {n:expr.exponent}) # elif expr.base == Real: # membership = real_vec_set_is_vec_space.instantiate({n:expr.exponent}) # elif expr.base == Complex: # membership = complex_vec_set_is_vec_space.instantiate({ # n:expr.exponent}) # else: # raise NotImplementedError( # "'deduce_as_vec_space' is not implemented " # "to handle %s"%expr) # if hasattr(expr, 'deduce_as_vec_space'): # # If there is a 'deduce_as_vec_space' class method for the # # expression, try that. # membership = expr.deduce_as_vec_space() # if membership is not None: # InClass.check_proven_class_membership( # membership, expr, VecSpaces) # if field is not None and membership.domain.field != field: # raise ValueError("'deduce_as_vec_space' proved membership in " # "vector spaces over %s, not over the requested " # "%s field"%(membership.domain.field, field)) # return membership # raise NotImplementedError( # "'deduce_as_vec_space' is only implemented when " # "the element is a CartExp expression or has a " # "'deduce_as_vec_space' method; %s " # "does not have such a method"%expr.__class__)
[docs]@prover def deduce_as_mon_dec_func(fxn, *, domain=None, strict=False, **defaults_config): ''' Prove that the Lambda-map specified by fxn is contained in the set of monotonically-decreasing functions defined over the domain. Unless strict is True, the returned proven membership may be over a broader domain (that is, a stronger statement than required). For example, we might have fxn = Lambda(x, 1/x^2) and domain = RealPos, in which case we try to prove that Lambda(x, 1/x^2) is in the set of MonDecFuncs(RealPos). ''' membership = None # This current implementation cheats to handle a specific case of # intrest. We can make this more general at a later date. from proveit import x from proveit.numbers.functions import one_over_x_sqrd_in_mon_dec_fxns from proveit.numbers import RealPos if fxn == one_over_x_sqrd_in_mon_dec_fxns.element: if domain is not None: SubsetEq(domain, RealPos).prove() return one_over_x_sqrd_in_mon_dec_fxns.instantiate({x:fxn.parameter}) if domain is not None and InSet(fxn, MonDecFuncs(domain)).proven(): # fxn already known to be a monotonically-decreasing function. return InSet(fxn, MonDecFuncs(domain)).prove() if hasattr(fxn, 'deduce_as_mon_dec_func'): # If there is a 'deduce_as_mon_dec_func' class method for the # fxn, try that. membership = fxn.deduce_as_mon_dec_func() # in the original VecSpaces.deduce_as_vec_space(), the following # checked for proper class membership before returning the # the membership; instead we are dealing with a set membership # and temporarily achieve this check manually further below # if membership is not None: # InClass.check_proven_class_membership( # membership, expr, VecSpaces) # if field is not None and membership.domain.field != field: # raise ValueError("'deduce_as_vec_space' proved membership in " # "vector spaces over %s, not over the requested " # "%s field"%(membership.domain.field, field)) # 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)) if membership is not None: if (not isinstance(membership, Judgment) or not isinstance(membership.expr, InSet) or membership.element != fxn or not isinstance(membership.domain, MonDecFuncs)): raise ValueError( "Failed ... with message to be completed!") return membership raise NotImplementedError( "'deduce_as_mon_dec_func' is not implemented for this case")