# Axioms for the theory of proveit.numbers.rounding¶

In [1]:
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import x, y
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import (one, two, Abs, Ceil, Floor, frac, greater_eq,
Integer, LessEq, Real, Round, subtract)

In [2]:
%begin axioms

Defining axioms for theory 'proveit.numbers.rounding'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions


#### The ceiling of a real number x, denoted $\lceil x \rceil$, is the least integer greater than or equal to x. This notion is captured in the following three axioms:¶

In [3]:
ceil_is_an_int = Forall(
x,
InSet(Ceil(x), Integer),
domain=Real)

ceil_is_an_int:
In [4]:
ceil_of_x_greater_eq_x = Forall(
x,
greater_eq(Ceil(x), x),
domain=Real)

ceil_of_x_greater_eq_x:
In [5]:
ceil_of_x_less_eq = Forall(
(x, y),
LessEq(Ceil(x), y),
domains=[Real, Integer],
conditions=[greater_eq(y, x)])

ceil_of_x_less_eq:

#### The floor of a real number x, denoted $\lfloor x \rfloor$ (in some literature, denoted by $[x]$), can be described as the greatest integer less than or equal to x. This notion is captured in the following three axioms:¶

In [6]:
floor_is_an_int = Forall(
x,
InSet(Floor(x), Integer),
domain=Real)

floor_is_an_int:
In [7]:
floor_of_x_less_eq_x = Forall(
x,
LessEq(Floor(x), x),
domain=Real)

floor_of_x_less_eq_x:
In [8]:
floor_of_x_greater_eq = Forall(
(x, y),
greater_eq(Floor(x), y),
domains=[Real, Integer],
conditions=[LessEq(y, x)])

floor_of_x_greater_eq:

#### The rounding of a real number $x$, denoted here by $\text{round}(x)$, can be described as the nearest integer to $x$, with tie-breaking upward (e.g., $\text{round}(3.5) = 4$). This notion is captured in the following axioms:¶

In [9]:
round_is_an_int = Forall(
x,
InSet(Round(x), Integer),
domain=Real)

round_is_an_int:
In [10]:
round_is_closest_int = Forall(
(x, y),
LessEq(Abs(subtract(Round(x), x)), Abs(subtract(y, x))),
domains=[Real, Integer])

round_is_closest_int:
In [11]:
# Leaving this instantiation for futher consider later;
# see next cell for current round_up axiom
# round_up = Forall(
#         x,
#         greater_eq(Round(x), x),
#         domain=Real,
#         conditions=[Equals(Abs(subtract(Round(x), x)), frac(one, two))])

In [12]:
round_up = Forall(
x,
Equals(Round(x), Ceil(x)),
domain=Real,
conditions=[Equals(subtract(x, Floor(x)), subtract(Ceil(x), x))])

round_up:
In [13]:
%end axioms

These axioms may now be imported from the theory package: proveit.numbers.rounding