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.

    intro.
    rewrite fl_cg_in_Z; auto with zarith.
    intro.
    rewrite fl_cg_not_in_Z; auto with zarith.
Qed.
*)

    intro.
    rewrite fl_minus_in_Z; auto with zarith.
    intro.
    rewrite fl_minus_not_in_Z; auto with zarith.
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.

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