Demonstrations for the theory of proveit.numbers.multiplication ¶

import proveit
from proveit import defaults
from proveit import a, b, c, d, f, j, k, m, n, w, x, y, z, delta, theta
from proveit.core_expr_types import b_1_to_m
from proveit.logic import InSet, NotEquals, Equals
from proveit.numbers import (
    Natural, NaturalPos, Integer, IntegerNeg, IntegerNonPos, Interval,
    Rational, RationalPos, RationalNeg, RationalNonNeg, RationalNonPos,
    Real, RealPos, RealNeg, RealNonNeg, Complex)
from proveit.numbers import zero, one, two, three, four, five, e, i, pi
from proveit.numbers import (Add, Neg, Exp, frac, Less, LessEq, Mult, 
                             sqrt, sqrd, num, subtract, Sum)
from proveit.numbers.exponentiation import products_of_complex_powers
%begin demonstrations

Basic arithmetic with numerals¶

Mult(num(2), num(5)).evaluation()

Mult(num(-3), num(4)).evaluation()

Mult(num(3), num(-4)).evaluation()

Mult(num(-3), num(-3)).evaluation()

# multi-digit multiplication is not yet implemented
from proveit.logic import EvaluationError
try:
    Mult(num(12), num(-3)).evaluation()
except EvaluationError as _e:
    print(_e)
    print('because multi-digit multiplication is not implemented')

Evaluation of 12 * (-3) under assumptions {} is not known
because multi-digit multiplication is not implemented

Mult(frac(num(2), num(3)), frac(num(3), num(2))).evaluation()

Mult(frac(num(2), num(3)), frac(num(5), num(3))).evaluation()

Mult(frac(num(-2), num(3)), frac(num(5), num(3))).evaluation()

Mult(frac(num(-2), num(3)), frac(num(6), num(-5))).evaluation()

expr = Mult(four, Exp(three, n), Exp(four, n), two, three, frac(one, five))

expr.simplification(assumptions=[InSet(n, NaturalPos)])

expr.simplification(assumptions=[InSet(n, NaturalPos)])

with Mult.temporary_simplification_directives() as tmp_directives:
    tmp_directives.combine_numeric_rationals=False
    display(expr.simplification(assumptions=[InSet(n, NaturalPos)]))

with Mult.temporary_simplification_directives() as mult_directives:
    mult_directives.combine_numeric_rationals=False
    mult_directives.combine_all_exponents=True
    with Exp.temporary_simplification_directives() as exp_directives:
        exp_directives.factor_numeric_rational=False
        expr.simplification(assumptions=[InSet(n, NaturalPos)])

Deduce in a number set¶

InSet(Mult(a, b), IntegerNeg).prove(assumptions=[InSet(a, IntegerNeg), 
                                                 InSet(b, NaturalPos)])

InSet(Mult(a, b), RationalNonPos).prove(assumptions=[InSet(a, RationalNonNeg), 
                                                     InSet(b, RationalNeg)])

InSet(Mult(a, b, c, d), RealPos).prove(assumptions=[InSet(a, RationalNeg), 
                                                    InSet(b, NaturalPos),
                                                    InSet(c, RationalNeg),
                                                    InSet(d, RealPos)])

Miscellaneous examples that need to be organized better¶

Mult(four, a).conversion_to_addition(assumptions=[InSet(a, Complex)])

complex_assumptions = \
    [InSet(a, Complex), InSet(b, Complex), InSet(c, Complex), InSet(d, Complex), InSet(f, Complex)]

Mult(a,b,c,d,f).association(0,2, assumptions=complex_assumptions)

naturals_assumptions = \
    [InSet(a, Natural), InSet(b, Natural), InSet(c, Natural), InSet(d, Natural), InSet(f, Natural)]

InSet(Mult(a,b),Natural).prove(assumptions=naturals_assumptions)

naturals_pos_assumptions = \
    [InSet(a, NaturalPos), InSet(b, NaturalPos), InSet(c, NaturalPos), InSet(d, NaturalPos), InSet(f, NaturalPos)]

InSet(Mult(a,b),NaturalPos).prove(assumptions=naturals_pos_assumptions)

integers_assumptions = \
    [InSet(a, Integer), InSet(b, Integer), InSet(c, Integer), InSet(d, Integer), InSet(f, Integer)]

InSet(Mult(a,b,c,d,f),Integer).prove(assumptions=integers_assumptions)

reals_assumptions = \
    [InSet(a, Real), InSet(b, Real), InSet(c, Real), InSet(d, Real), InSet(f, Real)]

InSet(Mult(a,b,c,d,f),Real).prove(assumptions=reals_assumptions)

reals_pos_assumptions = \
    [InSet(a, RealPos), InSet(b, RealPos), InSet(c, RealPos), InSet(d, RealPos), InSet(f, RealPos)]

InSet(Mult(a,b,c,d,f),RealPos).prove(assumptions=reals_pos_assumptions)

Distribution¶

assumptions = [InSet(var, Complex) for var in [c, d, w, x, y, z]]
assumptions = assumptions + [InSet(var, Integer) for var in [a, b]]

expr = Mult(a, b, Add(x, y, z), c, d)

expr.distribution(2, assumptions=assumptions)

expr = Mult(a, b, subtract(x, y), c, d)

expr.distribution(2, assumptions=assumptions)

We can specify specific factors to distribute on the left and right¶

via expressions:

expr.distribution(2, left_factors=[b], right_factors=[d], assumptions=assumptions)

or via indices:

expr.distribution(2, left_factors=[4], right_factors=[1, 3], assumptions=assumptions)

expr.distribution(2, left_factors=[0, 4], right_factors=[1], assumptions=assumptions)

expr.distribution(2, left_factors=[0, 4], right_factors=[1, 3], assumptions=assumptions)

Mult.distribution must be updated for the Sum case.¶

expr = Mult(Add(a, b), Sum(k, k, domain=Interval(a, b)), frac(a, b))

assumptions = [InSet(var, Integer) for var in [a, b]] + [NotEquals(b, num(0))]

Broken demonstrations below need to be fixed
Shown as markdown instead of code temporarily

InSet(k, Integer).prove(assumptions=[InSet(k, Interval(a, b))]).generalize(k, domain=Interval(a, b))

InSet(Sum(k, k, domain=Interval(a, b)), Complex).prove()

expr.distribute(0, assumptions)

expr.distribute(1, assumptions)

expr.distribute(2, assumptions)

expr = Mult(z, y, Sum(x, x, domain=Interval(a, b)), z, y)

expr.distribution(2, assumptions=assumptions)

Factoring¶

assumptions = [InSet(var, Complex) for var in [c, d, w, x, y, z]]
assumptions = assumptions + [InSet(var, Integer) for var in [a, b]]

expr = Mult(x, y)

expr.factorization(x, 'left', assumptions=assumptions)

expr.factorization(x, 'right', assumptions=assumptions)

expr.factorization(y, 'left', assumptions=assumptions)

expr.factorization(y, 'right', assumptions=assumptions)

expr = Mult(x, y, z)

expr.factorization(x, 'left', assumptions=assumptions)

expr.factorization(x, 'left', group_remainder=True, assumptions=assumptions)

expr.factorization(x, 'right', assumptions=assumptions)

expr.factorization(x, 'right', group_remainder=True, assumptions=assumptions)

expr.factorization(y, 'left', assumptions=assumptions)

expr.factorization(y, 'right', assumptions=assumptions)

expr.factorization(z, 'left', assumptions=assumptions)

expr.factorization(z, 'right', assumptions=assumptions)

Factor multiple factors¶

Note: the functionality is the same whether we provide the factors as an iterable or as a Mult.

expr.factorization(Mult(x, y), 'left', assumptions=assumptions)

expr.factorization((x, y), 'right', assumptions=assumptions)

expr.factorization((y, z), 'left', assumptions=assumptions)

expr.factorization(Mult(y, z), 'right', assumptions=assumptions)

expr.factorization(Mult(x, z), 'left', assumptions=assumptions)

expr.factorization((x, z), 'right', assumptions=assumptions)

expr = Mult(x, y, z, w)

expr.factorization((x, z), 'left', assumptions=assumptions)

expr.factorization((x, w), 'left', assumptions=assumptions, group_remainder=True)

expr.factorization((y, w), 'left', assumptions=assumptions, group_factors=False)

expr.factorization((x, z), 'right', assumptions=assumptions)

expr.factorization(Mult(y, w), 'right', assumptions=assumptions, group_remainder=True)

expr.factorization(Mult(x, w), 'right', assumptions=assumptions, group_factors=False, group_remainder=True)

Recursive factorization¶

Mult(x, y, Add(Mult(z, w), Mult(y, z))).readily_factorable(z)

True

Mult(x, y, Add(Mult(z, w), Mult(y, z)), w).readily_factorable(Mult(x, z, w))

False

Mult(x, y, Add(Mult(z, w), Mult(y, z)), w).factorization(
    z, 'right', assumptions=assumptions)

Mult(x, y, Add(Mult(z, w), Mult(y, z)), w).factorization(
    z, 'right', assumptions=assumptions, group_remainder=True)

Mult(x, y, Add(Mult(z, w), Mult(y, z)), w).factorization(
    z, 'left', assumptions=assumptions, group_remainder=True)

Mult(x, y, Add(Mult(z, w), Mult(y, z)), w).factorization(
    Mult(w, z, x), 'left', assumptions=assumptions)

Mult(x, y, Add(Mult(z, w), Mult(y, z)), w).factorization(
    Mult(w, z, x), 'right', assumptions=assumptions)

Mult(x, y, Add(Mult(z, w), Mult(y, z)), w).factorization(
    Mult(x, y, z), 'left', group_remainder=True, assumptions=assumptions)

Mult(x, y, Add(Mult(z, w), Mult(y, z)), w).factorization(
    Mult(x, y, z), 'right', group_factors=False, assumptions=assumptions)

Canceling Factors Appearing in Numerator/Denominator: `Mult.cancelations()`¶

mult_3_factors_01 = Mult(a, Mult(b, frac(c, a)))

mult_3_factors_02 = Mult(Mult(a, b), frac(c, a))

mult_3_factors_03 = Mult(Mult(a, b), frac(one, a))

temp_assumptions_for_cancelation = (
    [InSet(a, Real), InSet(b, Real), InSet(c, Real), NotEquals(a, zero)])

mult_3_factors_01.cancelations(assumptions=temp_assumptions_for_cancelation)

mult_3_factors_01.simplification(assumptions=temp_assumptions_for_cancelation)

mult_3_factors_02.cancelations(assumptions=temp_assumptions_for_cancelation)

mult_3_factors_02.simplification(assumptions=temp_assumptions_for_cancelation)

mult_3_factors_03.cancelations(assumptions=temp_assumptions_for_cancelation)

mult_3_factors_03.simplification(assumptions=temp_assumptions_for_cancelation)

`Mult.combining_exponents()`: Combining Exponential Factors with the Same Base¶

# some example products of exponentials
mult_exps_01, mult_exps_02, mult_exps_03, mult_exps_04 = (
    Mult(Exp(two, three), Exp(two, four)),
    Mult(Exp(a, b), Exp(a, c)),
    Mult(Exp(a, b), Exp(a, c), Exp(a, b)),
    Mult(Exp(a, b), Exp(a, c), Exp(a, b), Exp(a, d)))

# some useful assumptions for the testing
temp_assumptions = [InSet(a, RealPos), InSet(b, Real), InSet(c, Real), InSet(d, Real)]

mult_exps_01.combining_exponents(auto_simplify=False)

mult_exps_02.combining_exponents(assumptions=temp_assumptions)

# here notice: the combo of 3 operands and the simplification
mult_exps_03.combining_exponents(assumptions=temp_assumptions)

# here notice: the combo of 4 operands and the simplification
mult_exps_04.combining_exponents(assumptions=temp_assumptions)

# define a product with a non-matching base
mult_of_exps_with_non_exp = Mult(Exp(a, b), Exp(a, c), Exp(a, b), Exp(a, d), b)

# without specifying what to combine, we have an error:
try:
    mult_of_exps_with_non_exp.combining_exponents(assumptions=temp_assumptions)
except Exception as the_exception:
    print("Error: {}".format(the_exception))

Error: Unable to combine exponents because exponential bases differ: a^{b} * a^{c} * a^{b} * a^{d} * b

# But if we specify the factors to combine:
mult_of_exps_with_non_exp.combining_exponents(start_idx = 1, end_idx=3, assumptions=temp_assumptions)

Trying the newly-coded method (in progress):

# special case where only start index is specified
mult_exps_04.combining_exponents(start_idx = 0, assumptions=temp_assumptions)

# special case where only end index is specified
mult_exps_04.combining_exponents(end_idx=2, assumptions=temp_assumptions)

# using start and end indices
mult_exps_04.combining_exponents(start_idx = 1, end_idx=3, assumptions=temp_assumptions)

# an example expression with all numeric values
mult_exps_pows_of_2 = Mult(Exp(two, one), Exp(two, two), Exp(two, three))

# by default, combine all exponentials into a single exponential
# and simplify the resulting exponent
mult_exps_pows_of_2.combining_exponents(auto_simplify=False)

# special case of same bases but one without an exponent
mult_exps_left_without_exp = Mult(two, Exp(two, two))

# combine exponents for the special case
mult_exps_left_without_exp.combining_exponents(auto_simplify=False)

# special case of same bases but one without an exponent
mult_exps_right_without_exp = Mult(Exp(three, two), three)

# combine exponents for the special case
mult_exps_right_without_exp.combining_exponents(auto_simplify=False)

# variable version of a special case
mult_exps_right_without_exp_var = Mult(Exp(a, b), a)

mult_exps_right_without_exp_var.combining_exponents(assumptions=temp_assumptions)

# Recall this from earlier:
mult_exps_03.combining_exponents(assumptions=temp_assumptions)

# and the same thing, but now disallow the simplification of the resulting exponent
mult_exps_03.combining_exponents(auto_simplify=False, assumptions=temp_assumptions)

`Mult.common_power_extraction()`: Combining Exponential Factors with the Same Exponent¶

# some example products of exponentials
mult_exps_05, mult_exps_06, mult_exps_07 = (
    Mult(Exp(two, three), Exp(three, three)),
    Mult(Exp(a, d), Exp(b, d)),
    Mult(Exp(a, d), Exp(b, d), Exp(c, d)))

# some useful assumptions for the testing
temp_assumptions_02 = [InSet(a, RealPos), InSet(b, RealPos), InSet(c, RealPos), InSet(d, RealPos)]

# automatic reductions of the new base are not performed (but see next cell)
example_exponent_combination = mult_exps_05.common_power_extraction(
    exp_factor=three, assumptions=temp_assumptions_02, auto_simplify=False)

# We can dig into the inner_expr, though, to simplify/evaluate:
example_exponent_combination.inner_expr().rhs.base.evaluate()

mult_exps_06.common_power_extraction(exp_factor=d, 
                                     assumptions=temp_assumptions_02)

mult_exps_07.common_power_extraction(exp_factor=d, assumptions=temp_assumptions_02)

mult_exps_08 = Mult(Exp(a, Mult(i, j)), Exp(b, Mult(j, k)))

mult_exps_08.common_power_extraction(
        exp_factor = j,
        assumptions=[NotEquals(a, zero), InSet(a, Real),
                     NotEquals(b, zero), InSet(b, Real),
                     InSet(j, Integer), InSet(k, Integer)])

mult_exps_09 = Exp(a, j)

An example expression similar to one found in the QPE package:

mult_exps_10 = Mult(Exp(e, Mult(two, pi, i, k, delta)), Exp(e, Mult(two, pi, i, theta, k)))

mult_exps_10.common_power_extraction(
        exp_factor = k,
        assumptions=[InSet(k, Integer), InSet(delta, Integer), InSet(theta, RealPos)])

# here we specify the factors we want to extract from
# in this case consisting of the entire expression
mult_exps_10.common_power_extraction(
        start_idx=0, end_idx=1,
        exp_factor = k,
        assumptions=[InSet(k, Integer), InSet(delta, Integer), InSet(theta, RealPos)])

Another one, this time with common exponent factor in just a subset of the exponential multiplicands (i.e. at indices 1 and 2):

mult_exps_11 = Mult(
        Exp(e, Mult(two, pi, i, a)),
        Exp(e, Mult(two, pi, i, k, delta)),
        Exp(e, Mult(two, pi, i, theta, k)),
        Exp(e, Mult(two, pi, i, b)))

mult_exps_11.common_power_extraction(
        start_idx=1, end_idx=2,
        exp_factor = k,
        assumptions=[InSet(k, Integer), InSet(delta, Integer),
                     InSet(theta, RealPos), InSet(a, Real), InSet(b, Real)])

# and a potential error case, where the Mult has non-Exp operands:
mult_exps_12 = Mult(
        Add(a, b),
        Exp(e, Mult(two, pi, i, k, delta)),
        Exp(e, Mult(two, pi, i, theta, k)),
        Exp(e, Mult(two, pi, i, b)))

# specifying multiplicands that are not Exps should give
# an informative error message
try:
    mult_exps_12.common_power_extraction(
            start_idx=0, end_idx=2,
            exp_factor = k,
            assumptions=[InSet(k, Integer), InSet(delta, Integer),
                         InSet(theta, RealPos), InSet(a, Real), InSet(b, Real)])
except ValueError as the_error:
    print("ValueError: {}".format(the_error))

ValueError: 'Mult.common_power_extraction()' method works only when all the specified multiplicands are instances of Exp (i.e. each factor must be an exponential). The method was instead called on the expression (a + b) * e^{2 * pi * i * k * delta} * e^{2 * pi * i * theta * k}

# but still works if Mult contains non-Exp multiplicands
# but index-specified pieces are indeed Exps
mult_exps_12.common_power_extraction(
            start_idx=1, end_idx=2,
            exp_factor = k,
            assumptions=[InSet(k, Integer), InSet(delta, Integer),
                         InSet(theta, RealPos), InSet(a, Real), InSet(b, Real)])

# another potential error case, where the Mult has Exp operands,
# but one or more of those operands have the exp_factor alone as an exponent
mult_exps_13 = Mult(
        Exp(a, k),
        Exp(e, Mult(two, pi, i, theta, k)),
        Exp(Add(a, b), k),
        Exp(e, Mult(two, pi, i, b)))

mult_exps_13.common_power_extraction(
            start_idx=1, end_idx=2,
            exp_factor = k,
            assumptions=[InSet(k, Integer), InSet(delta, Integer), NotEquals(a, zero),
                         NotEquals(Add(a, b), zero),
                         InSet(theta, RealPos), InSet(a, Real), InSet(b, Real)])

Deduce bounds¶

relations = [Less(a, x), Less(b, y), Less(c, z)]
assumptions = relations + [InSet(_x, RealPos) for _x in (a, b, c, x, y, z)]
Mult(a, b, c).deduce_bound(relations, assumptions=assumptions)

relations = [Less(a, x), LessEq(b, y), Less(c, z)]
assumptions = relations + [InSet(_x, RealNonNeg) for _x in (a, b, c, x, y, z)]
Mult(a, b, c).deduce_bound(relations, assumptions=assumptions)

relations = [Less(a, x)]
assumptions = relations + [InSet(a, Real), InSet(b, RealNeg), InSet(x, Real)]
Mult(a, b).deduce_bound(relations, assumptions=assumptions)

Automation via canonical forms¶

Two expressions that have the same canonical form can be proven to be equal via automation.

defaults.assumptions = [InSet(a, RealNeg), InSet(b, RealNeg), InSet(c, Real), InSet(d, RealNeg)]

expr1 = Mult(a, sqrt(b), two, sqrd(d), frac(two, three), c)
display(expr1)
expr1.canonical_form()

expr2 = frac(Mult(d, b, four, a, frac(one, three), d, c), sqrt(b))
display(expr2)
expr2.canonical_form()

Equals(expr1, expr2).prove()

Equals(Mult(a, b, d, c), Mult(d, b, c, a)).prove()

Equals(Mult(d, b, a, c), Mult(c, b, d, a)).prove()

Equals(Mult(b, a, d, c), Mult(d, c, b, a)).prove()

This even works in a nested manner

Equals(Mult(d, c, Add(a, b), a), Mult(Add(b, a), d, c, a)).prove()

%end demonstrations

Demonstrations for the theory of proveit.numbers.multiplication¶