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

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)

%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

ceil_of_integer = Forall(x, Equals(Ceil(x), x), domain=Integer)

ceil_of_integer (conjecture without proof):

floor_of_integer = Forall(x, Equals(Floor(x), x), domain=Integer)

floor_of_integer (conjecture without proof):

round_of_integer = Forall(x, Equals(Round(x), x), domain=Integer)

round_of_integer (conjecture without proof):

ceil_of_sum_less_eq = Forall(
    (x, y),
    LessEq(Ceil(Add(x,y)), Add(Ceil(x), Ceil(y))),
    domain=Real)

ceil_of_sum_less_eq (conjecture without proof):

ceil_of_sum_greater_eq = Forall(
    (x, y),
    greater_eq(Ceil(Add(x,y)), subtract(Add(Ceil(x), Ceil(y)), one)),
    domain=Real)

ceil_of_sum_greater_eq (conjecture without proof):

floor_of_sum_less_eq = Forall(
    (x, y),
    LessEq(Floor(Add(x,y)), Add(Floor(x), Floor(y), one)),
    domain=Real)

floor_of_sum_less_eq (conjecture without proof):

floor_of_sum_greater_eq = Forall(
    (x, y),
    greater_eq(Floor(Add(x,y)), Add(Floor(x), Floor(y))),
    domain=Real)

floor_of_sum_greater_eq (conjecture without proof):

ceil_of_real_plus_int = Forall(
    x,
    Forall(n,
           Equals(Ceil(Add(x, n)), Add(Ceil(x), n)),
           domain=Integer),
    domain=Real)

ceil_of_real_plus_int (conjecture without proof):

floor_of_real_plus_int = Forall(
    x,
    Forall(n,
           Equals(Floor(Add(x, n)), Add(Floor(x), n)),
           domain=Integer),
    domain=Real)

floor_of_real_plus_int (conjecture without proof):

round_of_real_plus_int = Forall(
    x,
    Forall(n,
           Equals(Round(Add(x, n)), Add(Round(x), n)),
           domain=Integer),
    domain=Real)

round_of_real_plus_int (conjecture without proof):

Bounding Ceil, Floor, or Rounded Value

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

ceil_increasing_less (conjecture without proof):

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

floor_increasing_less (conjecture without proof):

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

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

ceil_of_real_above_int = (
    Forall((x, y),
           LessEq(Add(x, one), Ceil(y)),
           domains=[Integer, Real],
           condition=Less(x, y)
    ))

ceil_of_real_above_int (conjecture without proof):

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

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

ceil_x_ge_x (conjecture without proof):

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

floor_x_le_x (conjecture without proof):

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

real_minus_floor_upper_bound = Forall(
    x,
    Less(subtract(x, Floor(x)), one),
    domain=Real)

real_minus_floor_upper_bound (conjecture without proof):

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

ceil_of_ceil = Forall(
    x,
    Equals(Ceil(Ceil(x)), Ceil(x)),
    domain=Real)

ceil_of_ceil (conjecture without proof):

floor_of_floor = Forall(
    x,
    Equals(Floor(Floor(x)), Floor(x)),
    domain=Real)

floor_of_floor (conjecture without proof):

round_of_round = Forall(
    x,
    Equals(Round(Round(x)), Round(x)),
    domain=Real)

round_of_round (conjecture without proof):

Relating Ceil, Floor, and Round

floor_less_eq_ceil = Forall(
    x,
    LessEq(Floor(x), Ceil(x)),
    domain=Real)

floor_less_eq_ceil (conjecture without proof):

floor_equal_ceil_for_int = Forall(
    n,
    Equals(Floor(n), Ceil(n)),
    domain=Integer)

floor_equal_ceil_for_int (conjecture without proof):

floor_plus_ceil_of_neg = Forall(
    x,
    Equals(Add(Floor(x), Ceil(Neg(x))), zero),
    domain=Real)

floor_plus_ceil_of_neg (conjecture without proof):

floor_of_ceil = Forall(
    x,
    Equals(Floor(Ceil(x)), Ceil(x)),
    domain=Real)

floor_of_ceil (conjecture without proof):

ceil_of_floor = Forall(
    x,
    Equals(Ceil(Floor(x)), Floor(x)),
    domain=Real)

ceil_of_floor (conjecture without proof):

round_in_terms_of_floor = Forall(
    x,
    Equals(Round(x), Floor(Add(x, frac(one, two)))),
    domain=Real)

round_in_terms_of_floor (conjecture without proof):

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.

round_real_pos_closure = Forall(x, InSet(Round(x), Natural), domain=RealPos)

round_real_pos_closure (conjecture without proof):

ceil_real_pos_closure = Forall(x, InSet(Ceil(x), NaturalPos), domain=RealPos)

ceil_real_pos_closure (conjecture without proof):

floor_real_pos_closure = Forall(x, InSet(Floor(x), Natural), domain=RealPos)

floor_real_pos_closure (conjecture without proof):

ceil_of_real_is_real = Forall(x, InSet(Ceil(x), Real), domain=Real)

ceil_of_real_is_real (conjecture with conjecture-based proof):

floor_of_real_is_real = Forall(x, InSet(Floor(x), Real), domain=Real)

floor_of_real_is_real (conjecture with conjecture-based proof):

round_of_real_is_real = Forall(x, InSet(Round(x), Real), domain=Real)

round_of_real_is_real (conjecture with conjecture-based proof):

%end theorems

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