diff options
Diffstat (limited to 'theories/QArith/Qabs.v')
| -rw-r--r-- | theories/QArith/Qabs.v | 59 |
1 files changed, 47 insertions, 12 deletions
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v index 747c2c3c..50aee530 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,7 +11,7 @@ Require Export Qreduction. Hint Resolve Qlt_le_weak : qarith. -Definition Qabs (x:Q) := let (n,d):=x in (Zabs n#d). +Definition Qabs (x:Q) := let (n,d):=x in (Z.abs n#d). Lemma Qabs_case : forall (x:Q) (P : Q -> Type), (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P (Qabs x). Proof. @@ -26,9 +26,9 @@ intros [xn xd] [yn yd] H. simpl. unfold Qeq in *. simpl in *. -change (' yd)%Z with (Zabs (' yd)). -change (' xd)%Z with (Zabs (' xd)). -repeat rewrite <- Zabs_Zmult. +change (' yd)%Z with (Z.abs (' yd)). +change (' xd)%Z with (Z.abs (' xd)). +repeat rewrite <- Z.abs_mul. congruence. Qed. @@ -61,7 +61,7 @@ auto. apply (Qopp_le_compat x 0). Qed. -Lemma Zabs_Qabs : forall n d, (Zabs n#d)==Qabs (n#d). +Lemma Zabs_Qabs : forall n d, (Z.abs n#d)==Qabs (n#d). Proof. intros [|n|n]; reflexivity. Qed. @@ -85,21 +85,28 @@ intros [xn xd] [yn yd]. unfold Qplus. unfold Qle. simpl. -apply Zmult_le_compat_r;auto with *. -change (' yd)%Z with (Zabs (' yd)). -change (' xd)%Z with (Zabs (' xd)). -repeat rewrite <- Zabs_Zmult. -apply Zabs_triangle. +apply Z.mul_le_mono_nonneg_r;auto with *. +change (' yd)%Z with (Z.abs (' yd)). +change (' xd)%Z with (Z.abs (' xd)). +repeat rewrite <- Z.abs_mul. +apply Z.abs_triangle. Qed. Lemma Qabs_Qmult : forall a b, Qabs (a*b) == (Qabs a)*(Qabs b). Proof. intros [an ad] [bn bd]. simpl. -rewrite Zabs_Zmult. +rewrite Z.abs_mul. reflexivity. Qed. +Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x). +Proof. + unfold Qminus, Qopp. simpl. + rewrite Pos.mul_comm, <- Z.abs_opp. + do 2 f_equal. ring. +Qed. + Lemma Qle_Qabs : forall a, a <= Qabs a. Proof. intros a. @@ -122,3 +129,31 @@ apply Qabs_triangle. apply Qabs_wd. ring. Qed. + +Lemma Qabs_Qle_condition x y: Qabs x <= y <-> -y <= x <= y. +Proof. + split. + split. + rewrite <- (Qopp_opp x). + apply Qopp_le_compat. + apply Qle_trans with (Qabs (-x)). + apply Qle_Qabs. + now rewrite Qabs_opp. + apply Qle_trans with (Qabs x); auto using Qle_Qabs. + intros (H,H'). + apply Qabs_case; trivial. + intros. rewrite <- (Qopp_opp y). now apply Qopp_le_compat. +Qed. + +Lemma Qabs_diff_Qle_condition x y r: Qabs (x - y) <= r <-> x - r <= y <= x + r. +Proof. + intros. unfold Qminus. + rewrite Qabs_Qle_condition. + rewrite <- (Qplus_le_l (-r) (x+-y) (y+r)). + rewrite <- (Qplus_le_l (x+-y) r (y-r)). + setoid_replace (-r + (y + r)) with y by ring. + setoid_replace (r + (y - r)) with y by ring. + setoid_replace (x + - y + (y + r)) with (x + r) by ring. + setoid_replace (x + - y + (y - r)) with (x - r) by ring. + intuition. +Qed. |