logo

Demonstrations for the theory of proveit.numbers.addition

In [1]:
import proveit
from proveit import defaults
from proveit import ExprTuple, ExprRange
from proveit import a, b, c, d, e, f, g, k, l, m, n, x, y, A, B, C
from proveit.core_expr_types import a_k
from proveit.logic import Equals, Forall, InSet, NotEquals
from proveit.numbers import Less, greater, LessEq, greater_eq, Neg, Exp, Mult, Div, frac
from proveit.numbers import zero, one,two, three,four, five, six, seven, eight
from proveit.numbers import Integer, Natural, NaturalPos, Real, RealPos, RealNeg, RealPos, RealNonNeg, RealNonPos
from proveit.numbers import Add, Complex, Neg, subtract, num
%begin demonstrations

Basic addition with numerals

In [2]:
Add(num(2), num(5)).evaluation()
 ⊢  
In [3]:
Add(num(-3), num(4)).evaluation()
 ⊢  
In [4]:
Add(num(3), num(-4)).evaluation()
 ⊢  
In [5]:
Add(num(-3), num(-3)).evaluation()
 ⊢  
In [6]:
Add(num(12), num(-3)).evaluation()
 ⊢  
In [7]:
Add(num(10), num(1)).evaluation()
 ⊢  
In [8]:
Add(num(19), num(1)).evaluation()
 ⊢  
In [9]:
# multi-digit addition is currently only implemented for adding 1.
from proveit.logic import EvaluationError
try:
    Add(num(19), num(10)).evaluation()
except EvaluationError as _e:
    print(_e)
    print('because multi-digit addition is not implemented beyond adding 1')

Evaluation of 19 + 10 under assumptions {} is not known
because multi-digit addition is not implemented beyond adding 1
In [10]:
Add(frac(one, two), frac(one, two)).evaluation()
 ⊢  
In [11]:
Add(one, frac(one, two)).evaluation()
 ⊢  
In [12]:
Add(frac(one, three), one).evaluation()
 ⊢  
In [13]:
subtract(one, frac(one, two)).evaluation()
 ⊢  
In [14]:
Add(frac(num(2), num(3)), frac(num(3), num(2))).evaluation()
 ⊢  
In [15]:
# This one fails because mult-digit addition is not implemented
try:
    Add(frac(num(5), num(4)), frac(num(3), num(2))).evaluation()
except EvaluationError as _e:
    print(_e)
    print('because multi-digit addition is not implemented beyond adding 1')

Evaluation of (5 / 4) + (3 / 2) under assumptions {} is not known
because multi-digit addition is not implemented beyond adding 1

quick_simplification method

The quick_simplification method performs simplifications with respect to combining integers and expanding expression ranges in a quick-n-dirty manner that is appropriate for displaying purposes (e.g, expression ranges) where an actual proof is not necessary.

In [16]:
Add(Add(b, num(5)), num(4)).quick_simplification()
In [17]:
Add(num(5), num(5)).quick_simplification()
In [18]:
Add(num(5), num(-5)).quick_simplification()
In [19]:
Add(b, num(5)).quick_simplification()
In [20]:
Add(b, num(0)).quick_simplification()
In [21]:
Add(b, Add(Neg(c), num(-5))).quick_simplification()
In [22]:
Add(Add(b, num(2)), Add(c, num(5))).quick_simplification()
In [23]:
Add(Add(b, num(2)), Add(Neg(b), num(2))).quick_simplification()
In [24]:
Add(Add(b, num(5)), Add(c, num(-5))).quick_simplification()
In [25]:
Add(Add(b, num(5)), Add(Neg(c), num(5))).quick_simplification()
In [26]:
Add(num(-5), Add(c, num(5))).quick_simplification()
In [27]:
Add(num(-5), num(5)).quick_simplification()

Can also handle ranges of terms.

In [28]:
Add(Add(ExprRange(k, a_k, one, n), b), 
    Add(Neg(c), Neg(Add(ExprRange(k, a_k, one, n))))).quick_simplification()
In [29]:
Add(Add(ExprRange(k, a_k, one, n), b), 
    Add(c, ExprRange(k, a_k, one, n))).quick_simplification()
In [30]:
Add(Add(ExprRange(k, a_k, one, n), b), 
    Add(Neg(c), Neg(Add(ExprRange(k, a_k, one, subtract(n, two)))))).quick_simplification()
In [31]:
Add(Add(ExprRange(k, a_k, one, n), b), 
    Add(Neg(c), Add(ExprRange(k, a_k, one, subtract(n, two))))).quick_simplification()
In [32]:
Add(Add(ExprRange(k, a_k, one, n), b), 
    Add(Neg(c), Neg(Add(ExprRange(k, a_k, three, subtract(n, two)))))).quick_simplification()
In [33]:
Add(Add(ExprRange(k, a_k, one, n), b), 
    Add(Neg(c), Add(ExprRange(k, a_k, three, subtract(n, two))))).quick_simplification()
In [34]:
Add(Add(ExprRange(k, a_k, three, n), b), 
    Add(Neg(c), Neg(Add(ExprRange(k, a_k, one, subtract(n, two)))))).quick_simplification()
In [35]:
Add(Add(ExprRange(k, a_k, one, m), b), 
    Add(Neg(c), Neg(Add(ExprRange(k, a_k, one, n))))).quick_simplification()
In [36]:
Add(Add(ExprRange(k, Neg(a_k), one, m), b), 
    Add(Neg(c), Neg(Add(ExprRange(k, a_k, one, n))))).quick_simplification()
In [37]:
Add(Add(ExprRange(k, a_k, one, num(5)), b), 
    Add(Neg(c), Neg(Add(ExprRange(k, a_k, one, num(7)))))).quick_simplification()
In [38]:
Add(ExprRange(k, a_k, one, zero), b).quick_simplification()

Simplification

The following simplifications come with actual proofs.

In [39]:
Add(b, b, b, b).simplification(assumptions=[InSet(b, Complex)])
 ⊢  
In [40]:
Add(b, b, b, b).simplified(assumptions=[InSet(b, Complex)])
In [41]:
help(Add(b, b, b, b).simplified)

Help on method simplified in module proveit._core_.expression.expr:

simplified(*args, **kwargs) method of proveit.numbers.addition.add.Add instance
    Return an equivalent form of this expression derived via 'simplification'.
In [42]:
help(Equals(c, Add(b, b, b, b)).prove(
    assumptions=[Equals(c, Add(b, b, b, b))]).inner_expr().rhs.simplify)

Help on function simplify in module proveit._core_.expression.inner_expr:

simplify(*args, **kwargs)
    Derive an equivalent form of the top-level judgment by replacing the inner expression via 'simplification'.
In [43]:
Equals(c, Add(b, b, b, b)).prove(
    assumptions=[Equals(c, Add(b, b, b, b))]).inner_expr().rhs.simplification(
        assumptions=[InSet(b, Complex)])
 ⊢  
In [44]:
Add(one, zero, four, three).evaluation()
 ⊢  
In [45]:
Equals(Add(one, two, three, one), seven).prove()
 ⊢  
In [46]:
Add(Mult(one, b), Mult(three, b)).simplification(assumptions=[InSet(b, Complex)])
 ⊢  
In [47]:
Add(b, Mult(three, b)).factorization(b, pull='right', assumptions=[InSet(a, Complex), InSet(c, Complex), InSet(b, Complex)])
 ⊢  
In [48]:
Add(b, Mult(three, b), Mult(two, b)).factorization(b, pull='right', assumptions=[InSet(a, Complex), InSet(c, Complex), InSet(b, Complex)])
 ⊢  
In [49]:
Add(b, Mult(three, b), Mult(two, b)).simplification(
    assumptions=[InSet(a, Complex), InSet(c, Complex), InSet(b, Complex)])
 ⊢  
In [50]:
Add(Mult(one, two), b, c, Mult(three, b), Mult(two, b), Mult(one, c)).simplification(
    assumptions=[InSet(a, Complex), InSet(c, Complex), InSet(b, Complex)])
,  ⊢  
In [51]:
Add(Mult(one, two), b, c, Mult(three, b), Mult(two, b), Neg(b), Mult(one, c)).simplification(
    assumptions=[InSet(a, Complex), InSet(c, Complex), InSet(b, Complex)])
,  ⊢  
In [52]:
#Add(Mult(c,b), Mult(b,c), Mult(c, a), a, b, c, one, two, three, Mult(two, c), Mult(three,b), Mult(four, a)).simplification([InSet(a, Complex), InSet(b, Complex), InSet(c, Complex)])
In [53]:
#Add(Mult(a,b), c, b,a).simplification([InSet(a, Complex), InSet(b, Complex), InSet(c, Complex)])
In [54]:
Add(a, one, a).simplification(assumptions=[InSet(a, Complex)])
 ⊢  
In [55]:
Add(Mult(two, b), b, a, c, Mult(zero, d)).simplification(
    assumptions=[InSet(a, Complex), InSet(c, Complex), InSet(b, Complex), InSet(d, Complex)])
, , ,  ⊢  
In [56]:
Add(a,b,c,a,b,a,c).simplification(assumptions=[InSet(a, Complex), InSet(b, Complex), InSet(c, Complex)])
, ,  ⊢  
In [57]:
Add(a,b,c,a,b,a,c,b,a,c,a).simplification(assumptions=[InSet(a, Complex), InSet(b, Complex), InSet(c, Complex)])
, ,  ⊢  
In [58]:
Add(Neg(one), Neg(two)).evaluation()
 ⊢  
In [59]:
# Multi-digit arithmetic needs to be implemented in order to
# get this to work w.r.t. indexing.  So we comment this out for now.
#Add(a,b,c,a,b,a,c,b,a,c,a,a).simplification([InSet(a, Complex), InSet(b, Complex), InSet(c, Complex)]).proof()
In [60]:
Add(one, c, two, three, c, one,c).simplification(assumptions=[InSet(c, Complex)])
 ⊢  
In [61]:
expr = Add(c, Neg(one), b, Add(two, three), Neg(c), Add(c, zero, c)).simplified(
    assumptions=[InSet(c, Complex),InSet(b, Complex)])
expr:
In [62]:
Add(one, Neg(one), two, Neg(two)).cancelation(0, 1, auto_simplify=False)
 ⊢  
In [63]:
Add(one, Neg(one), two, Neg(two)).cancelation(0, 1, auto_simplify=True)
 ⊢  
In [64]:
Add(a, Neg(b), Neg(a), b).cancelations(assumptions=[InSet(a, Complex), InSet(b, Complex)], auto_simplify=False)
,  ⊢  
In [65]:
Add(a, Neg(b), Neg(a), b).cancelations(assumptions=[InSet(a, Complex), InSet(b, Complex)], auto_simplify=True)
,  ⊢  
In [66]:
Add(one, a, A, zero, b, B, C, c, one, three, A).simplification(
    assumptions=[InSet(a, Complex), InSet(A, Complex), InSet(b, Complex), InSet(B, Complex), 
                 InSet(c, Complex), InSet(C, Complex)])
, , , , ,  ⊢  
In [67]:
Add(a, one, two , c, b, a, zero, b, c, c, three).simplification(
    assumptions=[InSet(a, Complex), InSet(b, Complex), InSet(c, Complex)])
, ,  ⊢  
In [68]:
Add(two, three, four, a, a, c, zero, c, b, b).simplification(
    assumptions=[InSet(a, Complex), InSet(b, Complex), InSet(c, Complex)])
, ,  ⊢  
In [69]:
Add(Neg(one), Neg(one)).simplification()
 ⊢  
In [70]:
subtract(three, one).evaluation()
 ⊢  
In [71]:
Add(zero, two, three, zero).evaluation()
 ⊢  
In [72]:
Add(one, zero, one, three).evaluation()
 ⊢  
In [73]:
Add(a, one, two , c, b, a, zero, b, c, c, three).simplification(
    assumptions=[InSet(a, Real), InSet(b, Real), InSet(c, Real)])
, ,  ⊢  
In [74]:
InSet(Add(a,b), Integer).prove(assumptions=[InSet(a, Integer), InSet(b,Integer)])
,  ⊢  
In [75]:
InSet(Add(a,b,c,d), Integer).prove(
    assumptions=[InSet(a,Integer),InSet(b, Integer), InSet(c, Integer), InSet(d,Integer)])
, , ,  ⊢  
In [76]:
InSet(Add(a,b), Natural).prove(assumptions=[InSet(a, Natural), InSet(b, Natural)])
,  ⊢  
In [77]:
InSet(Add(a,b,c,d), Natural).prove(assumptions=[InSet(a,Natural), InSet(b, Natural), InSet(c,Natural), InSet(d, Natural)])
, , ,  ⊢  
In [78]:
InSet(Add(a,b), Real).prove(assumptions=[InSet(a, Real), InSet(b,Real)])
,  ⊢  
In [79]:
InSet(Add(a,b,c,d), Real).prove(assumptions=[InSet(a,Real), InSet(b,Real), InSet(c, Real), InSet(d, Real)])
, , ,  ⊢  
In [80]:
InSet(Add(a,b), Complex).prove(assumptions=[InSet(a, Complex), InSet(b, Complex)])
,  ⊢  
In [81]:
InSet(Add(a,b,c,d), Complex).prove(assumptions=[InSet(a, Complex), InSet(b, Complex), InSet(c, Complex), InSet(d,Complex)])
, , ,  ⊢  
In [82]:
InSet(Add(a,b,one,d), NaturalPos).prove(assumptions=[InSet(a, Natural), InSet(b, Natural), InSet(c, Natural), InSet(d, Natural)])
, ,  ⊢  
In [83]:
Add(zero, b).zero_eliminations(assumptions=[InSet(b,Complex)])
 ⊢  
In [84]:
Add(a,b,c,d).commutation(1,3, assumptions=[InSet(a,Real), InSet(b,Real), InSet(c, Real), InSet(d,Real)])
, , ,  ⊢  
In [85]:
Add(one, two, three, four, five, six, one).association(3, length=2, assumptions = [], auto_simplify=False)
#Equals(subtract(two, one),one), Equals(subtract(one, one), zero), Equals(subtract(three, one), two), Less(zero,Less(one, Less(two, three)))
 ⊢  
In [86]:
greater(Add(one, two, three, one), three)
In [87]:
greater(Add(one, two, three, one), three).prove(
    assumptions=[InSet(two, RealPos), InSet(three, Real), InSet(one, RealPos)])
 ⊢  
In [88]:
Less(Add(Neg(one), Neg(two), three, Neg(one)), three).prove(
    assumptions=[InSet(two, RealNeg), InSet(three, Real), InSet(one, RealNeg),
                 InSet(Neg(one), RealNeg), InSet(Neg(two), RealNeg)])
, , , ,  ⊢  
In [89]:
subtract(x,x).evaluation(assumptions=[InSet(x, Complex)])
 ⊢  
In [90]:
subtract(one,one).evaluation()
 ⊢  
In [91]:
InSet(Neg(one), Real).prove()
 ⊢  
In [92]:
#test = Add(Mult(two, b), Mult(three,b), b, Neg(b)).factor(b, assumptions=[InSet(two, Complex), InSet(three, Complex), InSet(b, Exp(Complex,one)),InSet(one, Complex), InSet(Neg(one), Complex), InSet(b, Real)])
#test = Add(Mult(two, b), Mult(three,b), b, Neg(b)).factor(b, assumptions=[InSet(Neg(one), Complex), InSet(b, Real)])
Add(Mult(two, b), Mult(three,b), b, Neg(b)).factorization(
    b, pull='right', assumptions=[InSet(b, Real)], auto_simplify=False)
 ⊢  
In [93]:
Add(Mult(two, b), Mult(three,b), b, Neg(b)).factorization(
    b, pull='left', assumptions=[InSet(b, Real)], auto_simplify=False)
 ⊢  
In [94]:
Add(Mult(two, b), Mult(three,b), b, Neg(b)).factorization(
    b, pull='left', assumptions=[InSet(b, Real)])
 ⊢  
In [95]:
Add(a,b,c,d,e,f,g).commutation(4, 2, assumptions=[InSet(a,Real),InSet(b,Real),InSet(c,Real),InSet(d,Real),InSet(e,Real),InSet(f,Real),InSet(g,Real)])
, , , , , ,  ⊢  
In [96]:
#m.prove([Add(m, subtract(one, one))])

Adding Fractions with Common Denominators: Basic Simplification and Automation

Some working assumptions about some variables and parameters (side note: it might be useful to create an incidental derivation to produce the ExprRange $(a_1 \in \mathbb{C}), ..., (a_n \in \mathbb{C})$ from the Forall expression $\forall_{k\in\{1, 2, \ldots, n\}}\left(a_{k}\in\mathbb{C}\right)$).

In [97]:
assumptions = [InSet(a, Complex), InSet(b, Complex), InSet(c, Complex), InSet(d, Complex),
              NotEquals(b, zero), NotEquals(d, zero), InSet(n, NaturalPos),
              InSet(m, Natural), ExprRange(k, InSet(a_k, Complex), one, n)]
assumptions:

Some example Divs to add together:

In [98]:
example_div_01, example_div_02, example_div_03 = (
    frac(a, d), frac(b, d), frac(c, b) )
example_div_01:
example_div_02:
example_div_03:

And (at last!), some example sums:

In [99]:
example_sum_01, example_sum_02, example_sum_03, example_sum_04, example_sum_05, example_sum_06 = (
    Add(example_div_01, example_div_02),
    Add(ExprRange(k, frac(a_k, d), one, n)),
    Add(example_div_01, example_div_02, ExprRange(k, frac(a_k, d), one, n)),
    Add(example_div_01, example_div_02, example_div_03),
    Add(example_div_01, example_div_02, Mult(a,d)),
    Add(ExprRange(k, frac(d, a_k), one, m)))
example_sum_01:
example_sum_02:
example_sum_03:
example_sum_04:
example_sum_05:
example_sum_06:
In [100]:
example_sum_01
In [101]:
example_sum_01.combining_terms(assumptions=assumptions)
, , ,  ⊢  
In [102]:
# The Add.combine_like_denoms simplification directive is False by default:
example_sum_01.simplification(assumptions=assumptions)
 ⊢  
In [103]:
# We can temporarily set Add.combine_like_denoms to True
with Add.temporary_simplification_directives() as tmp_directives:
    tmp_directives.combine_like_denoms = True
    example_sum_01.simplification(assumptions=assumptions)
, , ,  ⊢  
In [104]:
example_sum_02
In [105]:
example_sum_02.combining_terms(assumptions=assumptions)
, , ,  ⊢  
In [106]:
# The Add.combine_like_denoms simplification directive is False by default:
example_sum_02.simplification(assumptions=assumptions)
 ⊢  
In [107]:
# We can temporarily set Add.combine_like_denoms to True
with Add.temporary_simplification_directives() as tmp_directives:
    tmp_directives.combine_like_denoms = True
    example_sum_02.simplification(assumptions=assumptions)
, , ,  ⊢  

Given that the simplification() process works with that single ExprRange of Divs, it's interesting to see that we run into trouble when taking the sum of two such sums. Consider:

In [108]:
sum_two_expr_ranges = Add(example_sum_02, example_sum_02)
sum_two_expr_ranges:
In [109]:
try:
    InSet(example_sum_02, Complex).prove(assumptions=assumptions)
except Exception as the_exception:
    print("Exception: {}".format(the_exception))

Exception: Unable to prove ((a_{1} / d) +  (a_{2} / d) +  ... +  (a_{n} / d)) in Complex assuming {a in Complex, b in Complex, c in Complex, d in Complex, b != 0, d != 0, n in NaturalPos, m in Natural, (a_{1} in Complex), (a_{2} in Complex), ..., (a_{n} in Complex)}:
((a_{1} / d) +  (a_{2} / d) +  ... +  (a_{n} / d)).readily_provable_number_set() does not return a number set that is readily included by Complex

In fact, that InstantiationFailure due to the unsatisfied condition of the sum being in Complex is an interesting error. Notice that we cannot even get that from a goal-oriented manual request, even if we augment the assumptions to be more explicit about each frac itself being Complex:

In [110]:
try:
    InSet(example_sum_02, Complex).prove(
        assumptions=assumptions+[ExprRange(k, InSet(frac(a_k, d), Complex), one, n)])
except Exception as the_exception:
    print("Exception: {}".format(the_exception))

Exception: Unable to prove ((a_{1} / d) +  (a_{2} / d) +  ... +  (a_{n} / d)) in Complex assuming {a in Complex, b in Complex, c in Complex, d in Complex, b != 0, d != 0, n in NaturalPos, m in Natural, (a_{1} in Complex), (a_{2} in Complex), ..., (a_{n} in Complex), ((a_{1} / d) in Complex), ((a_{2} / d) in Complex), ..., ((a_{n} / d) in Complex)}:
((a_{1} / d) +  (a_{2} / d) +  ... +  (a_{n} / d)).readily_provable_number_set() does not return a number set that is readily included by Complex

Simplifying a term that is an Add consisting of both simple terms and an ExprRange leads to a problem not yet addressed.

In [111]:
example_sum_03

The direct calling of the Add.combining_terms() works just fine:

In [112]:
example_sum_03.combining_terms(assumptions=assumptions)
, , , , ,  ⊢  

But the automatic simplification (without setting Add.combine_like_denoms to True) raises an AttributeError:

In [113]:
try:
    example_sum_03.simplification(assumptions=assumptions)
except AttributeError as the_exception:
    print("AttributeError: {}".format(the_exception))

AttributeError: No attribute 'combining_operands' in '<class 'proveit._core_.expression.inner_expr.InnerExpr'>' or '<class 'proveit._core_.expression.composite.expr_tuple.ExprTuple'>'

But the automatic simplification when setting Add.combine_like_denoms to True works just fine:

In [114]:
# interestingly, this still works fine:
with Add.temporary_simplification_directives() as tmp_directives:
    tmp_directives.combine_like_denoms = True
    example_sum_03.simplification(assumptions=assumptions)
, , , , ,  ⊢  
In [115]:
example_sum_04
In [116]:
# this should raise an error, because the addends are not all like terms
try:
    example_sum_04.combining_terms(assumptions=assumptions)
except ValueError as the_error:
    print("ValueError: {}".format(the_error))

ValueError: The likeness keys of the operands of (a / d) + (b / d) + (c / b) are not all the same: {b, d}
In [117]:
example_sum_04.simplification(assumptions=assumptions)
 ⊢  
In [118]:
with Add.temporary_simplification_directives() as tmp_directives:
    tmp_directives.combine_like_denoms = True
    example_sum_04.simplification(assumptions=assumptions)
, , , , ,  ⊢  
In [119]:
example_sum_05
In [120]:
# this should raise an error, because the addends are not all like terms
try:
    example_sum_05.combining_terms(assumptions=assumptions)
except Exception as the_exception:
    print("Exception: {}".format(the_exception))

Exception: @prover method <function Add.combining_terms at 0x7efe80dbe950> is expected to return a proven Judgment, not The likeness keys of the operands of (a / d) + (b / d) + (a * d) are not all the same: {b / d, a * d, a / d} of type <class 'ValueError'>.
In [121]:
# The Add.combine_like_denoms simplification directive is False by default:
example_sum_05.simplification(assumptions=assumptions)
 ⊢  
In [122]:
# But we can temporarily set Add.combine_like_denoms to True:
with Add.temporary_simplification_directives() as tmp_directives:
    tmp_directives.combine_like_denoms = True
    example_sum_05.simplification(assumptions=assumptions)
, , ,  ⊢  

We shouldn't be able to combine a sum of terms like $(\frac{d}{a_1}+\frac{d}{a_2}+\ldots+\frac{d}{a_m})$, but the error(s) being raised indicate that there is some other problem occurring that needs addressed (in fact there are both ValueError and NotImplementedError being raised):

In [123]:
example_sum_06
In [124]:
# should raise an error when blindly calling combining_terms()
# when not all terms are like-terms:
try:
    example_sum_06.combining_terms(assumptions=assumptions)
except Exception as the_exception:
    print("Exception: {}".format(the_exception))

Exception: Not enough supplied operands for extracting init args of a <class 'proveit.numbers.division.divide.Div'>: needed 2 got 1
In [125]:
# simplification should do nothing here:
example_sum_06.simplification(assumptions=assumptions)
 ⊢  
In [126]:
# Now, combine Div terms where possible,
# BUT the parameter-dependent fractions are a problem
try:
    with Add.temporary_simplification_directives() as tmp_directives:
        tmp_directives.combine_like_denoms = True
        example_sum_06.simplification(assumptions=assumptions)
except Exception as the_exception:
    print("Exception: {}".format(the_exception))

Exception: Not enough supplied operands for extracting init args of a <class 'proveit.numbers.division.divide.Div'>: needed 2 got 1

Deducing Bounds

Testing the deduce_bound() method.

In [127]:
term_relations = [Less(a, c), Less(b, d)]
assumptions = term_relations + [InSet(a, Real), InSet(b, Real), InSet(c, Real), InSet(d, Real)]
Add(a, b).deduce_bound(term_relations[0], assumptions=assumptions)
, , ,  ⊢  
In [128]:
Add(a, b).deduce_bound(term_relations[1], assumptions=assumptions)
, , ,  ⊢  
In [129]:
Add(a, b).deduce_bound(term_relations, assumptions=assumptions)
, , , , ,  ⊢  
In [130]:
term_relations = [greater(a, c), greater(b, d)]
assumptions = term_relations + [InSet(a, Real), InSet(b, Real), InSet(c, Real), InSet(d, Real)]
assumptions:
In [131]:
Add(a, b).deduce_bound(term_relations[0], assumptions=assumptions)
, , ,  ⊢  
In [132]:
Add(a, b).deduce_bound(term_relations[1], assumptions=assumptions)
, , ,  ⊢  
In [133]:
Add(a, b).deduce_bound(term_relations, assumptions=assumptions)
, , , , ,  ⊢  
In [134]:
Add(a, b, c, d).bound_by_term(
    1, assumptions=[InSet(a, RealPos), InSet(b, Real), InSet(c, RealPos), InSet(d, RealPos)])
, , ,  ⊢  
In [135]:
Add(a, b, c, d).bound_by_term(
    2, assumptions=[InSet(a, RealNeg), InSet(b, RealNeg), InSet(c, Real), InSet(d, RealNeg)])
, , ,  ⊢  
In [136]:
Add(a, b, c, d).bound_by_term(
    0, assumptions=[InSet(a, Real), InSet(b, RealNonNeg), InSet(c, RealNonNeg), InSet(d, RealNonNeg)])
, , ,  ⊢  
In [137]:
Add(a, b, c, d).bound_by_term(
    3, assumptions=[InSet(a, RealNonPos), InSet(b, RealNonPos), InSet(c, RealNonPos), InSet(d, Real)])
, , ,  ⊢  

Automation via canonical forms

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

In [138]:
defaults.assumptions = [InSet(a, RealNeg), InSet(b, RealNeg), InSet(c, Real), InSet(d, RealNeg)]
defaults.assumptions:
In [139]:
expr1 = Add(d, c, Mult(two, b), c, frac(a, two))
display(expr1)
expr1.canonical_form()
In [140]:
expr2 = Add(a, Neg(frac(a, two)), b, d, b, Mult(two, c))
display(expr2)
expr2.canonical_form()
In [141]:
Equals(expr1, expr2).prove()
, , ,  ⊢  
In [142]:
Equals(Add(c, b, d, a), Add(d, b, a, c)).prove()
, , ,  ⊢  
In [143]:
Equals(Add(d, c, b, a), Add(b, a, d, c)).prove()
, , ,  ⊢  

This even works in a nested manner

In [144]:
Equals(Add(Mult(b, a), d, c, a), Add(d, c, Mult(a, b), a)).prove()
, , ,  ⊢  
In [145]:
%end demonstrations