Library comparison
Require Import ZArith.
Require Import QArith.
Require Import misc.
Require Import Q_misc.
Require Import floor.
Coercion Local Z_of_nat : nat >-> Z.
Property Zlt_impl_Zle:
forall x y: Z,
(x < y + 1%nat)%Z -> (x <= y)%Z.
Proof.
intros.
apply Zle_left_rev.
replace (y + - x)%Z with ((y + 1) + -1 + - x)%Z; try omega.
apply Zlt_left.
auto.
Qed.
Property Zle_impl_Zlt:
forall x y: Z,
(x <= y)%Z -> (x < y + 1)%Z.
Proof.
intros.
apply (Zle_lt_trans x y (y + 1)%Z); auto with zarith.
Qed.
Property Zgt_impl_Zge:
forall (x: nat) (y: Z),
(x+1%nat > y )%Z -> (x >= y)%Z.
Proof.
intros x y H_cmp.
apply Zle_ge.
apply Zgt_lt in H_cmp.
apply Zlt_impl_Zle.
assumption.
Qed.
Property Qle_impl_Qlt:
forall x y epsilon : Q,
forall H_epsilon: epsilon > 0,
x <= y -> x < y + epsilon.
Proof.
intros x y epsilon H_epsilon H_le.
apply (Qle_lt_trans x (y + 0) (y + epsilon)); try solve [ring_simplify; auto].
apply Qplus_lt_compat_l.
assumption.
Qed.
Property Qlt_impl_Qle_aux:
forall x: Z,
forall y: Q,
forall epsilon: Q,
forall H_epsilon: epsilon = 1 # Qden y,
x < y -> x <= y - epsilon.
Proof.
intros x y epsilon H_epsilon H_lt.
apply (Qle_trans
x
(fl (y - epsilon))
(y - epsilon));
try solve [ elim (fl_def (y - epsilon)); auto].
apply Zle_impl_Qle.
apply Zlt_impl_Zle.
rewrite <- Zopp_involutive.
assert (H_aux:
(- - (fl (y - epsilon) + 1%nat))%Z = (- (- fl (y - epsilon) - 1))%Z).
ring.
rewrite H_aux; clear H_aux.
rewrite H_epsilon.
rewrite <- fl_m_n.
fold (cg y).
apply Qlt_impl_Zlt.
apply (Qlt_le_trans x y (cg y)); auto.
elim (cg_def_linear y); auto.
Qed.
Property Qlt_impl_Qle:
forall x: Z,
forall y: Q,
forall epsilon: Q,
forall H_epsilon: epsilon <= 1 # Qden y,
x < y -> x <= y - epsilon.
Proof.
intros x y epsilon H_epsilon H_lt.
apply (Qle_trans
x
(y - (1 # Qden y))
(y - epsilon)).
apply Qlt_impl_Qle_aux; auto.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
apply Qopp_le_compat.
assumption.
Qed.
Property Qlt_impl_Qle_red:
forall x: Z,
forall y: Q,
forall epsilon: Q,
forall H_epsilon: epsilon <= 1 # Qden (Qred y),
x < y -> x <= Qred y - epsilon.
Proof.
intros x y epsilon H_epsilon H_lt.
apply Qlt_impl_Qle; auto.
rewrite Qred_correct.
assumption.
Qed.