Axioms for the theory of proveit.numbers.rounding

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)

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

ceil_is_an_int = Forall(
        x,
        InSet(Ceil(x), Integer),
        domain=Real)

ceil_is_an_int:

ceil_of_x_greater_eq_x = Forall(
        x,
        greater_eq(Ceil(x), x),
        domain=Real)

ceil_of_x_greater_eq_x:

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:

floor_is_an_int = Forall(
        x,
        InSet(Floor(x), Integer),
        domain=Real)

floor_is_an_int:

floor_of_x_less_eq_x = Forall(
        x,
        LessEq(Floor(x), x),
        domain=Real)

floor_of_x_less_eq_x:

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:

round_is_an_int = Forall(
        x,
        InSet(Round(x), Integer),
        domain=Real)

round_is_an_int:

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

round_is_closest_int:

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

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

round_up:

%end axioms

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