Source code for proveit.numbers.ordering.less_eq

from proveit import (Literal, Operation, USE_DEFAULTS, as_expression,
                     UnsatisfiedPrerequisites, prover, relation_prover)
from proveit.logic import Equals
from proveit.util import OrderedSet
from proveit import a, b, c, d, x, y, z
from .number_ordering_relation import NumberOrderingRelation

[docs]class LessEq(NumberOrderingRelation): # operator of the LessEq operation. _operator_ = Literal( string_format='<=', latex_format=r'\leq', theory=__file__) # map left-hand-sides to "<=" Judgments # (populated in TransitivityRelation._record_as_proven) known_left_sides = dict() # map right-hand-sides to "<=" Judgments # (populated in TransitivityRelation._record_as_proven) known_right_sides = dict() # map canonical left hand sides to '<' Judgments paired with # canonical left hand sides. known_canonical_bounds = dict() def __init__(self, a, b, *, styles=None): r''' Create an expression representing a <= b. ''' NumberOrderingRelation.__init__(self, LessEq._operator_, a, b, styles=styles)
[docs] @staticmethod def reversed_operator_str(formatType): ''' Reversing '<=' gives '>='. ''' return r'\geq' if formatType=='latex' else '>='
[docs] def remake_constructor(self): if self.is_reversed(): # Use the 'greater_eq' function if it is reversed. return 'greater_eq' # Use the default. return Operation.remake_constructor(self)
def _record_as_proven(self, judgment): ''' Remember the canonical bound of this proven LessEq. ''' NumberOrderingRelation._record_as_proven(self, judgment) canonical_form = self.canonical_form() known_canonical_bounds = LessEq.known_canonical_bounds known_canonical_bounds.setdefault( canonical_form.lhs, OrderedSet()).add( (judgment, canonical_form.rhs)) def side_effects(self, judgment): ''' In addition to the NumberOrderingRelation side-effects, also derive a ≠ b from a < b as a side-effect. ''' for side_effect in NumberOrderingRelation.side_effects( self, judgment): yield side_effect yield self.derive_complement # if is_numeric_int(self.lhs) or is_numeric_int(self.rhs): # yield self.derive_one_side_in_real_subset def negation_side_effects(self, judgment): ''' From Not(a <= b) derive a > b as a side-effect. ''' yield self.deduce_complement_of_complement @prover def conclude(self, **defaults_config): ''' Conclude something of the form a ≤ b. ''' from proveit.numbers import (Add, Real, RealNonNeg, RealNonPos, readily_provable_number_set, deduce_number_set) if Equals(self.lower, self.upper).readily_provable(): # We can prove that a = b, therefore a ≤ b. return self.conclude_via_equality() lower, upper = self.lower, self.upper lower_ns = readily_provable_number_set( lower, _check_order_against_zero=False, default=Real) upper_ns = readily_provable_number_set( upper, _check_order_against_zero=False, default=Real) if RealNonPos.readily_includes(lower_ns) and ( RealNonNeg.readily_includes(upper_ns)): # The inequality is determined by the number sets. deduce_number_set(lower) deduce_number_set(upper) try: # If there is a known bound that is similar and at least # as strong, we can derive this bound from the known one. return self.conclude_from_known_bound() except UnsatisfiedPrerequisites: pass if ((isinstance(self.lower, Add) and self.upper in self.lower.terms.entries) or (isinstance(self.upper, Add) and self.lower in self.upper.terms.entries)): try: # Conclude an sum is bounded by one of its terms. return self.conclude_as_bounded_by_term() except UnsatisfiedPrerequisites: # If prerequisites weren't satisfied to do this, # we can still try something else. pass return NumberOrderingRelation.conclude(self)
[docs] @prover def conclude_via_equality(self, **defaults_config): ''' Conclude a ≤ b from a = b. ''' from . import relax_equal_to_less_eq return relax_equal_to_less_eq.instantiate( {x: self.operands[0], y: self.operands[1]})
@prover def conclude_as_bounded_by_term(self, **defaults_config): ''' Conclude something of the form a_1 + ... + a_i + b + c_1 + ... + c_j ≥ b assuming a_1, ..., a_i and c_1, ..., c_j all in RealNonNeg or a_1 + ... + a_i + b + c_1 + ... + c_j ≤ b assuming a_1, ..., a_i and c_1, ..., c_j all in RealNonPos ''' from proveit.numbers import Add if (isinstance(self.lower, Add) and self.upper in self.lower.terms.entries): return self.lower.bound_by_term(self.upper, use_weak_bound=True) elif (isinstance(self.upper, Add) and self.lower in self.upper.terms.entries): return self.upper.bound_by_term(self.lower, use_weak_bound=True) else: raise ValueError("LessEq.conclude_as_bounded_by_term is only " "applicable if one side of the Less " "expression is an addition and the other " "side is one of the terms") @prover def conclude_negation(self, **defaults_config): ''' Automatically conclude the negation an OrderingRelation. For example, not(7 ≤ 3) from 3 < 7. ''' from .less import Less return Less(self.upper, self.lower).derive_complement()
[docs] @relation_prover def deduce_in_bool(self, **defaults_config): from . import less_than_equals_is_bool is_bool_stmt = less_than_equals_is_bool.instantiate( {x: self.lower, y: self.upper}) return is_bool_stmt.inner_expr().element.with_matching_style(self)
[docs] @prover def unfold(self, **defaults_config): from . import less_eq_def unfolded = less_eq_def.instantiate({x: self.lower, y: self.upper}) return unfolded.inner_expr().operands[0].with_mimicked_style(self)
[docs] @prover def apply_transitivity(self, other, **defaults_config): ''' Apply a transitivity rule to derive from this x<=y expression and something of the form y<z, y<=z, z>y, z>=y, or y=z to obtain x<z or x<=z as appropriate. In the special case of x<=y and y<=x (or x>=y), derive x=z. ''' from . import (transitivity_less_eq_less, transitivity_less_less_eq, transitivity_less_eq_less_eq, symmetric_less_eq) from .less import Less other = as_expression(other) if isinstance(other, Equals): return NumberOrderingRelation.apply_transitivity( self, other) # handles this special case if other.lower == self.upper and other.upper == self.lower: # x <= y and y <= x implies that x=y return symmetric_less_eq.instantiate( {x: self.lower, y: self.upper}) elif other.lower == self.upper: if isinstance(other, Less): new_rel = transitivity_less_eq_less.instantiate( {x: self.lower, y: self.upper, z: other.upper}, preserve_all=True) elif isinstance(other, LessEq): new_rel = transitivity_less_eq_less_eq.instantiate( {x: self.lower, y: self.upper, z: other.upper}, preserve_all=True) elif other.upper == self.lower: if isinstance(other, Less): new_rel = transitivity_less_less_eq.instantiate( {x: other.lower, y: other.upper, z: self.upper}, preserve_all=True) elif isinstance(other, LessEq): new_rel = transitivity_less_eq_less_eq.instantiate( {x: other.lower, y: other.upper, z: self.upper}, preserve_all=True) else: raise ValueError( "Cannot perform transitivity with %s and %s!" % (self, other)) return new_rel.with_mimicked_style(self)
[docs] @prover def derive_negated(self, **defaults_config): ''' From a <= b, derive and return -b <= -a. ''' from proveit.numbers.negation import negated_weak_bound new_rel = negated_weak_bound.instantiate( {x: self.lower, y: self.upper}) return new_rel.with_mimicked_style(self)
# Temporarily leaving the original here while testing continues. # @prover # def deduce_complement(self, **defaults_config): # ''' # From Not(a <= b), derive and return (b < a). # ''' # from . import less_eq_complement_is_greater # return less_eq_complement_is_greater.instantiate( # {x:self.lower, y:self.upper}).derive_consequent() @prover def derive_complement(self, **defaults_config): ''' From (a <= b), derive and return Not(b < a). ''' from . import not_less_from_less_eq return not_less_from_less_eq.instantiate( {x: self.lower, y: self.upper}) @prover def deduce_complement_of_complement(self, **defaults_config): ''' From Not(a <= b), derive and return (b < a); and from (a <= b), derive and return Not(b < a). ''' from . import less_from_not_less_eq return less_from_not_less_eq.instantiate( {x: self.lower, y: self.upper}) @prover def shallow_simplification_of_negation(self, **defaults_config): ''' Prove and return Not(a <= b) = (b < a) as a simplification. ''' from . import less_eq_complement_is_greater return less_eq_complement_is_greater.instantiate( {x:self.lower, y:self.upper})
[docs] @prover def derive_shifted(self, addend, addend_side='right', **defaults_config): r''' From a <= b, derive and return a + c <= b + c where c is the given 'addend'. Assumptions may be required to prove that a, b, and c are in Real. ''' from . import less_eq_shift_add_right, less_eq_shift_add_left # , less_than_subtract if addend_side == 'right': new_rel = less_eq_shift_add_right.instantiate( {a: self.lower, b: self.upper, c: addend}) elif addend_side == 'left': new_rel = less_eq_shift_add_left.instantiate( {a: self.lower, b: self.upper, c: addend}) else: raise ValueError( "Unrecognized addend side (should be 'left' or 'right'): " + str(addend_side)) return new_rel.with_mimicked_style(self)
[docs] @prover def add_left(self, addend, *, strong=False, **defaults_config): ''' From a <= b, derive and return a + c <= b given c <= 0 Or from a >= b, derive and return a + c >= b given 0 <= c (and a, b, c are all Real) where c is the given 'addend'. If 'strong' is True, we derive the strong < (>) form and c must be provably non-zero. ''' if self.get_style('direction', 'normal') == 'reversed': # Left and right are reversed. temp_rel = self.with_styles(direction='normal') new_rel = temp_rel.add_right(addend, strong=strong) else: from . import less_eq_add_left, less_eq_add_left_strong if strong: new_rel = less_eq_add_left_strong.instantiate( {a: self.lower, b: self.upper, c: addend}) else: new_rel = less_eq_add_left.instantiate( {a: self.lower, b: self.upper, c: addend}) return new_rel.with_mimicked_style(self)
[docs] @prover def add_right(self, addend, *, strong=False, **defaults_config): ''' From a <= b, derive and return a <= b + c given 0 <= c Or from a >= b, derive and return a >= b + c given c <= 0 (and a, b, c are all Real) where c is the given 'addend'. If 'strong' is True, we derive the strong < (>) form and c must be provably non-zero. ''' if self.get_style('direction', 'normal') == 'reversed': # Left and right are reversed. temp_rel = self.with_styles(direction='normal') new_rel = temp_rel.add_left(addend, strong=strong) else: from . import less_eq_add_right, less_eq_add_right_strong if strong: new_rel = less_eq_add_right_strong.instantiate( {a: self.lower, b: self.upper, c: addend}) else: new_rel = less_eq_add_right.instantiate( {a: self.lower, b: self.upper, c: addend}) return new_rel.with_mimicked_style(self)
[docs] @prover def add(self, relation, **defaults_config): ''' From a <= b, derive and return a + c <= b + d given c <= d (and a, b, c, d are all Real). c and d are determined from the given 'relation'. ''' from . import less_eq_add_both from .less import Less if not (isinstance(relation, Less) or isinstance(relation, LessEq)): raise ValueError("Less.add 'relation' must be of type Less or " "LessEq, not %s" % str(relation.__class__)) _c = relation.lower _d = relation.upper new_rel = less_eq_add_both.instantiate( {a: self.lower, b: self.upper, c: _c, d: _d}) return new_rel.with_mimicked_style(self)
[docs] @prover def left_mult_both_sides(self, multiplier, **defaults_config): ''' Multiply both sides of the relation by the 'multiplier' on the left. ''' from proveit.numbers import greater_eq, zero, deduce_number_set from proveit.numbers.multiplication import ( weak_bound_via_right_factor_bound, reversed_weak_bound_via_right_factor_bound) was_reversed = False deduce_number_set(multiplier) if greater_eq(multiplier, zero).proven(): new_rel = weak_bound_via_right_factor_bound.instantiate( {a: multiplier, x: self.lower, y: self.upper}) elif LessEq(multiplier, zero).proven(): new_rel = reversed_weak_bound_via_right_factor_bound.instantiate( {a: multiplier, x: self.lower, y: self.upper}) was_reversed = True else: raise Exception( "Cannot left-multiply both sides of %s by %s " "without knowing the multiplier's relation with zero." %(self, multiplier)) new_rel = new_rel.with_mimicked_style(self) if was_reversed: new_rel = new_rel.with_direction_reversed() return new_rel
[docs] @prover def right_mult_both_sides(self, multiplier, **defaults_config): ''' Multiply both sides of the relation by the 'multiplier' on the right. ''' from proveit.numbers import zero, deduce_number_set from proveit.numbers.multiplication import ( weak_bound_via_left_factor_bound, reversed_weak_bound_via_left_factor_bound) was_reversed = False deduce_number_set(multiplier) if LessEq(zero, multiplier).proven(): new_rel = weak_bound_via_left_factor_bound.instantiate( {a: multiplier, x: self.lower, y: self.upper}) elif LessEq(multiplier, zero).proven(): new_rel = reversed_weak_bound_via_left_factor_bound.instantiate( {a: multiplier, x: self.lower, y: self.upper}) was_reversed = True else: raise Exception( "Cannot right-multiply both sides of %s by %s " "without knowing the multiplier's relation with zero." %(self, multiplier)) new_rel = new_rel.with_mimicked_style(self) if was_reversed: new_rel = new_rel.with_direction_reversed() return new_rel
[docs] @prover def divide_both_sides(self, divisor, **defaults_config): ''' Divide both sides of the relation by the 'divisor'. ''' from proveit.numbers import Less, zero, deduce_number_set from proveit.numbers.division import ( weak_div_from_numer_bound__pos_denom, weak_div_from_numer_bound__neg_denom) deduce_number_set(divisor) if Less(zero, divisor).proven(): thm = weak_div_from_numer_bound__pos_denom elif Less(divisor, zero).proven(): thm = weak_div_from_numer_bound__neg_denom else: raise Exception("Cannot divide both sides of %s by %s " "without knowing the divisors " "relation to zero."%(self, divisor)) new_rel = thm.instantiate( {a: divisor, x: self.lower, y: self.upper}) return new_rel.with_mimicked_style(self)
[docs] @prover def left_add_both_sides(self, addend, **defaults_config): ''' Add to both sides of the relation by the 'addend' on the left. ''' from proveit.numbers.addition import weak_bound_via_right_term_bound new_rel = weak_bound_via_right_term_bound.instantiate( {a: addend, x: self.lower, y: self.upper}) return new_rel.with_mimicked_style(self)
[docs] @prover def right_add_both_sides(self, addend, **defaults_config): ''' Add to both sides of the relation by the 'addend' on the right. ''' from proveit.numbers.addition import weak_bound_via_left_term_bound new_rel = weak_bound_via_left_term_bound.instantiate( {a: addend, x: self.lower, y: self.upper}) return new_rel.with_mimicked_style(self)
[docs] @prover def exponentiate_both_sides(self, exponent, **defaults_config): ''' Exponentiate both sides of the relation by the 'exponent'. ''' from proveit.numbers import Less, zero, deduce_number_set from proveit.numbers.exponentiation import ( exp_pos_lesseq, exp_nonneg_lesseq, exp_neg_lesseq, exp_nonpos_lesseq) # We need to know how the exponent relates to zero. deduce_number_set(exponent) LessEq.sort([zero, exponent]) if Less(zero, exponent).proven(): new_rel = exp_pos_lesseq.instantiate( {a: exponent, x: self.lower, y: self.upper}) elif Less(exponent, zero).proven(): new_rel = exp_neg_lesseq.instantiate( {a: exponent, x: self.lower, y: self.upper}) elif LessEq(zero, exponent).proven(): new_rel = exp_nonneg_lesseq.instantiate( {a: exponent, x: self.lower, y: self.upper}) elif LessEq(exponent, zero).proven(): new_rel = exp_nonpos_lesseq.instantiate( {a: exponent, x: self.lower, y: self.upper}) else: raise Exception("Cannot exponentiate both sides of %s by %s " "without knowing the exponent's relation with " "zero"%(self, exponent)) return new_rel.with_mimicked_style(self)
@prover def derive_one_side_in_real_subset(self, **defaults_config): # FINISH THIS UP # check for one side or the other equal to some literal number # go for RealPos, RealNeg, RealNonNeg, etc # using conclude_via_transitivity # actually can put this one level up in the number_ordering_relation pass
[docs]def greater_eq(a, b): ''' Return an expression representing a >= b, internally represented as b <= a but with a style that reverses the direction. ''' return LessEq(b, a).with_styles(direction='reversed')