Demonstrations for the theory of proveit.numbers.division¶

In [1]:
from proveit.logic import InSet, NotEquals
from proveit.numbers import (zero, one, frac, Add, subtract, Sum, Mult,
Less, LessEq, greater, greater_eq,
Integer, Interval, Real, Complex)
from proveit import a, b, c, d, w, x, y, z, Px
%begin demonstrations
In [2]:
assumptions = [InSet(var, Complex) for var in [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]]
#assupmtions += [InSet(var, Complex) for var in [c, d, x, y, z]]

Factorization¶

In [3]:
expr = frac(Add(a, b, c), d)
Out[3]:
expr:
In [4]:
expr.factorization(frac(one, d), assumptions=assumptions)
Out[4]:
, , , ,  ⊢
In [5]:
expr.factorization(frac(one, d), pull='right', assumptions=assumptions)
Out[5]:
, , , ,  ⊢
In [6]:
expr.factorization(frac(expr.numerator, d), assumptions=assumptions)
Out[6]:
In [7]:
expr.factorization(frac(expr.numerator, d), pull='right', assumptions=assumptions)
Out[7]:
In [8]:
expr = frac(Mult(Add(a, b, c), b), d)
Out[8]:
expr:
In [9]:
expr.factorization(frac(b, d), assumptions=assumptions)
Out[9]:
, , , ,  ⊢
In [10]:
expr.factorization(frac(b, d), pull='right', assumptions=assumptions)
Out[10]:
, , , ,  ⊢
In [11]:
expr = frac(Mult(Add(a, b, c), b), Mult(a, d))
Out[11]:
expr:
In [12]:
expr.factorization(frac(b, d), assumptions=assumptions)
Out[12]:
, , , , ,  ⊢
In [13]:
expr.factorization(frac(b, d), pull='right', assumptions=assumptions)
Out[13]:
, , , , ,  ⊢
In [14]:
expr.factorization(frac(one, d), assumptions=assumptions)
Out[14]:
, , , , ,  ⊢
In [15]:
expr.factorization(frac(one, d), pull='right', assumptions=assumptions)
Out[15]:
, , , , ,  ⊢
In [16]:
expr.factorization(frac(expr.numerator, d), pull='right', assumptions=assumptions)
Out[16]:
, , , , ,  ⊢
In [17]:
expr.factorization(frac(expr.numerator, d), pull='left', assumptions=assumptions)
Out[17]:
, , , , ,  ⊢

Deduce bounds¶

In [18]:
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 [19]:
relation = greater(a, x)
frac(a, y).deduce_bound(relation, assumptions+[relation])
Out[19]:
, , , ,  ⊢
In [20]:
relation = Less(a, x)
frac(a, y).deduce_bound(relation, assumptions+[relation])
Out[20]:
, , , ,  ⊢
In [21]:
relation = greater_eq(a, x)
frac(a, y).deduce_bound(relation, assumptions+[relation])
Out[21]:
, , , ,  ⊢
In [22]:
relation = LessEq(a, x)
frac(a, y).deduce_bound(relation, assumptions+[relation])
Out[22]:
, , , ,  ⊢

Bound by the numerator with a negative denominator

In [23]:
relation = greater(a, x)
frac(a, d).deduce_bound(relation, assumptions+[relation])
Out[23]:
, , , ,  ⊢
In [24]:
relation = Less(a, x)
frac(a, d).deduce_bound(relation, assumptions+[relation])
Out[24]:
, , , ,  ⊢
In [25]:
relation = greater_eq(a, x)
frac(a, d).deduce_bound(relation, assumptions+[relation])
Out[25]:
, , , ,  ⊢
In [26]:
relation = LessEq(a, x)
frac(a, d).deduce_bound(relation, assumptions+[relation])
Out[26]:
, , , ,  ⊢

Bound by the denominator with everything positive

In [27]:
relation = greater(x, y)
frac(a, x).deduce_bound(relation, assumptions+[relation])
Out[27]:
, , , , , ,  ⊢
In [28]:
relation = Less(x, y)
frac(a, x).deduce_bound(relation, assumptions+[relation])
Out[28]:
, , , , , ,  ⊢
In [29]:
relation = greater_eq(x, y)
frac(b, x).deduce_bound(relation, assumptions+[relation])
Out[29]:
, , , , , ,  ⊢
In [30]:
relation = LessEq(x, y)
frac(b, x).deduce_bound(relation, assumptions+[relation])
Out[30]:
, , , , , ,  ⊢

Bound by the denominator with everything negative

In [31]:
relation = greater(w, c)
frac(w, d).deduce_bound(relation, assumptions+[relation])
Out[31]:
, , , ,  ⊢
In [32]:
relation = Less(w, c)
frac(w, d).deduce_bound(relation, assumptions+[relation])
Out[32]:
, , , ,  ⊢
In [33]:
relation = greater_eq(c, w)
frac(c, d).deduce_bound(relation, assumptions+[relation])
Out[33]:
, , , ,  ⊢
In [34]:
relation = LessEq(c, w)
frac(c, d).deduce_bound(relation, assumptions+[relation])
Out[34]:
, , , ,  ⊢

Bound by the denominator with the numerator positive and denominator negative

In [35]:
relation = greater(d, w)
frac(a, d).deduce_bound(relation, assumptions+[relation])
Out[35]:
, , , , , ,  ⊢
In [36]:
relation = Less(d, w)
frac(a, d).deduce_bound(relation, assumptions+[relation])
Out[36]:
, , , , , ,  ⊢
In [37]:
relation = greater_eq(d, w)
frac(b, d).deduce_bound(relation, assumptions+[relation])
Out[37]:
, , , , , ,  ⊢
In [38]:
relation = LessEq(d, w)
frac(b, d).deduce_bound(relation, assumptions+[relation])
Out[38]:
, , , , , ,  ⊢

Bound by the denominator with the numerator negative and denominator positive

In [39]:
relation = greater(a, x)
frac(d, a).deduce_bound(relation, assumptions+[relation])
Out[39]:
, , , , , ,  ⊢
In [40]:
relation = Less(a, x)
frac(d, a).deduce_bound(relation, assumptions+[relation])
Out[40]:
, , , , , ,  ⊢
In [41]:
relation = greater_eq(a, x)
frac(c, a).deduce_bound(relation, assumptions+[relation])
Out[41]:
, , , , , ,  ⊢
In [42]:
relation = LessEq(a, x)
frac(c, a).deduce_bound(relation, assumptions+[relation])
Out[42]:
, , , , , ,  ⊢

Bound numerator and denominator simulataneously

In [43]:
# Here, we automatically prove that z < 0 indirectly.
relations = [Less(z, d), greater(a, x)]
frac(a, d).deduce_bound(relations, assumptions+relations)
Out[43]:
, , , , , , ,  ⊢
In [44]:
# Here, we automatically prove that z > 0 indirectly.
relations = [LessEq(a, z), LessEq(c, d)]
frac(c, a).deduce_bound(relations, assumptions+relations)
Out[44]:
, , , , , , ,  ⊢
In [45]:
%end demonstrations

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

Distribution¶

expr.distribution(assumptions=assumptions)

expr = frac(Sub(a, b), d)

sub.distribute(assumptions=assumptions)

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

expr.distribute(assumptions=assumptions)

%end demonstrations