diff options
Diffstat (limited to 'theories/QArith/Qreals.v')
| -rw-r--r-- | theories/QArith/Qreals.v | 33 |
1 files changed, 6 insertions, 27 deletions
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 029ae8e3..add43b96 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-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -14,6 +14,7 @@ Require Export QArith_base. Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R. Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R. +Proof. intros; apply not_O_IZR; auto with qarith. Qed. @@ -162,19 +163,19 @@ field; auto. Qed. Lemma Q2R_minus : forall x y : Q, Q2R (x-y) = (Q2R x - Q2R y)%R. +Proof. 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; intros (x1, x2); unfold Qden, Qnum. -case x1. +unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden. simpl; intros; elim H; trivial. -intros; field; auto. +intros; field; auto. intros; change (IZR (Zneg x2)) with (- IZR (' x2))%R; change (IZR (Zneg p)) with (- IZR (' p))%R; - field; (*auto 8 with real.*) + simpl; field; (*auto 8 with real.*) repeat split; auto; auto with real. Qed. @@ -187,25 +188,3 @@ rewrite Q2R_inv; auto. Qed. Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl. - -Section LegacyQField. - -(** In the past, the field tactic was not able to deal with setoid datatypes, - so translating from Q to R and applying field on reals was a workaround. - See now Qfield for a direct field tactic on Q. *) - -Ltac QField := apply eqR_Qeq; autorewrite with q2r_simpl; try field; auto. - -(** Examples of use: *) - -Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z). -intros; QField. -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; simpl; field; auto with real. -Qed. - -End LegacyQField. |