# Demonstrations for the theory of proveit.numbers.division¶

In [1]:
from proveit import defaults
from proveit import a, b, c, d, m, n, w, x, y, z, P, S, Px
from proveit.logic import Forall, InSet, NotEquals
from proveit.numbers import (
zero, one, two, three, four, Add, frac, Div, Exp, greater,
greater_eq, Less, LessEq, Mult, Neg, num, subtract, Sum)
from proveit.numbers import Complex, ComplexNonZero, Integer, Interval, Real
%begin demonstrations

In [2]:
assumptions = [InSet(var, Complex) for var in [a, b, c, d, x, y, z]]
assumptions = assumptions + [InSet(var, Integer) for var in [a, b]]
assumptions += [NotEquals(var, zero) for var in [a, b, c, d]]
#assumptions += [InSet(var, Complex) for var in [c, d, x, y, z]]


## Reducing rationals¶

In [3]:
frac(Neg(four), four).evaluation()

In [4]:
frac(four, Neg(four)).evaluation()

In [5]:
frac(frac(four, three), two).evaluation()

In [6]:
frac(frac(four, three), frac(two, three)).evaluation()

In [7]:
frac(Mult(frac(four, three), a, b), Mult(frac(two, three), c)).simplification(assumptions=assumptions)

, , ,  ⊢

## Factorization¶

In [8]:
expr_01 = frac(Add(a, b, c), d)

expr_01:
In [9]:
expr_01.factorization(frac(one, d), assumptions=assumptions)

, , , ,  ⊢
In [10]:
expr_01.factorization(frac(one, d), pull='right', assumptions=assumptions)

, , , ,  ⊢

Test trivial cases where the factor is the entire expression.

In [11]:
expr_01.factorization(frac(expr_01.numerator, d), assumptions=assumptions)

In [12]:
expr_01.factorization(frac(expr_01.numerator, d), pull='right', assumptions=assumptions)

In [13]:
expr_02 = frac(Mult(Add(a, b, c), b), d)

expr_02:
In [14]:
expr_02.factorization(frac(b, d), assumptions=assumptions)

, , , ,  ⊢
In [15]:
expr_02.factorization(frac(b, d), pull='right', assumptions=assumptions)

, , , ,  ⊢
In [16]:
expr_03 = frac(Mult(Add(a, b, c), b), Mult(a, d))

expr_03:
In [17]:
expr_03.factorization(frac(b, d), assumptions=assumptions)

, , , , ,  ⊢
In [18]:
expr_03.factorization(frac(b, d), pull='right', assumptions=assumptions)

, , , , ,  ⊢
In [19]:
expr_03.factorization(frac(one, d), assumptions=assumptions)

, , , , ,  ⊢
In [20]:
expr_03.factorization(frac(one, d), pull='right', assumptions=assumptions)

, , , , ,  ⊢
In [21]:
expr_03.factorization(frac(expr_03.numerator, d), pull='right', assumptions=assumptions)

, , , , ,  ⊢
In [22]:
expr_03.factorization(frac(expr_03.numerator, d), pull='left', assumptions=assumptions)

, , , , ,  ⊢
In [23]:
expr_03.reduction_to_mult(assumptions=assumptions).rhs.factorization(b, assumptions=assumptions)

, , ,  ⊢
In [24]:
expr_03.factorization(Exp(d, Neg(one)), pull='left', assumptions=assumptions)

, , , , ,  ⊢
In [25]:
expr_03.factorization(frac(Mult(b, Exp(a, Neg(one))), d), pull='right', assumptions=assumptions)

, , , , ,  ⊢

## Distribution¶

In [26]:
expr_01

In [27]:
our_assumptions = [InSet(var, Real) for var in [a, b, c, d]]
our_assumptions = our_assumptions + [NotEquals(d, zero)]
our_assumptions = our_assumptions + [InSet(Px, Real)]

our_assumptions:
In [28]:
# distribute_frac_through_sum

In [29]:
from proveit.numbers.division import distribute_frac_through_sum
distribute_frac_through_sum

In [30]:
_n_sub = num(expr_01.numerator.operands.num_entries())
_x_sub = expr_01.numerator.operands
_y_sub = expr_01.denominator
distribute_frac_through_sum.instantiate(
{n: _n_sub, x: _x_sub, y: _y_sub}, assumptions=our_assumptions)

, , , ,  ⊢
In [31]:
expr_01.distribution(assumptions=our_assumptions)

, , , ,  ⊢
In [32]:
expr_04 = frac(subtract(a, b), d)

expr_04:
In [33]:
expr_04_dist = expr_04.distribution(assumptions=our_assumptions)

expr_04_dist: , , ,  ⊢
In [34]:
expr_05 = frac(Sum(x, Px, domain=Interval(y, z)), d)

expr_05:
In [35]:
from proveit.numbers.division import distribute_frac_through_summation
distribute_frac_through_summation

In [36]:
# We have a theorem for distributing a non-zero divisor over a summation
distribute_frac_through_summation.instantiate(
{P: P, S: Interval(y, z), y: x, z: d},
assumptions=our_assumptions+[Forall(x, InSet(Px, Complex), domain=Interval(y, z))])

In [37]:
# but we have not integrated the distribute_frac_through_summation
# into the general distribution() method:
try:
expr_05.distribution(
assumptions=our_assumptions+[Forall(x, InSet(Px, Complex), domain=Interval(y, z))])
assert False, "Expecting NotImplementedError; should not make it this far!"
except NotImplementedError as the_error:
print("NotImplementedError: {}".format(the_error))

NotImplementedError: Distribution of division through summation not yet implemented.


### Div.neg_extraction()¶

In [38]:
from proveit.numbers import Neg
from proveit.numbers.division import neg_frac_neg_numerator, neg_frac_neg_numerator_gen

In [39]:
# create a few example expressions
neg_a_over_b, a_over_neg_b, neg_mult_over_b, neg_mult_02_over_b, a_over_neg_mult = (
frac(Neg(a), b), frac(a, Neg(b)), frac(Mult(Neg(a), c), b),
frac(Mult(a, Neg(c)), b), frac(a, Mult(Neg(b), c)))

neg_a_over_b:
a_over_neg_b:
neg_mult_over_b:
neg_mult_02_over_b:
a_over_neg_mult:
In [40]:
# with no neg_loc kwarg supplied, finds the Neg to factor out of numerator
neg_a_over_b.neg_extraction(assumptions=[InSet(a, Real), InSet(b, Real), NotEquals(b, zero)])

, ,  ⊢
In [41]:
# with no neg_loc kwarg supplied, finds the Neg to factor out of numerator
neg_a_over_b.simplification(assumptions=[InSet(a, Real), InSet(b, Real), NotEquals(b, zero)])

, ,  ⊢
In [42]:
# with no neg_loc kwarg supplied, finds the Neg to factor out of denominator
a_over_neg_b.neg_extraction(assumptions=[InSet(a, Real), InSet(b, Real), NotEquals(b, zero)])

, ,  ⊢
In [43]:
# can instead specify to factor out Neg from numerator
neg_a_over_b.neg_extraction(neg_loc = 'numerator', assumptions=[InSet(a, Real), InSet(b, Real), NotEquals(b, zero)])

, ,  ⊢
In [44]:
# can instead specify to factor out Neg from denominator
a_over_neg_b.neg_extraction(neg_loc = 'denominator', assumptions=[InSet(a, Real), InSet(b, Real), NotEquals(b, zero)])

, ,  ⊢
In [45]:
neg_mult_over_b.neg_extraction(
assumptions=[InSet(a, Real), InSet(b, Real), InSet(c, Real), NotEquals(b, zero)])

, , ,  ⊢
In [46]:
neg_mult_02_over_b.neg_extraction(
assumptions=[InSet(a, Real), InSet(b, Real), InSet(c, Real), NotEquals(b, zero)])

, , ,  ⊢
In [47]:
a_over_neg_mult

In [48]:
a_over_neg_mult.neg_extraction(
assumptions=[InSet(a, Real), InSet(b, Real), InSet(c, Real),
NotEquals(b, zero), NotEquals(c, zero)])

, , , ,  ⊢
In [49]:
# notice that the neg_extraction has been integrated into the
# shallow_simplification() method
neg_a_over_b.shallow_simplification(assumptions=[InSet(a, Real), InSet(b, Real), NotEquals(b, zero)])

, ,  ⊢
In [50]:
# notice that the neg_extraction has been integrated into the
# simplification() method
neg_mult_over_b.simplification(assumptions=[InSet(a, Real), InSet(b, Real), NotEquals(b, zero),
InSet(c, Real), NotEquals(c, zero)])

, , ,  ⊢
In [51]:
# notice that the neg_extraction has been integrated into the
# simplification() method
neg_mult_02_over_b.simplification(assumptions=[InSet(a, Real), InSet(b, Real), NotEquals(b, zero),
InSet(c, Real), NotEquals(c, zero)])

, , ,  ⊢
In [52]:
# example expression with no Neg component
no_neg_expr = frac(a, Mult(b, c))

no_neg_expr:
In [53]:
# informative error message when no Neg available to extract:
try:
no_neg_expr.neg_extraction(
assumptions=[InSet(a, Real), InSet(b, Real), InSet(c, Real),
NotEquals(b, zero), NotEquals(c, zero)])
except ValueError as the_error:
print("ValueError: {}".format(the_error))

ValueError: No Neg expression component found to extract. The expression supplied was: a / (b * c)


## Deduce bounds¶

In [54]:
assumptions = [InSet(var, Real) for var in [a, b, c, d, w, x, y]]
assumptions += [greater(var, zero) for var in [a, x, y]] + [greater_eq(b, zero)]
assumptions += [LessEq(c, zero)] + [Less(var, zero) for var in [d, w]]
assumptions += [InSet(z, Real)]


Bound by the numerator with a positive denominator

In [55]:
relation = greater(a, x)
frac(a, y).deduce_bound(relation, assumptions=assumptions+[relation])

, , , ,  ⊢
In [56]:
relation = Less(a, x)
frac(a, y).deduce_bound(relation, assumptions=assumptions+[relation])

, , , ,  ⊢
In [57]:
relation = greater_eq(a, x)
frac(a, y).deduce_bound(relation, assumptions=assumptions+[relation])

, , , ,  ⊢
In [58]:
relation = LessEq(a, x)
frac(a, y).deduce_bound(relation, assumptions=assumptions+[relation])

, , , ,  ⊢

Bound by the numerator with a negative denominator

In [59]:
relation = greater(a, x)
frac(a, d).deduce_bound(relation, assumptions=assumptions+[relation])

, , , ,  ⊢
In [60]:
relation = Less(a, x)
frac(a, d).deduce_bound(relation, assumptions=assumptions+[relation])

, , , ,  ⊢
In [61]:
relation = greater_eq(a, x)
frac(a, d).deduce_bound(relation, assumptions=assumptions+[relation])

, , , ,  ⊢
In [62]:
relation = LessEq(a, x)
frac(a, d).deduce_bound(relation, assumptions=assumptions+[relation])

, , , ,  ⊢

Bound by the denominator with everything positive

In [63]:
relation = greater(x, y)
frac(a, x).deduce_bound(relation, assumptions=assumptions+[relation])

, , , , , ,  ⊢
In [64]:
relation = Less(x, y)
frac(a, x).deduce_bound(relation, assumptions=assumptions+[relation])

, , , , , ,  ⊢
In [65]:
relation = greater_eq(x, y)
frac(b, x).deduce_bound(relation, assumptions=assumptions+[relation])

, , , , , ,  ⊢
In [66]:
relation = LessEq(x, y)
frac(b, x).deduce_bound(relation, assumptions=assumptions+[relation])

, , , , , ,  ⊢

Bound by the denominator with everything negative

In [67]:
relation = greater(w, c)
frac(w, d).deduce_bound(relation, assumptions=assumptions+[relation])

, , , ,  ⊢
In [68]:
relation = Less(w, c)
frac(w, d).deduce_bound(relation, assumptions=assumptions+[relation])

, , , ,  ⊢
In [69]:
relation = greater_eq(c, w)
frac(c, d).deduce_bound(relation, assumptions=assumptions+[relation])

, , , ,  ⊢
In [70]:
relation = LessEq(c, w)
frac(c, d).deduce_bound(relation, assumptions=assumptions+[relation])

, , , ,  ⊢

Bound by the denominator with the numerator positive and denominator negative

In [71]:
relation = greater(d, w)
frac(a, d).deduce_bound(relation, assumptions=assumptions+[relation])

, , , , , ,  ⊢
In [72]:
relation = Less(d, w)
frac(a, d).deduce_bound(relation, assumptions=assumptions+[relation])

, , , , , ,  ⊢
In [73]:
relation = greater_eq(d, w)
frac(b, d).deduce_bound(relation, assumptions=assumptions+[relation])

, , , , , ,  ⊢
In [74]:
relation = LessEq(d, w)
frac(b, d).deduce_bound(relation, assumptions=assumptions+[relation])

, , , , , ,  ⊢

Bound by the denominator with the numerator negative and denominator positive

In [75]:
relation = greater(a, x)
frac(d, a).deduce_bound(relation, assumptions=assumptions+[relation])

, , , , , ,  ⊢
In [76]:
relation = Less(a, x)
frac(d, a).deduce_bound(relation, assumptions=assumptions+[relation])

, , , , , ,  ⊢
In [77]:
relation = greater_eq(a, x)
frac(c, a).deduce_bound(relation, assumptions=assumptions+[relation])

, , , , , ,  ⊢
In [78]:
relation = LessEq(a, x)
frac(c, a).deduce_bound(relation, assumptions=assumptions+[relation])

, , , , , ,  ⊢

Bound numerator and denominator simultaneously

In [79]:
# Here, we automatically prove that z < 0 indirectly.
relations = [greater(d, z), greater(a, x)]
frac(a, d).deduce_bound(relations, assumptions=assumptions+relations)

, , , , , , ,  ⊢
In [80]:
# Here, we automatically prove that z > 0 indirectly.
relations = [LessEq(a, z), LessEq(c, d)]
frac(c, a).deduce_bound(relations, assumptions=assumptions+relations)

, , , , , , ,  ⊢

## Distribution¶

In [81]:
defaults.assumptions = [InSet(_x, Complex) for _x in (a, b, c, d)] + [NotEquals(d, zero)]

defaults.assumptions:
In [82]:
frac(Add(a, b, c), d).distribution()

, , , ,  ⊢
In [83]:
frac(subtract(a, b), d).distribution()

, , ,  ⊢

## Testing Div.div_in_denominator_reduction()¶

In [84]:
frac(a, frac(b, c)).div_in_denominator_reduction(
assumptions=[InSet(a, Complex), InSet(b, Complex), InSet(c, Complex),
NotEquals(b, zero), NotEquals(c, zero)])

, , , ,  ⊢
In [85]:
# and the div_in_denominator_reduction() should be integrated into the shallow_simplification() method
frac(a, frac(b, c)).simplification(
assumptions=[InSet(a, Complex), InSet(b, Complex), InSet(c, Complex),
NotEquals(b, zero), NotEquals(c, zero)])

, , , ,  ⊢

## Multiplying The Top & Bottom by The Same (Non-Zero) Value¶

The top_and_bottom_multiplication() method relies on the frac_cancel_left and frac_cancel_right theorems in the division package:

In [86]:
from proveit.numbers.division import frac_cancel_left
display(frac_cancel_left)

In [87]:
from proveit.numbers.division import frac_cancel_right
display(frac_cancel_right)


Technically, we could omit the requirement that $z \ne 0$ (because that would then give an undefined or nonsensical expression equal to another undefined or nonsensical expression), but for simplicity we maintain the $z \ne 0$ condition.

First, some simple assumptions about term domains:

In [88]:
assumptions = [InSet(var, Complex) for var in [a, b, c, d]]
assumptions = assumptions + [InSet(var, Integer) for var in [a, b]]
assumptions += [NotEquals(var, zero) for var in [a, b, c, d]]


First, some example Divs (in the form of fracs) to play with:

In [89]:
example_frac_01, example_frac_02, example_frac_03, example_frac_04 = (
frac(a, b),
frac(Mult(c, a), Mult(c, b)),

example_frac_01:
example_frac_02:
example_frac_03:
example_frac_04:

And note the working assumptions:

In [90]:
assumptions


The most basic result: $\frac{a}{b} = \frac{ca}{cb}$

In [91]:
temp_result = example_frac_01.top_and_bottom_multiplication(c, assumptions=assumptions)

temp_result: , , , ,  ⊢

Notice if we now pull out the factor of a on the rhs, Prove-It automatically re-cancels the common factor of c in the top and bottom:

In [92]:
temp_result.inner_expr().rhs.factor(a)

, , , ,  ⊢

unless we explicitly suspend the cancelation simplification proccess:

In [93]:
with Div.temporary_simplification_directives() as tmp_directives:
tmp_directives.cancel_factors = False
temp_result.inner_expr().rhs.factor(a)

, , , ,  ⊢

The top_and_bottom_multiplication works without automatically distributing across more complicated numerators or denominators:

In [94]:
example_frac_03.top_and_bottom_multiplication(c, assumptions=assumptions+[InSet(Add(b, d), ComplexNonZero)])

, , , ,  ⊢

but will combine terms into Exp expressions when like terms are found, such as taking $bb$ to $b^{2}$ in the following example:

In [95]:
temp_result = example_frac_01.top_and_bottom_multiplication(b, assumptions=assumptions)

temp_result: , ,  ⊢

Notice in this case that if we now pull out the factor of a on the rhs, Prove-It does not automatically cancel the introduced common factor of b in the top and bottom, but this is because it doesn't yet recognize the factor of b in the Exp expression in the denominator:

In [96]:
temp_result.inner_expr().rhs.factor(a)

, ,  ⊢

Combining like terms after the top_and_bottom_multiplication happens with more complicated terms as well:

In [97]:
temp_result = example_frac_03.top_and_bottom_multiplication(

temp_result: , ,  ⊢

We could then commute the multiplicands if desired:

In [98]:
temp_result.rhs.inner_expr().numerator.commutation(0,1, assumptions=assumptions+[InSet(Add(b, d), ComplexNonZero)])

, ,  ⊢

or we could avail ourselves of the numerator_mult and denominator_mult options (left-multiplication is the default for both numerator and denominator):

In [99]:
example_frac_03.top_and_bottom_multiplication(

, ,  ⊢
In [100]:
temp_result = example_frac_04.top_and_bottom_multiplication(

temp_result: , , ,  ⊢
In [101]:
temp_result = example_frac_04.top_and_bottom_multiplication(

temp_result: , , , ,  ⊢

The automatic combining of like terms might produce somewhat unexpected results, such as the following numerator where left-multiplication would initially produce $(a+b)\cdot c \cdot (a+b)$ but automatic combining of like terms then gives $(a+b)^{2} \cdot c$:

In [102]:
temp_result = example_frac_04.top_and_bottom_multiplication(

temp_result: , , , ,  ⊢

Notice at the end of all these examples that common-factors cancelation should still happen automatically in other contexts (in other words, the suspension of the automatic cancelation simplifications was temporary):

In [103]:
# recall
print("example_frac_02 = ")
display(example_frac_02)
example_frac_02.simplification(assumptions=assumptions)

example_frac_02 =

, , , ,  ⊢
In [104]:
%end demonstrations