Demonstrations for the theory of proveit.numbers ¶

import proveit
from proveit import defaults
%begin demonstrations

Demonstration of '..._both_sides' methods for number relations¶

from proveit import a, b, c, d, x, y
from proveit.logic import Equals, NotEquals, InSet
from proveit.numbers import Add, Mult, Less, LessEq, greater, greater_eq, Real, RealPos, Complex, zero

basic_assumptions = (InSet(a, Real), InSet(b, Real), InSet(c, Real), InSet(d, Real), 
                     InSet(x, Real), InSet(y, Real), 
                     greater(a, zero), greater_eq(b, zero), Less(c, zero), LessEq(d, zero), NotEquals(c, zero))

defaults.assumptions = (*basic_assumptions, Equals(x, y))

num_rel = Equals(x, y).prove()

help(num_rel.right_add_both_sides)

Help on function right_add_both_sides_of_equals in module proveit.numbers.number_sets.real_numbers.real:

right_add_both_sides_of_equals(relation, addend, **defaults_config)
    Add both sides of the Equals relation by the 'addend'
    on the right.
    
    Keyword arguments are accepted for temporarily changing any
    of the attributes of proveit.defaults.

num_rel = num_rel.right_add_both_sides(b)

num_rel = num_rel.left_mult_both_sides(a)

num_rel = num_rel.right_mult_both_sides(c)

num_rel.divide_both_sides(c)

num_rel.divide_both_sides(c, auto_simplify=False)

# After implementing some division closure automation, we should be able to get this to work 
#num_rel.square()

num_rel = Equals(x, y)
num_rel = num_rel.square_both_sides()

num_rel.square_root_both_sides(auto_simplify=False)

num_rel = num_rel.square_root_both_sides()

num_rel.left_add_both_sides(c)

defaults.assumptions = (*basic_assumptions, Less(x, y))

num_rel = Less(x, y).prove()

num_rel = num_rel.left_add_both_sides(a)

num_rel = num_rel.right_add_both_sides(b)

num_rel = num_rel.left_mult_both_sides(c)

# After implementing NumberRelations for greater and greater_eq (or, better yet,
# Issue #180 which makes 'greater' as a style variant of Less, etc.), this should work
#num_rel.mult_left(d)

num_rel = Less(x, y).prove()
num_rel.left_mult_both_sides(d)

num_rel = Less(x, y).prove()
num_rel.right_mult_both_sides(c)

num_rel = Less(x, y).prove()
num_rel.right_mult_both_sides(d)

num_rel = Less(x, y).prove()
num_rel.divide_both_sides(a)

try:
    num_rel = Less(x, y).prove()
    num_rel.divide_both_sides(b)
    assert False, "Expected Exception"
except Exception as e:
    print("Expected error: ", e)

Expected error:  Cannot divide both sides of x < y by b without knowing the divisors relation to zero.

# Need some work on LesserSequences to get this to work.
#num_rel.square()

defaults.assumptions = (*basic_assumptions, NotEquals(x, y))

num_rel = NotEquals(x, y).prove()

help(num_rel.divide_both_sides)

Help on function divide_both_sides_of_notequals in module proveit.numbers.number_sets.real_numbers.real:

divide_both_sides_of_notequals(relation, divisor, **defaults_config)
    Divide both sides of the NotEquals relation by the 'divisor'.
    
    Keyword arguments are accepted for temporarily changing any
    of the attributes of proveit.defaults.

num_rel.divide_both_sides(c)

num_rel.left_mult_both_sides(c)

Test deducing bounds through multiple layers of operations¶

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

defaults.assumptions = (InSet(a, RealPos), InSet(b, RealPos), InSet(c, RealPos), InSet(d, RealPos), 
                        InSet(x, RealPos), InSet(y, RealPos),
                        greater(a, d), greater(x, y))

InSet(Add(b, c), RealPos).prove()

InSet(Add(c, y), RealPos).prove()

expr.deduce_bound(greater(a, d))

expr.deduce_bound([greater(a, d), greater(x, y)])

%end demonstrations

Demonstrations for the theory of proveit.numbers¶

Demonstration of '..._both_sides' methods for number relations¶

Test deducing bounds through multiple layers of operations¶

Demonstrations for the theory of proveit.numbers ¶