# 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
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:

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:

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_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_2:
round_x:
round_x_plus_y:
round_1_plus_2:
round_x_plus_2:
In [38]:
# Some more example test expressions involving Round

## 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:
In [47]:
floor_x_plus_y_in_ints_2.proof().disable()
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]:
In [75]:
In [76]:
round_02 = Round(Add(x, y, one, two))
round_02:
In [77]:

## 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]:

## 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]:
In [102]:
Floor(Add(x, one, y)).simplification(assumptions=[InSet(x, Real), InSet(y, Real)])

### Round.simplification()¶

In [103]:
In [104]:
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]:
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
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