Adding Qround.v (and helper lemmas and hints)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10282 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 139 insertions, 1 deletions

diff --git a/Makefile.common b/Makefile.common
index 19821e718..bf466da7a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -536,7 +536,7 @@ QARITHVO:=\
  theories/QArith/Qring.vo       theories/QArith/Qreals.vo \
  theories/QArith/QArith.vo	theories/QArith/Qcanon.vo \
  theories/QArith/Qfield.vo	theories/QArith/Qpower.vo \
- theories/QArith/Qabs.vo
+ theories/QArith/Qabs.vo        theories/QArith/Qround.vo
 
 LISTSVO:=\
  theories/Lists/MonoList.vo \
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index f46f6f021..75bd9c5e6 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -492,6 +492,8 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
+Hint Resolve Qle_trans : qarith.
+
 Lemma Qlt_not_eq : forall x y, x<y -> ~ x==y.
 Proof.
   unfold Qlt, Qeq; auto with zarith.
@@ -595,6 +597,8 @@ Proof.
   do 2 rewrite <- Zopp_mult_distr_l; omega.
 Qed.
 
+Hint Resolve Qopp_le_compat : qarith.
+
 Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.
 Proof.
   intros (x1,x2) (y1,y2); unfold Qle; simpl.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
new file mode 100644
index 000000000..c5b06af7f
--- /dev/null
+++ b/theories/QArith/Qround.v
@@ -0,0 +1,123 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import QArith.
+
+Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p.
+Proof.
+intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl.
+do 2 rewrite <- Zopp_mult_distr_l; omega.
+Qed.
+
+Hint Resolve Qopp_lt_compat : qarith.
+
+(************)
+
+Coercion Local inject_Z : Z >-> Q.
+
+Definition Qfloor (x:Q) := let (n,d) := x in Zdiv n (Zpos d).
+Definition Qceiling (x:Q) := (-(Qfloor (-x)))%Z.
+
+Lemma Qfloor_Z : forall z:Z, Qfloor z = z.
+Proof.
+intros z.
+simpl.
+auto with *.
+Qed.
+
+Lemma Qceiling_Z : forall z:Z, Qceiling z = z.
+Proof.
+intros z.
+unfold Qceiling.
+simpl.
+rewrite Z_div_1.
+auto with *.
+Qed.
+
+Lemma Qfloor_le : forall x, Qfloor x <= x.
+Proof.
+intros [n d].
+simpl.
+unfold Qle.
+simpl.
+replace (n*1)%Z with n by ring.
+rewrite Zmult_comm.
+apply Z_mult_div_ge.
+auto with *.
+Qed.
+
+Hint Resolve Qfloor_le : qarith.
+
+Lemma Qle_ceiling : forall x, x <= Qceiling x.
+Proof.
+intros x.
+apply Qle_trans with (- - x).
+ rewrite Qopp_involutive.
+ auto with *.
+change (Qceiling x:Q) with (-(Qfloor(-x))).
+auto with *.
+Qed.
+
+Hint Resolve Qle_ceiling : qarith.
+
+Lemma Qle_floor_ceiling : forall x, Qfloor x <= Qceiling x.
+Proof.
+eauto with qarith.
+Qed.
+
+Lemma Qlt_floor : forall x, x < (Qfloor x+1)%Z.
+Proof.
+intros [n d].
+simpl.
+unfold Qlt.
+simpl.
+replace (n*1)%Z with n by ring.
+ring_simplify.
+replace (n / ' d * ' d + ' d)%Z with
+  (('d * (n / 'd) + n mod 'd) + 'd - n mod 'd)%Z by ring.
+rewrite <- Z_div_mod_eq; auto with*.
+rewrite <- Zlt_plus_swap.
+destruct (Z_mod_lt n ('d)); auto with *.
+Qed.
+
+Hint Resolve Qlt_floor : qarith.
+
+Lemma Qceiling_lt : forall x, (Qceiling x-1)%Z < x.
+Proof.
+intros x.
+unfold Qceiling.
+replace (- Qfloor (- x) - 1)%Z with (-(Qfloor (-x) + 1))%Z by ring.
+change ((- (Qfloor (- x) + 1))%Z:Q) with (-(Qfloor (- x) + 1)%Z).
+apply Qlt_le_trans with (- - x); auto with *.
+rewrite Qopp_involutive.
+auto with *.
+Qed.
+
+Hint Resolve Qceiling_lt : qarith.
+
+Lemma Qfloor_resp_le : forall x y, x <= y -> (Qfloor x <= Qfloor y)%Z.
+Proof.
+intros [xn xd] [yn yd] Hxy.
+unfold Qle in *.
+simpl in *.
+rewrite <- (Zdiv_mult_cancel_r xn ('xd) ('yd)); auto with *.
+rewrite <- (Zdiv_mult_cancel_r yn ('yd) ('xd)); auto with *.
+rewrite (Zmult_comm ('yd) ('xd)).
+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.
+Proof.
+intros x y Hxy.
+unfold Qceiling.
+cut (Qfloor (-y) <= Qfloor (-x))%Z; auto with *.
+Qed.
+
+Hint Resolve Qceiling_resp_le : qarith.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 57b0fa15c..57c0af02f 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -480,6 +480,17 @@ Proof.
   ring.
 Qed.
 
+Lemma Z_div_1 : forall z:Z, (z/1 = z)%Z.
+Proof.
+intros z.
+set (z':=z).
+unfold z' at 1.
+replace z with (0 + z*1)%Z by ring.
+rewrite (Z_div_plus 0 z 1);[reflexivity|constructor].
+Qed.
+
+Hint Resolve Z_div_1 : zarith.
+
 Lemma Z_div_exact_1 : forall a b:Z, b > 0 -> a = b * (a / b) -> a mod b = 0.
   intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *.
   case (Zdiv_eucl a b); intros q r; omega.