From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 plugins/micromega/RMicromega.v | 325 ++++-------------------------------------
 1 file changed, 30 insertions(+), 295 deletions(-)

(limited to 'plugins/micromega/RMicromega.v')

diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 2352d78d..c2b40c73 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
@@ -18,7 +20,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 +40,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 +54,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 +96,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 +106,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 +126,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 +188,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.
-- 
cgit v1.2.3