From 0a235f0d6ed807600ccf5534af7ed6f8657d1274 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 21 Sep 2006 12:07:32 +0000 Subject: better scope/require managment (patch by Russel O'Connor) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9155 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/QArith/QArith_base.v | 24 ++++++++++++------------ theories/QArith/Qcanon.v | 1 + theories/QArith/Qreduction.v | 5 +++-- 3 files changed, 16 insertions(+), 14 deletions(-) diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 4354b5f95c..f22f12a4c0 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -173,7 +173,7 @@ rewrite H. replace ('s2 * ('q2 * r1)) with (r1 * 's2 * 'q2) by ring. rewrite H0. ring. -Open Scope Q_scope. +Close Scope Z_scope. Qed. Add Morphism Qopp : Qopp_comp. @@ -200,7 +200,7 @@ rewrite <- H. replace ('s2 * ('q2 * r1)) with (r1 * 's2 * 'q2) by ring. rewrite H0. ring. -Open Scope Q_scope. +Close Scope Z_scope. Qed. Add Morphism Qinv : Qinv_comp. @@ -218,7 +218,7 @@ 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. -Open Scope Q_scope. +Close Scope Z_scope. Qed. Add Morphism Qdiv : Qdiv_comp. @@ -246,7 +246,7 @@ rewrite <- H0. replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring. replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring. auto with zarith. -Open Scope Q_scope. +Close Scope Z_scope. Qed. Add Morphism Qlt with signature Qeq ==> Qeq ==> iff as Qlt_comp. @@ -269,7 +269,7 @@ replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring. replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring. apply Zlt_gt. apply Zmult_gt_0_lt_compat_l; auto with zarith. -Open Scope Q_scope. +Close Scope Z_scope. Qed. @@ -455,7 +455,7 @@ 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. -Open Scope Q_scope. +Close Scope Z_scope. Qed. Lemma Qlt_not_eq : forall x y, x ~ x==y. @@ -483,7 +483,7 @@ 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. -Open Scope Q_scope. +Close Scope Z_scope. Qed. Lemma Qlt_le_trans : forall x y z, x y<=z -> x y x 0 <= z -> x*z <= y*z. @@ -598,7 +598,7 @@ 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. -Open Scope Q_scope. +Close Scope Z_scope. Qed. Lemma Qmult_lt_0_le_reg_r : forall x y z, 0 < z -> x*z <= y*z -> x <= y. @@ -609,7 +609,7 @@ 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. -Open Scope Q_scope. +Close Scope Z_scope. Qed. Lemma Qmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x*z < y*z. @@ -623,7 +623,7 @@ apply Zmult_lt_compat_r; auto with zarith. apply Zmult_lt_0_compat. omega. compute; auto. -Open Scope Q_scope. +Close Scope Z_scope. Qed. (** Rational to the n-th power *) diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index bc87e05d3c..026e850ea0 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -9,6 +9,7 @@ (*i $Id$ i*) Require Import QArith. +Require Import Znumtheory. Require Import Eqdep_dec. (** [Qc] : A canonical representation of rational numbers. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 41e0d9a456..657a00ed5b 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -11,7 +11,7 @@ (** * Normalisation functions for rational numbers. *) Require Export QArith_base. -Require Export Znumtheory. +Require Import Znumtheory. (** First, a function that (tries to) build a positive back from a Z. *) @@ -60,6 +60,7 @@ assert (0 < dd). rewrite <- H4; compute; auto. rewrite Z2P_correct; auto. ring. +Close Scope Z_scope. Qed. Lemma Qred_complete : forall p q, p==q -> Qred p = Qred q. @@ -132,7 +133,7 @@ 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. -Open Scope Q_scope. +Close Scope Z_scope. Qed. Add Morphism Qred : Qred_comp. -- cgit v1.2.3