Round

class proveit.numbers.Round(A, *, styles=None)

Bases: proveit.Function

Methods Summary

deduce_in_number_set(self, number_set, …)	Given a number set number_set, attempt to prove that the given Round expression is in that number set using the appropriate closure theorem.
rounding_eliminated(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘rounding_elimination’.
rounding_elimination(self, \*\*defaults_config)	For the trivial case of Round(x) where the operand x is already an integer, derive and return this Round expression equated with the operand itself: Round(x) = x.
rounding_extracted(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘rounding_extraction’.
rounding_extraction(self[, idx_to_extract])	For the case of Round(x) where the operand x = x_real + x_int, derive and return Round(x) = Round(x_real) + x_int (thus ‘extracting’ the integer component out from the Round() fxn).

Methods Documentation

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

Given a number set number_set, attempt to prove that the given Round 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.

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

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

rounding_elimination(self, \*\*defaults_config)

For the trivial case of Round(x) where the operand x is already an integer, derive and return this Round expression equated with the operand itself: Round(x) = x. Assumptions may be necessary to deduce necessary conditions (for example, that x actually is an integer) for the simplification. This method is utilized by the do_reduced_simplification() method only after the operand x is verified to already be proven (or assumed) to be an integer. For the case where the operand is of the form x = real + int, see the rounding_extraction() method.

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

‘rounding_eliminated’ returns the right-hand side of ‘rounding_elimination’. ‘rounding_eliminate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘rounding_elimination’ for the inner expression.

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

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

rounding_extraction(self, idx_to_extract=None, \*\*defaults_config)

For the case of Round(x) where the operand x = x_real + x_int, derive and return Round(x) = Round(x_real) + x_int (thus ‘extracting’ the integer component out from the Round() fxn). The idx_to_extract is the zero-based index of the item in the operands of an Add(a, b, …, n) expression to attempt to extract. Assumptions may be necessary to deduce necessary conditions (for example, that x_int actually is an integer) for the simplification. This method is utilized by the do_reduced_simplification() method only after the operand x is verified to already be proven (or assumed) to be of the form x = x_real + x_int. For the case where the entire operand x is itself an integer, see the rounding_elimination() method.

This works only if the operand x is an instance of the Add class at its outermost level, e.g. x = Add(a, b, …, n). The operands of that Add class can be other things, but the extraction is guaranteed to work only if the inner operands a, b, etc., are simple.

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

‘rounding_extracted’ returns the right-hand side of ‘rounding_extraction’. ‘rounding_extract’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘rounding_extraction’ for the inner expression.