diff options
-rw-r--r-- | Makefile.common | 2 | ||||
-rw-r--r-- | theories/QArith/QArith_base.v | 4 | ||||
-rw-r--r-- | theories/QArith/Qround.v | 123 | ||||
-rw-r--r-- | theories/ZArith/Zdiv.v | 11 |
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. |