Small cleanup

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9996 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 31 insertions, 17 deletions

diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
index 4d8a80611..f54a6c286 100644
--- a/theories/QArith/Qfield.v
+++ b/theories/QArith/Qfield.v
@@ -12,7 +12,7 @@ Require Export Field.
 Require Export QArith_base.
 Require Import NArithRing.
 
-(** * A ring tactic for rational numbers *)
+(** * field and ring tactics for rational numbers *)
 
 Definition Qeq_bool (x y : Q) :=
   if Qeq_dec x y then true else false.
@@ -23,6 +23,11 @@ Proof.
   intros _ H; inversion H.
 Qed.
 
+Lemma Qeq_bool_complete : forall x y : Q, x==y -> Qeq_bool x y = true.
+Proof.
+  intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
+Qed.
+
 Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq.
 Proof.
   constructor.
@@ -77,7 +82,12 @@ Ltac Qpow_tac t :=
   | _ => NotConstant
   end.
 
-Add Field Qfield : Qsft(decidable Qeq_bool_correct, constants [Qcst], power_tac Qpower_theory [Qpow_tac]).
+Add Field Qfield : Qsft 
+ (decidable Qeq_bool_correct, 
+  completeness Qeq_bool_complete,
+  constants [Qcst], 
+  power_tac Qpower_theory [Qpow_tac]).
+
 (** Exemple of use: *)
 
 Section Examples. 
@@ -109,7 +119,7 @@ Let ex6 : (1#1)+(1#1) == 2#1.
   ring.
 Qed.
 
-Let ex7 : forall x : Q, x-x== 0#1.
+Let ex7 : forall x : Q, x-x== 0.
   intro.
   ring.
 Qed.
@@ -124,7 +134,7 @@ Let ex9 : forall x : Q, x^0 == 1.
   ring.
 Qed.
 
-Example test_field : forall x y : Q, ~(y==0) -> (x/y)*y == x.
+Let ex10 : forall x y : Q, ~(y==0) -> (x/y)*y == x.
 intros.
 field.
 auto.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 1b6b4722b..d57a8c824 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -11,19 +11,15 @@
 Require Export Rbase.
 Require Export QArith_base.
 
-(** A field tactic for rational numbers. *)
+(** Injection of rational numbers into real numbers. *)
 
-(** Since field cannot operate on setoid datatypes (yet?), 
-  we translate Q goals into reals before applying field. *)
+Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R.
 
 Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R.
 intros; apply not_O_IZR; auto with qarith.
 Qed.
 
-Hint Immediate IZR_nz.
-Hint Resolve Rmult_integral_contrapositive.
-
-Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R.
+Hint Resolve IZR_nz Rmult_integral_contrapositive.
 
 Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y.
 Proof.
@@ -171,7 +167,7 @@ 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.
 Qed.
 
-Lemma Q2R_inv : forall x : Q, ~ x==0#1 -> Q2R (/x) = (/ Q2R x)%R.
+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 |- *.
 case x1.
@@ -185,7 +181,7 @@ intros;
 Qed.
 
 Lemma Q2R_div :
- forall x y : Q, ~ y==0#1 -> Q2R (x/y) = (Q2R x / Q2R y)%R.
+ forall x y : Q, ~ y==0 -> Q2R (x/y) = (Q2R x / Q2R y)%R.
 Proof.
 unfold Qdiv, Rdiv in |- *.
 intros; rewrite Q2R_mult.
@@ -194,16 +190,24 @@ 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: *)
 
-Goal forall x y z : Q, (x+y)*z == (x*z)+(y*z).
+Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z).
 intros; QField.
-Abort.
+Qed.
 
-Goal forall x y : Q, ~ y==0#1 -> (x/y)*y == x.
+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.
-Abort.
+Qed.
+
+End LegacyQField.
\ No newline at end of file