Demonstrations for the theory of proveit.numbers.division ¶

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

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¶

frac(Neg(four), four).evaluation()

frac(four, Neg(four)).evaluation()

frac(frac(four, three), two).evaluation()

frac(frac(four, three), frac(two, three)).evaluation()

frac(Mult(frac(four, three), a, b), Mult(frac(two, three), c)).simplification(assumptions=assumptions)

Factorization¶

expr_01 = frac(Add(a, b, c), d)

expr_01.factorization(frac(one, d), assumptions=assumptions)

expr_01.factorization(frac(one, d), pull='right', assumptions=assumptions)

Test trivial cases where the factor is the entire expression.

expr_01.factorization(frac(expr_01.numerator, d), assumptions=assumptions)

expr_01.factorization(frac(expr_01.numerator, d), pull='right', assumptions=assumptions)

expr_02 = frac(Mult(Add(a, b, c), b), d)

expr_02.factorization(frac(b, d), assumptions=assumptions)

expr_02.factorization(frac(b, d), pull='right', assumptions=assumptions)

expr_03 = frac(Mult(Add(a, b, c), b), Mult(a, d))

expr_03.factorization(frac(b, d), assumptions=assumptions)

expr_03.factorization(frac(b, d), pull='right', assumptions=assumptions)

expr_03.factorization(frac(one, d), assumptions=assumptions)

expr_03.factorization(frac(one, d), pull='right', assumptions=assumptions)

expr_03.factorization(frac(expr_03.numerator, d), pull='right', assumptions=assumptions)

expr_03.factorization(frac(expr_03.numerator, d), pull='left', assumptions=assumptions)

expr_03.reduction_to_mult(assumptions=assumptions).rhs.factorization(b, assumptions=assumptions)

expr_03.factorization(Exp(d, Neg(one)), pull='left', assumptions=assumptions)

expr_03.factorization(frac(Mult(b, Exp(a, Neg(one))), d), pull='right', assumptions=assumptions)

Distribution¶

expr_01

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)]

# distribute_frac_through_sum

from proveit.numbers.division import distribute_frac_through_sum
distribute_frac_through_sum

_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)

expr_01.distribution(assumptions=our_assumptions)

expr_04 = frac(subtract(a, b), d)

expr_04_dist = expr_04.distribution(assumptions=our_assumptions)

expr_05 = frac(Sum(x, Px, domain=Interval(y, z)), d)

from proveit.numbers.division import distribute_frac_through_summation
distribute_frac_through_summation

# 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))])

# 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()¶

from proveit.numbers import Neg
from proveit.numbers.division import neg_frac_neg_numerator, neg_frac_neg_numerator_gen

# 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)))

# 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)])

# 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)])

# 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)])

# 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)])

# 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)])

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

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

a_over_neg_mult

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

# 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)])

# 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)])

# 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)])

# example expression with no Neg component
no_neg_expr = frac(a, Mult(b, c))

# 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¶

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

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

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

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

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

Bound by the numerator with a negative denominator

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

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

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

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

Bound by the denominator with everything positive

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

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

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

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

Bound by the denominator with everything negative

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

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

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

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

Bound by the denominator with the numerator positive and denominator negative

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

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

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

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

Bound by the denominator with the numerator negative and denominator positive

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

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

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

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

Bound numerator and denominator simultaneously

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

# 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¶

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

frac(Add(a, b, c), d).distribution()

frac(subtract(a, b), d).distribution()

Testing `Div.div_in_denominator_reduction()`¶

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)])

# 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)])

Testing `Div.top_and_bottom_multiplication()`¶

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:

from proveit.numbers.division import frac_cancel_left
display(frac_cancel_left)

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:

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:

example_frac_01, example_frac_02, example_frac_03, example_frac_04 = (
    frac(a, b),
    frac(Mult(c, a), Mult(c, b)),
    frac(Add(a, b), Add(b, d)),
    frac(Mult(c, Add(a, b)), Add(b, d)))

And note the working assumptions:

assumptions

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

temp_result = example_frac_01.top_and_bottom_multiplication(c, assumptions=assumptions)

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:

temp_result.inner_expr().rhs.factor(a)

unless we explicitly suspend the cancelation simplification proccess:

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:

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:

temp_result = example_frac_01.top_and_bottom_multiplication(b, assumptions=assumptions)

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:

temp_result.inner_expr().rhs.factor(a)

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

temp_result = example_frac_03.top_and_bottom_multiplication(
    Add(b, d), assumptions=assumptions+[InSet(Add(b, d), ComplexNonZero)])

We could then commute the multiplicands if desired:

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):

example_frac_03.top_and_bottom_multiplication(
        Add(b, d), numerator_mult="right",
        assumptions=assumptions+[InSet(Add(b, d), ComplexNonZero)])

temp_result = example_frac_04.top_and_bottom_multiplication(
        Add(b, d), numerator_mult="right",
        assumptions=assumptions+[InSet(Add(b, d), ComplexNonZero)])

temp_result = example_frac_04.top_and_bottom_multiplication(
        Add(a, b), numerator_mult="right",
        assumptions=assumptions+[InSet(Add(b, d), ComplexNonZero), InSet(Add(a,b), ComplexNonZero)])

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$:

temp_result = example_frac_04.top_and_bottom_multiplication(
        Add(a, b), numerator_mult="left", denominator_mult="right",
        assumptions=assumptions+[InSet(Add(b, d), ComplexNonZero), InSet(Add(a,b), ComplexNonZero)])

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):

# recall
print("example_frac_02 = ")
display(example_frac_02)
example_frac_02.simplification(assumptions=assumptions)

example_frac_02 =

%end demonstrations

Demonstrations for the theory of proveit.numbers.division¶

Reducing rationals¶

Factorization¶

Distribution¶

Div.neg_extraction()¶

Deduce bounds¶

Distribution¶

Testing Div.div_in_denominator_reduction()¶

Testing Div.top_and_bottom_multiplication()¶

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

Demonstrations for the theory of proveit.numbers.division ¶

Testing `Div.div_in_denominator_reduction()`¶

Testing `Div.top_and_bottom_multiplication()`¶