logo

Demonstrations for the theory of proveit.numbers.rounding

In [1]:
import proveit
from proveit import used_vars, free_vars
from proveit import n, x, y
from proveit.logic import InSet
from proveit.numbers import Add, Mult, subtract
from proveit.numbers import zero, one, two, three, Integer, Natural, Real, RealPos, Complex
from proveit.numbers.rounding import Ceil, Floor, Round
%begin demonstrations

Rounding: $\textit{round}(x), \lceil{x}\rceil, \lfloor{x}\rfloor$

Introduction

The `Round`, `Ceil`, and `Floor` classes allow us to represent standard rounding functions that take arbitrary real numbers to nearby integers in the usual way: $\text{Round}(x) = z$ represents the rounding of a real number $x$ to the nearest integer $z$; $\text{Ceil}(x) = \lceil{x}\rceil = z$ represents the rounding of a real number x to the smallest integer $z$ that is greater than or equal to $x$; and $\text{Floor}(x) = \lfloor{x}\rfloor = z$ represents the rounding of a real number x to the largest integer $z$ that is less than or equal to $x$. This ``_demonstrations_`` notebook explores the `Round`, `Ceil`, and `Floor` classes, their axioms and common theorems, and related methods.

Simple Expressions Involving Rounding: $\text{Round}(x)$, $\text{Ceil}(x) = \lceil{x}\rceil$, $\text{Floor}(x) = \lfloor{x}\rfloor$

It is straightforward to construct expressions to represent the various types of rounding operations on real numbers. Here are some basic examples of such expressions:

In [2]:
# representing basic rounding of a real number x
Round(x)
In [3]:
# representing the ceiling of a real sum
Ceil(Add(x, y))
In [4]:
# representing the floor of a real difference
Floor(subtract(x, y))

Common Attributes of a Floor expression $\lfloor{x}\rfloor$

Let's define a simple example `Floor()` expression, $\lfloor{x-y}\rfloor$, and look at some of its attributes.

In [5]:
floor_x_minus_y = Floor(subtract(x,y))
floor_x_minus_y:
In [6]:
floor_x_minus_y.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 1
operand: 3
1Literal
2ExprTuple3
3Operationoperator: 4
operands: 5
4Literal
5ExprTuple6, 7
6Variable
7Operationoperator: 8
operand: 10
8Literal
9ExprTuple10
10Variable

We can access the Floor operand $x-y$, and identify the `Floor` operator as the outermost operation:

In [7]:
floor_x_minus_y.operand
In [8]:
floor_x_minus_y.operator

Notice in this case that the Floor's operand $x-y$ itself has operands $(x, -y)$ (because the subtract() expression is internally represented as an instance of `Add(x, -y))`:

We can also get a list of the variables and a list of the free variables:

In [9]:
used_vars(floor_x_minus_y)
In [10]:
free_vars(floor_x_minus_y)

And of course, we can reach down inside and look at the structure of the operand itself, which in this case consists of an Add() expression (even though we created it using the subtract() function):

In [11]:
# operator inside the operand inside the Floor
floor_x_minus_y.operand.operator
In [12]:
floor_x_minus_y.operand.operands
In [13]:
# info about the operand itself
floor_x_minus_y.operand.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 1
operands: 2
1Literal
2ExprTuple3, 4
3Variable
4Operationoperator: 5
operand: 7
5Literal
6ExprTuple7
7Variable

Axioms

The axioms for the rounding theory establish the basic properties of the `Ceil`, `Floor`, and `Round` class functions. Some examples are shown below (and the entire complement of axioms can be found in the notebook `proveit.numbers.rounding .ipynb`).

In [14]:
from proveit.numbers.rounding  import (ceil_is_an_int, ceil_of_x_greater_eq_x, round_up)
In [15]:
# When defined, Ceil is always an integer
ceil_is_an_int
 ⊢  
In [16]:
# When defined, Ceil(x) is always greater than or equal to x
ceil_of_x_greater_eq_x
 ⊢  
In [17]:
# The round function rounds up for reals mid-way between two integers
round_up
 ⊢  

Theorems

The theorems for the rounding theory capture many of the basic derivable properties of the `Ceil`, `Floor`, and `Round` class functions. Many of the theorems are then used for related class methods.
Below we show a few examples of such theorems (the current collection of theorems can be found in the notebook `proveit.numbers.rounding._theorems_.ipynb`):

In [18]:
from proveit.numbers.rounding import (
        ceil_of_integer, floor_of_sum_greater_eq, floor_of_floor,
        floor_plus_ceil_of_neg, round_in_terms_of_floor)
In [19]:
# The ceiling of an integer is just itself
ceil_of_integer
 ⊢  
In [20]:
# The floor of a sum is greater than or equal to the sum of the floors
floor_of_sum_greater_eq
 ⊢  
In [21]:
# The floor function is idempotent
floor_of_floor
 ⊢  
In [22]:
# The floor and ceiling functions are related in a variety of ways
floor_plus_ceil_of_neg
 ⊢  
In [23]:
# We can express the Round function in terms of the Floor
round_in_terms_of_floor
 ⊢  

Demonstrations

1. Simplifying $\texttt{round}((x+1)+(y+2))$

We consider the simplification of the rounding expression `Round((x+1)+(y+2))`, calling upon the general `Expr.simplification()` method, which itself behind the scenes eventually utilizes the `Round.do_reduced_simplification()` method and works to apply two possible simplification theorems involving integer operands of the `Round` class.
First, we define our expression:

In [24]:
round_xplus1_plus_yplus2 = Round(Add(Add(x,one), Add(y, two)))
round_xplus1_plus_yplus2:

We then try calling the Expression `simplification()` method. If we know nothing about the addends $x$ and $y$, we will get an error:

In [25]:
# If addends are not known to be integers or reals 
from proveit import InstantiationFailure
try:
    round_xplus1_plus_yplus2.simplification()
    assert False, "Expected a ProofFailure error"
except InstantiationFailure as e:
    print("EXCEPTION: the simplification theorems do not apply without more constraints. ", e)

EXCEPTION: the simplification theorems do not apply without more constraints.  Proof step failed:
Attempting to instantiate |- forall_{i, j, k in Natural} [forall_{a_{1}, a_{2}, ..., a_{i}, b_{1}, b_{2}, ..., b_{j}, c_{1}, c_{2}, ..., c_{k} in Complex} ((a_{1} +  a_{2} +  ... +  a_{i} + (b_{1} +  b_{2} +  ... +  b_{j})+ c_{1} +  c_{2} +  ... +  c_{k}) =  \\ (a_{1} +  a_{2} +  ... +  a_{i}+ b_{1} +  b_{2} +  ... +  b_{j}+ c_{1} +  c_{2} +  ... +  c_{k}))] with {i: 0, j: 2, k: 1, a: (), b: (x, 1), c: (y + 2)}:
Unsatisfied condition: x in Complex. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

But if we know that $x$ and $y$ are real (either because we already know that from previous work or, as we do here, we supply that information as assumptions), the simplification goes through, with Prove-It automatically simplifying $1+2$ to $3\in\mathbb{Z}$, and eventually applying a rounding theorem of the form $\forall_{x\in\mathbb{R},i\in\mathbb{Z}}\texttt{ round}(x + i) = \texttt{ round}(x) + i$:

In [26]:
round_xplus1_plus_yplus2.simplification(assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  

Interestingly, if we try to directly call the `Round.shallow_simplification()` method on our `Round(Add(Add(x+1),Add(y+2)))` expression, we get only the trivial self-equivalence back, because we now lack the `simplification()` method's pre-processing of the operand to produce $x+y+3$ first and now fail to be able to segregate the operands into a partition of reals and integers:

In [27]:
round_xplus1_plus_yplus2.shallow_simplification(
        assumptions=[InSet(x, Real), InSet(y, Real)])
 ⊢  

2. Simplification and deductions involving $\texttt{Floor}(\alpha, \beta) = \lfloor \alpha + \beta \rfloor$

Here we consider the floor of a sum of two variables, $\lfloor \alpha + \beta \rfloor$, produced using the Expression $\texttt{Floor}(\texttt{Add}(\alpha, \beta))$, and try to simplify the expression and deduce that the $\texttt{Floor}$ expression represents an integer.
First, we define our expression:

In [28]:
from proveit import alpha, beta
floor_alpha_plus_beta = Floor(Add(alpha, beta))
floor_alpha_plus_beta:

And the `Floor.deduce_in_number_set()` method will return an error:

In [29]:
# If Floor operand(s) uncharacterized 
from proveit import UnsatisfiedPrerequisites
try:
    floor_alpha_plus_beta.deduce_in_number_set(Integer)
    assert False, "Expected a ProofFailure error"
except UnsatisfiedPrerequisites as e:
    print("EXCEPTION: the simplification theorems do not apply without more constraints. ", e)

EXCEPTION: the simplification theorems do not apply without more constraints.  Prerequisites not met while assuming (): No readily provable number set for alpha + beta

But if we know or can assume some basic properties of $\alpha$ and $\beta$, we can simplify and make a deduction about the resulting form of the result. For example, suppose we know or can assume that $\alpha\in\mathbb{R}$ while $\beta\in\mathbb{Z}$. Then we can derive the equivalence $\lfloor\alpha+\beta\rfloor = \lfloor\alpha\rfloor + \beta$ (extracting the integer $\beta$ out from inside the `Floor` function):

In [30]:
floor_alpha_plus_beta.simplification(assumptions=[InSet(alpha, Real), InSet(beta, Integer)])
,  ⊢  

And we can deduce that the `Floor` function will produce an integer:

In [31]:
floor_alpha_plus_beta.deduce_in_number_set(Integer, assumptions=[InSet(alpha, Real), InSet(beta, Integer)])
,  ⊢  

3. Prove that $\forall_{x\in\mathbb{R}}(\lceil x \rceil + \lfloor -x \rfloor = 0)$ from the theorem $\forall_{x\in\mathbb{R}}(\lfloor x \rfloor + \lceil -x \rceil = 0)$.

One of our theorems in the rounding theory is that $\forall_{x\in\mathbb{R}}(\lfloor x \rfloor + \lceil -x \rceil = 0)$. We can use that theorem to prove the complementary theorem that $\forall_{x\in\mathbb{R}}(\lceil x \rceil + \lfloor -x \rfloor = 0)$, essentially by performing a substitution $x \mapsto -x$.

We begin by importing and displaying the original theorem:

In [32]:
from proveit.numbers.rounding import floor_plus_ceil_of_neg
floor_plus_ceil_of_neg
 ⊢  

Then we instantiate that general theorem, mapping $x$ to $-x$ (and explicitly include the required assumption that $x\in\mathbb{R}$).

In [33]:
from proveit.numbers import Neg
floor_plus_ceil_of_neg_spec = floor_plus_ceil_of_neg.instantiate(
    {x:Neg(x)}, assumptions=[InSet(x, Real)])
floor_plus_ceil_of_neg_spec:  ⊢  

And generalize to our desired universal claim:

In [34]:
floor_plus_ceil_of_neg_spec.generalize(x, domain=Real)
 ⊢  

Misc Testing

The material below was developed to test various rounding-related methods. Some of this material could be integrated into the _demonstrations_ page eventually and/or deleted as development continues.

Example Ceil, Floor, and Round Expressions

In [35]:
# Some example test expressions involving Ceil
ceil_2, ceil_x_minus_y, ceil_x_minus_y_plus_2, ceil_x, ceil_y = (
    Ceil(two), Ceil(subtract(x,y)), Ceil(Add(subtract(x,y), two)), Ceil(x), Ceil(y))
ceil_2:
ceil_x_minus_y:
ceil_x_minus_y_plus_2:
ceil_x:
ceil_y:
In [36]:
# Some example test expressions involving Floor
floor_2, floor_x_plus_y, floor_x_plus_y_plus_1 = (
    Floor(two), Floor(Add(x, y)), Floor(Add(Add(x,y), one)))
floor_2:
floor_x_plus_y:
floor_x_plus_y_plus_1:
In [37]:
# Some example test expressions involving Round
round_2, round_x, round_x_plus_y, round_1_plus_2, round_x_plus_2 = (
    Round(two), Round(x), Round(Add(x, y)), Round(Add(one, two)), Round(Add(x, two)))
round_2:
round_x:
round_x_plus_y:
round_1_plus_2:
round_x_plus_2:
In [38]:
# Some more example test expressions involving Round
round_add_xy12, round_add_add, round_add_mult_mult = (
    Round(Add(x, y, one, two)), Round(Add(Add(x, y),Add(one, two))),
    Round(Add(Mult(x,y), Mult(one, two))))
round_add_xy12:
round_add_add:
round_add_mult_mult:

Testing the deduce_in_number_set() methods

Ceil.deduce_in_number_set()

In [39]:
ceil_2.deduce_in_number_set(Integer)
 ⊢  
In [40]:
ceil_x_minus_y_in_ints = ceil_x_minus_y.deduce_in_number_set(
    Integer, assumptions=[InSet(x, Real), InSet(y, Real)])
ceil_x_minus_y_in_ints: ,  ⊢  
In [41]:
ceil_x_minus_y_in_ints.proof().disable()
ceil_x_minus_y.deduce_in_number_set(
    Integer, assumptions=[InSet(subtract(x, y), Real)])
 ⊢  
In [42]:
ceil_x_minus_y.deduce_in_number_set(Natural, assumptions=[InSet(subtract(x,y), RealPos)])
 ⊢  
In [43]:
# If we don't at least know the operand is real-valued,
# difficult to know what set(s) the result belongs to 
try:
    ceil_x_minus_y.deduce_in_number_set(Integer)
except Exception as e:
    print("EXCEPTION: the closure theorems do not apply without more constraints. ", e)

EXCEPTION: the closure theorems do not apply without more constraints.  Prerequisites not met while assuming (): No readily provable number set for x - y

Floor.deduce_in_number_set()

In [44]:
floor_2.deduce_in_number_set(Natural)
 ⊢  
In [45]:
floor_x_plus_y_in_ints = floor_x_plus_y.deduce_in_number_set(
    Integer, assumptions=[InSet(x, Real), InSet(y, Real)])
floor_x_plus_y_in_ints: ,  ⊢  
In [46]:
floor_x_plus_y_in_ints.proof().disable()
floor_x_plus_y_in_ints_2 = floor_x_plus_y.deduce_in_number_set(Integer, assumptions=[InSet(Add(x,y), Real)])
floor_x_plus_y_in_ints_2:  ⊢  
In [47]:
floor_x_plus_y_in_ints_2.proof().disable()
floor_x_plus_y.deduce_in_number_set(Natural, assumptions=[InSet(Add(x,y), RealPos)])
 ⊢  
In [48]:
# If we don't at least know the operand is real-valued,
# difficult to know what set(s) the result belongs to 
try:
    floor_x_plus_y.deduce_in_number_set(Integer)
except Exception as e:
    print("EXCEPTION: the closure theorems do not apply without more constraints. ", e)

EXCEPTION: the closure theorems do not apply without more constraints.  Prerequisites not met while assuming (): No readily provable number set for x + y

Round.deduce_in_number_set()

In [49]:
round_2.deduce_in_number_set(Natural)
 ⊢  
In [50]:
round_x.deduce_in_number_set(Integer, assumptions=[InSet(x, Real)])
 ⊢  
In [51]:
round_x.deduce_in_number_set(Natural, assumptions=[InSet(x, RealPos)])
 ⊢  
In [52]:
# If we don't at least know the operand is real-valued,
# difficult to know what set(s) the result belongs to 
try:
    round_x.deduce_in_number_set(Integer)
except Exception as e:
    print("EXCEPTION: the closure theorems do not apply without more constraints. ", e)

EXCEPTION: the closure theorems do not apply without more constraints.  Prerequisites not met while assuming (): No readily provable number set for x

Testing the rounding_elimination() method

Some testing of the `rounding_elimination()` utility method(s), allowing the simplification of `Ceil(x)`, `Floor(x)`, and `Round(x)` to the operand $x$ when we know $x\in\mathbb{Z}$.

In [53]:
ceil_2
In [54]:
ceil_2.rounding_elimination()
 ⊢  
In [55]:
ceil_x_minus_y
In [56]:
ceil_x_minus_y.rounding_elimination(assumptions=[InSet(x, Integer), InSet(y, Integer)])
,  ⊢  
In [57]:
ceil_x_minus_y_plus_2
In [58]:
ceil_x_minus_y_plus_2.rounding_elimination(assumptions=[InSet(x, Integer), InSet(y, Integer)])
,  ⊢  
In [59]:
floor_2.rounding_elimination()
 ⊢  
In [60]:
floor_x_plus_y.rounding_elimination(assumptions=[InSet(x, Integer), InSet(y, Integer)])
,  ⊢  
In [61]:
round_2.rounding_elimination()
 ⊢  
In [62]:
round_x.rounding_elimination(assumptions=[InSet(x, Integer)])
 ⊢  
In [63]:
round_x_plus_y.rounding_elimination(assumptions=[InSet(x, Integer), InSet(y, Integer)])
,  ⊢  
In [64]:
round_1_plus_2.rounding_elimination()
 ⊢  
In [65]:
round_x_plus_2.rounding_elimination(assumptions=[InSet(x, Integer)])
 ⊢  

The rounding_extraction() method

Some testing of the utility `rounding_extraction()` method(s), allowing the conclusion of an equivalence from `Ceil(x+i)`, `Floor(x+i)`, and `Round(x+i)` to the expression $F(x)+i$ when we know $x\in\mathbb{R}$ and $i\in\mathbb{Z}$.

Ceil.rounding_extraction()

In [66]:
ceil_x_minus_y
In [67]:
ceil_x_minus_y_plus_2
In [68]:
ceil_x_minus_y.rounding_extraction(1, assumptions=[InSet(x, Real), InSet(y, Integer)])
,  ⊢  
In [69]:
ceil_x_minus_y_plus_2.rounding_extraction(1, assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  

Floor.rounding_extraction()

In [70]:
floor_x_plus_y
In [71]:
floor_x_plus_y_plus_1
In [72]:
floor_x_plus_y.rounding_extraction(1, assumptions=[InSet(x, Real), InSet(y, Integer)])
,  ⊢  
In [73]:
floor_x_plus_y_plus_1.rounding_extraction(1, assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  

Round.rounding_extraction()

In [74]:
round_add_xy12.rounding_extraction(2, assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  
In [75]:
round_add_mult_mult.rounding_extraction(1, assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  
In [76]:
round_02 = Round(Add(x, y, one, two))
round_02:
In [77]:
round_add_add.rounding_extraction(1, assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  

The shallow_simplification() method

Some testing of the `do_reduced_simplification()` method(s), allowing the simplification of `Ceil(x)`, `Floor(x)`, and `Round(x)` to the operand $x$ when we know $x\in\mathbb{Z}$, and simplification of `f(x+n)` to `f(x)+n` when $x$ is real and $n\in\mathbb{Z}$. This is not a method that would typically be called directly — instead it ends up getting called by the more general Expr.simplification() method.

Ceil.shallow_simplification()

In [78]:
# simplifying ceiling of an integer
ceil_2.shallow_simplification()
 ⊢  
In [79]:
# simplifying ceiling of expression assumed to be an integer
ceil_x_minus_y.shallow_simplification(assumptions=[InSet(subtract(x, y), Integer)])
 ⊢  
In [80]:
# simplifying ceiling of a sum of an assumed real and an assumed integer
ceil_x_minus_y.shallow_simplification(assumptions=[InSet(x, Real), InSet(y, Integer)])
,  ⊢  
In [81]:
# simplifying ceiling of sum of some assumed real numbers and an actual integer
ceil_x_minus_y_plus_2.shallow_simplification(assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  

Floor.shallow_simplification()

In [82]:
# simplifying floor of an integer
floor_2.shallow_simplification()
 ⊢  
In [83]:
# simplifying floor of a sum of assumed integers
floor_x_plus_y.shallow_simplification(assumptions=[InSet(x, Integer), InSet(y, Integer)])
,  ⊢  
In [84]:
# simplifying floor of a sum of an assumed real and an assumed integer
floor_x_plus_y.shallow_simplification(assumptions=[InSet(x, Real), InSet(y, Integer)])
,  ⊢  
In [85]:
# simplifying floor of a sum of some assumed real numbers and an actual integer
floor_x_plus_y_plus_1.shallow_simplification(assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  

Round.shallow_simplification()

In [86]:
round_2.shallow_simplification()
 ⊢  
In [87]:
round_1_plus_2
In [88]:
round_1_plus_2.shallow_simplification()
 ⊢  
In [89]:
round_x.shallow_simplification(assumptions=[InSet(x, Integer)])
 ⊢  
In [90]:
round_x_plus_y.shallow_simplification(assumptions=[InSet(x, Real), InSet(y, Integer)])
,  ⊢  
In [91]:
round_x_plus_2.shallow_simplification(assumptions=[InSet(x, Real)])
 ⊢  
In [92]:
round_add_add.shallow_simplification(assumptions=[InSet(Add(x,y), Real)])
 ⊢  

The Expr.simplification() method

Ceil.simplification()

In [93]:
# simplifying ceiling of an integer
ceil_2.simplification()
 ⊢  
In [94]:
# simplifying ceiling of expression assumed to be an integer
ceil_x_minus_y.simplification(assumptions=[InSet(subtract(x, y), Integer)])
 ⊢  
In [95]:
# from proveit.logic.sets import SubsetEq
# from proveit.numbers import NaturalPos
# SubsetEq(NaturalPos, Integer).proven()
In [96]:
# simplifying ceiling of a sum of an assumed real and an assumed integer
ceil_x_minus_y.simplification(assumptions=[InSet(x, Real), InSet(y, Integer)])
,  ⊢  
In [97]:
# simplifying ceiling of sum of an assumed real,
# as assumed integer, and an actual integer
ceil_x_minus_y_plus_2.simplification(assumptions=[InSet(x, Real), InSet(y, Integer)])
,  ⊢  

Floor.simplification()

In [98]:
floor_x_plus_y_plus_1
In [99]:
Floor(Add(x, y, one)).inner_expr().operand.association(0, 2, assumptions=[InSet(x, Real), InSet(y, Real)], auto_simplify=False)
,  ⊢  
In [100]:
floor_x_plus_y_plus_1.simplification(assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  
In [101]:
Floor(Add(x, one, y))
In [102]:
Floor(Add(x, one, y)).simplification(assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  

Round.simplification()

In [103]:
round_add_add
In [104]:
round_add_add.simplification(assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  
In [105]:
round_01 = Round(Add(x, y, one, two))
round_01:
In [106]:
round_01_alt = Round(Add(x, one, y, two))
round_01_alt:
In [107]:
try:
    # if we don't know that the variables x and y are real, 
    # we cannot perform a simplification
    round_01.simplification(assumptions=[InSet(x, Complex), InSet(y, Complex)])
    assert False
except Exception as e:
    print("Expected exception: ", e)

Expected exception:  Proof step failed assuming {x in Complex, y in Complex}:
Attempting to instantiate |- forall_{x in Real} [forall_{n in Integer} (round(x + n) = (round(x) + n))] with {x: x + y, n: 3}:
Unsatisfied condition: (x + y) in Real. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.
In [108]:
round_01.simplification(
    assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  
In [109]:
round_01_alt.simplification(
    assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  
In [110]:
from proveit.numbers import Mult
Round(Mult(x,y)).shallow_simplification(assumptions=[InSet(Mult(x, y), Integer)])
 ⊢  
In [111]:
Round(Add(Mult(x,y), Add(one, two))).simplification(assumptions=[InSet(Mult(x, y), Real)])
 ⊢  
In [112]:
Round(Add(one, Mult(x,y), two)).simplification(assumptions=[InSet(x, Real), InSet(y, Real)])
,  ⊢  
In [113]:
# If operand is not known or assumed to be an integer
# or a simple Add expression, we do not get an error but
# instead the trivial self-equivalence
Round(Mult(x,y)).shallow_simplification()
 ⊢  
In [114]:
# If we try to nudge things along by assuming x, y in the set of Integer numbers,
# simplification will (by design) not automatically deduce that the
# product is an integer, so we still get the trivial self-equivalence
Round(Mult(x,y)).simplification(
        assumptions=[InSet(x, Integer), InSet(y, Integer)])
,  ⊢  
In [115]:
# But if we assume the entire product is an integer, the simplification
# process will find the expected equivalence and extract out the
# product from the round() function
Round(Mult(x,y)).simplification(assumptions=[InSet(Mult(x, y), Integer)])
 ⊢  

Testing bound_via_operand_bound() for Ceil

In [116]:
from proveit import a, b, c, x, y, z
from proveit.logic import InSet
from proveit.numbers import Integer, Real
from proveit.numbers import Less, LessEq, greater, greater_eq
In [117]:
ceil_assumptions = [InSet(a, Integer), InSet(b, Integer), InSet(c, Integer), InSet(x, Real), InSet(y, Real),
                   Less(a, x), Less(y, b), greater(y, c)]
ceil_assumptions:
In [118]:
ceil_x.bound_via_operand_bound(greater(x, a), assumptions=ceil_assumptions)
, ,  ⊢  
In [119]:
ceil_y.bound_via_operand_bound(greater(y, c), assumptions=ceil_assumptions)
, ,  ⊢  
In [120]:
%end demonstrations