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 Less(NumberOrderingRelation):
# operator of the Less operation.
_operator_ = Literal(string_format='<', 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, lhs, rhs, *, styles=None):
r'''
Create an expression of the form lhs < rhs.
'''
NumberOrderingRelation.__init__(self, Less._operator_, lhs, rhs,
styles=styles)
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 = Less.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_not_equal
yield self.derive_complement
def negation_side_effects(self, judgment):
'''
From Not(a < b) derive a >= b as a side-effect.
'''
yield self.deduce_complement_of_complement
[docs] @staticmethod
def reversed_operator_str(formatType):
'''
Reversing '<' gives '>'.
'''
return '>'
[docs] def remake_constructor(self):
if self.is_reversed():
# Use the 'greater' function if it is reversed.
return 'greater'
# Use the default.
return Operation.remake_constructor(self)
[docs] @prover
def conclude(self, **defaults_config):
'''
Conclude something of the form
a < b.
'''
from proveit.numbers import (Add, Real, RealPos, RealNeg,
RealNonPos, RealNonNeg,
readily_provable_number_set,
deduce_number_set)
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
RealPos.readily_includes(upper_ns)) or (
RealNeg.readily_includes(lower_ns) and
RealNonNeg.readily_includes(upper_ns)):
# The inequality is determined by the number sets.
deduce_number_set(upper)
deduce_number_set(lower)
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(lower, Add) and upper in lower.terms.entries) or
(isinstance(upper, Add) and lower in 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)
@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 RealPos
and i + j > 0
or
a_1 + ... + a_i + b + c_1 + ... + c_j < b
assuming a_1, ..., a_i and c_1, ..., c_j all in RealNeg
and i + j > 0
'''
from proveit.numbers import Add, one
from proveit.numbers.ordering import (less_than_successor,
less_than_left_successor,
less_than_an_increase,
less_than_an_left_increase)
if (isinstance(self.lower, Add) and
self.upper in self.lower.terms.entries):
concluded = self.lower.bound_by_term(self.upper)
elif (isinstance(self.upper, Add) and
self.lower in self.upper.terms.entries):
if self.upper.terms.is_double():
# special binary cases
if self.lower == self.upper.terms[0]:
if self.upper.terms[1] == one:
# a + 1 > a
concluded = less_than_successor.instantiate(
{a: self.lower})
else:
# a + b > a assuming b in RealPos
concluded = less_than_an_increase.instantiate(
{a: self.lower, b: self.upper.terms[1]})
else:
assert self.lower == self.upper.terms[1]
if self.upper.terms[0] == one:
# 1 + a > a
concluded = less_than_left_successor.instantiate(
{a: self.lower})
else:
# b + a > a assuming b in RealPos
concluded = less_than_an_left_increase.instantiate(
{a: self.lower, b: self.upper.terms[0]})
else:
concluded = self.upper.bound_by_term(self.lower)
else:
raise ValueError("Less.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")
return concluded
@prover
def conclude_negation(self, **defaults_config):
'''
Automatically conclude the negation an OrderingRelation.
For example, not(7 < 3) from 3 ≤ 7.
'''
from .less_eq import LessEq
return LessEq(self.upper, self.lower).derive_complement()
def readily_in_bool(self):
'''
Number ordering relation is readily provable as a Boolean iff
both sides are readily provable as real numbers.
'''
from proveit.logic import InSet
from proveit.numbers import Real
return InSet(self.lhs, Real).readily_provable() and (
InSet(self.rhs, Real).readily_provable())
[docs] @relation_prover
def deduce_in_bool(self, **defaults_config):
from . import less_than_is_bool
is_bool_stmt = less_than_is_bool.instantiate(
{x: self.lower, y: self.upper})
return is_bool_stmt.inner_expr().element.with_matching_style(self)
[docs] @prover
def derive_relaxed(self, **defaults_config):
'''
Relax a < b to a <= b, deducing the latter from the former
(self) and returning the latter. Assumptions may be required
to deduce that a and b are in Real.
'''
from . import relax_less
new_rel = relax_less.instantiate(
{x: self.lower, y: self.upper})
return new_rel.with_mimicked_style(self)
@prover
def derive_not_equal(self, **defaults_config):
'''
Derive a ≠ b from a < b.
'''
from proveit.numbers.ordering import less_is_not_eq
_a, _b = self.lower, self.upper
return less_is_not_eq.instantiate({a: _a, b: _b})
[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.
'''
from . import transitivity_less_less
from . import transitivity_less_less_eq
from . import transitivity_less_eq_less
from .less_eq import LessEq
other = as_expression(other)
if isinstance(other, Equals):
return NumberOrderingRelation.apply_transitivity(
self, other) # handles this special case
elif other.lower == self.upper:
if isinstance(other, Less):
new_rel = transitivity_less_less.instantiate(
{x: self.lower, y: self.upper, z: other.upper},
preserve_all=True)
elif isinstance(other, LessEq):
new_rel = transitivity_less_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.instantiate(
{x: other.lower, y: self.lower, z: self.upper},
preserve_all=True)
elif isinstance(other, LessEq):
new_rel = transitivity_less_eq_less.instantiate(
{x: other.lower, y: self.lower, 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)
@prover
def derive_negated(self, **defaults_config):
'''
From a < b, derive and return -b < -a.
'''
from proveit.numbers.negation import negated_strong_bound
new_rel = negated_strong_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_complement_is_greater_eq
# return less_complement_is_greater_eq.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_eq_from_less
return not_less_eq_from_less.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.
'''
from . import less_eq_from_not_less
return less_eq_from_not_less.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_complement_is_greater_eq
return less_complement_is_greater_eq.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_shift_add_right, less_shift_add_left
if addend_side == 'right':
new_rel = less_shift_add_right.instantiate(
{a: self.lower, b: self.upper, c: addend})
elif addend_side == 'left':
new_rel = less_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=True, **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 False, we derive the weak ≤ (≥) form
(same as if we use the derive_relaxed method on the result).
'''
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 proveit.logic import InSet
from proveit.numbers import Integer
_a, _b, _c = self.lower, self.upper, addend
if strong:
from . import less_add_left
new_rel = less_add_left.instantiate({a:_a, b:_b, c:_c})
else:
if InSet(_a, Integer).readily_provable() and (
InSet(_b, Integer).readily_provable() and
InSet(_c, Integer).readily_provable()):
from . import less_add_left_weak_int
thm = less_add_left_weak_int
else:
from . import less_add_left_weak
thm = less_add_left_weak
new_rel = thm.instantiate({a:_a, b:_b, c:_c})
return new_rel.with_mimicked_style(self)
[docs] @prover
def add_right(self, addend, *, strong=True, **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 False, we derive the weak ≤ (≥) form
(same as if we use the derive_relaxed method on the result).
'''
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 proveit.logic import InSet
from proveit.numbers import Integer
_a, _b, _c = self.lower, self.upper, addend
if strong:
from . import less_add_right
new_rel = less_add_right.instantiate({a:_a, b:_b, c:_c})
else:
if InSet(_a, Integer).readily_provable() and (
InSet(_b, Integer).readily_provable() and
InSet(_c, Integer).readily_provable()):
from . import less_add_right_weak_int
thm = less_add_right_weak_int
else:
from . import less_add_right_weak
thm = less_add_right_weak
new_rel = thm.instantiate({a:_a, b:_b, c:_c})
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 or
given c <= d (and a, b, c, d are all Real). c and d are
determined from the given 'relation'.
'''
from . import less_add_both
from .less_eq import LessEq
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_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 Less, LessEq, zero, deduce_number_set
from proveit.numbers.multiplication import (
strong_bound_via_right_factor_bound,
weak_bound_via_right_factor_bound,
reversed_strong_bound_via_right_factor_bound,
reversed_weak_bound_via_right_factor_bound)
was_reversed = False
deduce_number_set(multiplier)
if Less(zero, multiplier).proven():
new_rel = strong_bound_via_right_factor_bound.instantiate(
{a: multiplier, x: self.lower, y: self.upper})
elif Less(multiplier, zero).proven():
new_rel = reversed_strong_bound_via_right_factor_bound.instantiate(
{a: multiplier, x: self.lower, y: self.upper})
was_reversed = True
elif LessEq(zero, multiplier).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 LessEq, zero, deduce_number_set
from proveit.numbers.multiplication import (
strong_bound_via_left_factor_bound,
weak_bound_via_left_factor_bound,
reversed_strong_bound_via_left_factor_bound,
reversed_weak_bound_via_left_factor_bound)
was_reversed = False
deduce_number_set(multiplier)
if Less(zero, multiplier).proven():
new_rel = strong_bound_via_left_factor_bound.instantiate(
{a: multiplier, x: self.lower, y: self.upper})
elif Less(multiplier, zero).proven():
new_rel = reversed_strong_bound_via_left_factor_bound.instantiate(
{a: multiplier, x: self.lower, y: self.upper})
was_reversed = True
elif 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 (
strong_div_from_numer_bound__pos_denom,
strong_div_from_numer_bound__neg_denom)
deduce_number_set(divisor)
if Less(zero, divisor).proven():
thm = strong_div_from_numer_bound__pos_denom
elif Less(divisor, zero).proven():
thm = strong_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 strong_bound_via_right_term_bound
new_rel = strong_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 strong_bound_via_left_term_bound
new_rel = strong_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, LessEq, zero, deduce_number_set
from proveit.numbers.exponentiation import (
exp_pos_less, exp_nonneg_less, exp_neg_less, exp_nonpos_less)
# 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_less.instantiate(
{a: exponent, x: self.lower, y: self.upper})
elif Less(exponent, zero).proven():
new_rel = exp_neg_less.instantiate(
{a: exponent, x: self.lower, y: self.upper})
elif LessEq(zero, exponent).proven():
new_rel = exp_nonneg_less.instantiate(
{a: exponent, x: self.lower, y: self.upper})
elif LessEq(exponent, zero).proven():
new_rel = exp_nonpos_less.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)
[docs]def greater(a, b):
'''
Return an expression representing a > b, internally represented
as b < a but with a style that reverses the direction.
'''
return Less(b, a).with_styles(direction='reversed')