# Library floor

Require Import misc.
Require Import Q_misc.
Require Import QArith.
Require Import ZArith.
Require Import Qround.

Definition Z_of_positive (x:positive) := Zpos x.

Definition fl (x:Q) : Z := Qfloor x.

Lemma fl_def:
forall x: Q,
fl x <= x /\ x < fl x + 1.
Proof.
intros.
split.
apply Qfloor_le.
assert (H_aux: fl x + 1 == (fl x + 1)%Z).
unfold Qeq, Qplus, Q_of_nat; simpl; ring_simplify; auto.
rewrite H_aux; clear H_aux.
apply Qlt_floor.
Qed.

Lemma fl_integerp:
forall x: Q, fl x == x <-> in_Z x.
Proof.
intros.
split.
intros.
unfold in_Z.
exists (fl x).
auto with qarith.
intros H_in_Z.
elim H_in_Z.
intros x' H_x.
rewrite H_x.
rewrite Qfloor_Z.
auto with qarith.
Qed.

Axiom fl_minus_in_Z:
forall x: Q,
forall H_in_Z: in_Z x,
fl (- x) = (- (fl x))%Z.

Axiom fl_minus_not_in_Z:
forall x: Q,
forall H_not_in_Z: ~ in_Z x,
fl (- x) = (- (fl x) - 1)%Z.

Axiom fl_m_n:
forall x: Q,
( fl (-x) = - fl ((x - (1#Qden(x)))%Q) - 1)%Z.

Lemma fl_monotone_linear:
forall x y : Q,
x <= y -> (fl x <= fl y)%Z.
Proof.
intros.
apply Qfloor_resp_le.
assumption.
Qed.

Axiom n_le_fl_linear:
forall x: Q,
forall n: Z,
n <= x -> (n <= fl x)%Z.

Axiom fl_plus_int_rewrite:
forall x: Q,
forall n: Z,
(fl (x + n) = fl x + n)%Z.

Axiom fl_div_int_rewrite:
forall x: Q,
forall n: Z,
forall H_n_pos: (n > 0)%Z,
(fl (fl x / n) == fl (x / n))%Z.

Definition cg (x: Q) : Z := Qceiling x.

Lemma cg_def:
forall x: Q,
(cg x = - fl (- x))%Z.
Proof.
intros.
unfold fl, cg.
unfold Qceiling, Qfloor.
reflexivity.
Qed.

Lemma cg_def_linear:
forall x: Q,
(cg x - 1%Z)%Z < x /\ x <= cg x.
Proof.
intros; split; auto with qarith.
Qed.

Lemma cg_integerp:
forall x: Q, cg x == x <-> in_Z x.
Proof.
intros.
split.
intros.
unfold in_Z.
exists (cg x).
auto with qarith.
intros H_in_Z.
elim H_in_Z.
intros x' H_x.
rewrite H_x.
unfold cg.
rewrite Qceiling_Z.
auto with qarith.
Qed.

Property cg_monotone_linear:
forall x y : Q,
x <= y -> (cg x <= cg y)%Z.
Proof.
intros.
unfold cg, Qceiling.
apply Zle_left_rev.
rewrite Zopp_involutive.
rewrite Zplus_comm.
apply Zle_left.
apply Qfloor_resp_le.
auto with qarith.
Qed.

Axiom n_ge_cg_linear:
forall x: Q,
forall n: Z,
n >= x -> (n >= cg x)%Z.

Axiom cg_plus_int_rewrite:
forall x: Q,
forall n: Z,
(cg (x + n) = cg x + n)%Z.

Axiom cg_div_int_rewrite:
forall x: Q,
forall n: Z,
forall H_n_pos: (n > 0)%Z,
(cg (cg x / n) = cg (x / n))%Z.

Lemma fl_cg_in_Z:
forall x: Q,
forall H_in_Z: in_Z x,
(cg x = fl x)%Z.
Proof.
intros.
unfold cg, Qceiling.
fold (fl ( -x)).
rewrite (fl_minus_in_Z x).
ring.
assumption.
Qed.

Lemma fl_cg_not_in_Z:
forall x: Q,
forall H_not_in_Z: ~ in_Z x,
(cg x = fl x + 1%Z)%Z.
Proof.
intros.
unfold cg, Qceiling.
fold (fl ( -x)).
rewrite (fl_minus_not_in_Z x).
ring.
assumption.
Qed.

Axiom fl_rewrite:
forall x y: Q,
x == y -> fl x = fl y.

Lemma cg_rewrite:
forall x y: Q,
x == y -> cg x = cg y.
Proof.
intros.
unfold cg, Qceiling.
fold (fl (- x)).
fold (fl (- y)).
assert (H_cc: (fl (- x))%Z = (fl (- y))%Z).
apply fl_rewrite.
apply Qopp_comp.
assumption.
auto with zarith.
Qed.

Lemma fl_le_cg:
forall x: Q,
(fl x <= cg x)%Z.
Proof.
intro x.
apply Qle_impl_Zle.
apply
(Qle_trans
(fl x)
x
(cg x)).
elim (fl_def x); auto.
elim (cg_def_linear x); auto.
Qed.

Lemma x_lt_y_impl_fl_x_lt_cg_y:
forall x y: Q,
forall H_x_lt_y: x < y,
(fl x < cg y)%Z.
Proof.
intros.
apply Qlt_impl_Zlt.
apply
(Qle_lt_trans
(fl x)
x
(cg y));
try solve [ elim (fl_def x); auto ].
apply (Qlt_le_trans x y (cg y)); auto.
elim (cg_def_linear y); auto.
Qed.

Lemma fl_eq_cg:
forall x: Q,
(fl x = cg (x - (1 - (1#(Qden x)))))%Z.
Proof.
intros.
Qed.

Lemma fl_minus_cg_le_fl:
forall x y: Q,
(fl x - cg y <= fl (x - y))%Z.
Proof.
intros.