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_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.