Qround.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import QArith.

Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p.forall p q : Q, p < q -> - q < - p
Proof.forall p q : Q, p < q -> - q < - p
intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl.a1:Z
a2:positive
b1:Z
b2:positive
(a1 * Z.pos b2 < b1 * Z.pos a2)%Z ->
(- b1 * Z.pos a2 < - a1 * Z.pos b2)%Z
rewrite !Z.mul_opp_l; omega.
Qed.

Hint Resolve Qopp_lt_compat : qarith.

(************)

Coercion inject_Z : Z >-> Q.

Definition Qfloor (x:Q) := let (n,d) := x in Z.div n (Zpos d).
Definition Qceiling (x:Q) := (-(Qfloor (-x)))%Z.

Lemma Qfloor_Z : forall z:Z, Qfloor z = z.forall z : Z, Qfloor z = z
Proof.forall z : Z, Qfloor z = z
intros z.z:Z
Qfloor z = z
simpl.z:Z
(z / 1)%Z = z
auto with *.
Qed.

Lemma Qceiling_Z : forall z:Z, Qceiling z = z.forall z : Z, Qceiling z = z
Proof.forall z : Z, Qceiling z = z
intros z.z:Z
Qceiling z = z
unfold Qceiling.z:Z
(- Qfloor (- z))%Z = z
simpl.z:Z
(- (- z / 1))%Z = z
rewrite Zdiv_1_r.z:Z
(- - z)%Z = z
auto with *.
Qed.

Lemma Qfloor_le : forall x, Qfloor x <= x.forall x : Q, Qfloor x <= x
Proof.forall x : Q, Qfloor x <= x
intros [n d].n:Z
d:positive
Qfloor (n # d) <= n # d
simpl.n:Z
d:positive
(n / Z.pos d)%Z <= n # d
unfold Qle.n:Z
d:positive
(Qnum (n / Z.pos d)%Z * QDen (n # d) <=
 Qnum (n # d) * QDen (n / Z.pos d)%Z)%Z
simpl.n:Z
d:positive
(n / Z.pos d * Z.pos d <= n * 1)%Z
replace (n*1)%Z with n by ring.n:Z
d:positive
(n / Z.pos d * Z.pos d <= n)%Z
rewrite Z.mul_comm.n:Z
d:positive
(Z.pos d * (n / Z.pos d) <= n)%Z
apply Z_mult_div_ge.n:Z
d:positive
(Z.pos d > 0)%Z
auto with *.
Qed.

Hint Resolve Qfloor_le : qarith.

Lemma Qle_ceiling : forall x, x <= Qceiling x.forall x : Q, x <= Qceiling x
Proof.forall x : Q, x <= Qceiling x
intros x.x:Q
x <= Qceiling x
apply Qle_trans with (- - x).x:Q
x <= - - x
x:Q
- - x <= Qceiling x
 rewrite Qopp_involutive.x:Q
x <= x
x:Q
- - x <= Qceiling x
 auto with *.x:Q
- - x <= Qceiling x
change (Qceiling x:Q) with (-(Qfloor(-x))).x:Q
- - x <= - Qfloor (- x)
auto with *.
Qed.

Hint Resolve Qle_ceiling : qarith.

Lemma Qle_floor_ceiling : forall x, Qfloor x <= Qceiling x.forall x : Q, Qfloor x <= Qceiling x
Proof.forall x : Q, Qfloor x <= Qceiling x
eauto with qarith.
Qed.

Lemma Qlt_floor : forall x, x < (Qfloor x+1)%Z.forall x : Q, x < (Qfloor x + 1)%Z
Proof.forall x : Q, x < (Qfloor x + 1)%Z
intros [n d].n:Z
d:positive
n # d < (Qfloor (n # d) + 1)%Z
simpl.n:Z
d:positive
n # d < (n / Z.pos d + 1)%Z
unfold Qlt.n:Z
d:positive
(Qnum (n # d) * QDen (n / Z.pos d + 1)%Z <
 Qnum (n / Z.pos d + 1)%Z * QDen (n # d))%Z
simpl.n:Z
d:positive
(n * 1 < (n / Z.pos d + 1) * Z.pos d)%Z
replace (n*1)%Z with n by ring.n:Z
d:positive
(n < (n / Z.pos d + 1) * Z.pos d)%Z
ring_simplify.n:Z
d:positive
(n < n / Z.pos d * Z.pos d + Z.pos d)%Z
replace (n / Zpos d * Zpos d + Zpos d)%Z with
  ((Zpos d * (n / Zpos d) + n mod Zpos  d) + Zpos  d - n mod Zpos d)%Z by ring.n:Z
d:positive
(n <
 Z.pos d * (n / Z.pos d) + n mod Z.pos d + Z.pos d -
 n mod Z.pos d)%Z
rewrite <- Z_div_mod_eq; auto with*.n:Z
d:positive
(n < n + Z.pos d - n mod Z.pos d)%Z
rewrite <- Z.lt_add_lt_sub_r.n:Z
d:positive
(n + n mod Z.pos d < n + Z.pos d)%Z
destruct (Z_mod_lt n (Zpos d)); auto with *.
Qed.

Hint Resolve Qlt_floor : qarith.

Lemma Qceiling_lt : forall x, (Qceiling x-1)%Z < x.forall x : Q, (Qceiling x - 1)%Z < x
Proof.forall x : Q, (Qceiling x - 1)%Z < x
intros x.x:Q
(Qceiling x - 1)%Z < x
unfold Qceiling.x:Q
(- Qfloor (- x) - 1)%Z < x
replace (- Qfloor (- x) - 1)%Z with (-(Qfloor (-x) + 1))%Z by ring.x:Q
(- (Qfloor (- x) + 1))%Z < x
change ((- (Qfloor (- x) + 1))%Z:Q) with (-(Qfloor (- x) + 1)%Z).x:Q
- (Qfloor (- x) + 1)%Z < x
apply Qlt_le_trans with (- - x); auto with *.x:Q
- - x <= x
rewrite Qopp_involutive.x:Q
x <= x
auto with *.
Qed.

Hint Resolve Qceiling_lt : qarith.

Lemma Qfloor_resp_le : forall x y, x <= y -> (Qfloor x <= Qfloor y)%Z.forall x y : Q, x <= y -> (Qfloor x <= Qfloor y)%Z
Proof.forall x y : Q, x <= y -> (Qfloor x <= Qfloor y)%Z
intros [xn xd] [yn yd] Hxy.xn:Z
xd:positive
yn:Z
yd:positive
Hxy:xn # xd <= yn # yd
(Qfloor (xn # xd) <= Qfloor (yn # yd))%Z
unfold Qle in *.xn:Z
xd:positive
yn:Z
yd:positive
Hxy:(Qnum (xn # xd) * QDen (yn # yd) <= Qnum (yn # yd) * QDen (xn # xd))%Z
(Qfloor (xn # xd) <= Qfloor (yn # yd))%Z
simpl in *.xn:Z
xd:positive
yn:Z
yd:positive
Hxy:(xn * Z.pos yd <= yn * Z.pos xd)%Z
(xn / Z.pos xd <= yn / Z.pos yd)%Z
rewrite <- (Zdiv_mult_cancel_r xn (Zpos xd) (Zpos yd)); auto with *.xn:Z
xd:positive
yn:Z
yd:positive
Hxy:(xn * Z.pos yd <= yn * Z.pos xd)%Z
(xn * Z.pos yd / (Z.pos xd * Z.pos yd) <=
 yn / Z.pos yd)%Z
rewrite <- (Zdiv_mult_cancel_r yn (Zpos yd) (Zpos xd)); auto with *.xn:Z
xd:positive
yn:Z
yd:positive
Hxy:(xn * Z.pos yd <= yn * Z.pos xd)%Z
(xn * Z.pos yd / (Z.pos xd * Z.pos yd) <=
 yn * Z.pos xd / (Z.pos yd * Z.pos xd))%Z
rewrite (Z.mul_comm (Zpos yd) (Zpos xd)).xn:Z
xd:positive
yn:Z
yd:positive
Hxy:(xn * Z.pos yd <= yn * Z.pos xd)%Z
(xn * Z.pos yd / (Z.pos xd * Z.pos yd) <=
 yn * Z.pos xd / (Z.pos xd * Z.pos yd))%Z
apply Z_div_le; auto with *.
Qed.

Hint Resolve Qfloor_resp_le : qarith.

Lemma Qceiling_resp_le : forall x y, x <= y -> (Qceiling x <= Qceiling y)%Z.forall x y : Q, x <= y -> (Qceiling x <= Qceiling y)%Z
Proof.forall x y : Q, x <= y -> (Qceiling x <= Qceiling y)%Z
intros x y Hxy.x, y:Q
Hxy:x <= y
(Qceiling x <= Qceiling y)%Z
unfold Qceiling.x, y:Q
Hxy:x <= y
(- Qfloor (- x) <= - Qfloor (- y))%Z
cut (Qfloor (-y) <= Qfloor (-x))%Z; auto with *.
Qed.

Hint Resolve Qceiling_resp_le : qarith.

Add Morphism Qfloor with signature Qeq ==> eq as Qfloor_comp.forall x y : Q, x == y -> Qfloor x = Qfloor y
Proof.forall x y : Q, x == y -> Qfloor x = Qfloor y
intros x y H.x, y:Q
H:x == y
Qfloor x = Qfloor y
apply Z.le_antisymm.x, y:Q
H:x == y
(Qfloor x <= Qfloor y)%Z
x, y:Q
H:x == y
(Qfloor y <= Qfloor x)%Z
 auto with *.x, y:Q
H:x == y
(Qfloor y <= Qfloor x)%Z
symmetry in H; auto with *.
Qed.

Add Morphism Qceiling with signature Qeq ==> eq as Qceiling_comp.forall x y : Q, x == y -> Qceiling x = Qceiling y
Proof.forall x y : Q, x == y -> Qceiling x = Qceiling y
intros x y H.x, y:Q
H:x == y
Qceiling x = Qceiling y
apply Z.le_antisymm.x, y:Q
H:x == y
(Qceiling x <= Qceiling y)%Z
x, y:Q
H:x == y
(Qceiling y <= Qceiling x)%Z
 auto with *.x, y:Q
H:x == y
(Qceiling y <= Qceiling x)%Z
symmetry in H; auto with *.
Qed.

Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (n / m).n, m:Z
(n / m)%Z = Qfloor (n / m)
Proof.n, m:Z
(n / m)%Z = Qfloor (n / m)
 unfold Qfloor.n, m:Z
(n / m)%Z = (let (n0, d) := n / m in (n0 / Z.pos d)%Z) intros.n, m:Z
(n / m)%Z = (let (n0, d) := n / m in (n0 / Z.pos d)%Z) simpl.n, m:Z
(n / m)%Z = (n * Qnum (/ m) / QDen (/ m))%Z
 destruct m as [ | | p]; simpl.n:Z
(n / 0)%Z = (n * 0 / 1)%Z
n:Z
p:positive
(n / Z.pos p)%Z = (n * 1 / Z.pos p)%Z
n:Z
p:positive
(n / Z.neg p)%Z = (n * -1 / Z.pos p)%Z
  now rewrite Zdiv_0_r, Z.mul_0_r.n:Z
p:positive
(n / Z.pos p)%Z = (n * 1 / Z.pos p)%Z
n:Z
p:positive
(n / Z.neg p)%Z = (n * -1 / Z.pos p)%Z
  now rewrite Z.mul_1_r.n:Z
p:positive
(n / Z.neg p)%Z = (n * -1 / Z.pos p)%Z
 rewrite <- Z.opp_eq_mul_m1.n:Z
p:positive
(n / Z.neg p)%Z = (- n / Z.pos p)%Z
 rewrite <- (Z.opp_involutive (Zpos p)).n:Z
p:positive
(n / Z.neg p)%Z = (- n / - - Z.pos p)%Z
 now rewrite Zdiv_opp_opp.
Qed.