import math
from proveit import (Judgment, Expression, Literal, Operation,
maybe_fenced_latex, defaults,
Function, ExprTuple, InnerExpr, USE_DEFAULTS,
UnsatisfiedPrerequisites, relation_prover,
equality_prover, auto_relation_prover,
auto_equality_prover, SimplificationDirectives)
from proveit import TransRelUpdater
from proveit import a, b, c, m, n, w, x, y, z
from proveit.logic import Equals, NotEquals, InSet
from proveit.numbers import (zero, NumberOperation,
is_numeric_int, is_numeric_rational,
numeric_rational_ints,
simplified_numeric_rational,
deduce_number_set, readily_factorable,
readily_provable_number_set)
from proveit.numbers.number_sets import (
ZeroSet, Natural, NaturalPos,
Integer, IntegerNonZero, IntegerNeg, IntegerNonPos,
Rational, RationalNonZero, RationalPos, RationalNeg, RationalNonNeg,
RationalNonPos,
Real, RealNonZero, RealNeg, RealPos, RealNonNeg, RealNonPos,
Complex, ComplexNonZero)
[docs]class Div(NumberOperation):
# operator of the Div operation
_operator_ = Literal(
string_format='/',
latex_format=r'\div',
theory=__file__)
# The following _simplification_directives are used as flags
# to control automatic simplification of Div (or frac) exprs,
# with:
# cancel_factors: controls canceling of common factors in
# numerator and denominator
#
_simplification_directives_ = SimplificationDirectives(
factor_negation = True,
reduce_zero_numerator = True,
reduce_to_multiplication = False,
reduce_rational = True,
distribute = False,
cancel_factors = True)
def __init__(self, numerator, denominator, *, styles=None):
r'''
Divide two operands.
'''
NumberOperation.__init__(self, Div._operator_, [numerator, denominator],
styles=styles)
self.numerator = self.operands[0]
self.denominator = self.operands[1]
[docs] def latex(self, **kwargs):
if self.get_style('division') == 'fraction':
# only fence if force_fence=True (a fraction within an
# exponentiation is an example of when fencing should be forced)
kwargs['fence'] = kwargs['force_fence'] if 'force_fence' in kwargs else False
return maybe_fenced_latex(
r'\frac{' +
self.numerator.latex() +
'}{' +
self.denominator.latex() +
'}',
**kwargs)
else:
# normal division
return NumberOperation.latex(self, **kwargs)
[docs] def style_options(self):
'''
Return the StyleOptions object for this Div.
'''
options = NumberOperation.style_options(self)
options.add_option(
name='division',
description=("'inline': uses '/'; 'fraction': "
"numerator over the denominator "
"(also see 'frac' function)"),
default='fraction',
related_methods=('with_inline_style',
'with_fraction_style'))
return options
[docs] def with_inline_style(self):
return self.with_styles(division='inline')
[docs] def with_fraction_style(self):
return self.with_styles(division='fraction')
[docs] def remake_constructor(self):
if self.get_style('division') == 'fraction':
return 'frac' # use a different constructor if using the fraction style
return Operation.remake_constructor(self)
def _build_canonical_form(self):
'''
If this is a literal rational, returns the irreducible form.
Otherwise, returns the canonical form of the numerator
multiplied by the denominator raised to the power of -1:
x/y = x*y^{-1}
'''
from proveit.numbers import (one, Neg, Mult, Exp,
simplified_numeric_rational)
if is_numeric_rational(self):
# Return the irreducible rational.
return simplified_numeric_rational(self.numerator.as_int(),
self.denominator.as_int())
as_mult = Mult(self.numerator, Exp(self.denominator, Neg(one)))
return as_mult.canonical_form()
@equality_prover('shallow_simplified', 'shallow_simplify')
def shallow_simplification(self, *, must_evaluate=False,
**defaults_config):
'''
Returns a proven simplification equation for this Divide
expression assuming the operands have been simplified.
Specifically, cancels common factors and eliminates ones.
'''
from proveit.logic import is_irreducible_value
from proveit.numbers import one, Neg, Add, Sum, Mult, num
if self.is_irreducible_value():
# already irreducible
return Equals(self, self).conclude_via_reflexivity()
numer, denom = self.numerator, self.denominator
if Div._simplification_directives_.reduce_rational and (
is_numeric_rational(numer) and is_numeric_rational(denom)
and denom != zero):
# If the numerator and denominator are rational numerals,
# so go ahead and evaluate it to an irreducible form.
return self.rational_reduction()
if Div._simplification_directives_.reduce_to_multiplication:
# (x/y) = x*y^{-1}_deduce
return self.reduction_to_mult(auto_simplify=True)
# for convenience updating our equation
expr = self
eq = TransRelUpdater(expr)
# perform cancelations where possible
if Div._simplification_directives_.cancel_factors:
expr = eq.update(expr.cancelations(preserve_all=True))
if not isinstance(expr, Div):
# complete cancelation.
return eq.relation
if must_evaluate:
if not all(is_irreducible_value(operand) for operand
in self.operands):
for operand in self.operands:
if not is_irreducible_value(operand):
# The simplification of the operands may not have
# worked hard enough. Let's work harder if we
# must evaluate.
operand.evaluation()
return self.evaluation()
canonical_form = self.canonical_form()
if is_numeric_rational(canonical_form):
return self.rational_reduction()
elif is_irreducible_value(canonical_form):
# Equate to the irreducible canonical form.
return Equals(self, canonical_form).prove()
raise NotImplementedError(
"Evaluation of %s is not implemented"%self)
if expr.denominator == one:
# eliminate division by one
expr = eq.update(expr.divide_by_one_elimination(preserve_all=True))
if (isinstance(expr, Div) and
Div._simplification_directives_.factor_negation and
isinstance(expr.numerator, Neg)):
# we have something like (-a)/b but want -(a/b)
expr = eq.update(expr.neg_extraction())
# return eq.relation # no more division simplifications.
if (Div._simplification_directives_.reduce_zero_numerator and
isinstance(expr, Div)):
if ((expr.numerator==zero or Equals(expr.numerator,
zero).readily_provable())
and NotEquals(expr.denominator, zero).readily_provable()):
# we have something like 0/x so reduce to 0
expr = eq.update(expr.zero_numerator_reduction())
# finally, check if we have something like
# (x/(y/z)) or ((x/y)/z)
# but! remember to check here if we still even have a Div expr
# b/c some of the work above might have changed it to
# something else!
if (isinstance(expr, Div) # (x/(y/z))
and isinstance(expr.denominator, Div)
and NotEquals(expr.denominator.numerator, zero).readily_provable()
and NotEquals(expr.denominator.denominator,
zero).readily_provable()):
expr = eq.update(expr.div_in_denominator_reduction())
if (isinstance(expr, Div) # (x/y)/z)
and isinstance(expr.numerator, Div)
and NotEquals(expr.numerator.denominator, zero).proven()
and NotEquals(expr.denominator, zero).proven() ):
expr = eq.update(expr.div_in_numerator_reduction())
if Div._simplification_directives_.distribute and (
isinstance(self.numerator, Add) or
isinstance(self.numerator, Sum)):
expr = eq.update(expr.distribution())
if Div._simplification_directives_.reduce_rational and (
isinstance(expr, Div)):
# Reduce numeric rationals in the numerator and denominator
# to an irreducible rational form.
expr = eq.update(expr.rational_reduction())
return eq.relation
def is_irreducible_value(self):
'''
This needs work, but we know that 1/x is irreducible if
x is irreducible, not a negation, not 0 and not 1.
'''
if is_numeric_int(self.numerator) and is_numeric_int(self.denominator):
# This is an irreducible rational if and only if it is the
# same as the corresponding 'simiplified_rational_expr'.
# (which divides out the gcd and extracts any negation).
numer_int = self.numerator.as_int()
denom_int = self.denominator.as_int()
return self == simplified_numeric_rational(numer_int, denom_int)
return False
@equality_prover('rational_reduced',
'reduce_rational')
def rational_reduction(self, **defaults_config):
'''
Equate this fraction to an irreducible, numeric rational if
it is a numeric rational. More generally, reduce the numeric
rationals in the numerator and denominator to an irreducible
rational form. For example:
((4/3) x) / ((2/3) y) = (2 x) / y
'''
from proveit.numbers import Mult, num, one, compose_product
from proveit.numbers.division import frac_cancel_left
numerator, denominator = self.numerator, self.denominator
canonical_numer = self.numerator.canonical_form()
canonical_denom = self.denominator.canonical_form()
# Treat the case where the numerator and denominator evaluate
# to integers.
if is_numeric_int(canonical_numer) and is_numeric_int(canonical_denom):
# Find out the greatest common divisor.
numer, denom = canonical_numer, canonical_denom
numer_int, denom_int = numer.as_int(), denom.as_int()
if abs(numer_int) == abs(denom_int):
if numer_int != denom_int:
# -n/n = -1 or n/(-n) = -1
return self.neg_extraction(auto_simplify=True)
# n/n=1
replacements = [Equals(numer, self.numerator).prove(),
Equals(denom, self.denominator).prove()]
return Div(numer, denom).cancelation(
num(abs(numer_int)), replacements=replacements,
preserve_expr=self, alter_lhs=True)
gcd = math.gcd(numer_int, denom_int)
expr = self
eq = TransRelUpdater(expr)
if gcd == 1:
# No common divisor to factor out.
expr = eq.update(expr.inner_expr().numerator.evaluation())
expr = eq.update(expr.inner_expr().denominator.evaluation())
else:
# Factor out the gcd and cancel it.
# Replace the factored numerator and denominator with
# the original form.
factored_numer = Mult(num(gcd), num(numer_int//gcd))
factored_denom = Mult(num(gcd), num(denom_int//gcd))
numer_eval = self.numerator.evaluation()
denom_eval = self.denominator.evaluation()
replacements = [
factored_numer.evaluation().apply_transitivity(
numer_eval),
factored_denom.evaluation().apply_transitivity(
denom_eval),
]
expr = eq.update(frac_cancel_left.instantiate(
{x: num(gcd), y: factored_numer.factors[1],
z: factored_denom.factors[1]},
replacements=replacements, preserve_expr=self))
if numer_int < 0 and denom_int < 0:
# cancel negations in the numerator and denominator
expr = eq.update(expr.neg_cancelation())
elif numer_int < 0 or denom_int < 0:
# extract the negation for the irreducible form.
expr = eq.update(expr.neg_extraction())
if abs(denom_int) == 1:
expr = eq.update(expr.divide_by_one_elimination())
return eq.relation
canonical_form = self.canonical_form()
if is_numeric_rational(canonical_form):
# Reduce to a multiplication and then sort it out to handle
# the more general case.
return self.reduction_to_mult(auto_simplify=True)
# Extract the rational and remainder parts of the
# numerator and denominator.
numer_rational = denom_rational = one
numer_remainder_factors = denom_remainder_factors = []
if is_numeric_rational(numerator):
numer_rational = numerator
elif isinstance(numerator, Mult) and (
len(numerator.operands) > 0 and
is_numeric_rational(numerator.operands[0])):
numer_rational = numerator.operands[0]
numer_remainder_factors = numerator.operands[1:]
elif numerator != one:
numer_remainder_factors = [numerator]
if is_numeric_rational(denominator):
denom_rational = denominator
elif isinstance(denominator, Mult) and (
len(denominator.operands) > 0 and
is_numeric_rational(denominator.operands[0])):
denom_rational = denominator.operands[0]
denom_remainder_factors = denominator.operands[1:]
elif denominator != one:
denom_remainder_factors = [denominator]
numer_ints = numeric_rational_ints(numer_rational)
denom_ints = numeric_rational_ints(denom_rational)
# (a/b)/(c/d) = (a*d)/(b*c):
numer_int = numer_ints[0] * denom_ints[1]
denom_int = denom_ints[0] * numer_ints[1]
numer_int, denom_int = numeric_rational_ints(
simplified_numeric_rational(numer_int, denom_int))
if numer_int != numer_rational or denom_int != denom_rational:
# A simplification should be performed.
if numer_int == 1:
numer = compose_product(*numer_remainder_factors)
else:
numer = compose_product(num(numer_int),
*numer_remainder_factors)
if denom_int == 1:
denom = compose_product(*denom_remainder_factors)
else:
denom = compose_product(num(denom_int),
*denom_remainder_factors)
if denom == one:
rhs = numer
else:
rhs = Div(numer, denom)
return self.deduce_canonically_equal(rhs)
return Equals(self, self).conclude_via_reflexivity()
@equality_prover('reduced_to_mult', 'reduce_to_mult')
def reduction_to_mult(self, **defaults_config):
'''
Equate (x/y) to x*y^{-1}.
'''
from proveit.numbers.division import div_as_mult
return div_as_mult.instantiate({x:self.numerator,
y:self.denominator})
@equality_prover('zero_numerator_reduced', 'zero_numerator_reduce')
def zero_numerator_reduction(self, **defaults_config):
'''
Deduce and return an equality between self of the form 0/x
and the number 0. Will need to know or assume that the
denominator x is non-zero.
'''
from proveit.numbers.division import frac_zero_numer
_x_sub = self.denominator
return frac_zero_numer.instantiate({x: _x_sub})
@equality_prover('div_in_denominator_reduced', 'div_in_denominator_reduce')
def div_in_denominator_reduction(self, **defaults_config):
'''
Deduce and return an equality between self of the form
(x/(y/z)) (i.e. a fraction with a fraction as it denominator)
and the form x (z/y). Will need to know or assume that x, y, z
are Complex with y != 0 and z != 0.
'''
if (not isinstance(self.denominator, Div)):
raise ValueError(
"Div.div_in_denominator_reduction() method only "
"applicable when the denominator is itself a Div."
"Instead we have the expr {0} with denominator {1}.".
format(self, self.denominator))
from proveit.numbers.division import div_by_frac_is_mult_by_reciprocal
return div_by_frac_is_mult_by_reciprocal.instantiate(
{x: self.numerator, y: self.denominator.numerator,
z: self.denominator.denominator})
@equality_prover('div_in_numerator_reduced', 'div_in_numerator_reduce')
def div_in_numerator_reduction(self, **defaults_config):
'''
Deduce and return an equality between self of the form
(x/y)/z (i.e. a fraction with a fraction as its numerator)
and the form x/(yz). Will need to know or assume that x, y, z
are Complex with y != 0 and z != 0.
'''
if (not isinstance(self.numerator, Div)):
raise ValueError(
"Div.div_in_numerator_reduction() method only "
"applicable when the numerator is itself a Div."
"Instead we have the expr {0} with numerator {1}.".
format(self, self.numerator))
from proveit.numbers.division import numerator_frac_reduction
return numerator_frac_reduction.instantiate(
{x: self.numerator.numerator, y: self.numerator.denominator,
z: self.denominator})
[docs] @equality_prover('all_canceled', 'all_cancel')
def cancelations(self, **defaults_config):
'''
Deduce and return an equality between self and a form in which
all simple division cancelations are performed.
'''
from proveit.numbers import Neg, Mult
expr = self
# A convenience to allow successive update to the equation via transitivities.
# (starting with self=self).
eq = TransRelUpdater(self)
if isinstance(expr.numerator, Neg) and (
isinstance(expr.denominator, Neg)):
# cancel negation in the numerator and denominator.
expr = eq.update(expr.neg_cancelation(preserve_all=True))
numer_factors = (expr.numerator.operands if
isinstance(expr.numerator, Mult) else
[expr.numerator])
denom_factors = (expr.denominator.operands if
isinstance(expr.denominator, Mult) else
[expr.denominator])
denom_factors_set = set(denom_factors)
for numer_factor in numer_factors:
if numer_factor in denom_factors_set:
expr = eq.update(expr.cancelation(numer_factor,
preserve_all=True))
denom_factors_set.remove(numer_factor)
return eq.relation
[docs] @equality_prover('canceled', 'cancel')
def cancelation(self, term_to_cancel, **defaults_config):
'''
Deduce and return an equality between self and a form in which
the given operand has been canceled on the numerator and
denominator. For example,
[(a*b)/(b*c)].cancelation(b) would return
(a*b)/(b*c) = a / c.
Assumptions or previous work might be required to establish
that the term_to_cancel is non-zero.
'''
from proveit.numbers import one, Exp, Mult, Neg
if self.numerator == self.denominator == term_to_cancel:
# x/x = 1
from . import frac_cancel_complete
return frac_cancel_complete.instantiate(
{x: term_to_cancel})
expr = self
eq = TransRelUpdater(expr)
if term_to_cancel != self.numerator:
# try to catch Exp objects here as well?
# after all, Exp(term_to_cancel, n) has factors!
# if (not isinstance(self.numerator, Mult) or
# term_to_cancel not in self.numerator.operands):
# raise ValueError("%s not in the numerator of %s"
# % (term_to_cancel, self))
if ((not isinstance(self.numerator, Mult)
and not isinstance(self.numerator, Exp)
and not isinstance(self.numerator, Neg))
or (isinstance(self.numerator, Mult)
and term_to_cancel not in self.numerator.operands)
or (isinstance(self.numerator, Exp)
and not (term_to_cancel == self.numerator.base
or (isinstance(term_to_cancel, Exp)
and term_to_cancel.base == self.numerator.base )))
or (isinstance(self.numerator, Neg)
and not (term_to_cancel == self.numerator.operand )
and not (isinstance(self.numerator.operand, Mult)
and term_to_cancel in self.numerator.operand.operands) ) ):
raise ValueError("%s not in the numerator of %s"
% (term_to_cancel, self))
# Factor the term_to_cancel from the numerator to the left.
expr = eq.update(expr.inner_expr().numerator.factorization(
term_to_cancel, group_factors=True, group_remainder=True,
preserve_all=True))
if term_to_cancel != self.denominator:
if (not isinstance(self.denominator, Mult) or
term_to_cancel not in self.denominator.operands):
raise ValueError("%s not in the denominator of %s"
% (term_to_cancel, self))
# Factor the term_to_cancel from the denominator to the left.
expr = eq.update(expr.inner_expr().denominator.factorization(
term_to_cancel, group_factors=True, group_remainder=True,
preserve_all=True))
if expr.numerator == expr.denominator == term_to_cancel:
# Perhaps it reduced to the trivial x/x = 1 case via
# auto-simplification.
expr = eq.update(expr.cancelation(term_to_cancel))
return eq.relation
else:
# (x*y) / (x*z) = y/z with possible automatic reductions
# via 1 eliminations.
from . import frac_cancel_left
replacements = list(defaults.replacements)
if expr.numerator == term_to_cancel:
numer_prod = Mult(term_to_cancel, one)
_y = one
replacements.append(numer_prod.one_elimination(
1, preserve_expr=term_to_cancel))
else:
_y = expr.numerator.operands[1]
if expr.denominator == term_to_cancel:
denom_prod = Mult(term_to_cancel, one)
_z = one
replacements.append(denom_prod.one_elimination(
1, preserve_expr=term_to_cancel))
else:
_z = expr.denominator.operands[1]
expr = eq.update(frac_cancel_left.instantiate(
{x: term_to_cancel, y: _y, z: _z},
replacements=replacements, preserve_expr=expr))
return eq.relation
@equality_prover('top_and_bottom_multiplied',
'top_and_bottom_multiply')
def top_and_bottom_multiplication(
self, multiplier, numerator_mult="left",
denominator_mult="left", **defaults_config):
'''
Deduce and return an equality between self and a form in which
the given multiplier now appears as a multiplicand in both the
numerator and denominator. This is essentially the inverse
method for the Div.cancelation() method defined above.
For example,[(a*b)/(b*c)].cancelation(b) would return
(a*b)/(b*c) = a / c,
whereas [a/c].top_and_bottom_multiplication(b) would return
a/c = ba/(bc).
Assumptions or previous work might be required to establish
that the multiplier and original denominator are non-zero.
Although technically it shouldn't matter if the original Div
had a zero in the denom (multiplying top and bottom by
something non-zero will give an undefined term equal to
another undefined term), we go ahead and maintain the
requirement that the original Div expression has a non-zero
denom.
The method initially only allows multiplication "on the left"
for the introduced multipler in both the numerator and
denominator (i.e. a/c can be taken to ba/bc but not directly
to ab/(bc) nor ba/(cb) nor ab/(cb)).
'''
from proveit.numbers import Mult
expr = self
# A convenience to allow successive updates to the equation
# via transitivities (starting with self=self).
eq = TransRelUpdater(expr)
replacements = list(defaults.replacements)
# We want to avoid automatically canceling the multiplier
# we're introducing in the numerator and denominator, so
# we modify the cancel_factors directive, and we do so within
# a 'with' construct in case the process fails (keeping us
# from inadvertently getting stuck with the changed directive).
with Div.temporary_simplification_directives() as tmp_directives:
tmp_directives.cancel_factors = False
_y_sub = self.numerator
_z_sub = self.denominator
# expr = eq.update(frac_cancel_left.instantiate(
# {x: multiplier, y: _y_sub, z: _z_sub},
# replacements=replacements, preserve_expr=expr))
if numerator_mult=="left":
from . import frac_cancel_left
expr = eq.update(frac_cancel_left.instantiate(
{x: multiplier, y: _y_sub, z: _z_sub},
replacements=replacements, preserve_expr=expr))
if (denominator_mult=="right" and
isinstance(expr.denominator, Mult)):
# commute multiplicands in denominator;
# skip this if denom has already been simplified
# to be an Exp
_init_idx = 0
_final_idx = len(expr.denominator.operands) - 1
expr = eq.update(
expr.inner_expr().denominator.
commutation(_init_idx, _final_idx))
if numerator_mult=="right":
from . import frac_cancel_right
expr = eq.update(frac_cancel_right.instantiate(
{x: multiplier, y: _y_sub, z: _z_sub},
replacements=replacements, preserve_expr=expr))
if (denominator_mult=="left" and
isinstance(expr.denominator, Mult)):
# commute multiplicands in denominator;
# skip this if denom has already been simplified
# to be an Exp
_init_idx = 0
_final_idx = len(expr.denominator.operands)-1
expr = eq.update(
expr.inner_expr().denominator.
commutation(_init_idx, _final_idx))
return eq.relation
[docs] @equality_prover('deep_eliminated_ones', 'deep_eliminate_ones')
def deep_one_eliminations(self, **defaults_config):
'''
Eliminate ones from the numerator, the denominator,
and as a division by one.
'''
from proveit.numbers import one
expr = self
# A convenience to allow successive update to the equation
# via transitivities (starting with self=self).
eq = TransRelUpdater(self)
for _i, operand in enumerate(self.operands):
if hasattr(operand, 'deep_one_eliminations'):
expr = eq.update(expr.inner_expr().operands[_i].
deep_one_eliminations())
if expr.denominator == one:
expr = eq.update(expr.divide_by_one_elimination())
return eq.relation
@equality_prover('divide_by_one_eliminated', 'eliminate_divide_by_one')
def divide_by_one_elimination(self, **defaults_config):
from proveit.numbers import one
from . import frac_one_denom
if self.denominator != one:
raise ValueError("'divide_by_one_elimination' is only applicable "
"if the denominator is precisely one.")
return frac_one_denom.instantiate({x: self.numerator})
def readily_factorable(self, factor):
'''
Return True iff 'factor' is factorable from 'self' in an
obvious manner. For this Div, it is readily factorable if
it is readily factorable from the correxponding Mult:
x/y = x*(y^{-1})
'''
cf = self.canonical_form()
if cf != self:
return readily_factorable(self.canonical_form(), factor)
else:
return False
@auto_equality_prover('factorized', 'factor')
def factorization(self, the_factors, pull="left",
group_factors=True, group_remainder=False,
**defaults_config):
'''
Return the proven factorization (equality with the factored
form) from pulling the factor(s) from this division to the
"left" or "right". If there are multiple occurrences, the first
occurrence is used.
If group_factors is True, the factors are
grouped together as a sub-product.
The group_remainder parameter ensures that the remainder is
grouped together as a sub-product (which is only relevant
if this division needed to be converted into a product in
order to perform this factoring).
Examples:
[(a*b)/(c*d)].factorization((a/c))
proves (a*b)/(c*d) = (a/c)*(b/d)
[(a*b)/(c*d)].factorization((1/c))
proves (a*b)/(c*d) = (1/c)*(a*b/d)
[(a*b)/(c*d)].factorization(a, pull='right')
proves (a*b)/(c*d) = (b/(c*d))*a
[a/(c*d)].factorization(a, pull='right')
proves a/(c*d) = (1/(c*d))*a
[(a*b)/d].factorization((a/d), pull='right')
proves (a*b)/d = b*(a/d)
'''
from proveit.numbers import one, Mult, Neg, Exp, readily_factorable
from . import mult_frac_left, mult_frac_right, prod_of_fracs
expr = self
eq = TransRelUpdater(expr)
if the_factors == self:
return eq.relation # self = self
if isinstance(the_factors, Div):
the_factor_numer = the_factors.numerator
the_factor_denom = the_factors.denominator
else:
the_factor_numer = the_factors
the_factor_denom = one
replacements = []
# Factor out a fraction.
if expr.denominator == the_factor_denom:
# Factor (x/z) from (x*y)/z.
# x or y may be 1.
if the_factor_numer not in (one, expr.numerator):
expr = eq.update(expr.inner_expr().numerator.factorization(
the_factors.numerator, pull=pull,
group_factors=True, group_remainder=True))
if pull == 'left':
# factor (x*y)/z into (x/z)*y
thm = mult_frac_left
if the_factor_numer == one:
# factor y/z into (1/z)*y
_x = one
_y = expr.numerator
replacements.append(Mult(_x, _y).one_elimination(0))
else:
# factor (x*y)/z into x*(y/z)
thm = mult_frac_right
if the_factor_numer == one:
# factor x/z into x*(1/z)
_x = expr.numerator
_y = one
replacements.append(Mult(_x, _y).one_elimination(1))
if the_factor_numer != one:
assert expr.numerator.operands.num_entries() == 2
_x = expr.numerator.operands.entries[0]
_y = expr.numerator.operands.entries[1]
_z = expr.denominator
eq.update(thm.instantiate({x:_x, y:_y, z:_z},
preserve_expr=expr,
replacements=replacements))
elif (readily_factorable(expr.numerator, the_factor_numer) and
(the_factor_denom == one or
readily_factorable(expr.denominator, the_factor_denom))):
# Factor (x*y)/(z*w) into (x/z)*(y/w).
thm = prod_of_fracs
if the_factor_denom not in (one, expr.denominator):
expr = eq.update(expr.inner_expr().denominator.factorization(
the_factor_denom, pull=pull,
group_factors=True))
assert expr.denominator.operands.num_entries() == 2
_z = expr.denominator.operands.entries[0]
_w = expr.denominator.operands.entries[1]
elif (pull == 'left') == (the_factor_denom == one):
# Factor (x*y)/w into x*(y/w).
_z = one
_w = expr.denominator
replacements.append(Mult(_z, _w).one_elimination(0))
else:
# Factor (x*y)/z into (x/z)*y.
_z = expr.denominator
_w = one
replacements.append(Mult(_z, _w).one_elimination(1))
# Factor the numerator parts unless there is a 1 numerator.
if the_factor_numer not in (one, expr.numerator):
expr = eq.update(expr.inner_expr().numerator.factorization(
the_factor_numer, pull=pull,
group_factors=True, group_remainder=True))
assert expr.numerator.operands.num_entries() == 2
# Factor (x*y)/(z*w) into (x/z)*(y/w)
_x = expr.numerator.operands.entries[0]
_y = expr.numerator.operands.entries[1]
elif (pull == 'left') == (the_factor_numer == one):
# Factor y/(z*w) into (1/z)*(y/w)
_x = one
_y = expr.numerator
replacements.append(Mult(_x, _y).one_elimination(0))
else:
# Factor x/(y*z) into (x/y)*(1/z)
_x = expr.numerator
_y = one
replacements.append(Mult(_x, _y).one_elimination(1))
# create POSSIBLE replacements for inadvertently generated
# fractions of the form _x/1 (i.e. _z = 1)
# or _y/1 (i.e. _w = 1):
if _z == one:
replacements.append(frac(_x, _z).divide_by_one_elimination())
if _w == one:
replacements.append(frac(_y, _w).divide_by_one_elimination())
eq.update(thm.instantiate({x:_x, y:_y, z:_z, w:_w},
preserve_expr=expr, replacements=replacements))
else:
# As a last resort, convert this division to a
# multiplication and factor that.
if isinstance(expr.denominator, Mult):
replacements = [Exp(expr.denominator, Neg(one)).distribution()]
expr = eq.update(expr.reduction_to_mult(replacements=replacements))
if isinstance(expr.operands[1], Mult):
expr = eq.update(expr.disassociation(1))
if isinstance(expr.operands[0], Mult):
expr = eq.update(expr.disassociation(0))
expr = eq.update(expr.factorization(
the_factors, pull=pull,
group_factors=group_factors,
group_remainder=group_remainder))
return eq.relation
[docs] @equality_prover('distributed', 'distribute')
def distribution(self, **defaults_config):
r'''
Distribute the denominator through the numerator, returning
the equality that equates self to this new version.
Examples:
:math:`(a + b + c) / d = a / d + b / d + c / d`
:math:`(a - b) / d = a / d - b / d`
:math:`\left(\sum_x f(x)\right / y = \sum_x [f(x) / y]`
Give any assumptions necessary to prove that the operands are
in the Complex numbers so that the associative and commutation
theorems are applicable.
'''
from proveit.numbers import Add, Sum, Neg
from . import (distribute_frac_through_sum,
distribute_frac_through_subtract)
if isinstance(self.numerator, Add):
if (self.numerator.operands.is_double()
and isinstance(self.numerator.operands[1], Neg)):
_x = self.numerator.operands[0]
_y = self.numerator.operands[1].operand
_z = self.denominator
return distribute_frac_through_subtract.instantiate(
{x:_x, y:_y, z:_z})
_x = self.numerator.operands
_y = self.denominator
_n = _x.num_elements()
return distribute_frac_through_sum.instantiate(
{n: _n, x: _x, y: _y})
elif isinstance(self.numerator, Sum):
# Should deduce in Complex, but
# distribute_through_summation doesn't have a domain
# restriction right now because this is a little tricky.
# To do.
# deduce_in_complex(self.operands, assumptions)
raise NotImplementedError(
"Distribution of division through summation not yet "
"implemented.")
"""
y_etc_sub = self.numerator.indices
Pop, Pop_sub = Function(
P, self.numerator.indices), self.numerator.summand
S_sub = self.numerator.domain
dummy_var = safe_dummy_var(self)
spec1 = distributefrac_through_summation.instantiate(
{Pop: Pop_sub, S: S_sub, y_etc: y_etc_sub, z: dummy_var})
return spec1.derive_conclusion().instantiate(
{dummy_var: self.denominator})
"""
else:
raise Exception(
"Unsupported operand type to distribute over: " +
str(self.numerator.__class__))
@equality_prover('neg_canceled', 'neg_cancel')
def neg_cancelation(self, **defaults_config):
'''
Derive ((-x)/(-y)) = (x/y).
'''
from proveit.numbers import Neg
from proveit.numbers.division import cancel_negations
if not isinstance(self.numerator, Neg) or not(
isinstance(self.denominator, Neg)):
return cancel_negations.instantiate(
{x:self.numerator.operator,
y:self.denominator.operator})
@equality_prover('neg_extracted', 'neg_extract')
def neg_extraction(self, neg_loc=None, **defaults_config):
'''
Factor out a negation from the numerator (default) or
denominator (specified with neg_loc='denominator'),
returning the equality between the original self and the
resulting fraction with the negative (Neg) out in front.
For example, given expr = (-x)/y, then expr.neg_extraction()
(with suitable assumptions or info about x and y) returns:
|- (-x)/y = -(x/y).
The theorems being applied require numerator and denom elements
to be Complex with denom != 0. If neg_loc is None, attempts
to find a suitable Neg component to extract.
Implemented in a naive way for cases in which the Neg is one
of several factors in the numerator or denominator, giving for
example:
|- (x(-z))/y = -((xz)/y)
'''
from proveit.numbers import Mult, Neg
if neg_loc is None:
# Check if entire numerator is a Neg
if isinstance(self.numerator, Neg):
neg_loc = 'numerator'
elif isinstance(self.numerator, Mult):
# check if one of the numerator's factors is a Neg:
for factor in self.numerator.factors:
if isinstance(factor, Neg):
neg_loc = 'numerator_factor'
numerator_factor = factor
break
elif isinstance(self.denominator, Neg):
neg_loc = 'denominator'
elif isinstance(self.denominator, Mult):
# check if one of the denominator's factors is a Neg:
for factor in self.denominator.factors:
if isinstance(factor, Neg):
neg_loc = 'denominator_factor'
denominator_factor = factor
break
if neg_loc is None:
raise ValueError(
"No Neg expression component found to extract. "
"The expression supplied was: {}".format(self))
else:
raise ValueError(
"No Neg expression component found to extract. "
"The expression supplied was: {}".format(self))
if neg_loc == 'numerator' and not isinstance(self.numerator, Neg):
raise ValueError(
"The numerator version of Div.neg_extraction() can "
"only be applied if the entire numerator is negated "
"(i.e. inside a Neg). The numerator supplied was: "
"{}".format(self.numerator))
if neg_loc == 'denominator' and not isinstance(self.denominator, Neg):
raise ValueError(
"The denominator version of Div.neg_extraction() can "
"only be applied if the entire denominator is negated "
"(i.e. inside a Neg). The denominator supplied was: "
"{}".format(self.denominator))
# add error checks here for neg_loc values 'numerator_factor'
# and 'denominator_factor'
import proveit.numbers.division as div_pkg
# Case (1) Neg(x)/y = Neg(x/y)
if neg_loc == 'numerator':
thm = div_pkg.neg_frac_neg_numerator
_x, _y = thm.instance_params
_x_sub = self.numerator.operand
_y_sub = self.denominator
return thm.instantiate(
{_x: _x_sub, _y: _y_sub})
# Case (2) x/Neg(y) = Neg(x/y)
if neg_loc == 'denominator':
thm = div_pkg.neg_frac_neg_denominator
_x, _y = thm.instance_params
_x_sub = self.numerator
_y_sub = self.denominator.operand
return thm.instantiate(
{_x: _x_sub, _y: _y_sub})
# Case (3) Neg is a factor in the numerator
# -- first pull the Neg out in front of the numerator
# -- then re-call the exp_extraction() method
if neg_loc == 'numerator_factor':
intermed_equality = (
self.inner_expr().numerator.neg_simplifications(
preserve_all=True))
return intermed_equality.inner_expr().rhs.neg_extract()
# # Case (4) Neg is a factor in the denominator
# -- first pull the Neg out in front of the numerator
# -- then re-call the exp_extraction() method
if neg_loc == 'denominator_factor':
intermed_equality = (
self.inner_expr().denominator.neg_simplifications())
return intermed_equality.inner_expr().rhs.neg_extract()
# Other cases here?
# Consider more generality by allowing user to specify the
# neg_loc = 'numerator/denominator_factor' and allowing
# a 0-based index for the factor. Related: see more general
# neg_frac_neg theorems in division pkg.
[docs] @equality_prover('combined_exponents', 'combine_exponents')
def exponent_combination(self, start_idx=None, end_idx=None,
**defaults_config):
'''
Equates $a^m/a^n$ to $a^{m-n} or
$a^c/b^c$ to $(a/b)^c$.
'''
from proveit.numbers import Exp
from proveit.numbers.exponentiation import (
quotient_of_posnat_powers, quotient_of_pos_powers,
quotient_of_real_powers, quotient_of_complex_powers)
if (isinstance(self.numerator, Exp)
and isinstance(self.denominator, Exp)):
if self.numerator.base == self.denominator.base:
# Same base: (a^b/a^c) = a^{b-c}
same_base = self.numerator.bas
exponents = (self.numerator.exponent,
self.denominator.exponent)
# Find out the known type of the exponents.
possible_exponent_types = [NaturalPos, RealPos, Real,
Complex]
for exponent in exponents:
exp_ns = readily_provable_number_set(exponent,
default=Complex)
while len(possible_exponent_types) > 1:
exponent_type = possible_exponent_types[0]
if exponent_type.readily_includes(exp_ns):
# This type is known for this exponent.
break
# We've eliminated a type from being known.
possible_exponent_types.pop(0)
known_exponent_type = possible_exponent_types[0]
if known_exponent_type == NaturalPos:
_m, _n = exponents
return quotient_of_posnat_powers.instantiate(
{a: same_base, m: _m, n: _n})
else:
_b, _c = exponents
if known_exponent_type == RealPos:
thm = quotient_of_pos_powers
elif known_exponent_type == Real:
thm = quotient_of_real_powers
else: # Complex is the default
thm = quotient_of_complex_powers
thm.instantiate({a: same_base, b: _b, c: _c})
elif self.numerator.exponent == self.denominator.exponent:
# Same exponent: (a^c/b^c) = (a/b)^c
same_exponent = self.numerator.exponent
bases = (self.numerator.base, self.denominator.base)
# Combining the exponents in this case is the reverse
# of disibuting an exponent.
quotient = Div(*bases).with_matching_style(self)
exp = Exp(quotient, same_exponent)
return exp.distribution().derive_reversed()
else:
raise NotImplementedError("Need to implement degenerate cases "
"of a^b/a and a/a^b.")
def readily_not_equal(self, other):
'''
Return True iff self and other are numeric rationals (at least
in canonical form) that are not equal to each other.
'''
from proveit.numbers import not_equal_numeric_rationals
return not_equal_numeric_rationals(self, other.canonical_form())
@relation_prover
def deduce_not_equal(self, other, **defaults_config):
'''
Prove and return self ≠ other if self and other are numeric
rational.
'''
from proveit.numbers import (
is_numeric_rational, deduce_not_equal_numeric_rationals)
if not (is_numeric_rational(self) and is_numeric_rational(other)):
raise NotImplementedError(
"Divide.deduce_not_equal only handles the case of "
"numeric rationals. Given %s and %s"%(self, other))
return deduce_not_equal_numeric_rationals(self, other)
[docs] @relation_prover
def deduce_in_number_set(self, number_set, **defaults_config):
'''
Given a number set number_set, attempt to prove that the given
expression is in that number set using the appropriate closure
theorem.
'''
from proveit import a, b
from proveit.numbers import Less, zero
import proveit.numbers.division as div_pkg
thm = None
if number_set == ZeroSet:
# prove 0/x in {0}; while we are at it, prove 0/x = 0
div_pkg.frac_zero_numer.instantiate({x:self.denominator})
thm = div_pkg.frac_in_zero_set
elif number_set == Rational:
thm = div_pkg.div_rational_closure
elif number_set == RationalNonZero:
thm = div_pkg.div_rational_nonzero_closure
elif number_set == RationalPos:
deduce_number_set(self.denominator)
if Less(self.denominator, zero).readily_provable():
thm = div_pkg.div_rational_pos_from_double_neg
else:
thm = div_pkg.div_rational_pos_closure
elif number_set == RationalNeg:
deduce_number_set(self.denominator)
if Less(self.denominator, zero).readily_provable():
thm = div_pkg.div_rational_neg_from_neg_denom
else:
thm = div_pkg.div_rational_neg_from_neg_numer
elif number_set == RationalNonNeg:
deduce_number_set(self.denominator)
if Less(self.denominator, zero).readily_provable():
thm = div_pkg.div_rational_nonneg_from_double_neg
else:
thm = div_pkg.div_rational_nonneg_closure
elif number_set == RationalNonPos:
deduce_number_set(self.denominator)
if Less(self.denominator, zero).readily_provable():
thm = div_pkg.div_rational_nonpos_from_neg_denom
else:
thm = div_pkg.div_rational_nonpos_from_nonpos_numer
elif number_set == Real:
thm = div_pkg.div_real_closure
elif number_set == RealNonZero:
thm = div_pkg.div_real_nonzero_closure
elif number_set == RealPos:
deduce_number_set(self.denominator)
if Less(self.denominator, zero).readily_provable():
thm = div_pkg.div_real_pos_from_double_neg
else:
thm = div_pkg.div_real_pos_closure
elif number_set == RealNeg:
deduce_number_set(self.denominator)
if Less(self.denominator, zero).readily_provable():
thm = div_pkg.div_real_neg_from_neg_denom
else:
thm = div_pkg.div_real_neg_from_neg_numer
elif number_set == RealNonNeg:
deduce_number_set(self.denominator)
if Less(self.denominator, zero).readily_provable():
thm = div_pkg.div_real_nonneg_from_double_neg
else:
thm = div_pkg.div_real_nonneg_closure
elif number_set == RealNonPos:
deduce_number_set(self.denominator)
if Less(self.denominator, zero).readily_provable():
thm = div_pkg.div_real_nonpos_from_neg_denom
else:
thm = div_pkg.div_real_nonpos_from_nonpos_numer
elif number_set == ComplexNonZero:
thm = div_pkg.div_complex_nonzero_closure
elif number_set == Complex:
thm = div_pkg.div_complex_closure
if thm is not None:
return thm.instantiate({a: self.numerator, b: self.denominator})
raise NotImplementedError(
"'Div.deduce_in_number_set()' not implemented for the %s set"
% str(number_set))
def readily_provable_number_set(self):
'''
Return the most restrictive number set we can readily
prove contains the evaluation of this number operation.
'''
numer_ns = readily_provable_number_set(self.numerator)
denom_ns = readily_provable_number_set(self.denominator)
if numer_ns is None or denom_ns is None: return None
if numer_ns == ZeroSet: return ZeroSet
if RationalPos.readily_includes(numer_ns) and (
RationalPos.readily_includes(denom_ns)):
return RationalPos
if RationalNeg.readily_includes(numer_ns) and (
RationalNeg.readily_includes(denom_ns)):
return RationalPos
if RationalNeg.readily_includes(numer_ns) and (
RationalPos.readily_includes(denom_ns)):
return RationalNeg
if RationalPos.readily_includes(numer_ns) and (
RationalNeg.readily_includes(denom_ns)):
return RationalNeg
if (RationalNonNeg.readily_includes(numer_ns)
and RationalPos.readily_includes(denom_ns)):
return RationalNonNeg
if (RationalNonPos.readily_includes(numer_ns)
and RationalPos.readily_includes(denom_ns)):
return RationalNonPos
if (RationalNonNeg.readily_includes(numer_ns)
and RationalNeg.readily_includes(denom_ns)):
return RationalNonPos
if (RationalNonPos.readily_includes(numer_ns)
and RationalNeg.readily_includes(denom_ns)):
return RationalNonNeg
if (RationalNonZero.readily_includes(numer_ns) and
RationalNonZero.readily_includes(denom_ns)):
return RationalNonZero
if Rational.readily_includes(numer_ns) and (
RationalNonZero.readily_includes(denom_ns)):
return Rational
if RealPos.readily_includes(numer_ns) and (
RealPos.readily_includes(denom_ns)):
return RealPos
if RealNeg.readily_includes(numer_ns) and (
RealNeg.readily_includes(denom_ns)):
return RealPos
if RealPos.readily_includes(numer_ns) and (
RealNeg.readily_includes(denom_ns)):
return RealNeg
if RealNeg.readily_includes(numer_ns) and (
RealPos.readily_includes(denom_ns)):
return RealNeg
if RealNonNeg.readily_includes(numer_ns) and (
RealPos.readily_includes(denom_ns)):
return RealNonNeg
if RealNonPos.readily_includes(numer_ns) and (
RealPos.readily_includes(denom_ns)):
return RealNonPos
if RealNonNeg.readily_includes(numer_ns) and (
RealNeg.readily_includes(denom_ns)):
return RealNonPos
if RealNonPos.readily_includes(numer_ns) and (
RealNeg.readily_includes(denom_ns)):
return RealNonNeg
if Real.readily_includes(numer_ns) and (
RealNonZero.readily_includes(denom_ns)):
return Real
if RealNonZero.readily_includes(numer_ns) and (
RealNonZero.readily_includes(denom_ns)):
return RealNonZero
if Real.readily_includes(numer_ns) and (
RealNonZero.readily_includes(denom_ns)):
return Real
if (ComplexNonZero.readily_includes(numer_ns)
and ComplexNonZero.readily_includes(denom_ns)):
return ComplexNonZero
return Complex
@relation_prover
def bound_via_operand_bound(self, operand_relation, **defaults_config):
'''
Deduce a bound of this division (fraction) given a bound on
either the numerator or the denominator.
'''
from proveit.numbers import NumberOrderingRelation
if isinstance(operand_relation, Judgment):
operand_relation = operand_relation.expr
if not isinstance(operand_relation, NumberOrderingRelation):
raise TypeError("'operand_relation' expected to be a number "
"relation (<, >, ≤, or ≥)")
lhs = operand_relation.lhs
if lhs == self.numerator:
return self.bound_via_numerator_bound(operand_relation)
elif lhs == self.denominator:
return self.bound_via_denominator_bound(operand_relation)
else:
raise ValueError("Left side of %s expected to be the numerator "
"or denominator of %s"%(operand_relation, self))
@relation_prover
def bound_via_numerator_bound(self, relation, **defaults_config):
'''
Given a relation applicable to the numerator, bound this
division accordingly. For example,
if self is "a / b" and the relation is a < x
return (a / b) < (x / b), provided b > 0.
Also see NumberOperation.deduce_bound.
'''
from proveit.numbers import zero, Less, LessEq, greater
from . import (strong_div_from_numer_bound__pos_denom,
weak_div_from_numer_bound__pos_denom,
strong_div_from_numer_bound__neg_denom,
weak_div_from_numer_bound__neg_denom)
if isinstance(relation, Judgment):
relation = relation.expr
if not (isinstance(relation, Less) or
isinstance(relation, LessEq)):
raise TypeError("relation is expected to be Less "
"or LessEq number relations, not %s"
%relation)
if self.numerator not in relation.operands:
raise ValueError("relation is expected to involve the "
"numerator of %s. %s does not."
%(self, relation))
_a = self.denominator
_x = relation.normal_lhs
_y = relation.normal_rhs
try:
deduce_number_set(self.denominator)
except UnsatisfiedPrerequisites:
pass
if greater(self.denominator, zero).readily_provable():
if isinstance(relation, Less):
bound = strong_div_from_numer_bound__pos_denom.instantiate(
{a: _a, x: _x, y: _y})
elif isinstance(relation, LessEq):
bound = weak_div_from_numer_bound__pos_denom.instantiate(
{a: _a, x: _x, y: _y})
elif Less(self.denominator, zero).readily_provable():
if isinstance(relation, Less):
bound = strong_div_from_numer_bound__neg_denom.instantiate(
{a: _a, x: _x, y: _y})
elif isinstance(relation, LessEq):
bound = weak_div_from_numer_bound__neg_denom.instantiate(
{a: _a, x: _x, y: _y})
else:
raise UnsatisfiedPrerequisites(
"We must know whether the denominator of %s "
"is positive or negative before we can use "
"'bound_via_numerator_bound'."%self)
if bound.rhs == self:
return bound.with_direction_reversed()
return bound
@relation_prover
def bound_via_denominator_bound(self, relation, **defaults_config):
'''
Given a relation applicable to the numerator, bound this
division accordingly. For example,
if self is "a / b" and the relation is b > y
return (a / b) < (a / y), provided a, b, and y are positive.
Also see NumberOperation.deduce_bound.
'''
from proveit.numbers import zero, Less, LessEq, greater, greater_eq
from . import (strong_div_from_denom_bound__all_pos,
weak_div_from_denom_bound__all_pos,
strong_div_from_denom_bound__all_neg,
weak_div_from_denom_bound__all_neg,
strong_div_from_denom_bound__neg_over_pos,
weak_div_from_denom_bound__neg_over_pos,
strong_div_from_denom_bound__pos_over_neg,
weak_div_from_denom_bound__pos_over_neg)
if isinstance(relation, Judgment):
relation = relation.expr
if not (isinstance(relation, Less) or
isinstance(relation, LessEq)):
raise TypeError("relation is expected to be Less "
"or LessEq number relations, not %s"
%relation)
if self.denominator not in relation.operands:
raise ValueError("relation is expected to involve the "
"denominator of %s. %s does not."
%(self, relation))
_a = self.numerator
_x = relation.normal_lhs
_y = relation.normal_rhs
try:
# Ensure that we relate both _x and _y to zero by knowing
# one of these.
ordering = LessEq.sort((_x, _y, zero))
ordering.operands[0].apply_transitivity(ordering.operands[1])
except:
pass # We'll generate an appropriate error below.
try:
deduce_number_set(self.numerator)
deduce_number_set(self.denominator)
except UnsatisfiedPrerequisites:
pass
pos_numer = greater_eq(self.numerator, zero).readily_provable()
neg_numer = LessEq(self.numerator, zero).readily_provable()
pos_denom = greater(self.denominator, zero).readily_provable()
neg_denom = Less(self.denominator, zero).readily_provable()
if not (pos_numer or neg_numer) or not (pos_denom or neg_denom):
raise UnsatisfiedPrerequisites(
"We must know the sign of the numerator and "
"denominator of %s before we can use "
"'bound_via_denominator_bound'."%self)
if pos_numer and pos_denom:
if isinstance(relation, Less):
bound = strong_div_from_denom_bound__all_pos.instantiate(
{a: _a, x: _x, y: _y})
elif isinstance(relation, LessEq):
bound = weak_div_from_denom_bound__all_pos.instantiate(
{a: _a, x: _x, y: _y})
elif neg_numer and neg_denom:
if isinstance(relation, Less):
bound = strong_div_from_denom_bound__all_neg.instantiate(
{a: _a, x: _x, y: _y})
elif isinstance(relation, LessEq):
bound = weak_div_from_denom_bound__all_neg.instantiate(
{a: _a, x: _x, y: _y})
elif pos_numer and neg_denom:
if isinstance(relation, Less):
bound = strong_div_from_denom_bound__pos_over_neg.instantiate(
{a: _a, x: _x, y: _y})
elif isinstance(relation, LessEq):
bound = weak_div_from_denom_bound__pos_over_neg.instantiate(
{a: _a, x: _x, y: _y})
elif neg_numer and pos_denom:
if isinstance(relation, Less):
bound = strong_div_from_denom_bound__neg_over_pos.instantiate(
{a: _a, x: _x, y: _y})
elif isinstance(relation, LessEq):
bound = weak_div_from_denom_bound__neg_over_pos.instantiate(
{a: _a, x: _x, y: _y})
else:
raise UnsatisfiedPrerequisites(
"We must know whether or not the denominator of %s "
"is positive or negative before we can use "
"'bound_via_denominator_bound'."%self)
if bound.rhs == self:
return bound.with_direction_reversed()
return bound
[docs]def frac(numer, denom):
return Div(numer, denom)
[docs]def compose_fraction(numerator, denominator):
'''
Return the expression representing a fraction making obvious
simplifications if the denominator is one or if either/both the
numerator/denominator are fractions.
'''
from proveit.numbers import one, compose_product, negated, Neg
if isinstance(denominator, Neg):
denominator = denominator.operand
numerator = negated(numerator)
if denominator == one:
return numerator
if isinstance(numerator, Div) and isinstance(denominator, Div):
numerator, denominator = (
compose_product(numerator.numerator, denominator.denominator),
compose_product(numerator.denominator, denominator.numerator))
elif isinstance(numerator, Div):
denominator = compose_product(numerator.denominator, denominator)
numerator = numerator.numerator
elif isinstance(denominator, Div):
numerator = compose_product(numerator, denominator.denominator)
denominator = denominator.numerator
if isinstance(numerator, Neg):
return Neg(Div(numerator.operand, denominator))
return Div(numerator, denominator)