diff options
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/QArith.v | 4 | ||||
| -rw-r--r-- | theories/QArith/QArith_base.v | 169 | ||||
| -rw-r--r-- | theories/QArith/QOrderedType.v | 2 | ||||
| -rw-r--r-- | theories/QArith/Qabs.v | 37 | ||||
| -rw-r--r-- | theories/QArith/Qcanon.v | 16 | ||||
| -rw-r--r-- | theories/QArith/Qfield.v | 4 | ||||
| -rw-r--r-- | theories/QArith/Qminmax.v | 4 | ||||
| -rw-r--r-- | theories/QArith/Qpower.v | 6 | ||||
| -rw-r--r-- | theories/QArith/Qreals.v | 6 | ||||
| -rw-r--r-- | theories/QArith/Qreduction.v | 52 | ||||
| -rw-r--r-- | theories/QArith/Qring.v | 4 | ||||
| -rw-r--r-- | theories/QArith/Qround.v | 15 |
12 files changed, 249 insertions, 70 deletions
diff --git a/theories/QArith/QArith.v b/theories/QArith/QArith.v index 2255cd41..fe8d639c 100644 --- a/theories/QArith/QArith.v +++ b/theories/QArith/QArith.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: QArith.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export QArith_base. Require Export Qring. Require Export Qreduction. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 18b8823d..94ea4906 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: QArith_base.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export ZArith. Require Export ZArithRing. Require Export Morphisms Setoid Bool. @@ -20,7 +18,7 @@ Record Q : Set := Qmake {Qnum : Z; Qden : positive}. Delimit Scope Q_scope with Q. Bind Scope Q_scope with Q. -Arguments Scope Qmake [Z_scope positive_scope]. +Arguments Qmake _%Z _%positive. Open Scope Q_scope. Ltac simpl_mult := repeat rewrite Zpos_mult_morphism. @@ -29,7 +27,7 @@ Ltac simpl_mult := repeat rewrite Zpos_mult_morphism. Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope. Definition inject_Z (x : Z) := Qmake x 1. -Arguments Scope inject_Z [Z_scope]. +Arguments inject_Z x%Z. Notation QDen p := (Zpos (Qden p)). Notation " 0 " := (0#1) : Q_scope. @@ -48,6 +46,13 @@ Notation "x > y" := (Qlt y x)(only parsing) : Q_scope. Notation "x >= y" := (Qle y x)(only parsing) : Q_scope. Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope. +(** injection from Z is injective. *) + +Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b. +Proof. + unfold Qeq. simpl. omega. +Qed. + (** Another approach : using Qcompare for defining order relations. *) Definition Qcompare (p q : Q) := (Qnum p * QDen q ?= Qnum q * QDen p)%Z. @@ -92,7 +97,7 @@ Proof. unfold "?=". intros. apply Zcompare_antisym. Qed. -Lemma Qcompare_spec : forall x y, CompSpec Qeq Qlt x y (x ?= y). +Lemma Qcompare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (x ?= y). Proof. intros. destruct (x ?= y) as [ ]_eqn:H; constructor; auto. @@ -387,6 +392,26 @@ Proof. red; simpl; intro; ring. Qed. +(** Injectivity of addition (uses theory about Qopp above): *) + +Lemma Qplus_inj_r (x y z: Q): + x + z == y + z <-> x == y. +Proof. + split; intro E. + rewrite <- (Qplus_0_r x), <- (Qplus_0_r y). + rewrite <- (Qplus_opp_r z); auto. + do 2 rewrite Qplus_assoc. + rewrite E. reflexivity. + rewrite E. reflexivity. +Qed. + +Lemma Qplus_inj_l (x y z: Q): + z + x == z + y <-> x == y. +Proof. + rewrite (Qplus_comm z x), (Qplus_comm z y). + apply Qplus_inj_r. +Qed. + (** * Properties of [Qmult] *) @@ -462,6 +487,21 @@ Proof. rewrite <- H0; ring. Qed. + +(** * inject_Z is a ring homomorphism: *) + +Lemma inject_Z_plus (x y: Z): inject_Z (x + y) = inject_Z x + inject_Z y. +Proof. + unfold Qplus, inject_Z. simpl. f_equal. ring. +Qed. + +Lemma inject_Z_mult (x y: Z): inject_Z (x * y) = inject_Z x * inject_Z y. +Proof. reflexivity. Qed. + +Lemma inject_Z_opp (x: Z): inject_Z (- x) = - inject_Z x. +Proof. reflexivity. Qed. + + (** * Inverse and division. *) Lemma Qinv_involutive : forall q, (/ / q) == q. @@ -500,6 +540,25 @@ Proof. apply Qdiv_mult_l; auto. Qed. +(** Injectivity of Qmult (requires theory about Qinv above): *) + +Lemma Qmult_inj_r (x y z: Q): ~ z == 0 -> (x * z == y * z <-> x == y). +Proof. + intro z_ne_0. + split; intro E. + rewrite <- (Qmult_1_r x), <- (Qmult_1_r y). + rewrite <- (Qmult_inv_r z); auto. + do 2 rewrite Qmult_assoc. + rewrite E. reflexivity. + rewrite E. reflexivity. +Qed. + +Lemma Qmult_inj_l (x y z: Q): ~ z == 0 -> (z * x == z * y <-> x == y). +Proof. + rewrite (Qmult_comm z x), (Qmult_comm z y). + apply Qmult_inj_r. +Qed. + (** * Properties of order upon Q. *) Lemma Qle_refl : forall x, x<=x. @@ -539,6 +598,19 @@ Proof. unfold Qlt, Qeq; auto with zarith. Qed. +Lemma Zle_Qle (x y: Z): (x <= y)%Z = (inject_Z x <= inject_Z y). +Proof. + unfold Qle. intros. simpl. + do 2 rewrite Zmult_1_r. reflexivity. +Qed. + +Lemma Zlt_Qlt (x y: Z): (x < y)%Z = (inject_Z x < inject_Z y). +Proof. + unfold Qlt. intros. simpl. + do 2 rewrite Zmult_1_r. reflexivity. +Qed. + + (** Large = strict or equal *) Lemma Qle_lteq : forall x y, x<=y <-> x<y \/ x==y. @@ -677,6 +749,54 @@ Proof. Close Scope Z_scope. Qed. +Lemma Qplus_lt_le_compat : + forall x y z t, x<y -> z<=t -> x+z < y+t. +Proof. + unfold Qplus, Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2) (t1, t2); + simpl; simpl_mult. + Open Scope Z_scope. + intros. + match goal with |- ?a < ?b => ring_simplify a b end. + rewrite Zplus_comm. + apply Zplus_le_lt_compat. + match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end. + auto with zarith. + match goal with |- ?a < ?b => ring_simplify x1 y1 ('x2) ('y2) a b end. + assert (forall p, 0 < ' p) by reflexivity. + repeat (apply Zmult_lt_compat_r; auto). + Close Scope Z_scope. +Qed. + +Lemma Qplus_le_l (x y z: Q): x + z <= y + z <-> x <= y. +Proof. + split; intros. + rewrite <- (Qplus_0_r x), <- (Qplus_0_r y), <- (Qplus_opp_r z). + do 2 rewrite Qplus_assoc. + apply Qplus_le_compat; auto with *. + apply Qplus_le_compat; auto with *. +Qed. + +Lemma Qplus_le_r (x y z: Q): z + x <= z + y <-> x <= y. +Proof. + rewrite (Qplus_comm z x), (Qplus_comm z y). + apply Qplus_le_l. +Qed. + +Lemma Qplus_lt_l (x y z: Q): x + z < y + z <-> x < y. +Proof. + split; intros. + rewrite <- (Qplus_0_r x), <- (Qplus_0_r y), <- (Qplus_opp_r z). + do 2 rewrite Qplus_assoc. + apply Qplus_lt_le_compat; auto with *. + apply Qplus_lt_le_compat; auto with *. +Qed. + +Lemma Qplus_lt_r (x y z: Q): z + x < z + y <-> x < y. +Proof. + rewrite (Qplus_comm z x), (Qplus_comm z y). + apply Qplus_lt_l. +Qed. + Lemma Qmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z. Proof. intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. @@ -699,6 +819,19 @@ Proof. Close Scope Z_scope. Qed. +Lemma Qmult_le_r (x y z: Q): 0 < z -> (x*z <= y*z <-> x <= y). +Proof. + split; intro. + now apply Qmult_lt_0_le_reg_r with z. + apply Qmult_le_compat_r; auto with qarith. +Qed. + +Lemma Qmult_le_l (x y z: Q): 0 < z -> (z*x <= z*y <-> x <= y). +Proof. + rewrite (Qmult_comm z x), (Qmult_comm z y). + apply Qmult_le_r. +Qed. + Lemma Qmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x*z < y*z. Proof. intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. @@ -713,6 +846,30 @@ Proof. Close Scope Z_scope. Qed. +Lemma Qmult_lt_r: forall x y z, 0 < z -> (x*z < y*z <-> x < y). +Proof. + Open Scope Z_scope. + intros (a1,a2) (b1,b2) (c1,c2). + unfold Qle, Qlt; simpl. + simpl_mult. + replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring. + replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring. + assert (forall p, 0 < ' p) by reflexivity. + split; intros. + apply Zmult_lt_reg_r with (c1*'c2); auto with zarith. + apply Zmult_lt_0_compat; auto with zarith. + apply Zmult_lt_compat_r; auto with zarith. + apply Zmult_lt_0_compat. omega. + compute; auto. + Close Scope Z_scope. +Qed. + +Lemma Qmult_lt_l (x y z: Q): 0 < z -> (z*x < z*y <-> x < y). +Proof. + rewrite (Qmult_comm z x), (Qmult_comm z y). + apply Qmult_lt_r. +Qed. + Lemma Qmult_le_0_compat : forall a b, 0 <= a -> 0 <= b -> 0 <= a*b. Proof. intros a b Ha Hb. diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v index be894419..238de6fa 100644 --- a/theories/QArith/QOrderedType.v +++ b/theories/QArith/QOrderedType.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v index 747c2c3c..557fabc8 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -100,6 +100,13 @@ rewrite Zabs_Zmult. reflexivity. Qed. +Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x). +Proof. + unfold Qminus, Qopp. simpl. + rewrite Pmult_comm, <- Zabs_Zopp. + do 2 f_equal. ring. +Qed. + Lemma Qle_Qabs : forall a, a <= Qabs a. Proof. intros a. @@ -122,3 +129,31 @@ apply Qabs_triangle. apply Qabs_wd. ring. Qed. + +Lemma Qabs_Qle_condition x y: Qabs x <= y <-> -y <= x <= y. +Proof. + split. + split. + rewrite <- (Qopp_opp x). + apply Qopp_le_compat. + apply Qle_trans with (Qabs (-x)). + apply Qle_Qabs. + now rewrite Qabs_opp. + apply Qle_trans with (Qabs x); auto using Qle_Qabs. + intros (H,H'). + apply Qabs_case; trivial. + intros. rewrite <- (Qopp_opp y). now apply Qopp_le_compat. +Qed. + +Lemma Qabs_diff_Qle_condition x y r: Qabs (x - y) <= r <-> x - r <= y <= x + r. +Proof. + intros. unfold Qminus. + rewrite Qabs_Qle_condition. + rewrite <- (Qplus_le_l (-r) (x+-y) (y+r)). + rewrite <- (Qplus_le_l (x+-y) r (y-r)). + setoid_replace (-r + (y + r)) with y by ring. + setoid_replace (r + (y - r)) with y by ring. + setoid_replace (x + - y + (y + r)) with (x + r) by ring. + setoid_replace (x + - y + (y - r)) with (x - r) by ring. + intuition. +Qed. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 71a3b474..fea2ba39 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qcanon.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Field. Require Import QArith. Require Import Znumtheory. @@ -20,7 +18,7 @@ Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }. Delimit Scope Qc_scope with Qc. Bind Scope Qc_scope with Qc. -Arguments Scope Qcmake [Q_scope]. +Arguments Qcmake this%Q _. Open Scope Qc_scope. Lemma Qred_identity : @@ -71,7 +69,7 @@ Proof. Qed. Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). -Arguments Scope Q2Qc [Q_scope]. +Arguments Q2Qc q%Q. Notation " !! " := Q2Qc : Qc_scope. Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'. @@ -468,18 +466,16 @@ Proof. destruct n; simpl. destruct 1; auto. intros. - apply Qc_is_canon. - simpl. - compute; auto. + now apply Qc_is_canon. Qed. Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n. Proof. induction n; simpl; auto with qarith. - intros; compute; intro; discriminate. + easy. intros. apply Qcle_trans with (0*(p^n)). - compute; intro; discriminate. + easy. apply Qcmult_le_compat_r; auto. Qed. diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v index 81d59714..5e27f381 100644 --- a/theories/QArith/Qfield.v +++ b/theories/QArith/Qfield.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qfield.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export Field. Require Export QArith_base. Require Import NArithRing. diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v index a458fc6e..2da24ee6 100644 --- a/theories/QArith/Qminmax.v +++ b/theories/QArith/Qminmax.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -64,4 +64,4 @@ Proof. apply plus_min_distr_l. Qed. -End Q.
\ No newline at end of file +End Q. diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v index 9568c796..b05ee649 100644 --- a/theories/QArith/Qpower.v +++ b/theories/QArith/Qpower.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -136,9 +136,9 @@ Proof. intros a [|n|n] [|m|m] H; simpl; try ring; try rewrite Qpower_plus_positive; try apply Qinv_mult_distr; try reflexivity; -case_eq ((n ?= m)%positive Eq); intros H0; simpl; +rewrite ?Z.pos_sub_spec; +case Pos.compare_spec; intros H0; simpl; subst; try rewrite Qpower_minus_positive; - try rewrite (Pcompare_Eq_eq _ _ H0); try (field; try split; apply Qpower_not_0_positive); try assumption; apply ZC2; diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 8a0ebcff..24f6d720 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qreals.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export Rbase. Require Export QArith_base. @@ -210,4 +208,4 @@ intro; apply H; apply eqR_Qeq. rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real. Qed. -End LegacyQField.
\ No newline at end of file +End LegacyQField. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index eb8c1164..e39eca0c 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qreduction.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Normalisation functions for rational numbers. *) Require Export QArith_base. @@ -43,23 +41,16 @@ Definition Qred (q:Q) := Lemma Qred_correct : forall q, (Qred q) == q. Proof. unfold Qred, Qeq; intros (n,d); simpl. - generalize (Zggcd_gcd n ('d)) (Zgcd_is_pos n ('d)) - (Zgcd_is_gcd n ('d)) (Zggcd_correct_divisors n ('d)). + generalize (Zggcd_gcd n ('d)) (Zgcd_nonneg n ('d)) + (Zggcd_correct_divisors n ('d)). destruct (Zggcd n (Zpos d)) as (g,(nn,dd)); simpl. Open Scope Z_scope. - intuition. - rewrite <- H in H0,H1; clear H. - rewrite H3; rewrite H4. - assert (0 <> g). - intro; subst g; discriminate. - - assert (0 < dd). - apply Zmult_gt_0_lt_0_reg_r with g. - omega. - rewrite Zmult_comm. - rewrite <- H4; compute; auto. - rewrite Z2P_correct; auto. - ring. + intros Hg LE (Hn,Hd). rewrite Hd, Hn. + rewrite <- Hg in LE; clear Hg. + assert (0 <> g) by (intro; subst; discriminate). + rewrite Z2P_correct. ring. + apply Zmult_gt_0_lt_0_reg_r with g; auto with zarith. + now rewrite Zmult_comm, <- Hd. Close Scope Z_scope. Qed. @@ -69,10 +60,10 @@ Proof. unfold Qred, Qeq in *; simpl in *. Open Scope Z_scope. generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) - (Zgcd_is_pos a ('b)) (Zggcd_correct_divisors a ('b)). + (Zgcd_nonneg a ('b)) (Zggcd_correct_divisors a ('b)). destruct (Zggcd a (Zpos b)) as (g,(aa,bb)). generalize (Zggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) - (Zgcd_is_pos c ('d)) (Zggcd_correct_divisors c ('d)). + (Zgcd_nonneg c ('d)) (Zggcd_correct_divisors c ('d)). destruct (Zggcd c (Zpos d)) as (g',(cc,dd)). simpl. intro H; rewrite <- H; clear H. @@ -80,10 +71,9 @@ Proof. intro H; rewrite <- H; clear H. intros Hg1 Hg2 (Hg3,Hg4). intros. - assert (g <> 0). - intro; subst g; discriminate. - assert (g' <> 0). - intro; subst g'; discriminate. + assert (g <> 0) by (intro; subst g; discriminate). + assert (g' <> 0) by (intro; subst g'; discriminate). + elim (rel_prime_cross_prod aa bb cc dd). congruence. unfold rel_prime in |- *. @@ -93,14 +83,13 @@ Proof. exists bb; auto with zarith. intros. inversion Hg1. - destruct (H6 (g*x)). + destruct (H6 (g*x)) as (x',Hx). rewrite Hg3. destruct H2 as (xa,Hxa); exists xa; rewrite Hxa; ring. rewrite Hg4. destruct H3 as (xb,Hxb); exists xb; rewrite Hxb; ring. - exists q. - apply Zmult_reg_l with g; auto. - pattern g at 1; rewrite H7; ring. + exists x'. + apply Zmult_reg_l with g; auto. rewrite Hx at 1; ring. (* /rel_prime *) unfold rel_prime in |- *. (* rel_prime *) @@ -109,14 +98,13 @@ Proof. exists dd; auto with zarith. intros. inversion Hg'1. - destruct (H6 (g'*x)). + destruct (H6 (g'*x)) as (x',Hx). rewrite Hg'3. destruct H2 as (xc,Hxc); exists xc; rewrite Hxc; ring. rewrite Hg'4. destruct H3 as (xd,Hxd); exists xd; rewrite Hxd; ring. - exists q. - apply Zmult_reg_l with g'; auto. - pattern g' at 1; rewrite H7; ring. + exists x'. + apply Zmult_reg_l with g'; auto. rewrite Hx at 1; ring. (* /rel_prime *) assert (0<bb); [|auto with zarith]. apply Zmult_gt_0_lt_0_reg_r with g. diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v index 173136b8..c88a8141 100644 --- a/theories/QArith/Qring.v +++ b/theories/QArith/Qring.v @@ -1,11 +1,9 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qring.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export Qfield. diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index 01a97870..ce363a33 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -136,4 +136,15 @@ intros x y H. apply Zle_antisym. auto with *. symmetry in H; auto with *. -Qed.
\ No newline at end of file +Qed. + +Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (n / m). +Proof. + unfold Qfloor. intros. simpl. + destruct m as [?|?|p]; simpl. + now rewrite Zdiv_0_r, Zmult_0_r. + now rewrite Zmult_1_r. + rewrite <- Zopp_eq_mult_neg_1. + rewrite <- (Zopp_involutive (Zpos p)). + now rewrite Zdiv_opp_opp. +Qed. |