Source code for proveit.numbers.ordering.min

from proveit import (equality_prover, ExprRange, Function,
                     Literal, relation_prover)
from proveit.numbers import (
        NumberOperation, readily_provable_number_set, union_number_set)
from proveit import a, b, m, n, x, y, S


[docs]class Min(NumberOperation, Function): # operator of the Min operation. _operator_ = Literal( string_format='Min', latex_format=r'{\rm Min}', theory=__file__) def __init__(self, *operands, styles=None): NumberOperation.__init__(self, Min._operator_, operands, styles=styles) @equality_prover('defined', 'define') def definition(self, **defaults_config): ''' For the unary case, where self = Min(a), deduce and return [Min(a) = a]. For the binary case, where self = Min(a, b), deduce and return [Min(a, b)] = [ a if a >= b, b if b > a ]. For the more general case (without an ExprRange), deduce and return [Min(a_1, a_2, ..., a_m, b)] = Min(Min(a_1, a_2, ..., a_{m}), b) For the binary case, if the conditions in the conditional fxn definition are known, then the Max.shallow_simplification() method may automatically further evaluate or simplify the rhs. If such further reduction is not desired, include auto_simplify=False as an argument. For the general case with an ExprRange in the arguments, the results are unpredictable. ''' if self.operands.is_single(): from . import min_def_unary _x_sub = self.operand return min_def_unary.instantiate({x: _x_sub}) elif self.operands.is_double(): from . import min_def_bin _x_sub = self.operands[0] _y_sub = self.operands[1] return min_def_bin.instantiate({x: _x_sub, y: _y_sub}) else: from . import min_def_multi _a_sub = self.operands[0:-1] _b_sub = self.operands[-1] _m_sub = _a_sub.num_elements() return min_def_multi.instantiate( {m: _m_sub, a: _a_sub, b: _b_sub}) @equality_prover('shallow_simplified', 'shallow_simplify') def shallow_simplification(self, *, must_evaluate=False, **defaults_config): ''' Returns a proven simplification equation for this Min expression assuming the operand(s) has/have been simplified and assuming the operand(s) is/are Real. For the simple unary case Min(a), returns the proven simplification Min(a) = a. For the simple binary case Min(a, b), returns a proven simplification equation for this Min expression assuming the operands 'a' and 'b' have been simplified and that we know or have assumed that either a >= b or b > a, etc. For the more general case Min(a_1, a_2, ..., a_m, b), returns a proven simplification equation of the form self = Min(Min(a_1, a_2, ..., a_m), b), where the nested Min() call might then be further simplified. For the binary case, if the requisite relational knowledge among arguments is not to be had, we simply return the equation of the Min expression with itself. Cases involving ExprRanges are not currently handled, instead simply returning the proven judgment |- self=self. ''' from proveit.logic import Equals from proveit.numbers import LessEq if self.operands.is_single(): from . import min_def_unary _x_sub = self.operand return min_def_unary.instantiate({x: _x_sub}) # If binary and we know how operands 'a' and 'b' are related ... # elif self.operands.is_double(): # op_01, op_02 = self.operands[0], self.operands[1] # if (greater_eq(op_01, op_02).proven() # or greater_eq(op_02, op_01).proven()): # from proveit.numbers.ordering import min_def_bin # return min_def_bin.instantiate({x: op_01, y: op_02}) # If binary and we know how operands 'a' and 'b' are related ... elif self.operands.is_double(): from proveit.numbers.ordering import min_def_bin op_01, op_02 = self.operands[0], self.operands[1] if (LessEq(op_01, op_02).proven()): return min_def_bin.instantiate({x: op_01, y: op_02}) elif (LessEq(op_02, op_01).proven()): from proveit import TransRelUpdater from proveit.numbers.ordering import min_bin_args_commute expr = self eq = TransRelUpdater(expr) # begins as self = self expr = eq.update(min_bin_args_commute.instantiate( {x: op_01, y: op_02}, preserve_all=True)) # then simplify the rhs only expr = eq.update(expr.simplification()) return eq.relation # If multi-argument but no ExprRanges elif (not any([isinstance (op, ExprRange) for op in self.operands])): from . import min_def_multi _a_sub = self.operands[0:-1] _b_sub = self.operands[-1] _m_sub = _a_sub.num_elements() return min_def_multi.instantiate( {m: _m_sub, a: _a_sub, b: _b_sub}) # Otherwise no simplification. return Equals(self, self).prove() @relation_prover def deduce_in_number_set(self, number_set, **defaults_config): ''' Deduce that the Min(a_1, ..., a_n) expression produces a value in number_set. This will depend on the Min arguments a_1, ..., a_n all being known or assumed to be subsets of some superset number_set. ''' from . import min_set_closure _S_sub = number_set _a_sub = self.operands _n_sub = _a_sub.num_elements() try: return min_set_closure.instantiate( {S: _S_sub, n: _n_sub, a: _a_sub}) except Exception as the_exception: raise ValueError( "Something went wrong in Min.deduce_in_number_set(), " "with the error: {}". format(the_exception)) def readily_provable_number_set(self): ''' Return the most restrictive number set we can readily prove contains the evaluation of this number operation. ''' list_of_operand_sets = [] # find a minimal std number set for operand for operand in self.operands: operand_ns = readily_provable_number_set(operand) if operand_ns is None: return None list_of_operand_sets.append(operand_ns) # merge the resulting list of std number sets into a # single superset, if possible # We could take this further and take the most negative of the # number sets. return union_number_set(*list_of_operand_sets)