summaryrefslogtreecommitdiff
path: root/theories/QArith
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /theories/QArith
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'theories/QArith')
-rw-r--r--theories/QArith/QArith.v4
-rw-r--r--theories/QArith/QArith_base.v169
-rw-r--r--theories/QArith/QOrderedType.v2
-rw-r--r--theories/QArith/Qabs.v37
-rw-r--r--theories/QArith/Qcanon.v16
-rw-r--r--theories/QArith/Qfield.v4
-rw-r--r--theories/QArith/Qminmax.v4
-rw-r--r--theories/QArith/Qpower.v6
-rw-r--r--theories/QArith/Qreals.v6
-rw-r--r--theories/QArith/Qreduction.v52
-rw-r--r--theories/QArith/Qring.v4
-rw-r--r--theories/QArith/Qround.v15
12 files changed, 249 insertions, 70 deletions
diff --git a/theories/QArith/QArith.v b/theories/QArith/QArith.v
index 2255cd41..fe8d639c 100644
--- a/theories/QArith/QArith.v
+++ b/theories/QArith/QArith.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* 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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: QArith.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export QArith_base.
Require Export Qring.
Require Export Qreduction.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 18b8823d..94ea4906 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* 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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: QArith_base.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export ZArith.
Require Export ZArithRing.
Require Export Morphisms Setoid Bool.
@@ -20,7 +18,7 @@ Record Q : Set := Qmake {Qnum : Z; Qden : positive}.
Delimit Scope Q_scope with Q.
Bind Scope Q_scope with Q.
-Arguments Scope Qmake [Z_scope positive_scope].
+Arguments Qmake _%Z _%positive.
Open Scope Q_scope.
Ltac simpl_mult := repeat rewrite Zpos_mult_morphism.
@@ -29,7 +27,7 @@ Ltac simpl_mult := repeat rewrite Zpos_mult_morphism.
Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope.
Definition inject_Z (x : Z) := Qmake x 1.
-Arguments Scope inject_Z [Z_scope].
+Arguments inject_Z x%Z.
Notation QDen p := (Zpos (Qden p)).
Notation " 0 " := (0#1) : Q_scope.
@@ -48,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.
@@ -92,7 +97,7 @@ Proof.
unfold "?=". intros. apply Zcompare_antisym.
Qed.
-Lemma Qcompare_spec : forall x y, CompSpec Qeq Qlt x y (x ?= y).
+Lemma Qcompare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (x ?= y).
Proof.
intros.
destruct (x ?= y) as [ ]_eqn:H; constructor; auto.
@@ -387,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] *)
@@ -462,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.
@@ -500,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.
@@ -539,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.
@@ -677,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.
@@ -699,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.
@@ -713,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/QOrderedType.v b/theories/QArith/QOrderedType.v
index be894419..238de6fa 100644
--- a/theories/QArith/QOrderedType.v
+++ b/theories/QArith/QOrderedType.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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index 747c2c3c..557fabc8 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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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/Qcanon.v b/theories/QArith/Qcanon.v
index 71a3b474..fea2ba39 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* 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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Qcanon.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Field.
Require Import QArith.
Require Import Znumtheory.
@@ -20,7 +18,7 @@ Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }.
Delimit Scope Qc_scope with Qc.
Bind Scope Qc_scope with Qc.
-Arguments Scope Qcmake [Q_scope].
+Arguments Qcmake this%Q _.
Open Scope Qc_scope.
Lemma Qred_identity :
@@ -71,7 +69,7 @@ Proof.
Qed.
Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q).
-Arguments Scope Q2Qc [Q_scope].
+Arguments Q2Qc q%Q.
Notation " !! " := Q2Qc : Qc_scope.
Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'.
@@ -468,18 +466,16 @@ Proof.
destruct n; simpl.
destruct 1; auto.
intros.
- apply Qc_is_canon.
- simpl.
- compute; auto.
+ now apply Qc_is_canon.
Qed.
Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n.
Proof.
induction n; simpl; auto with qarith.
- intros; compute; intro; discriminate.
+ easy.
intros.
apply Qcle_trans with (0*(p^n)).
- compute; intro; discriminate.
+ easy.
apply Qcmult_le_compat_r; auto.
Qed.
diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
index 81d59714..5e27f381 100644
--- a/theories/QArith/Qfield.v
+++ b/theories/QArith/Qfield.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* 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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Qfield.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Field.
Require Export QArith_base.
Require Import NArithRing.
diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v
index a458fc6e..2da24ee6 100644
--- a/theories/QArith/Qminmax.v
+++ b/theories/QArith/Qminmax.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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -64,4 +64,4 @@ Proof.
apply plus_min_distr_l.
Qed.
-End Q. \ No newline at end of file
+End Q.
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index 9568c796..b05ee649 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -136,9 +136,9 @@ Proof.
intros a [|n|n] [|m|m] H; simpl; try ring;
try rewrite Qpower_plus_positive;
try apply Qinv_mult_distr; try reflexivity;
-case_eq ((n ?= m)%positive Eq); intros H0; simpl;
+rewrite ?Z.pos_sub_spec;
+case Pos.compare_spec; intros H0; simpl; subst;
try rewrite Qpower_minus_positive;
- try rewrite (Pcompare_Eq_eq _ _ H0);
try (field; try split; apply Qpower_not_0_positive);
try assumption;
apply ZC2;
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 8a0ebcff..24f6d720 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* 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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Qreals.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Rbase.
Require Export QArith_base.
@@ -210,4 +208,4 @@ intro; apply H; apply eqR_Qeq.
rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real.
Qed.
-End LegacyQField. \ No newline at end of file
+End LegacyQField.
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index eb8c1164..e39eca0c 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* 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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Qreduction.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(** Normalisation functions for rational numbers. *)
Require Export QArith_base.
@@ -43,23 +41,16 @@ Definition Qred (q:Q) :=
Lemma Qred_correct : forall q, (Qred q) == q.
Proof.
unfold Qred, Qeq; intros (n,d); simpl.
- generalize (Zggcd_gcd n ('d)) (Zgcd_is_pos n ('d))
- (Zgcd_is_gcd n ('d)) (Zggcd_correct_divisors n ('d)).
+ generalize (Zggcd_gcd n ('d)) (Zgcd_nonneg n ('d))
+ (Zggcd_correct_divisors n ('d)).
destruct (Zggcd n (Zpos d)) as (g,(nn,dd)); simpl.
Open Scope Z_scope.
- intuition.
- rewrite <- H in H0,H1; clear H.
- rewrite H3; rewrite H4.
- assert (0 <> g).
- intro; subst g; discriminate.
-
- assert (0 < dd).
- apply Zmult_gt_0_lt_0_reg_r with g.
- omega.
- rewrite Zmult_comm.
- rewrite <- H4; compute; auto.
- rewrite Z2P_correct; auto.
- ring.
+ intros Hg LE (Hn,Hd). rewrite Hd, Hn.
+ rewrite <- Hg in LE; clear Hg.
+ assert (0 <> g) by (intro; subst; discriminate).
+ rewrite Z2P_correct. ring.
+ apply Zmult_gt_0_lt_0_reg_r with g; auto with zarith.
+ now rewrite Zmult_comm, <- Hd.
Close Scope Z_scope.
Qed.
@@ -69,10 +60,10 @@ Proof.
unfold Qred, Qeq in *; simpl in *.
Open Scope Z_scope.
generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b))
- (Zgcd_is_pos a ('b)) (Zggcd_correct_divisors a ('b)).
+ (Zgcd_nonneg a ('b)) (Zggcd_correct_divisors a ('b)).
destruct (Zggcd a (Zpos b)) as (g,(aa,bb)).
generalize (Zggcd_gcd c ('d)) (Zgcd_is_gcd c ('d))
- (Zgcd_is_pos c ('d)) (Zggcd_correct_divisors c ('d)).
+ (Zgcd_nonneg c ('d)) (Zggcd_correct_divisors c ('d)).
destruct (Zggcd c (Zpos d)) as (g',(cc,dd)).
simpl.
intro H; rewrite <- H; clear H.
@@ -80,10 +71,9 @@ Proof.
intro H; rewrite <- H; clear H.
intros Hg1 Hg2 (Hg3,Hg4).
intros.
- assert (g <> 0).
- intro; subst g; discriminate.
- assert (g' <> 0).
- intro; subst g'; discriminate.
+ assert (g <> 0) by (intro; subst g; discriminate).
+ assert (g' <> 0) by (intro; subst g'; discriminate).
+
elim (rel_prime_cross_prod aa bb cc dd).
congruence.
unfold rel_prime in |- *.
@@ -93,14 +83,13 @@ Proof.
exists bb; auto with zarith.
intros.
inversion Hg1.
- destruct (H6 (g*x)).
+ destruct (H6 (g*x)) as (x',Hx).
rewrite Hg3.
destruct H2 as (xa,Hxa); exists xa; rewrite Hxa; ring.
rewrite Hg4.
destruct H3 as (xb,Hxb); exists xb; rewrite Hxb; ring.
- exists q.
- apply Zmult_reg_l with g; auto.
- pattern g at 1; rewrite H7; ring.
+ exists x'.
+ apply Zmult_reg_l with g; auto. rewrite Hx at 1; ring.
(* /rel_prime *)
unfold rel_prime in |- *.
(* rel_prime *)
@@ -109,14 +98,13 @@ Proof.
exists dd; auto with zarith.
intros.
inversion Hg'1.
- destruct (H6 (g'*x)).
+ destruct (H6 (g'*x)) as (x',Hx).
rewrite Hg'3.
destruct H2 as (xc,Hxc); exists xc; rewrite Hxc; ring.
rewrite Hg'4.
destruct H3 as (xd,Hxd); exists xd; rewrite Hxd; ring.
- exists q.
- apply Zmult_reg_l with g'; auto.
- pattern g' at 1; rewrite H7; ring.
+ exists x'.
+ apply Zmult_reg_l with g'; auto. rewrite Hx at 1; ring.
(* /rel_prime *)
assert (0<bb); [|auto with zarith].
apply Zmult_gt_0_lt_0_reg_r with g.
diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index 173136b8..c88a8141 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -1,11 +1,9 @@
(************************************************************************)
(* 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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Qring.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Qfield.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 01a97870..ce363a33 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.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-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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.