Library Stdlib.Reals.Zfloor

Require Import Rbase Rfunctions Lra Lia.

Local Open Scope R_scope.

Definition Zfloor (x : R) := (up x - 1)%Z.

Lemma up_Zfloor x : up x = (Zfloor x + 1)%Z.

Lemma IZR_up_Zfloor x : IZR (up x) = IZR (Zfloor x) + 1.

Lemma Zfloor_bound x : IZR (Zfloor x) <= x < IZR (Zfloor x) + 1.

Lemma Zfloor_lub (z : Z) x : IZR z <= x -> (z <= Zfloor x)%Z.

Lemma Zfloor_eq (z : Z) x : IZR z <= x < IZR z + 1 -> Zfloor x = z.

Lemma Zfloor_le x y : x <= y -> (Zfloor x <= Zfloor y)%Z.

Lemma Zfloor_addz (z: Z) x : Zfloor (x + IZR z) = (Zfloor x + z)%Z.

Lemma ZfloorZ (z : Z) : Zfloor (IZR z) = z.

Lemma ZfloorNZ (z : Z) : Zfloor (- IZR z) = (- z)%Z.

Lemma ZfloorD_cond r1 r2 :
  if Rle_dec (IZR (Zfloor r1) + IZR (Zfloor r2) + 1) (r1 + r2)
  then Zfloor (r1 + r2) = (Zfloor r1 + Zfloor r2 + 1)%Z
  else Zfloor (r1 + r2) = (Zfloor r1 + Zfloor r2)%Z.

Definition Zceil (x : R) := (- Zfloor (- x))%Z.

Theorem Zceil_bound x : (IZR (Zceil x) - 1 < x <= IZR (Zceil x))%R.

Theorem Zfloor_ceil_bound x : (IZR (Zfloor x) <= x <= IZR (Zceil x))%R.

Theorem ZceilN x : (Zceil (- x) = - Zfloor x)%Z.

Theorem ZfloorN x : (Zfloor (- x) = - Zceil x)%Z.

Lemma Zceil_eq (z : Z) x : IZR z - 1 < x <= IZR z -> Zceil x = z.

Lemma Zceil_le x y : x <= y -> (Zceil x <= Zceil y)%Z.

Lemma Zceil_addz (z: Z) x : Zceil (x + IZR z) = (Zceil x + z)%Z.

Lemma ZceilD_cond r1 r2 :
  if Rle_dec (r1 + r2) (IZR (Zceil r1) + IZR (Zceil r2) - 1)
  then Zceil (r1 + r2) = (Zceil r1 + Zceil r2 - 1)%Z
  else Zceil (r1 + r2) = (Zceil r1 + Zceil r2)%Z.

Lemma ZfloorB_cond r1 r2 :
  if Rle_dec (IZR (Zfloor r1) - IZR (Zceil r2) + 1) (r1 - r2)
  then Zfloor (r1 - r2) = (Zfloor r1 - Zceil r2 + 1)%Z
  else Zfloor (r1 - r2) = (Zfloor r1 - Zceil r2)%Z.

Lemma ZceilB_cond r1 r2 :
  if Rle_dec (r1 - r2) (IZR (Zceil r1) - IZR (Zfloor r2) - 1)
  then Zceil (r1 - r2) = (Zceil r1 - Zfloor r2 - 1)%Z
  else Zceil (r1 - r2) = (Zceil r1 - Zfloor r2)%Z.