Merge branch 'trunk' into pr379

3 files changed, 27 insertions, 293 deletions

diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 2352d78d6..30e475b71 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -18,7 +18,7 @@ Require Import Refl.
 Require Import Raxioms RIneq Rpow_def DiscrR.
 Require Import QArith.
 Require Import Qfield.
-
+Require Import Qreals.
 
 Require Setoid.
 (*Declare ML Module "micromega_plugin".*)
@@ -38,15 +38,8 @@ Proof.
   exact Rplus_opp_r.
 Qed.
 
-Add Ring Rring : Rsrt.
 Open Scope R_scope.
 
-Lemma Rmult_neutral : forall x:R , 0 * x = 0.
-Proof.
-  intro ; ring.
-Qed.
-
-
 Lemma Rsor : SOR R0 R1 Rplus Rmult Rminus Ropp (@eq R)  Rle Rlt.
 Proof.
   constructor; intros ; subst ; try (intuition (subst; try ring ; auto with real)).
@@ -59,142 +52,41 @@ Proof.
   apply (Rlt_irrefl m) ; auto.
   apply Rnot_le_lt. auto with real.
   destruct (total_order_T n m) as [ [H1 | H1] | H1] ; auto.
-  intros.
-  rewrite <- (Rmult_neutral m).
-  apply (Rmult_lt_compat_r) ; auto.
-Qed.
-
-Definition IQR := fun x : Q => (IZR (Qnum x) * / IZR (' Qden x))%R.
-
-
-Lemma Rinv_elim : forall x y z, 
-  y <> 0 -> (z * y = x <->   x * / y = z).
-Proof.
-  intros.
-  split ; intros.
-  subst.
-  rewrite Rmult_assoc.
-  rewrite Rinv_r; auto.
-  ring.
-  subst.
-  rewrite Rmult_assoc.
-  rewrite (Rmult_comm (/ y)).
-  rewrite Rinv_r ; auto.
-  ring.
-Qed.  
-
-Ltac INR_nat_of_P :=
-  match goal with
-    | H : context[INR (Pos.to_nat ?X)] |- _ =>
-      revert H ; 
-      let HH := fresh in
-        assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (Pos.to_nat X))
-    | |- context[INR (Pos.to_nat ?X)] =>
-      let HH := fresh in
-        assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (Pos.to_nat X))
-  end.
-
-Ltac add_eq expr val := set (temp := expr) ; 
-  generalize (eq_refl temp) ;
-    unfold temp at 1 ; generalize temp ; intro val ; clear temp.
-
-Ltac Rinv_elim :=
-  match goal with
-    | |- context[?x * / ?y] => 
-      let z := fresh "v" in 
-      add_eq (x * / y) z  ;
-      let H := fresh in intro H ; rewrite <- Rinv_elim in H
-  end.
-
-Lemma Rlt_neq : forall r , 0 < r -> r <> 0.
-Proof.
-  red. intros.
-  subst.
-  apply (Rlt_irrefl 0 H).  
+  now apply Rmult_lt_0_compat.
 Qed.
 
+Notation IQR := Q2R (only parsing).
 
 Lemma Rinv_1 : forall x, x * / 1 = x.
 Proof.
   intro.
-  Rinv_elim.
-  subst ; ring.
-  apply R1_neq_R0.
+  rewrite Rinv_1.
+  apply Rmult_1_r.
 Qed.
 
-Lemma Qeq_true : forall x y,  
-  Qeq_bool x y = true -> 
-   IQR x = IQR y.
+Lemma Qeq_true : forall x y, Qeq_bool x y = true -> IQR x = IQR y.
 Proof.
-  unfold IQR.
-  simpl.
-  intros.
-  apply Qeq_bool_eq in H.
-  unfold Qeq in H.
-  assert (IZR (Qnum x * ' Qden y) = IZR (Qnum y * ' Qden x))%Z.
-     rewrite H. reflexivity.
-  repeat rewrite mult_IZR in H0.
-  simpl in H0.
-  revert H0.
-  repeat INR_nat_of_P.
   intros.
-  apply Rinv_elim in H2 ; [| apply Rlt_neq ; auto].
-  rewrite <- H2.
-  field.
-  split ; apply Rlt_neq ; auto.
+  now apply Qeq_eqR, Qeq_bool_eq.
 Qed.
 
 Lemma Qeq_false : forall x y, Qeq_bool x y = false -> IQR x <> IQR y.
 Proof.
   intros.
-  apply Qeq_bool_neq  in H.
-  intro. apply H.   clear H.
-  unfold Qeq,IQR in *.
-  simpl in *.
-  revert H0.
-  repeat Rinv_elim.
-  intros.
-  subst.
-  assert (IZR (Qnum x * ' Qden y)%Z = IZR (Qnum y * ' Qden x)%Z).
-  repeat rewrite mult_IZR.  
-  simpl.
-  rewrite <- H0. rewrite <- H.
-  ring.
-  apply eq_IZR ; auto.
-  INR_nat_of_P; intros; apply Rlt_neq ; auto. 
-  INR_nat_of_P; intros ; apply Rlt_neq ; auto. 
+  apply Qeq_bool_neq in H.
+  contradict H.
+  now apply eqR_Qeq.
 Qed.
 
-  
-
 Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> IQR x <= IQR y.
 Proof.
   intros.
-  apply Qle_bool_imp_le in H.
-  unfold Qle in H.
-  unfold IQR.
-  simpl in *.
-  apply IZR_le in H.
-  repeat rewrite mult_IZR in H.
-  simpl in H.
-  repeat INR_nat_of_P; intros.
-  assert (Hr := Rlt_neq r H).
-  assert (Hr0 := Rlt_neq r0 H0).
-  replace (IZR (Qnum x) * / r) with ((IZR (Qnum x) * r0) * (/r * /r0)).
-  replace (IZR (Qnum y) * / r0) with ((IZR (Qnum y) * r) * (/r * /r0)).
-  apply Rmult_le_compat_r ; auto.
-  apply Rmult_le_pos.
-  unfold Rle. left. apply Rinv_0_lt_compat ; auto.
-  unfold Rle. left. apply Rinv_0_lt_compat ; auto.
-  field ; intuition.
-  field ; intuition.
+  now apply Qle_Rle, Qle_bool_imp_le.
 Qed.
 
-
-
 Lemma IQR_0 : IQR 0 = 0.
 Proof.
-  compute. apply Rinv_1.
+  apply Rmult_0_l.
 Qed.
 
 Lemma IQR_1 : IQR 1 = 1.
@@ -202,160 +94,6 @@ Proof.
   compute. apply Rinv_1.
 Qed.
 
-Lemma IQR_plus : forall x y, IQR (x + y) = IQR x + IQR y.
-Proof.
-  intros.
-  unfold IQR.
-  simpl in *.
-  rewrite plus_IZR in *.
-  rewrite mult_IZR in *.
-  simpl.  
-  rewrite Pos2Nat.inj_mul.
-  rewrite mult_INR.
-  rewrite mult_IZR.
-  simpl.
-  repeat INR_nat_of_P.
-  intros. field. 
-  split ; apply Rlt_neq ; auto.
-Qed.
-
-Lemma IQR_opp : forall x, IQR (- x) = - IQR x.
-Proof.
-  intros.
-  unfold IQR.
-  simpl.
-  rewrite opp_IZR.
-  ring.  
-Qed.
-
-Lemma IQR_minus : forall x y, IQR (x - y) = IQR x - IQR y.
-Proof.
-  intros.
-  unfold Qminus.
-  rewrite IQR_plus.
-  rewrite IQR_opp.
-  ring.
-Qed.
-
-
-Lemma IQR_mult : forall x y, IQR (x * y) = IQR x * IQR y.
-Proof.
-  unfold IQR ; intros.
-  simpl.
-  repeat rewrite mult_IZR.
-  rewrite Pos2Nat.inj_mul.
-  rewrite mult_INR.
-  repeat INR_nat_of_P.
-  intros. field ; split ; apply Rlt_neq ; auto.
-Qed.
-
-Lemma IQR_inv_lt : forall x, (0 < x)%Q -> 
-  IQR (/ x) =  / IQR x.
-Proof.
-  unfold IQR ; simpl.
-  intros.
-  unfold Qlt in H.
-  revert H.
-  simpl.
-  intros.
-  unfold Qinv.
-  destruct x.
-  destruct Qnum ; simpl in *.
-  exfalso. auto with zarith.
-  clear H.
-  repeat INR_nat_of_P.
-  intros.
-  assert (HH := Rlt_neq _ H).
-  assert (HH0 := Rlt_neq _ H0).
-  rewrite Rinv_mult_distr ; auto.
-  rewrite Rinv_involutive ; auto.
-  ring.
-  apply Rinv_0_lt_compat in H0.
-  apply Rlt_neq ; auto.
-  simpl in H.
-  exfalso.
-  rewrite Pos.mul_comm  in H.
-  compute in H.
-  discriminate.
-Qed.
-
-Lemma Qinv_opp : forall x, (- (/ x) = / ( -x))%Q.
-Proof.
-  destruct x ; destruct Qnum ; reflexivity.
-Qed.
-
-Lemma Qopp_involutive_strong : forall x, (- - x = x)%Q.
-Proof.
-  intros.
-  destruct x.
-  unfold Qopp.
-  simpl.
-  rewrite Z.opp_involutive.
-  reflexivity.
-Qed.
-
-Lemma Ropp_0 : forall r , - r = 0 -> r = 0.
-Proof.
-  intros.
-  rewrite <- (Ropp_involutive r).
-  apply Ropp_eq_0_compat ; auto.
-Qed.
-
-Lemma IQR_x_0 : forall x, IQR x = 0 -> x == 0%Q.
-Proof.
-  destruct x ; simpl.
-  unfold IQR.
-  simpl.
-  INR_nat_of_P.
-  intros.
-  apply Rmult_integral in H0.  
-  destruct H0.
-  apply eq_IZR_R0 in H0.
-  subst.
-  reflexivity.
-  exfalso.
-  apply Rinv_0_lt_compat in H.
-  rewrite <- H0 in H.
-  apply Rlt_irrefl in H. auto.
-Qed.
-  
-
-Lemma IQR_inv_gt : forall x, (0 > x)%Q -> 
-  IQR (/ x) =  / IQR x.
-Proof.
-  intros.
-  rewrite <- (Qopp_involutive_strong x).
-  rewrite <- Qinv_opp.
-  rewrite IQR_opp.
-  rewrite IQR_inv_lt.
-  repeat rewrite IQR_opp.
-  rewrite Ropp_inv_permute.
-  auto.
-  intro.
-  apply Ropp_0 in H0.
-  apply IQR_x_0 in H0.
-  rewrite H0 in H.
-  compute in H. discriminate.
-  unfold Qlt in *.
-  destruct x ; simpl in *.
-  auto with zarith.
-Qed.
-
-Lemma IQR_inv : forall x, ~ x ==  0 -> 
-  IQR (/ x) =  / IQR x.
-Proof.
-  intros.
-  assert ( 0 > x \/ 0 < x)%Q.
-   destruct x ; unfold Qlt, Qeq in * ; simpl in *.
-   rewrite Z.mul_1_r in *.
-   destruct Qnum ; simpl in * ; intuition auto.
-   right. reflexivity.
-   left ; reflexivity.
-  destruct H0.
-  apply IQR_inv_gt ; auto.
-  apply IQR_inv_lt ; auto.
-Qed.
-
 Lemma IQR_inv_ext : forall x, 
   IQR (/ x) = (if Qeq_bool x 0 then 0 else / IQR x).
 Proof.
@@ -366,18 +104,13 @@ Proof.
   destruct x ; simpl.
   unfold Qeq in H.
   simpl in H.
-  replace Qnum with 0%Z.
-  compute. rewrite Rinv_1.
-  reflexivity.
-  rewrite <- H. ring.
+  rewrite Zmult_1_r in H.
+  rewrite H.
+  apply Rmult_0_l.
   intros.
-  apply IQR_inv.
-  intro.
-  rewrite <- Qeq_bool_iff in H0.
-  congruence.
+  now apply Q2R_inv, Qeq_bool_neq.
 Qed.
 
-
 Notation to_nat := N.to_nat.
 
 Lemma QSORaddon :
@@ -391,10 +124,10 @@ Proof.
   constructor ; intros ; try reflexivity.
   apply IQR_0.
   apply IQR_1.
-  apply IQR_plus.
-  apply IQR_minus.
-  apply IQR_mult.
-  apply IQR_opp.
+  apply Q2R_plus.
+  apply Q2R_minus.
+  apply Q2R_mult.
+  apply Q2R_opp.
   apply Qeq_true ; auto.
   apply R_power_theory.
   apply Qeq_false.
@@ -453,13 +186,13 @@ Proof.
     apply IQR_1. 
     reflexivity.
     unfold IQR. simpl. rewrite Rinv_1. reflexivity.
-    apply IQR_plus.
-    apply IQR_minus.
-    apply IQR_mult.
+    apply Q2R_plus.
+    apply Q2R_minus.
+    apply Q2R_mult.
     rewrite <- IHc.
     apply IQR_inv_ext.
     rewrite <- IHc.
-    apply IQR_opp.
+    apply Q2R_opp.
   Qed.
 
 Require Import EnvRing.
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 5b56fb35b..4b87e6e2e 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -368,6 +368,7 @@ struct
     [["Coq";"Reals" ; "Rdefinitions"];
      ["Coq";"Reals" ; "Rpow_def"] ;
      ["Coq";"Reals" ; "Raxioms"] ;
+     ["Coq";"QArith"; "Qreals"] ;
     ]
 
   let z_modules = [["Coq";"ZArith";"BinInt"]]
@@ -388,7 +389,6 @@ struct
   let coq_and = lazy (init_constant "and")
   let coq_or = lazy (init_constant "or")
   let coq_not = lazy (init_constant "not")
-  let coq_not_gl_ref = (Nametab.locate (  Libnames.qualid_of_string "Coq.Init.Logic.not"))
 
   let coq_iff = lazy (init_constant "iff")
   let coq_True = lazy (init_constant "True")
@@ -485,7 +485,7 @@ struct
   let coq_Rinv = lazy (r_constant "Rinv")
   let coq_Rpower = lazy (r_constant "pow")
   let coq_IZR    = lazy (r_constant "IZR")
-  let coq_IQR    = lazy (constant "IQR")
+  let coq_IQR    = lazy (r_constant "Q2R")
 
 
   let coq_PEX = lazy (constant "PEX" )
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 79020ed03..ccb6daa11 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -16,6 +16,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Stdarg
 open Tacarg