Add some hints to the "real" database to automatically discharge literal comparisons.

3 files changed, 15 insertions, 17 deletions

diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 05911cd53..7f26c1b86 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -22,11 +22,6 @@ Proof.
 intros; rewrite H; reflexivity.
 Qed.
 
-Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2.
-Proof.
-intros; red; intro; elim H; apply eq_IZR; assumption.
-Qed.
-
 Ltac discrR :=
   try
    match goal with
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 7e1cc3e03..711703ad7 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1926,6 +1926,17 @@ Proof.
   omega.
 Qed.
 
+Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2.
+Proof.
+intros; red; intro; elim H; apply eq_IZR; assumption.
+Qed.
+
+Hint Extern 0 (IZR _ <= IZR _) => apply IZR_le, Zle_bool_imp_le, eq_refl : real.
+Hint Extern 0 (IZR _ >= IZR _) => apply Rle_ge, IZR_le, Zle_bool_imp_le, eq_refl : real.
+Hint Extern 0 (IZR _ <  IZR _) => apply IZR_lt, eq_refl : real.
+Hint Extern 0 (IZR _ >  IZR _) => apply IZR_lt, eq_refl : real.
+Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : real.
+
 Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z.
 Proof.
   intros z [H1 H2].
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index f9da88aad..ccb4207ba 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -15,6 +15,7 @@ Require Import RiemannInt.
 Require Import SeqProp.
 Require Import Max.
 Require Import Omega.
+Require Import Lra.
 Local Open Scope R_scope.
 
 (** * Preliminaries lemmas *)
@@ -245,14 +246,8 @@ Lemma IVT_interv_prelim0 : forall (x y:R) (P:R->bool) (N:nat),
        x <= Dichotomy_ub x y P N <= y /\ x <= Dichotomy_lb x y P N <= y.
 Proof.
 assert (Sublemma : forall x y lb ub, lb <= x <= ub /\ lb <= y <= ub -> lb <= (x+y) / 2 <= ub).
- intros x y lb ub Hyp.
-  split.
-  replace lb with ((lb + lb) * /2) by field.
-  unfold Rdiv ; apply Rmult_le_compat_r ; intuition.
-  now apply Rlt_le, Rinv_0_lt_compat, IZR_lt.
-  replace ub with ((ub + ub) * /2) by field.
-  unfold Rdiv ; apply Rmult_le_compat_r ; intuition.
-  now apply Rlt_le, Rinv_0_lt_compat, IZR_lt.
+  intros x y lb ub Hyp.
+  lra.
 intros x y P N x_lt_y.
 induction N.
  simpl ; intuition.
@@ -1029,10 +1024,7 @@ Qed.
 Lemma ub_lt_2_pos : forall x ub lb, lb < x -> x < ub -> 0 < (ub-lb)/2.
 Proof.
 intros x ub lb lb_lt_x x_lt_ub.
- assert (T : 0 < ub - lb).
-  fourier.
- unfold Rdiv ; apply Rlt_mult_inv_pos ; intuition.
-now apply IZR_lt.
+lra.
 Qed.
 
 Definition mkposreal_lb_ub (x lb ub:R) (lb_lt_x:lb<x) (x_lt_ub:x<ub) : posreal.