Add small utility lemmas about nat/P/Z/Q arithmetic.

 Initial patch by Eelis van der Weegen, minor adaptations by myself

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

3 files changed, 206 insertions, 1 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index b07d3d512..fe37fccb8 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -46,6 +46,13 @@ Notation "x > y" := (Qlt y x)(only parsing) : Q_scope.
 Notation "x >= y" := (Qle y x)(only parsing) : Q_scope.
 Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope.
 
+(** injection from Z is injective. *)
+
+Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b.
+Proof.
+ unfold Qeq. simpl. omega.
+Qed.
+
 (** Another approach : using Qcompare for defining order relations. *)
 
 Definition Qcompare (p q : Q) := (Qnum p * QDen q ?= Qnum q * QDen p)%Z.
@@ -385,6 +392,26 @@ Proof.
   red; simpl; intro; ring.
 Qed.
 
+(** Injectivity of addition (uses theory about Qopp above): *)
+
+Lemma Qplus_inj_r (x y z: Q):
+  x + z == y + z <-> x == y.
+Proof.
+ split; intro E.
+  rewrite <- (Qplus_0_r x), <- (Qplus_0_r y).
+  rewrite <- (Qplus_opp_r z); auto.
+  do 2 rewrite Qplus_assoc.
+  rewrite E. reflexivity.
+ rewrite E. reflexivity.
+Qed.
+
+Lemma Qplus_inj_l (x y z: Q):
+  z + x == z + y <-> x == y.
+Proof.
+ rewrite (Qplus_comm z x), (Qplus_comm z y).
+ apply Qplus_inj_r.
+Qed.
+
 
 (** * Properties of [Qmult] *)
 
@@ -460,6 +487,21 @@ Proof.
   rewrite <- H0; ring.
 Qed.
 
+
+(** * inject_Z is a ring homomorphism: *)
+
+Lemma inject_Z_plus (x y: Z): inject_Z (x + y) = inject_Z x + inject_Z y.
+Proof.
+ unfold Qplus, inject_Z. simpl. f_equal. ring.
+Qed.
+
+Lemma inject_Z_mult (x y: Z): inject_Z (x * y) = inject_Z x * inject_Z y.
+Proof. reflexivity. Qed.
+
+Lemma inject_Z_opp (x: Z): inject_Z (- x) = - inject_Z x.
+Proof. reflexivity. Qed.
+
+
 (** * Inverse and division. *)
 
 Lemma Qinv_involutive : forall q, (/ / q) == q.
@@ -498,6 +540,25 @@ Proof.
   apply Qdiv_mult_l; auto.
 Qed.
 
+(** Injectivity of Qmult (requires theory about Qinv above): *)
+
+Lemma Qmult_inj_r (x y z: Q): ~ z == 0 -> (x * z == y * z <-> x == y).
+Proof.
+ intro z_ne_0.
+ split; intro E.
+  rewrite <- (Qmult_1_r x), <- (Qmult_1_r y).
+  rewrite <- (Qmult_inv_r z); auto.
+  do 2 rewrite Qmult_assoc.
+  rewrite E. reflexivity.
+ rewrite E. reflexivity.
+Qed.
+
+Lemma Qmult_inj_l (x y z: Q): ~ z == 0 -> (z * x == z * y <-> x == y).
+Proof.
+ rewrite (Qmult_comm z x), (Qmult_comm z y).
+ apply Qmult_inj_r.
+Qed.
+
 (** * Properties of order upon Q. *)
 
 Lemma Qle_refl : forall x, x<=x.
@@ -537,6 +598,19 @@ Proof.
   unfold Qlt, Qeq; auto with zarith.
 Qed.
 
+Lemma Zle_Qle (x y: Z): (x <= y)%Z = (inject_Z x <= inject_Z y).
+Proof.
+ unfold Qle. intros. simpl.
+ do 2 rewrite Zmult_1_r. reflexivity.
+Qed.
+
+Lemma Zlt_Qlt (x y: Z): (x < y)%Z = (inject_Z x < inject_Z y).
+Proof.
+ unfold Qlt. intros. simpl.
+ do 2 rewrite Zmult_1_r. reflexivity.
+Qed.
+
+
 (** Large = strict or equal *)
 
 Lemma Qle_lteq : forall x y, x<=y <-> x<y \/ x==y.
@@ -675,6 +749,54 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
+Lemma Qplus_lt_le_compat :
+  forall x y z t, x<y -> z<=t -> x+z < y+t.
+Proof.
+  unfold Qplus, Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2) (t1, t2);
+    simpl; simpl_mult.
+  Open Scope Z_scope.
+  intros.
+  match goal with |- ?a < ?b => ring_simplify a b end.
+  rewrite Zplus_comm.
+  apply Zplus_le_lt_compat.
+  match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end.
+  auto with zarith.
+  match goal with |- ?a < ?b => ring_simplify x1 y1 ('x2) ('y2) a b end.
+  assert (forall p, 0 < ' p) by reflexivity.
+  repeat (apply Zmult_lt_compat_r; auto).
+  Close Scope Z_scope.
+Qed.
+
+Lemma Qplus_le_l (x y z: Q): x + z <= y + z <-> x <= y.
+Proof.
+ split; intros.
+  rewrite <- (Qplus_0_r x), <- (Qplus_0_r y), <- (Qplus_opp_r z).
+  do 2 rewrite Qplus_assoc.
+  apply Qplus_le_compat; auto with *.
+ apply Qplus_le_compat; auto with *.
+Qed.
+
+Lemma Qplus_le_r (x y z: Q): z + x <= z + y <-> x <= y.
+Proof.
+ rewrite (Qplus_comm z x), (Qplus_comm z y).
+ apply Qplus_le_l.
+Qed.
+
+Lemma Qplus_lt_l (x y z: Q): x + z < y + z <-> x < y.
+Proof.
+ split; intros.
+  rewrite <- (Qplus_0_r x), <- (Qplus_0_r y), <- (Qplus_opp_r z).
+  do 2 rewrite Qplus_assoc.
+  apply Qplus_lt_le_compat; auto with *.
+ apply Qplus_lt_le_compat; auto with *.
+Qed.
+
+Lemma Qplus_lt_r (x y z: Q): z + x < z + y <-> x < y.
+Proof.
+ rewrite (Qplus_comm z x), (Qplus_comm z y).
+ apply Qplus_lt_l.
+Qed.
+
 Lemma Qmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z.
 Proof.
   intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
@@ -697,6 +819,19 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
+Lemma Qmult_le_r (x y z: Q): 0 < z -> (x*z <= y*z <-> x <= y).
+Proof.
+ split; intro.
+  now apply Qmult_lt_0_le_reg_r with z.
+ apply Qmult_le_compat_r; auto with qarith.
+Qed.
+
+Lemma Qmult_le_l (x y z: Q): 0 < z -> (z*x <= z*y <-> x <= y).
+Proof.
+ rewrite (Qmult_comm z x), (Qmult_comm z y).
+ apply Qmult_le_r.
+Qed.
+
 Lemma Qmult_lt_compat_r : forall x y z, 0 < z  -> x < y -> x*z < y*z.
 Proof.
   intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl.
@@ -711,6 +846,30 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
+Lemma Qmult_lt_r: forall x y z, 0 < z -> (x*z < y*z <-> x < y).
+Proof.
+ Open Scope Z_scope.
+ intros (a1,a2) (b1,b2) (c1,c2).
+ unfold Qle, Qlt; simpl.
+ simpl_mult.
+ replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.
+ replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.
+ assert (forall p, 0 < ' p) by reflexivity.
+ split; intros.
+  apply Zmult_lt_reg_r with (c1*'c2); auto with zarith.
+  apply Zmult_lt_0_compat; auto with zarith.
+ apply Zmult_lt_compat_r; auto with zarith.
+ apply Zmult_lt_0_compat. omega.
+ compute; auto.
+ Close Scope Z_scope.
+Qed.
+
+Lemma Qmult_lt_l (x y z: Q): 0 < z -> (z*x < z*y <-> x < y).
+Proof.
+ rewrite (Qmult_comm z x), (Qmult_comm z y).
+ apply Qmult_lt_r.
+Qed.
+
 Lemma Qmult_le_0_compat : forall a b, 0 <= a -> 0 <= b -> 0 <= a*b.
 Proof.
 intros a b Ha Hb.
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index 53528ec74..557fabc89 100644
--- a/theories/QArith/Qabs.v
+++ b/theories/QArith/Qabs.v
@@ -100,6 +100,13 @@ rewrite Zabs_Zmult.
 reflexivity.
 Qed.
 
+Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x).
+Proof.
+ unfold Qminus, Qopp. simpl.
+ rewrite Pmult_comm, <- Zabs_Zopp.
+ 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.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 58a7967ed..ce363a33b 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -136,4 +136,15 @@ intros x y H.
 apply Zle_antisym.
  auto with *.
 symmetry in H; auto with *.
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (n / m).
+Proof.
+ unfold Qfloor. intros. simpl.
+ destruct m as [?|?|p]; simpl.
+  now rewrite Zdiv_0_r, Zmult_0_r.
+  now rewrite Zmult_1_r.
+ rewrite <- Zopp_eq_mult_neg_1.
+ rewrite <- (Zopp_involutive (Zpos p)).
+ now rewrite Zdiv_opp_opp.
+Qed.