Add

class proveit.numbers.Add(*operands, styles=None)

Bases: proveit.numbers.NumberOperation

Attributes Summary

Methods Summary

all_canceled(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘cancelations’.
associated(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘association’.
association(self, start_idx, length, …)	Given numerical operands, deduce that this expression is equal to a form in which operands in the range [start_idx, start_idx+length) are grouped together. For example, (a + b + … + y + z) = (a + b … + (l + … + m) + … + y + z).
cancelation(self, idx1, idx2, …)	Attempt a simple cancelation between operands at index i and j.
cancelations(self, \*\*defaults_config)	Deduce and return an equality between self and a form in which all simple cancellations are performed (where there are exact negations that occur).
canceled(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘cancelation’.
commutation(self[, init_idx, final_idx])	Given numerical operands, deduce that this expression is equal to a form in which the operand at index init_idx has been moved to final_idx.
commuted(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘commutation’.
conversion_to_multiplication(self, …)	From the addition of the same values, derive and return the equivalence as a multiplication.
deduce_bound(self, inner_expr_bound_or_bounds)	Return a bound of this arithmetic expression based upon the bounds of any number of inner expressions.
deduce_difference_in_natural(self, …)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
deduce_difference_in_natural_pos(self, …)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
deduce_in_number_set(self, number_set, …)	given a number set, attempt to prove that the given expression is in that number set using the appropriate closure theorem
disassociated(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘disassociation’.
disassociation(self, idx, \*\*defaults_config)	Given numerical operands, deduce that this expression is equal to a form in which the operand at index idx is no longer grouped together. For example, (a + b … + (l + … + m) + … + y+ z) = (a + b + … + y + z).
eliminated_zero(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘zero_elimination’.
eliminated_zeros(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘zero_eliminations’.
equality_side_effects(self, judgment)	If the right side is irreducible and the left side is binary, a + b = c, derive the commutation b + a = c and if neither a nor b is a Neg, also derive the following: -a - b = -c c - b = a b - c = -a
factorization(self, the_factors[, pull, …])	Factor out the factor(s) from this sum, pulling it either to the “left” or “right”.
factorized(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘factorization’.
group_commutation(self, init_idx, final_idx, …)	Given numerical operands, deduce that this expression is equal to a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx.
group_commuted(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘group_commutation’.
remake_arguments(self)	Yield the argument values or (name, value) pairs that could be used to recreate the Operation.
remake_constructor(self)	Method to call to reconstruct this Expression.
remake_with_style_calls(self)	In order to reconstruct this Expression to have the same styles, what “with…” method calls are most appropriate? Return a tuple of strings with the calls to make.
style_options(self)	Return the StyleOptions object for the Operation.
subtraction_folding(self[, term_idx, …])	Given a negated term, term_idx or the first negated term if term_idx is None, deduce the equivalence between self and a Subtract form (with the specified negated term on the right of the subtraction).
zero_elimination(self, idx, \*\*defaults_config)	Derive and return this Add expression equal to a form in which a specific zero operand (at the given index) is eliminated.
zero_eliminations(self, \*\*defaults_config)	Derive and return this Add expression equal to a form in which all zero’s are eliminated.

Attributes Documentation

Methods Documentation

all_canceled(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘cancelations’.

associated(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘association’.

association(self, start_idx, length, \*\*defaults_config)

Given numerical operands, deduce that this expression is equal to a form in which operands in the range [start_idx, start_idx+length) are grouped together. For example, (a + b + … + y + z) =

(a + b … + (l + … + m) + … + y + z)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘associated’ returns the right-hand side of ‘association’. ‘associate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘association’ for the inner expression.

cancelation(self, idx1, idx2, \*\*defaults_config)

Attempt a simple cancelation between operands at index i and j. If one of these operands is the negation of the other, deduce and return an equality between self and a form in which these operands are canceled.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘canceled’ returns the right-hand side of ‘cancelation’. ‘cancel’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘cancelation’ for the inner expression.

cancelations(self, \*\*defaults_config)

Deduce and return an equality between self and a form in which all simple cancellations are performed (where there are exact negations that occur).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘all_canceled’ returns the right-hand side of ‘cancelations’. ‘all_cancel’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘cancelations’ for the inner expression.

canceled(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘cancelation’.

commutation(self, init_idx=None, final_idx=None, \*\*defaults_config)

Given numerical operands, deduce that this expression is equal to a form in which the operand at index init_idx has been moved to final_idx. For example, (a + b + … + y + z) = (a + … + y + b + z) via init_idx = 1 and final_idx = -2.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘commuted’ returns the right-hand side of ‘commutation’. ‘commute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘commutation’ for the inner expression.

commuted(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘commutation’.

conversion_to_multiplication(self, \*\*defaults_config)

From the addition of the same values, derive and return the equivalence as a multiplication. For example, a + a + a = 3 * a

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘multiplied’ returns the right-hand side of ‘conversion_to_multiplication’. ‘multiply’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘conversion_to_multiplication’ for the inner expression.

deduce_bound(self, inner_expr_bound_or_bounds, inner_exprs_to_bound=None, \*\*defaults_config)

Return a bound of this arithmetic expression based upon the bounds of any number of inner expressions. The inner expression should appear on the left side of the corresponding bound which should be a number ordering relation (< or <=). The returned, proven bound will have this expression on the left-hand side. The bounds of the inner expressions will be processed in the order they are provided.

If inner_exprs_to_bound is provided, restrict the bounding to these particular InnerExpr objects. Otherwise, all inner expressions are fair game.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_difference_in_natural(self, \*\*defaults_config)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_difference_in_natural_pos(self, \*\*defaults_config)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_in_number_set(self, number_set, \*\*defaults_config)

given a number set, attempt to prove that the given expression is in that number set using the appropriate closure theorem

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

disassociated(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘disassociation’.

disassociation(self, idx, \*\*defaults_config)

Given numerical operands, deduce that this expression is equal to a form in which the operand at index idx is no longer grouped together. For example, (a + b … + (l + … + m) + … + y+ z)

= (a + b + … + y + z)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘disassociated’ returns the right-hand side of ‘disassociation’. ‘disassociate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘disassociation’ for the inner expression.

eliminated_zero(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘zero_elimination’.

eliminated_zeros(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘zero_eliminations’.

equality_side_effects(self, judgment)

If the right side is irreducible and the left side is binary, a + b = c, derive the commutation

b + a = c

and if neither a nor b is a Neg, also derive the following:

-a - b = -c c - b = a b - c = -a

factorization(self, the_factors, pull='left', group_factors=True, group_remainder=True, \*\*defaults_config)

Factor out the factor(s) from this sum, pulling it either to the “left” or “right”. If group_factors is True, the factors are grouped together as a sub-product. In the Add case, the remainder will always be grouped (we have ‘group_remainder’ as a parameter just for recursion compatibility).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘factorized’ returns the right-hand side of ‘factorization’. ‘factor’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘factorization’ for the inner expression.

factorized(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘factorization’.

group_commutation(self, init_idx, final_idx, length, disassociate=True, \*\*defaults_config)

Given numerical operands, deduce that this expression is equal to a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx. final_idx+length). It will do this by performing association first. If disassocate is True, it will be disassociated afterwards.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘group_commuted’ returns the right-hand side of ‘group_commutation’. ‘group_commute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘group_commutation’ for the inner expression.

group_commuted(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘group_commutation’.

remake_arguments(self)

Yield the argument values or (name, value) pairs that could be used to recreate the Operation.

remake_constructor(self)

Method to call to reconstruct this Expression. The default is the class name itself to use the __init__ method, but sometimes a different method is more appropriate for setting the proper style (e.g. the Frac method in proveit.numbers.division.divide which constructs a Div object with a different style). This constructor method must be in the same module as the class.

remake_with_style_calls(self)

In order to reconstruct this Expression to have the same styles, what “with…” method calls are most appropriate? Return a tuple of strings with the calls to make. The default for the Operation class is to include appropriate ‘with_wrapping_at’ and ‘with_justification’ calls.

style_options(self)

Return the StyleOptions object for the Operation.

subtraction_folding(self, term_idx=None, assumptions=frozenset())

Given a negated term, term_idx or the first negated term if term_idx is None, deduce the equivalence between self and a Subtract form (with the specified negated term on the right of the subtraction). Assumptions may be necessary to deduce operands being in the set of Complex numbers.

zero_elimination(self, idx, \*\*defaults_config)

Derive and return this Add expression equal to a form in which a specific zero operand (at the given index) is eliminated.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘eliminated_zero’ returns the right-hand side of ‘zero_elimination’. ‘eliminate_zero’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘zero_elimination’ for the inner expression.

zero_eliminations(self, \*\*defaults_config)

Derive and return this Add expression equal to a form in which all zero’s are eliminated.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘eliminated_zeros’ returns the right-hand side of ‘zero_eliminations’. ‘eliminate_zeros’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘zero_eliminations’ for the inner expression.