diff options
Diffstat (limited to 'theories/QArith')
-rw-r--r-- | theories/QArith/QArith.v | 4 | ||||
-rw-r--r-- | theories/QArith/QArith_base.v | 386 | ||||
-rw-r--r-- | theories/QArith/QOrderedType.v | 2 | ||||
-rw-r--r-- | theories/QArith/Qabs.v | 59 | ||||
-rw-r--r-- | theories/QArith/Qcanon.v | 36 | ||||
-rw-r--r-- | theories/QArith/Qfield.v | 8 | ||||
-rw-r--r-- | theories/QArith/Qminmax.v | 4 | ||||
-rw-r--r-- | theories/QArith/Qpower.v | 92 | ||||
-rw-r--r-- | theories/QArith/Qreals.v | 66 | ||||
-rw-r--r-- | theories/QArith/Qreduction.v | 186 | ||||
-rw-r--r-- | theories/QArith/Qring.v | 4 | ||||
-rw-r--r-- | theories/QArith/Qround.v | 31 |
12 files changed, 479 insertions, 399 deletions
diff --git a/theories/QArith/QArith.v b/theories/QArith/QArith.v index 2255cd41..5d36ff12 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-2012 *) (* \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..cf5bb3f2 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-2012 *) (* \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,16 +18,16 @@ 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. +Ltac simpl_mult := rewrite ?Pos2Z.inj_mul. (** [a#b] denotes the fraction [a] over [b]. *) 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,84 +46,77 @@ 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. Notation "p ?= q" := (Qcompare p q) : Q_scope. -Lemma Qeq_alt : forall p q, (p == q) <-> (p ?= q) = Eq. +Lemma Qeq_alt p q : (p == q) <-> (p ?= q) = Eq. Proof. -unfold Qeq, Qcompare; intros; split; intros. -rewrite H; apply Zcompare_refl. -apply Zcompare_Eq_eq; auto. +symmetry. apply Z.compare_eq_iff. Qed. -Lemma Qlt_alt : forall p q, (p<q) <-> (p?=q = Lt). +Lemma Qlt_alt p q : (p<q) <-> (p?=q = Lt). Proof. -unfold Qlt, Qcompare, Zlt; split; auto. +reflexivity. Qed. -Lemma Qgt_alt : forall p q, (p>q) <-> (p?=q = Gt). +Lemma Qgt_alt p q : (p>q) <-> (p?=q = Gt). Proof. -unfold Qlt, Qcompare, Zlt. -intros; rewrite Zcompare_Gt_Lt_antisym; split; auto. +symmetry. apply Z.gt_lt_iff. Qed. -Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt). +Lemma Qle_alt p q : (p<=q) <-> (p?=q <> Gt). Proof. -unfold Qle, Qcompare, Zle; split; auto. +reflexivity. Qed. -Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt). +Lemma Qge_alt p q : (p>=q) <-> (p?=q <> Lt). Proof. -unfold Qle, Qcompare, Zle. -split; intros; contradict H. -rewrite Zcompare_Gt_Lt_antisym; auto. -rewrite Zcompare_Gt_Lt_antisym in H; auto. +symmetry. apply Z.ge_le_iff. Qed. Hint Unfold Qeq Qlt Qle : qarith. Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith. -Lemma Qcompare_antisym : forall x y, CompOpp (x ?= y) = (y ?= x). +Lemma Qcompare_antisym x y : CompOpp (x ?= y) = (y ?= x). Proof. - unfold "?=". intros. apply Zcompare_antisym. + symmetry. apply Z.compare_antisym. Qed. -Lemma Qcompare_spec : forall x y, CompSpec Qeq Qlt x y (x ?= y). +Lemma Qcompare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x ?= y). Proof. - intros. - destruct (x ?= y) as [ ]_eqn:H; constructor; auto. - rewrite Qeq_alt; auto. - rewrite Qlt_alt, <- Qcompare_antisym, H; auto. + unfold Qeq, Qlt, Qcompare. case Z.compare_spec; now constructor. Qed. (** * Properties of equality. *) -Theorem Qeq_refl : forall x, x == x. +Theorem Qeq_refl x : x == x. Proof. auto with qarith. Qed. -Theorem Qeq_sym : forall x y, x == y -> y == x. +Theorem Qeq_sym x y : x == y -> y == x. Proof. auto with qarith. Qed. -Theorem Qeq_trans : forall x y z, x == y -> y == z -> x == z. +Theorem Qeq_trans x y z : x == y -> y == z -> x == z. Proof. -unfold Qeq; intros. -apply Zmult_reg_l with (QDen y). -auto with qarith. -transitivity (Qnum x * QDen y * QDen z)%Z; try ring. -rewrite H. -transitivity (Qnum y * QDen z * QDen x)%Z; try ring. -rewrite H0; ring. +unfold Qeq; intros XY YZ. +apply Z.mul_reg_r with (QDen y); [auto with qarith|]. +now rewrite Z.mul_shuffle0, XY, Z.mul_shuffle0, YZ, Z.mul_shuffle0. Qed. -Hint Resolve Qeq_refl : qarith. -Hint Resolve Qeq_sym : qarith. -Hint Resolve Qeq_trans : qarith. +Hint Immediate Qeq_sym : qarith. +Hint Resolve Qeq_refl Qeq_trans : qarith. (** In a word, [Qeq] is a setoid equality. *) @@ -134,50 +125,48 @@ Proof. split; red; eauto with qarith. Qed. (** Furthermore, this equality is decidable: *) -Theorem Qeq_dec : forall x y, {x==y} + {~ x==y}. +Theorem Qeq_dec x y : {x==y} + {~ x==y}. Proof. - intros; case (Z_eq_dec (Qnum x * QDen y) (Qnum y * QDen x)); auto. + apply Z.eq_dec. Defined. Definition Qeq_bool x y := (Zeq_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z. Definition Qle_bool x y := - (Zle_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z. + (Z.leb (Qnum x * QDen y) (Qnum y * QDen x))%Z. -Lemma Qeq_bool_iff : forall x y, Qeq_bool x y = true <-> x == y. +Lemma Qeq_bool_iff x y : Qeq_bool x y = true <-> x == y. Proof. - unfold Qeq_bool, Qeq; intros. symmetry; apply Zeq_is_eq_bool. Qed. -Lemma Qeq_bool_eq : forall x y, Qeq_bool x y = true -> x == y. +Lemma Qeq_bool_eq x y : Qeq_bool x y = true -> x == y. Proof. - intros; rewrite <- Qeq_bool_iff; auto. + apply Qeq_bool_iff. Qed. -Lemma Qeq_eq_bool : forall x y, x == y -> Qeq_bool x y = true. +Lemma Qeq_eq_bool x y : x == y -> Qeq_bool x y = true. Proof. - intros; rewrite Qeq_bool_iff; auto. + apply Qeq_bool_iff. Qed. -Lemma Qeq_bool_neq : forall x y, Qeq_bool x y = false -> ~ x == y. +Lemma Qeq_bool_neq x y : Qeq_bool x y = false -> ~ x == y. Proof. - intros x y H; rewrite <- Qeq_bool_iff, H; discriminate. + rewrite <- Qeq_bool_iff. now intros ->. Qed. -Lemma Qle_bool_iff : forall x y, Qle_bool x y = true <-> x <= y. +Lemma Qle_bool_iff x y : Qle_bool x y = true <-> x <= y. Proof. - unfold Qle_bool, Qle; intros. symmetry; apply Zle_is_le_bool. Qed. -Lemma Qle_bool_imp_le : forall x y, Qle_bool x y = true -> x <= y. +Lemma Qle_bool_imp_le x y : Qle_bool x y = true -> x <= y. Proof. - intros; rewrite <- Qle_bool_iff; auto. + apply Qle_bool_iff. Qed. -Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x. +Theorem Qnot_eq_sym x y : ~x == y -> ~y == x. Proof. auto with qarith. Qed. @@ -218,12 +207,9 @@ Infix "/" := Qdiv : Q_scope. Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope. -Lemma Qmake_Qdiv : forall a b, a#b==inject_Z a/inject_Z ('b). +Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z ('b). Proof. -intros a b. -unfold Qeq. -simpl. -ring. +unfold Qeq. simpl. ring. Qed. (** * Setoid compatibility results *) @@ -276,17 +262,13 @@ Instance Qinv_comp : Proper (Qeq==>Qeq) Qinv. Proof. unfold Qeq, Qinv; simpl. Open Scope Z_scope. - intros (p1, p2) (q1, q2); simpl. - case p1; simpl. - intros. - assert (q1 = 0). - elim (Zmult_integral q1 ('p2)); auto with zarith. - intros; discriminate. - subst; auto. - case q1; simpl; intros; try discriminate. - rewrite (Pmult_comm p2 p); rewrite (Pmult_comm q2 p0); auto. - case q1; simpl; intros; try discriminate. - rewrite (Pmult_comm p2 p); rewrite (Pmult_comm q2 p0); auto. + intros (p1, p2) (q1, q2) EQ; simpl in *. + destruct q1; simpl in *. + - apply Z.mul_eq_0 in EQ. destruct EQ; now subst. + - destruct p1; simpl in *; try discriminate. + now rewrite Pos.mul_comm, <- EQ, Pos.mul_comm. + - destruct p1; simpl in *; try discriminate. + now rewrite Pos.mul_comm, <- EQ, Pos.mul_comm. Close Scope Z_scope. Qed. @@ -363,7 +345,7 @@ Qed. Lemma Qplus_0_r : forall x, x+0 == x. Proof. intros (x1, x2); unfold Qeq, Qplus; simpl. - rewrite Pmult_comm; simpl; ring. + rewrite Pos.mul_comm; simpl; ring. Qed. (** Commutativity of addition: *) @@ -371,7 +353,7 @@ Qed. Theorem Qplus_comm : forall x y, x+y == y+x. Proof. intros (x1, x2); unfold Qeq, Qplus; simpl. - intros; rewrite Pmult_comm; ring. + intros; rewrite Pos.mul_comm; ring. Qed. @@ -387,6 +369,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] *) @@ -394,7 +396,7 @@ Qed. Theorem Qmult_assoc : forall n m p, n*(m*p)==(n*m)*p. Proof. - intros; red; simpl; rewrite Pmult_assoc; ring. + intros; red; simpl; rewrite Pos.mul_assoc; ring. Qed. (** multiplication and zero *) @@ -419,15 +421,15 @@ Qed. Theorem Qmult_1_r : forall n, n*1==n. Proof. intro; red; simpl. - rewrite Zmult_1_r with (n := Qnum n). - rewrite Pmult_comm; simpl; trivial. + rewrite Z.mul_1_r with (n := Qnum n). + rewrite Pos.mul_comm; simpl; trivial. Qed. (** Commutativity of multiplication *) Theorem Qmult_comm : forall x y, x*y==y*x. Proof. - intros; red; simpl; rewrite Pmult_comm; ring. + intros; red; simpl; rewrite Pos.mul_comm; ring. Qed. (** Distributivity over [Qadd] *) @@ -449,19 +451,32 @@ Qed. Theorem Qmult_integral : forall x y, x*y==0 -> x==0 \/ y==0. Proof. intros (x1,x2) (y1,y2). - unfold Qeq, Qmult; simpl; intros. - destruct (Zmult_integral (x1*1)%Z (y1*1)%Z); auto. - rewrite <- H; ring. + unfold Qeq, Qmult; simpl. + now rewrite <- Z.mul_eq_0, !Z.mul_1_r. Qed. Theorem Qmult_integral_l : forall x y, ~ x == 0 -> x*y == 0 -> y == 0. Proof. intros (x1, x2) (y1, y2). - unfold Qeq, Qmult; simpl; intros. - apply Zmult_integral_l with x1; auto with zarith. - rewrite <- H0; ring. + unfold Qeq, Qmult; simpl. + rewrite !Z.mul_1_r, Z.mul_eq_0. intuition. 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,14 +515,33 @@ 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. +Lemma Qle_refl x : x<=x. Proof. unfold Qle; auto with zarith. Qed. -Lemma Qle_antisym : forall x y, x<=y -> y<=x -> x==y. +Lemma Qle_antisym x y : x<=y -> y<=x -> x==y. Proof. unfold Qle, Qeq; auto with zarith. Qed. @@ -516,39 +550,46 @@ Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z. Proof. unfold Qle; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. Open Scope Z_scope. - apply Zmult_le_reg_r with ('y2). - red; trivial. - apply Zle_trans with (y1 * 'x2 * 'z2). - replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring. - apply Zmult_le_compat_r; auto with zarith. - replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring. - replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring. - apply Zmult_le_compat_r; auto with zarith. + apply Z.mul_le_mono_pos_r with ('y2); [easy|]. + apply Z.le_trans with (y1 * 'x2 * 'z2). + - rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r. + - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1). + now apply Z.mul_le_mono_pos_r. Close Scope Z_scope. Qed. Hint Resolve Qle_trans : qarith. -Lemma Qlt_irrefl : forall x, ~x<x. +Lemma Qlt_irrefl x : ~x<x. Proof. unfold Qlt. auto with zarith. Qed. -Lemma Qlt_not_eq : forall x y, x<y -> ~ x==y. +Lemma Qlt_not_eq x y : x<y -> ~ x==y. 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. simpl. now rewrite !Z.mul_1_r. +Qed. + +Lemma Zlt_Qlt (x y: Z): (x < y)%Z = (inject_Z x < inject_Z y). +Proof. + unfold Qlt. simpl. now rewrite !Z.mul_1_r. +Qed. + + (** Large = strict or equal *) -Lemma Qle_lteq : forall x y, x<=y <-> x<y \/ x==y. +Lemma Qle_lteq x y : x<=y <-> x<y \/ x==y. Proof. - intros. rewrite Qeq_alt, Qle_alt, Qlt_alt. destruct (x ?= y); intuition; discriminate. Qed. -Lemma Qlt_le_weak : forall x y, x<y -> x<=y. +Lemma Qlt_le_weak x y : x<y -> x<=y. Proof. unfold Qle, Qlt; auto with zarith. Qed. @@ -557,15 +598,11 @@ Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z. Proof. unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. Open Scope Z_scope. - apply Zgt_lt. - apply Zmult_gt_reg_r with ('y2). - red; trivial. - apply Zgt_le_trans with (y1 * 'x2 * 'z2). - replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring. - replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring. - apply Zmult_gt_compat_r; auto with zarith. - replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring. - apply Zmult_le_compat_r; auto with zarith. + apply Z.mul_lt_mono_pos_r with ('y2); [easy|]. + apply Z.le_lt_trans with (y1 * 'x2 * 'z2). + - rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r. + - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1). + now apply Z.mul_lt_mono_pos_r. Close Scope Z_scope. Qed. @@ -573,15 +610,11 @@ Lemma Qlt_le_trans : forall x y z, x<y -> y<=z -> x<z. Proof. unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. Open Scope Z_scope. - apply Zgt_lt. - apply Zmult_gt_reg_r with ('y2). - red; trivial. - apply Zle_gt_trans with (y1 * 'x2 * 'z2). - replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring. - replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring. - apply Zmult_le_compat_r; auto with zarith. - replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring. - apply Zmult_gt_compat_r; auto with zarith. + apply Z.mul_lt_mono_pos_r with ('y2); [easy|]. + apply Z.lt_le_trans with (y1 * 'x2 * 'z2). + - rewrite Z.mul_shuffle0. now apply Z.mul_lt_mono_pos_r. + - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1). + now apply Z.mul_le_mono_pos_r. Close Scope Z_scope. Qed. @@ -616,7 +649,7 @@ Qed. Lemma Qle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y. Proof. - unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto. + unfold Qle, Qlt, Qeq; intros; now apply Z.lt_eq_cases. Qed. Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le @@ -641,7 +674,7 @@ Defined. Lemma Qopp_le_compat : forall p q, p<=q -> -q <= -p. Proof. intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl. - do 2 rewrite <- Zopp_mult_distr_l; omega. + rewrite !Z.mul_opp_l. omega. Qed. Hint Resolve Qopp_le_compat : qarith. @@ -649,15 +682,13 @@ 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. - rewrite <- Zopp_mult_distr_l. - split; omega. + rewrite Z.mul_opp_l. omega. Qed. Lemma Qlt_minus_iff : forall p q, p < q <-> 0 < q+-p. Proof. intros (x1,x2) (y1,y2); unfold Qlt; simpl. - rewrite <- Zopp_mult_distr_l. - split; omega. + rewrite Z.mul_opp_l. omega. Qed. Lemma Qplus_le_compat : @@ -668,8 +699,8 @@ Proof. Open Scope Z_scope. intros. match goal with |- ?a <= ?b => ring_simplify a b end. - rewrite Zplus_comm. - apply Zplus_le_compat. + rewrite Z.add_comm. + apply Z.add_le_mono. 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. @@ -677,42 +708,117 @@ 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 Z.add_comm. + apply Z.add_le_lt_mono. + 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. + do 2 (apply Z.mul_lt_mono_pos_r;try easy). + 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. Open Scope Z_scope. intros; 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. - apply Zmult_le_compat_r; auto with zarith. + rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). + apply Z.mul_le_mono_nonneg_r; auto with zarith. Close Scope Z_scope. Qed. -Lemma Qmult_lt_0_le_reg_r : forall x y z, 0 < z -> x*z <= y*z -> x <= y. +Lemma Qmult_lt_0_le_reg_r : forall x y z, 0 < z -> x*z <= y*z -> x <= y. Proof. intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. Open Scope Z_scope. 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. - intros; apply Zmult_le_reg_r with (c1*'c2); auto with zarith. + rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). + intros LT LE. + apply Z.mul_le_mono_pos_r in LE; trivial. + apply Z.mul_pos_pos; [omega|easy]. 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. Open Scope Z_scope. intros; 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. - apply Zmult_lt_compat_r; auto with zarith. - apply Zmult_lt_0_compat. - omega. - compute; auto. + rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). + apply Z.mul_lt_mono_pos_r; auto with zarith. + apply Z.mul_pos_pos; [omega|reflexivity]. 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. + rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). + intro LT. rewrite <- Z.mul_lt_mono_pos_r. reflexivity. + apply Z.mul_pos_pos; [omega|reflexivity]. + 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..e146da25 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-2012 *) (* \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..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. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 71a3b474..d1160cbe 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-2012 *) (* \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,43 +18,43 @@ 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 : - forall q:Q, Zgcd (Qnum q) (QDen q) = 1%Z -> Qred q = q. + forall q:Q, Z.gcd (Qnum q) (QDen q) = 1%Z -> Qred q = q. Proof. unfold Qred; intros (a,b); simpl. - generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)). + generalize (Z.ggcd_gcd a ('b)) (Z.ggcd_correct_divisors a ('b)). intros. rewrite H1 in H; clear H1. - destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. + destruct (Z.ggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. destruct H0. - rewrite Zmult_1_l in H, H0. + rewrite Z.mul_1_l in H, H0. subst; simpl; auto. Qed. Lemma Qred_identity2 : - forall q:Q, Qred q = q -> Zgcd (Qnum q) (QDen q) = 1%Z. + forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z. Proof. unfold Qred; intros (a,b); simpl. - generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)) (Zgcd_is_pos a ('b)). + generalize (Z.ggcd_gcd a ('b)) (Z.ggcd_correct_divisors a ('b)) (Z.gcd_nonneg a ('b)). intros. rewrite <- H; rewrite <- H in H1; clear H. - destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. + destruct (Z.ggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. injection H2; intros; clear H2. destruct H0. clear H0 H3. destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate. f_equal. - apply Pmult_reg_r with bb. + apply Pos.mul_reg_r with bb. injection H2; intros. rewrite <- H0. rewrite H; simpl; auto. elim H1; auto. Qed. -Lemma Qred_iff : forall q:Q, Qred q = q <-> Zgcd (Qnum q) (QDen q) = 1%Z. +Lemma Qred_iff : forall q:Q, Qred q = q <-> Z.gcd (Qnum q) (QDen q) = 1%Z. Proof. split; intros. apply Qred_identity2; auto. @@ -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. @@ -492,7 +488,7 @@ Definition Qc_eq_bool (x y : Qc) := Lemma Qc_eq_bool_correct : forall x y : Qc, Qc_eq_bool x y = true -> x=y. Proof. - intros x y; unfold Qc_eq_bool in |- *; case (Qc_eq_dec x y); simpl in |- *; auto. + intros x y; unfold Qc_eq_bool; case (Qc_eq_dec x y); simpl; auto. intros _ H; inversion H. Qed. diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v index 81d59714..3e162cdc 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-2012 *) (* \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. @@ -40,7 +38,7 @@ Proof. exact Hp. Qed. -Lemma Qpower_theory : power_theory 1 Qmult Qeq Z_of_N Qpower. +Lemma Qpower_theory : power_theory 1 Qmult Qeq Z.of_N Qpower. Proof. constructor. intros r [|n]; @@ -68,7 +66,7 @@ Ltac Qpow_tac t := match t with | Z0 => N0 | Zpos ?n => Ncst (Npos n) - | Z_of_N ?n => Ncst n + | Z.of_N ?n => Ncst n | NtoZ ?n => Ncst n | _ => NotConstant end. diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v index a458fc6e..2b6c3980 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-2012 *) (* \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..5d494c7c 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-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -101,10 +101,9 @@ Lemma Qpower_plus_positive : forall a n m, Qpower_positive a (n+m) == (Qpower_po Proof. intros a n m. unfold Qpower_positive. -apply pow_pos_Pplus. +apply pow_pos_add. apply Q_Setoid. apply Qmult_comp. -apply Qmult_comm. apply Qmult_assoc. Qed. @@ -114,21 +113,18 @@ intros a [|n|n]; simpl; try reflexivity. symmetry; apply Qinv_involutive. Qed. -Lemma Qpower_minus_positive : forall a (n m:positive), (Pcompare n m Eq=Gt)%positive -> Qpower_positive a (n-m)%positive == (Qpower_positive a n)/(Qpower_positive a m). +Lemma Qpower_minus_positive : forall a (n m:positive), + (m < n)%positive -> + Qpower_positive a (n-m)%positive == (Qpower_positive a n)/(Qpower_positive a m). Proof. intros a n m H. -destruct (Qeq_dec a 0). - rewrite q. - repeat rewrite Qpower_positive_0. - reflexivity. -rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)) by - (apply Qpower_not_0_positive; assumption). -apply Qdiv_comp;[|reflexivity]. -rewrite Qmult_comm. -rewrite <- Qpower_plus_positive. -rewrite Pplus_minus. -reflexivity. -assumption. +destruct (Qeq_dec a 0) as [EQ|NEQ]. +- now rewrite EQ, !Qpower_positive_0. +- rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)) by + (now apply Qpower_not_0_positive). + f_equiv. + rewrite <- Qpower_plus_positive. + now rewrite Pos.sub_add. Qed. Lemma Qpower_plus : forall a n m, ~a==0 -> a^(n+m) == a^n*a^m. @@ -136,12 +132,10 @@ 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; assumption. Qed. @@ -158,13 +152,14 @@ apply Qpower_plus. assumption. Qed. -Lemma Qpower_mult_positive : forall a n m, Qpower_positive a (n*m) == Qpower_positive (Qpower_positive a n) m. +Lemma Qpower_mult_positive : forall a n m, + Qpower_positive a (n*m) == Qpower_positive (Qpower_positive a n) m. Proof. intros a n m. -induction n using Pind. +induction n using Pos.peano_ind. reflexivity. -rewrite Pmult_Sn_m. -rewrite Pplus_one_succ_l. +rewrite Pos.mul_succ_l. +rewrite <- Pos.add_1_l. do 2 rewrite Qpower_plus_positive. rewrite IHn. rewrite Qmult_power_positive. @@ -184,11 +179,11 @@ Qed. Lemma Zpower_Qpower : forall (a n:Z), (0<=n)%Z -> inject_Z (a^n) == (inject_Z a)^n. Proof. intros a [|n|n] H;[reflexivity| |elim H; reflexivity]. -induction n using Pind. +induction n using Pos.peano_ind. replace (a^1)%Z with a by ring. ring. -rewrite Zpos_succ_morphism. -unfold Zsucc. +rewrite Pos2Z.inj_succ. +unfold Z.succ. rewrite Zpower_exp; auto with *; try discriminate. rewrite Qpower_plus' by discriminate. rewrite <- IHn by discriminate. @@ -209,31 +204,20 @@ setoid_replace (0+ - a) with (-a) in A by ring. apply Qmult_le_0_compat; assumption. Qed. -Theorem Qpower_decomp: forall p x y, - Qpower_positive (x #y) p == x ^ Zpos p # (Z2P ((Zpos y) ^ Zpos p)). -Proof. -induction p; intros; unfold Qmult; simpl. -(* xI *) -rewrite IHp, xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l. -repeat rewrite Zpower_pos_is_exp. -red; unfold Qmult, Qnum, Qden, Zpower. -repeat rewrite Zpos_mult_morphism. -repeat rewrite Z2P_correct. -repeat rewrite Zpower_pos_1_r; ring. -apply Zpower_pos_pos; red; auto. -repeat apply Zmult_lt_0_compat; red; auto; - apply Zpower_pos_pos; red; auto. -(* xO *) -rewrite IHp, <-Pplus_diag. -repeat rewrite Zpower_pos_is_exp. -red; unfold Qmult, Qnum, Qden, Zpower. -repeat rewrite Zpos_mult_morphism. -repeat rewrite Z2P_correct; try ring. -apply Zpower_pos_pos; red; auto. -repeat apply Zmult_lt_0_compat; auto; - apply Zpower_pos_pos; red; auto. -(* xO *) -unfold Qmult; simpl. -red; simpl; rewrite Zpower_pos_1_r; - rewrite Zpos_mult_morphism; ring. +Theorem Qpower_decomp p x y : + Qpower_positive (x#y) p = x ^ Zpos p # (y ^ p). +Proof. +induction p; intros; simpl Qpower_positive; rewrite ?IHp. +- (* xI *) + unfold Qmult, Qnum, Qden. f_equal. + + now rewrite <- Z.pow_twice_r, <- Z.pow_succ_r. + + apply Pos2Z.inj; rewrite !Pos2Z.inj_mul, !Pos2Z.inj_pow. + now rewrite <- Z.pow_twice_r, <- Z.pow_succ_r. +- (* xO *) + unfold Qmult, Qnum, Qden. f_equal. + + now rewrite <- Z.pow_twice_r. + + apply Pos2Z.inj; rewrite !Pos2Z.inj_mul, !Pos2Z.inj_pow. + now rewrite <- Z.pow_twice_r. +- (* xO *) + now rewrite Z.pow_1_r, Pos.pow_1_r. Qed. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 8a0ebcff..0c7a22bf 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-2012 *) (* \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. @@ -23,7 +21,7 @@ Hint Resolve IZR_nz Rmult_integral_contrapositive. Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y. Proof. -unfold Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; +unfold Qeq, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. apply eq_IZR. do 2 rewrite mult_IZR. @@ -38,24 +36,24 @@ Qed. Lemma Qeq_eqR : forall x y : Q, x==y -> Q2R x = Q2R y. Proof. -unfold Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; +unfold Qeq, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2); set (X2 := IZR (Zpos x2)) in *. set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); set (Y2 := IZR (Zpos y2)) in *. assert ((X1 * Y2)%R = (Y1 * X2)%R). - unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR. + unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR. apply IZR_eq; auto. clear H. field_simplify_eq; auto. ring_simplify X1 Y2 (Y2 * X1)%R. -rewrite H0 in |- *; ring. +rewrite H0; ring. Qed. Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y. Proof. -unfold Qle, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; +unfold Qle, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. apply le_IZR. do 2 rewrite mult_IZR. @@ -67,37 +65,37 @@ replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto). replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto). apply Rmult_le_compat_r; auto. apply Rmult_le_pos. -unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_le; +unfold X2; replace 0%R with (IZR 0); auto; apply IZR_le; auto with zarith. -unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_le; +unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_le; auto with zarith. Qed. Lemma Qle_Rle : forall x y : Q, x<=y -> (Q2R x <= Q2R y)%R. Proof. -unfold Qle, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; +unfold Qle, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2); set (X2 := IZR (Zpos x2)) in *. set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); set (Y2 := IZR (Zpos y2)) in *. assert (X1 * Y2 <= Y1 * X2)%R. - unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR. + unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR. apply IZR_le; auto. clear H. replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto). replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto). apply Rmult_le_compat_r; auto. apply Rmult_le_pos; apply Rlt_le; apply Rinv_0_lt_compat. -unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; +unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; auto with zarith. -unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; +unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; auto with zarith. Qed. Lemma Rlt_Qlt : forall x y : Q, (Q2R x < Q2R y)%R -> x<y. Proof. -unfold Qlt, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; +unfold Qlt, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. apply lt_IZR. do 2 rewrite mult_IZR. @@ -109,38 +107,38 @@ replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto). replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto). apply Rmult_lt_compat_r; auto. apply Rmult_lt_0_compat. -unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; +unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; auto with zarith. -unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; +unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; auto with zarith. Qed. Lemma Qlt_Rlt : forall x y : Q, x<y -> (Q2R x < Q2R y)%R. Proof. -unfold Qlt, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; +unfold Qlt, Q2R; intros (x1, x2) (y1, y2); unfold Qnum, Qden; intros. set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2); set (X2 := IZR (Zpos x2)) in *. set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); set (Y2 := IZR (Zpos y2)) in *. assert (X1 * Y2 < Y1 * X2)%R. - unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR. + unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR. apply IZR_lt; auto. clear H. replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto). replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto). apply Rmult_lt_compat_r; auto. apply Rmult_lt_0_compat; apply Rinv_0_lt_compat. -unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; +unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; auto with zarith. -unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; +unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; auto with zarith. Qed. Lemma Q2R_plus : forall x y : Q, Q2R (x+y) = (Q2R x + Q2R y)%R. Proof. -unfold Qplus, Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); - unfold Qden, Qnum in |- *. +unfold Qplus, Qeq, Q2R; intros (x1, x2) (y1, y2); + unfold Qden, Qnum. simpl_mult. rewrite plus_IZR. do 3 rewrite mult_IZR. @@ -149,8 +147,8 @@ Qed. Lemma Q2R_mult : forall x y : Q, Q2R (x*y) = (Q2R x * Q2R y)%R. Proof. -unfold Qmult, Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); - unfold Qden, Qnum in |- *. +unfold Qmult, Qeq, Q2R; intros (x1, x2) (y1, y2); + unfold Qden, Qnum. simpl_mult. do 2 rewrite mult_IZR. field; auto. @@ -158,24 +156,24 @@ Qed. Lemma Q2R_opp : forall x : Q, Q2R (- x) = (- Q2R x)%R. Proof. -unfold Qopp, Qeq, Q2R in |- *; intros (x1, x2); unfold Qden, Qnum in |- *. +unfold Qopp, Qeq, Q2R; intros (x1, x2); unfold Qden, Qnum. rewrite Ropp_Ropp_IZR. field; auto. Qed. Lemma Q2R_minus : forall x y : Q, Q2R (x-y) = (Q2R x - Q2R y)%R. -unfold Qminus in |- *; intros; rewrite Q2R_plus; rewrite Q2R_opp; auto. +unfold Qminus; intros; rewrite Q2R_plus; rewrite Q2R_opp; auto. Qed. Lemma Q2R_inv : forall x : Q, ~ x==0 -> Q2R (/x) = (/ Q2R x)%R. Proof. -unfold Qinv, Q2R, Qeq in |- *; intros (x1, x2); unfold Qden, Qnum in |- *. +unfold Qinv, Q2R, Qeq; intros (x1, x2); unfold Qden, Qnum. case x1. -simpl in |- *; intros; elim H; trivial. +simpl; intros; elim H; trivial. intros; field; auto. intros; - change (IZR (Zneg x2)) with (- IZR (' x2))%R in |- *; - change (IZR (Zneg p)) with (- IZR (' p))%R in |- *; + change (IZR (Zneg x2)) with (- IZR (' x2))%R; + change (IZR (Zneg p)) with (- IZR (' p))%R; field; (*auto 8 with real.*) repeat split; auto; auto with real. Qed. @@ -183,7 +181,7 @@ Qed. Lemma Q2R_div : forall x y : Q, ~ y==0 -> Q2R (x/y) = (Q2R x / Q2R y)%R. Proof. -unfold Qdiv, Rdiv in |- *. +unfold Qdiv, Rdiv. intros; rewrite Q2R_mult. rewrite Q2R_inv; auto. Qed. @@ -207,7 +205,7 @@ Qed. Let ex2 : forall x y : Q, ~ y==0 -> (x/y)*y == x. intros; QField. intro; apply H; apply eqR_Qeq. -rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real. +rewrite H0; unfold Q2R; simpl; 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..3b3a30eb 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -1,65 +1,39 @@ (************************************************************************) (* 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 *) (************************************************************************) -(*i $Id: Qreduction.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Normalisation functions for rational numbers. *) Require Export QArith_base. Require Import Znumtheory. -(** First, a function that (tries to) build a positive back from a Z. *) - -Definition Z2P (z : Z) := - match z with - | Z0 => 1%positive - | Zpos p => p - | Zneg p => p - end. - -Lemma Z2P_correct : forall z : Z, (0 < z)%Z -> Zpos (Z2P z) = z. -Proof. - simple destruct z; simpl in |- *; auto; intros; discriminate. -Qed. - -Lemma Z2P_correct2 : forall z : Z, 0%Z <> z -> Zpos (Z2P z) = Zabs z. -Proof. - simple destruct z; simpl in |- *; auto; intros; elim H; auto. -Qed. +Notation Z2P := Z.to_pos (compat "8.3"). +Notation Z2P_correct := Z2Pos.id (compat "8.3"). -(** Simplification of fractions using [Zgcd]. +(** Simplification of fractions using [Z.gcd]. This version can compute within Coq. *) Definition Qred (q:Q) := let (q1,q2) := q in - let (r1,r2) := snd (Zggcd q1 ('q2)) - in r1#(Z2P r2). + let (r1,r2) := snd (Z.ggcd q1 ('q2)) + in r1#(Z.to_pos r2). 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)). - destruct (Zggcd n (Zpos d)) as (g,(nn,dd)); simpl. + generalize (Z.ggcd_gcd n ('d)) (Z.gcd_nonneg n ('d)) + (Z.ggcd_correct_divisors n ('d)). + destruct (Z.ggcd 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 Z2Pos.id. ring. + rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hd | omega]. Close Scope Z_scope. Qed. @@ -68,71 +42,54 @@ Proof. intros (a,b) (c,d). 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)). - 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)). - destruct (Zggcd c (Zpos d)) as (g',(cc,dd)). - simpl. - intro H; rewrite <- H; clear H. - intros Hg'1 Hg'2 (Hg'3,Hg'4). - 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. + intros H. + generalize (Z.ggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) + (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)). + destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)). + simpl. intros <- Hg1 Hg2 (Hg3,Hg4). + assert (Hg0 : g <> 0) by (intro; now subst g). + generalize (Z.ggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) + (Z.gcd_nonneg c ('d)) (Z.ggcd_correct_divisors c ('d)). + destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)). + simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4). + assert (Hg'0 : g' <> 0) by (intro; now subst g'). + elim (rel_prime_cross_prod aa bb cc dd). - congruence. - unfold rel_prime in |- *. - (*rel_prime*) - constructor. - exists aa; auto with zarith. - exists bb; auto with zarith. - intros. - inversion Hg1. - destruct (H6 (g*x)). - 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. - (* /rel_prime *) - unfold rel_prime in |- *. - (* rel_prime *) - constructor. - exists cc; auto with zarith. - exists dd; auto with zarith. - intros. - inversion Hg'1. - destruct (H6 (g'*x)). - 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. - (* /rel_prime *) - assert (0<bb); [|auto with zarith]. - apply Zmult_gt_0_lt_0_reg_r with g. - omega. - rewrite Zmult_comm. - rewrite <- Hg4; compute; auto. - assert (0<dd); [|auto with zarith]. - apply Zmult_gt_0_lt_0_reg_r with g'. - omega. - rewrite Zmult_comm. - rewrite <- Hg'4; compute; auto. - apply Zmult_reg_l with (g'*g). - intro H2; elim (Zmult_integral _ _ H2); auto. - replace (g'*g*(aa*dd)) with ((g*aa)*(g'*dd)); [|ring]. - replace (g'*g*(bb*cc)) with ((g'*cc)*(g*bb)); [|ring]. - rewrite <- Hg3; rewrite <- Hg4; rewrite <- Hg'3; rewrite <- Hg'4; auto. + - congruence. + - (*rel_prime*) + constructor. + * exists aa; auto with zarith. + * exists bb; auto with zarith. + * intros x Ha Hb. + destruct Hg1 as (Hg11,Hg12,Hg13). + destruct (Hg13 (g*x)) as (x',Hx). + { rewrite Hg3. + destruct Ha as (xa,Hxa); exists xa; rewrite Hxa; ring. } + { rewrite Hg4. + destruct Hb as (xb,Hxb); exists xb; rewrite Hxb; ring. } + exists x'. + apply Z.mul_reg_l with g; auto. rewrite Hx at 1; ring. + - (* rel_prime *) + constructor. + * exists cc; auto with zarith. + * exists dd; auto with zarith. + * intros x Hc Hd. + inversion Hg'1 as (Hg'11,Hg'12,Hg'13). + destruct (Hg'13 (g'*x)) as (x',Hx). + { rewrite Hg'3. + destruct Hc as (xc,Hxc); exists xc; rewrite Hxc; ring. } + { rewrite Hg'4. + destruct Hd as (xd,Hxd); exists xd; rewrite Hxd; ring. } + exists x'. + apply Z.mul_reg_l with g'; auto. rewrite Hx at 1; ring. + - apply Z.lt_gt. + rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hg4 | omega]. + - apply Z.lt_gt. + rewrite <- (Z.mul_pos_cancel_l g'); [now rewrite <- Hg'4 | omega]. + - apply Z.mul_reg_l with (g*g'). + * rewrite Z.mul_eq_0. now destruct 1. + * rewrite Z.mul_shuffle1, <- Hg3, <- Hg'4. + now rewrite Z.mul_shuffle1, <- Hg'3, <- Hg4, H, Z.mul_comm. Close Scope Z_scope. Qed. @@ -149,39 +106,39 @@ Definition Qminus' x y := Qred (Qminus x y). Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q). Proof. - intros; unfold Qplus' in |- *; apply Qred_correct; auto. + intros; unfold Qplus'; apply Qred_correct; auto. Qed. Lemma Qmult'_correct : forall p q : Q, (Qmult' p q)==(Qmult p q). Proof. - intros; unfold Qmult' in |- *; apply Qred_correct; auto. + intros; unfold Qmult'; apply Qred_correct; auto. Qed. Lemma Qminus'_correct : forall p q : Q, (Qminus' p q)==(Qminus p q). Proof. - intros; unfold Qminus' in |- *; apply Qred_correct; auto. + intros; unfold Qminus'; apply Qred_correct; auto. Qed. Add Morphism Qplus' : Qplus'_comp. Proof. - intros; unfold Qplus' in |- *. - rewrite H; rewrite H0; auto with qarith. + intros; unfold Qplus'. + rewrite H, H0; auto with qarith. Qed. Add Morphism Qmult' : Qmult'_comp. - intros; unfold Qmult' in |- *. - rewrite H; rewrite H0; auto with qarith. + intros; unfold Qmult'. + rewrite H, H0; auto with qarith. Qed. Add Morphism Qminus' : Qminus'_comp. - intros; unfold Qminus' in |- *. - rewrite H; rewrite H0; auto with qarith. + intros; unfold Qminus'. + rewrite H, H0; auto with qarith. Qed. Lemma Qred_opp: forall q, Qred (-q) = - (Qred q). Proof. intros (x, y); unfold Qred; simpl. - rewrite Zggcd_opp; case Zggcd; intros p1 (p2, p3); simpl. + rewrite Z.ggcd_opp; case Z.ggcd; intros p1 (p2, p3); simpl. unfold Qopp; auto. Qed. @@ -190,4 +147,3 @@ Theorem Qred_compare: forall x y, Proof. intros x y; apply Qcompare_comp; apply Qeq_sym; apply Qred_correct. Qed. - diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v index 173136b8..39e023cf 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-2012 *) (* \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..be328c27 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-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,16 +11,16 @@ 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. +rewrite !Z.mul_opp_l; omega. Qed. Hint Resolve Qopp_lt_compat : qarith. (************) -Coercion Local inject_Z : Z >-> Q. +Local Coercion inject_Z : Z >-> Q. -Definition Qfloor (x:Q) := let (n,d) := x in Zdiv n (Zpos d). +Definition Qfloor (x:Q) := let (n,d) := x in Z.div n (Zpos d). Definition Qceiling (x:Q) := (-(Qfloor (-x)))%Z. Lemma Qfloor_Z : forall z:Z, Qfloor z = z. @@ -46,7 +46,7 @@ simpl. unfold Qle. simpl. replace (n*1)%Z with n by ring. -rewrite Zmult_comm. +rewrite Z.mul_comm. apply Z_mult_div_ge. auto with *. Qed. @@ -81,7 +81,7 @@ 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. +rewrite <- Z.lt_add_lt_sub_r. destruct (Z_mod_lt n ('d)); auto with *. Qed. @@ -107,7 +107,7 @@ 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)). +rewrite (Z.mul_comm ('yd) ('xd)). apply Z_div_le; auto with *. Qed. @@ -125,7 +125,7 @@ Hint Resolve Qceiling_resp_le : qarith. Add Morphism Qfloor with signature Qeq ==> eq as Qfloor_comp. Proof. intros x y H. -apply Zle_antisym. +apply Z.le_antisymm. auto with *. symmetry in H; auto with *. Qed. @@ -133,7 +133,18 @@ Qed. Add Morphism Qceiling with signature Qeq ==> eq as Qceiling_comp. Proof. intros x y H. -apply Zle_antisym. +apply Z.le_antisymm. 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, Z.mul_0_r. + now rewrite Z.mul_1_r. + rewrite <- Z.opp_eq_mul_m1. + rewrite <- (Z.opp_involutive (Zpos p)). + now rewrite Zdiv_opp_opp. +Qed. |