diff options
Diffstat (limited to 'theories/QArith')
-rw-r--r-- | theories/QArith/QArith.v | 2 | ||||
-rw-r--r-- | theories/QArith/QArith_base.v | 255 | ||||
-rw-r--r-- | theories/QArith/QOrderedType.v | 2 | ||||
-rw-r--r-- | theories/QArith/Qabs.v | 26 | ||||
-rw-r--r-- | theories/QArith/Qcanon.v | 22 | ||||
-rw-r--r-- | theories/QArith/Qfield.v | 6 | ||||
-rw-r--r-- | theories/QArith/Qminmax.v | 2 | ||||
-rw-r--r-- | theories/QArith/Qpower.v | 88 | ||||
-rw-r--r-- | theories/QArith/Qreals.v | 62 | ||||
-rw-r--r-- | theories/QArith/Qreduction.v | 166 | ||||
-rw-r--r-- | theories/QArith/Qring.v | 2 | ||||
-rw-r--r-- | theories/QArith/Qround.v | 26 |
12 files changed, 280 insertions, 379 deletions
diff --git a/theories/QArith/QArith.v b/theories/QArith/QArith.v index fe8d639c..5d36ff12 100644 --- a/theories/QArith/QArith.v +++ b/theories/QArith/QArith.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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/QArith_base.v b/theories/QArith/QArith_base.v index 94ea4906..cf5bb3f2 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -20,7 +20,7 @@ Delimit Scope Q_scope with Q. Bind Scope Q_scope with Q. 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]. *) @@ -58,79 +58,65 @@ Qed. 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, CompareSpec (x==y) (x<y) (y<x) (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. *) @@ -139,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. @@ -223,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 *) @@ -281,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. @@ -368,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: *) @@ -376,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. @@ -419,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 *) @@ -444,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] *) @@ -474,17 +451,15 @@ 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. @@ -561,12 +536,12 @@ 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. @@ -575,52 +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. intros. simpl. - do 2 rewrite Zmult_1_r. reflexivity. + 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. intros. simpl. - do 2 rewrite Zmult_1_r. reflexivity. + 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. @@ -629,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. @@ -645,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. @@ -688,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 @@ -713,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. @@ -721,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 : @@ -740,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. @@ -757,13 +716,12 @@ Proof. Open Scope Z_scope. intros. match goal with |- ?a < ?b => ring_simplify a b end. - rewrite Zplus_comm. - apply Zplus_le_lt_compat. + 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. - assert (forall p, 0 < ' p) by reflexivity. - repeat (apply Zmult_lt_compat_r; auto). + do 2 (apply Z.mul_lt_mono_pos_r;try easy). Close Scope Z_scope. Qed. @@ -802,20 +760,20 @@ 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. @@ -837,12 +795,9 @@ 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. @@ -852,15 +807,9 @@ Proof. 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. + 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. diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v index 238de6fa..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-2010 *) +(* <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 557fabc8..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-2010 *) +(* <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,25 +85,25 @@ 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 Pmult_comm, <- Zabs_Zopp. + rewrite Pos.mul_comm, <- Z.abs_opp. do 2 f_equal. ring. Qed. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index fea2ba39..d1160cbe 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -22,39 +22,39 @@ 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. @@ -488,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 5e27f381..3e162cdc 100644 --- a/theories/QArith/Qfield.v +++ b/theories/QArith/Qfield.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -38,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]; @@ -66,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 2da24ee6..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-2010 *) +(* <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/Qpower.v b/theories/QArith/Qpower.v index b05ee649..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-2010 *) +(* <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. @@ -140,8 +136,6 @@ rewrite ?Z.pos_sub_spec; case Pos.compare_spec; intros H0; simpl; subst; try rewrite Qpower_minus_positive; 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 24f6d720..0c7a22bf 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -21,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. @@ -36,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. @@ -65,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. @@ -107,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. @@ -147,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. @@ -156,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. @@ -181,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. @@ -205,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. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index e39eca0c..3b3a30eb 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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,46 +11,29 @@ Require Export QArith_base. Require Import Znumtheory. -(** First, a function that (tries to) build a positive back from a Z. *) +Notation Z2P := Z.to_pos (compat "8.3"). +Notation Z2P_correct := Z2Pos.id (compat "8.3"). -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. - -(** 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_nonneg 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. 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. + rewrite Z2Pos.id. ring. + rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hd | omega]. Close Scope Z_scope. Qed. @@ -59,68 +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_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_nonneg 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) by (intro; subst g; discriminate). - assert (g' <> 0) by (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)) 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 x'. - apply Zmult_reg_l with g; auto. rewrite Hx at 1; 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)) 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 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. - 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. @@ -137,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. @@ -178,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 c88a8141..39e023cf 100644 --- a/theories/QArith/Qring.v +++ b/theories/QArith/Qring.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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/Qround.v b/theories/QArith/Qround.v index ce363a33..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-2010 *) +(* <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,7 @@ 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. @@ -142,9 +142,9 @@ 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_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. |