1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
11
Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p.
13
intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl.
14
do 2 rewrite <- Zopp_mult_distr_l; omega.
17
Hint Resolve Qopp_lt_compat : qarith.
21
Coercion Local inject_Z : Z >-> Q.
23
Definition Qfloor (x:Q) := let (n,d) := x in Zdiv n (Zpos d).
24
Definition Qceiling (x:Q) := (-(Qfloor (-x)))%Z.
26
Lemma Qfloor_Z : forall z:Z, Qfloor z = z.
33
Lemma Qceiling_Z : forall z:Z, Qceiling z = z.
42
Lemma Qfloor_le : forall x, Qfloor x <= x.
48
replace (n*1)%Z with n by ring.
54
Hint Resolve Qfloor_le : qarith.
56
Lemma Qle_ceiling : forall x, x <= Qceiling x.
59
apply Qle_trans with (- - x).
60
rewrite Qopp_involutive.
62
change (Qceiling x:Q) with (-(Qfloor(-x))).
66
Hint Resolve Qle_ceiling : qarith.
68
Lemma Qle_floor_ceiling : forall x, Qfloor x <= Qceiling x.
73
Lemma Qlt_floor : forall x, x < (Qfloor x+1)%Z.
79
replace (n*1)%Z with n by ring.
81
replace (n / ' d * ' d + ' d)%Z with
82
(('d * (n / 'd) + n mod 'd) + 'd - n mod 'd)%Z by ring.
83
rewrite <- Z_div_mod_eq; auto with*.
84
rewrite <- Zlt_plus_swap.
85
destruct (Z_mod_lt n ('d)); auto with *.
88
Hint Resolve Qlt_floor : qarith.
90
Lemma Qceiling_lt : forall x, (Qceiling x-1)%Z < x.
94
replace (- Qfloor (- x) - 1)%Z with (-(Qfloor (-x) + 1))%Z by ring.
95
change ((- (Qfloor (- x) + 1))%Z:Q) with (-(Qfloor (- x) + 1)%Z).
96
apply Qlt_le_trans with (- - x); auto with *.
97
rewrite Qopp_involutive.
101
Hint Resolve Qceiling_lt : qarith.
103
Lemma Qfloor_resp_le : forall x y, x <= y -> (Qfloor x <= Qfloor y)%Z.
105
intros [xn xd] [yn yd] Hxy.
108
rewrite <- (Zdiv_mult_cancel_r xn ('xd) ('yd)); auto with *.
109
rewrite <- (Zdiv_mult_cancel_r yn ('yd) ('xd)); auto with *.
110
rewrite (Zmult_comm ('yd) ('xd)).
111
apply Z_div_le; auto with *.
114
Hint Resolve Qfloor_resp_le : qarith.
116
Lemma Qceiling_resp_le : forall x y, x <= y -> (Qceiling x <= Qceiling y)%Z.
120
cut (Qfloor (-y) <= Qfloor (-x))%Z; auto with *.
123
Hint Resolve Qceiling_resp_le : qarith.
125
Add Morphism Qfloor with signature Qeq ==> @eq _ as Qfloor_comp.
130
symmetry in H; auto with *.
133
Add Morphism Qceiling with signature Qeq ==> @eq _ as Qceiling_comp.
138
symmetry in H; auto with *.
b'\\ No newline at end of file'