# Theorems (or conjectures) for the theory of proveit.numbers.rounding¶

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import a, n, x, y
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import (Add, Ceil, Floor, frac, greater, greater_eq,
IntervalCO, Less, LessEq, Neg, Round, subtract)
from proveit.numbers import (zero, one, two, Integer, Natural,
NaturalPos, Real, RealPos)

In [2]:
%begin theorems

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


### Basic Properties of Ceil, Floor, & Round¶

In [3]:
ceil_of_integer = Forall(x, Equals(Ceil(x), x), domain=Integer)

ceil_of_integer (conjecture without proof):

In [4]:
floor_of_integer = Forall(x, Equals(Floor(x), x), domain=Integer)

floor_of_integer (conjecture without proof):

In [5]:
round_of_integer = Forall(x, Equals(Round(x), x), domain=Integer)

round_of_integer (conjecture without proof):

In [6]:
ceil_of_sum_less_eq = Forall(
(x, y),
domain=Real)

ceil_of_sum_less_eq (conjecture without proof):

In [7]:
ceil_of_sum_greater_eq = Forall(
(x, y),
domain=Real)

ceil_of_sum_greater_eq (conjecture without proof):

In [8]:
floor_of_sum_less_eq = Forall(
(x, y),
domain=Real)

floor_of_sum_less_eq (conjecture without proof):

In [9]:
floor_of_sum_greater_eq = Forall(
(x, y),
domain=Real)

floor_of_sum_greater_eq (conjecture without proof):

In [10]:
ceil_of_real_plus_int = Forall(
x,
Forall(n,
domain=Integer),
domain=Real)

ceil_of_real_plus_int (conjecture without proof):

In [11]:
floor_of_real_plus_int = Forall(
x,
Forall(n,
domain=Integer),
domain=Real)

floor_of_real_plus_int (conjecture without proof):

In [12]:
round_of_real_plus_int = Forall(
x,
Forall(n,
domain=Integer),
domain=Real)

round_of_real_plus_int (conjecture without proof):

### Bounding Ceil, Floor, or Rounded Value¶

In [13]:
ceil_increasing_less = (
Forall((x, y),
LessEq(Ceil(x), Ceil(y)),
conditions=[Less(x, y)],
domain=Real))

ceil_increasing_less (conjecture without proof):

In [14]:
floor_increasing_less = (
Forall((x, y),
LessEq(Floor(x), Floor(y)),
conditions=[Less(x, y)],
domain=Real))

floor_increasing_less (conjecture without proof):

In [15]:
ceil_increasing_less_eq = (
Forall((x, y),
LessEq(Ceil(x), Ceil(y)),
conditions=[LessEq(x, y)],
domain=Real))

ceil_increasing_less_eq (conjecture without proof):

In [16]:
floor_increasing_less_eq = (
Forall((x, y),
LessEq(Floor(x), Floor(y)),
conditions=[LessEq(x, y)],
domain=Real))

floor_increasing_less_eq (conjecture without proof):

In [17]:
ceil_of_real_above_int = (
Forall((x, y),
domains=[Integer, Real],
condition=Less(x, y)
))

ceil_of_real_above_int (conjecture without proof):

In [18]:
floor_of_real_below_int = (
Forall((x, y),
LessEq(Floor(x), subtract(y, one)),
domains=[Real, Integer],
condition=Less(x, y)
))

floor_of_real_below_int (conjecture without proof):

### Comparing a Number with its Ceil, Floor, or Rounded Value¶

In [19]:
ceil_x_ge_x = (
Forall(x,
greater_eq(Ceil(x), x),
domain=Real))

ceil_x_ge_x (conjecture without proof):

In [20]:
floor_x_le_x = (
Forall(x,
LessEq(Floor(x), x),
domain=Real))

floor_x_le_x (conjecture without proof):

In [21]:
real_minus_floor_lower_bound = Forall(
x,
greater_eq(subtract(x, Floor(x)), zero),
domain=Real)

real_minus_floor_lower_bound (conjecture with conjecture-based proof):

In [22]:
real_minus_floor_upper_bound = Forall(
x,
Less(subtract(x, Floor(x)), one),
domain=Real)

real_minus_floor_upper_bound (conjecture without proof):

In [23]:
real_minus_floor_interval = Forall(
x,
InSet(subtract(x, Floor(x)), IntervalCO(zero, one)),
domain=Real)

real_minus_floor_interval (conjecture with conjecture-based proof):

### Ceil, Floor, and Round functions are idempotent¶

In [24]:
ceil_of_ceil = Forall(
x,
Equals(Ceil(Ceil(x)), Ceil(x)),
domain=Real)

ceil_of_ceil (conjecture without proof):

In [25]:
floor_of_floor = Forall(
x,
Equals(Floor(Floor(x)), Floor(x)),
domain=Real)

floor_of_floor (conjecture without proof):

In [26]:
round_of_round = Forall(
x,
Equals(Round(Round(x)), Round(x)),
domain=Real)

round_of_round (conjecture without proof):

### Relating Ceil, Floor, and Round¶

In [27]:
floor_less_eq_ceil = Forall(
x,
LessEq(Floor(x), Ceil(x)),
domain=Real)

floor_less_eq_ceil (conjecture without proof):

In [28]:
floor_equal_ceil_for_int = Forall(
n,
Equals(Floor(n), Ceil(n)),
domain=Integer)

floor_equal_ceil_for_int (conjecture without proof):

In [29]:
floor_plus_ceil_of_neg = Forall(
x,
domain=Real)

floor_plus_ceil_of_neg (conjecture without proof):

In [30]:
floor_of_ceil = Forall(
x,
Equals(Floor(Ceil(x)), Ceil(x)),
domain=Real)

floor_of_ceil (conjecture without proof):

In [31]:
ceil_of_floor = Forall(
x,
Equals(Ceil(Floor(x)), Floor(x)),
domain=Real)

ceil_of_floor (conjecture without proof):

In [32]:
round_in_terms_of_floor = Forall(
x,
domain=Real)

round_in_terms_of_floor (conjecture without proof):

In [33]:
round_in_terms_of_ceil = Forall(
x,
Equals(Round(x), Ceil(subtract(x, frac(one, two)))),
domain=Real)

round_in_terms_of_ceil (conjecture without proof):

### Closure Theorems¶

#### Note: the identifications of Ceil(x), Floor(x), and Round(x) as Integer numbers appear as axioms in the axioms notebook.¶

In [34]:
round_real_pos_closure = Forall(x, InSet(Round(x), Natural), domain=RealPos)

round_real_pos_closure (conjecture without proof):

In [35]:
ceil_real_pos_closure = Forall(x, InSet(Ceil(x), NaturalPos), domain=RealPos)

ceil_real_pos_closure (conjecture without proof):

In [36]:
floor_real_pos_closure = Forall(x, InSet(Floor(x), Natural), domain=RealPos)

floor_real_pos_closure (conjecture without proof):

In [37]:
ceil_of_real_is_real = Forall(x, InSet(Ceil(x), Real), domain=Real)

ceil_of_real_is_real (conjecture with conjecture-based proof):

In [38]:
floor_of_real_is_real = Forall(x, InSet(Floor(x), Real), domain=Real)

floor_of_real_is_real (conjecture with conjecture-based proof):

In [39]:
round_of_real_is_real = Forall(x, InSet(Round(x), Real), domain=Real)

round_of_real_is_real (conjecture with conjecture-based proof):

In [40]:
%end theorems

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