From 177c8fbc523a171e8c8470fa675f9a69ef7f99de Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 8 Mar 2017 08:35:29 +0100
Subject: Adapt proofs to future handling of literal constants in Coq.

This commit is mainly a squash of the relevant compatibility commits from
Flocq's master. Most of the changes are meant to make the proofs oblivious
to the way constants such as 0, 1, 2, and -1 are represented.
---
 flocq/Appli/Fappli_IEEE.v         | 10 +++---
 flocq/Appli/Fappli_double_round.v | 30 ++++++++++--------
 flocq/Appli/Fappli_rnd_odd.v      | 67 +++++++++++++++------------------------
 flocq/Core/Fcore_FLT.v            |  2 +-
 flocq/Core/Fcore_FTZ.v            |  8 ++---
 flocq/Core/Fcore_Raux.v           | 56 ++++++++++++++++----------------
 flocq/Core/Fcore_float_prop.v     |  4 +--
 flocq/Core/Fcore_generic_fmt.v    | 34 ++++++++++----------
 flocq/Core/Fcore_rnd_ne.v         |  2 +-
 flocq/Core/Fcore_ulp.v            | 21 +++---------
 flocq/Prop/Fprop_Sterbenz.v       |  2 +-
 flocq/Prop/Fprop_div_sqrt_error.v |  9 +++---
 flocq/Prop/Fprop_plus_error.v     |  6 ++--
 flocq/Prop/Fprop_relative.v       | 13 ++++----
 14 files changed, 119 insertions(+), 145 deletions(-)

(limited to 'flocq')

diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v
index 6400304b..b6ccd84f 100644
--- a/flocq/Appli/Fappli_IEEE.v
+++ b/flocq/Appli/Fappli_IEEE.v
@@ -39,7 +39,7 @@ Inductive full_float :=
 Definition FF2R beta x :=
   match x with
   | F754_finite s m e => F2R (Float beta (cond_Zopp s (Zpos m)) e)
-  | _ => R0
+  | _ => 0%R
   end.
 
 End AnyRadix.
@@ -104,7 +104,7 @@ Definition B2FF x :=
 Definition B2R f :=
   match f with
   | B754_finite s m e _ => F2R (Float radix2 (cond_Zopp s (Zpos m)) e)
-  | _ => R0
+  | _ => 0%R
   end.
 
 Theorem FF2R_B2FF :
@@ -346,11 +346,11 @@ Proof.
 intros. destruct x, y; try (apply B2R_inj; now eauto).
 - simpl in H2. congruence.
 - symmetry in H1. apply Rmult_integral in H1.
-  destruct H1. apply eq_Z2R with (n:=0%Z) in H1. destruct b0; discriminate H1.
+  destruct H1. apply (eq_Z2R _ 0) in H1. destruct b0; discriminate H1.
   simpl in H1. pose proof (bpow_gt_0 radix2 e).
   rewrite H1 in H3. apply Rlt_irrefl in H3. destruct H3.
 - apply Rmult_integral in H1.
-  destruct H1. apply eq_Z2R with (n:=0%Z) in H1. destruct b; discriminate H1.
+  destruct H1. apply (eq_Z2R _ 0) in H1. destruct b; discriminate H1.
   simpl in H1. pose proof (bpow_gt_0 radix2 e).
   rewrite H1 in H3. apply Rlt_irrefl in H3. destruct H3.
 Qed.
@@ -1714,7 +1714,7 @@ Definition Bdiv div_nan m x y :=
 
 Theorem Bdiv_correct :
   forall div_nan m x y,
-  B2R y <> R0 ->
+  B2R y <> 0%R ->
   if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x / B2R y))) (bpow radix2 emax) then
     B2R (Bdiv div_nan m x y) = round radix2 fexp (round_mode m) (B2R x / B2R y) /\
     is_finite (Bdiv div_nan m x y) = is_finite x /\
diff --git a/flocq/Appli/Fappli_double_round.v b/flocq/Appli/Fappli_double_round.v
index 3ff6c31a..2c4937ab 100644
--- a/flocq/Appli/Fappli_double_round.v
+++ b/flocq/Appli/Fappli_double_round.v
@@ -183,8 +183,8 @@ destruct (Req_dec x' 0) as [Zx'|Nzx'].
   apply Rplus_le_compat_r.
   apply (Rmult_le_reg_r (bpow (- ln_beta x))); [now apply bpow_gt_0|].
   unfold ulp, canonic_exp; bpow_simplify.
-  rewrite <- (Rinv_r 2) at 3; [|lra].
-  rewrite Rmult_comm; apply Rmult_le_compat_r; [lra|].
+  apply Rmult_le_reg_l with (1 := Rlt_0_2).
+  replace (2 * (/ 2 * _)) with (bpow (fexp1 (ln_beta x) - ln_beta x)) by field.
   apply Rle_trans with 1; [|lra].
   change 1 with (bpow 0); apply bpow_le.
   omega.
@@ -1037,10 +1037,11 @@ destruct Hexp as (_,(_,(_,Hexp4))).
 assert (Hf2 : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z);
   [now apply Hexp4; omega|].
 assert (Bpow2 : bpow (- 2) <= / 2 * / 2).
-{ unfold Fcore_Raux.bpow, Z.pow_pos; simpl.
-  rewrite <- Rinv_mult_distr; [|lra|lra].
+{ replace (/2 * /2) with (/4) by field.
+  rewrite (bpow_opp _ 2).
   apply Rinv_le; [lra|].
-  change 4 with (Z2R (2 * 2)); apply Z2R_le; rewrite Zmult_1_r.
+  apply (Z2R_le (2 * 2) (beta * (beta * 1))).
+  rewrite Zmult_1_r.
   now apply Zmult_le_compat; omega. }
 assert (P2 : (0 < 2)%Z) by omega.
 unfold double_round_eq.
@@ -1384,10 +1385,11 @@ assert (Hf2 : (fexp2 (ln_beta x) <= fexp1 (ln_beta x))%Z);
 assert (Hfx : (fexp1 (ln_beta x) < ln_beta x)%Z);
   [now apply ln_beta_generic_gt; [|apply Rgt_not_eq|]|].
 assert (Bpow2 : bpow (- 2) <= / 2 * / 2).
-{ unfold Fcore_Raux.bpow, Z.pow_pos; simpl.
-  rewrite <- Rinv_mult_distr; [|lra|lra].
+{ replace (/2 * /2) with (/4) by field.
+  rewrite (bpow_opp _ 2).
   apply Rinv_le; [lra|].
-  change 4 with (Z2R (2 * 2)); apply Z2R_le; rewrite Zmult_1_r.
+  apply (Z2R_le (2 * 2) (beta * (beta * 1))).
+  rewrite Zmult_1_r.
   now apply Zmult_le_compat; omega. }
 assert (Ly : y < bpow (ln_beta y)).
 { apply Rabs_lt_inv.
@@ -1449,7 +1451,7 @@ apply double_round_gt_mid.
     unfold canonic_exp.
     apply (Rplus_le_reg_r (bpow (fexp2 (ln_beta (x - y))))); ring_simplify.
     apply Rle_trans with (2 * bpow (fexp1 (ln_beta (x - y)) - 1)).
-    * rewrite Rmult_plus_distr_r; rewrite Rmult_1_l.
+    * replace (2 * bpow (fexp1 (ln_beta (x - y)) - 1)) with (bpow (fexp1 (ln_beta (x - y)) - 1) + bpow (fexp1 (ln_beta (x - y)) - 1)) by ring.
       apply Rplus_le_compat_l.
       now apply bpow_le.
     * unfold Zminus; rewrite bpow_plus.
@@ -1458,10 +1460,10 @@ apply double_round_gt_mid.
       apply Rmult_le_compat_l; [now apply bpow_ge_0|].
       unfold Fcore_Raux.bpow, Z.pow_pos; simpl.
       rewrite Zmult_1_r.
-      rewrite <- (Rinv_r 2) at 3; [|lra].
-      rewrite Rmult_comm; apply Rmult_le_compat_l; [lra|].
-      apply Rinv_le; [lra|].
-      now change 2 with (Z2R 2); apply Z2R_le.
+      apply Z2R_le, Rinv_le in Hbeta.
+      simpl in Hbeta.
+      lra.
+      apply Rlt_0_2.
 Qed.
 
 (* double_round_minus_aux{0,1,2} together *)
@@ -4220,7 +4222,7 @@ destruct (Zle_or_lt Z0 (fexp1 (ln_beta x) - fexp1 (ln_beta (x / y))
     bpow_simplify.
     rewrite (Rmult_comm _ y).
     do 2 rewrite Rmult_assoc.
-    change (Z2R _ * _) with x'.
+    change (Z2R (Zfloor _) * _) with x'.
     change (bpow _) with u1.
     apply (Rmult_lt_reg_l (/ 2)); [lra|].
     rewrite Rmult_plus_distr_l.
diff --git a/flocq/Appli/Fappli_rnd_odd.v b/flocq/Appli/Fappli_rnd_odd.v
index 4741047f..b6d985ac 100644
--- a/flocq/Appli/Fappli_rnd_odd.v
+++ b/flocq/Appli/Fappli_rnd_odd.v
@@ -20,7 +20,7 @@ COPYING file for more details.
 (** * Rounding to odd and its properties, including the equivalence
       between rnd_NE and double rounding with rnd_odd and then rnd_NE *)
 
-
+Require Import Reals Psatz.
 Require Import Fcore.
 Require Import Fcalc_ops.
 
@@ -577,29 +577,23 @@ Qed.
 
 
 Lemma d_le_m: (F2R d <= m)%R.
-apply Rmult_le_reg_l with 2%R.
-auto with real.
-apply Rplus_le_reg_l with (-F2R d)%R.
-apply Rle_trans with (F2R d).
-right; ring.
-apply Rle_trans with (F2R u).
-apply Rle_trans with x.
-apply Hd.
-apply Hu.
-right; unfold m; field.
+Proof.
+assert (F2R d <= F2R u)%R.
+  apply Rle_trans with x.
+  apply Hd.
+  apply Hu.
+unfold m.
+lra.
 Qed.
 
 Lemma m_le_u: (m <= F2R u)%R.
-apply Rmult_le_reg_l with 2%R.
-auto with real.
-apply Rplus_le_reg_l with (-F2R u)%R.
-apply Rle_trans with (F2R d).
-right; unfold m; field.
-apply Rle_trans with (F2R u).
-apply Rle_trans with x.
-apply Hd.
-apply Hu.
-right; ring.
+Proof.
+assert (F2R d <= F2R u)%R.
+  apply Rle_trans with x.
+  apply Hd.
+  apply Hu.
+unfold m.
+lra.
 Qed.
 
 Lemma ln_beta_m: (0 < F2R d)%R -> (ln_beta beta m =ln_beta beta (F2R d) :>Z).
@@ -641,20 +635,13 @@ now apply Rgt_not_eq.
 now apply generic_format_canonic.
 now left.
 replace m with (F2R d).
-destruct  (ln_beta beta (F2R d)) as (e,He).
+destruct (ln_beta beta (F2R d)) as (e,He).
 simpl in *; rewrite Rabs_right in He.
 apply He.
 now apply Rgt_not_eq.
 apply Rle_ge; now left.
-assert (F2R d = F2R u).
-apply Rmult_eq_reg_l with (/2)%R.
-apply Rplus_eq_reg_l with (/2*F2R u)%R.
-apply trans_eq with m.
-unfold m, Rdiv; ring.
-rewrite H; field.
-auto with real.
-apply Rgt_not_eq, Rlt_gt; auto with real.
-unfold m; rewrite <- H0; field.
+unfold m in H |- *.
+lra.
 Qed.
 
 
@@ -666,7 +653,7 @@ apply ln_beta_unique_pos.
 unfold m; rewrite <- Y, Rplus_0_l.
 rewrite u_eq.
 destruct (ln_beta beta x) as (e,He).
-rewrite Rabs_right in He.
+rewrite Rabs_pos_eq in He by now apply Rlt_le.
 rewrite round_UP_small_pos with (ex:=e).
 rewrite ln_beta_bpow.
 ring_simplify (fexp e + 1 - 1)%Z.
@@ -676,7 +663,7 @@ unfold Rdiv; apply Rmult_le_compat_l.
 apply bpow_ge_0.
 simpl; unfold Z.pow_pos; simpl.
 rewrite Zmult_1_r; apply Rinv_le.
-auto with real.
+exact Rlt_0_2.
 apply (Z2R_le 2).
 specialize (radix_gt_1 beta).
 omega.
@@ -684,13 +671,11 @@ apply Rlt_le_trans with (bpow (fexp e)*1)%R.
 2: right; ring.
 unfold Rdiv; apply Rmult_lt_compat_l.
 apply bpow_gt_0.
-rewrite <- Rinv_1 at 3.
-apply Rinv_lt; auto with real.
+lra.
 now apply He, Rgt_not_eq.
 apply exp_small_round_0_pos with beta (Zfloor) x...
 now apply He, Rgt_not_eq.
 now rewrite <- d_eq, Y.
-now left.
 Qed.
 
 
@@ -723,9 +708,8 @@ unfold Rdiv; apply f_equal.
 unfold F2R; simpl; unfold Z.pow_pos; simpl.
 rewrite Zmult_1_r, Hb, Z2R_mult.
 simpl; field.
-apply Rgt_not_eq, Rmult_lt_reg_l with (Z2R 2).
-simpl; auto with real.
-rewrite Rmult_0_r, <-Z2R_mult, <-Hb.
+apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2).
+rewrite Rmult_0_r, <- (Z2R_mult 2), <-Hb.
 apply radix_pos.
 apply trans_eq with (-1+Fexp (Fplus beta d u'))%Z.
 unfold Fmult.
@@ -752,9 +736,8 @@ unfold Rdiv; apply f_equal.
 unfold F2R; simpl; unfold Z.pow_pos; simpl.
 rewrite Zmult_1_r, Hb, Z2R_mult.
 simpl; field.
-apply Rgt_not_eq, Rmult_lt_reg_l with (Z2R 2).
-simpl; auto with real.
-rewrite Rmult_0_r, <-Z2R_mult, <-Hb.
+apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2).
+rewrite Rmult_0_r, <- (Z2R_mult 2), <-Hb.
 apply radix_pos.
 apply trans_eq with (-1+Fexp u)%Z.
 unfold Fmult.
diff --git a/flocq/Core/Fcore_FLT.v b/flocq/Core/Fcore_FLT.v
index 372af6ad..53dc48a7 100644
--- a/flocq/Core/Fcore_FLT.v
+++ b/flocq/Core/Fcore_FLT.v
@@ -187,7 +187,7 @@ Qed.
 
 (** Links between FLT and FIX (underflow) *)
 Theorem canonic_exp_FLT_FIX :
-  forall x, x <> R0 ->
+  forall x, x <> 0%R ->
   (Rabs x < bpow (emin + prec))%R ->
   canonic_exp beta FLT_exp x = canonic_exp beta (FIX_exp emin) x.
 Proof.
diff --git a/flocq/Core/Fcore_FTZ.v b/flocq/Core/Fcore_FTZ.v
index 2ebc7851..a2fab00b 100644
--- a/flocq/Core/Fcore_FTZ.v
+++ b/flocq/Core/Fcore_FTZ.v
@@ -217,7 +217,7 @@ Variable rnd : R -> Z.
 Context { valid_rnd : Valid_rnd rnd }.
 
 Definition Zrnd_FTZ x :=
-  if Rle_bool R1 (Rabs x) then rnd x else Z0.
+  if Rle_bool 1 (Rabs x) then rnd x else Z0.
 
 Global Instance valid_rnd_FTZ : Valid_rnd Zrnd_FTZ.
 Proof with auto with typeclass_instances.
@@ -270,7 +270,7 @@ Proof.
 intros x Hx.
 unfold round, scaled_mantissa, canonic_exp.
 destruct (ln_beta beta x) as (ex, He). simpl.
-assert (Hx0: x <> R0).
+assert (Hx0: x <> 0%R).
 intros Hx0.
 apply Rle_not_lt with (1 := Hx).
 rewrite Hx0, Rabs_R0.
@@ -286,7 +286,7 @@ rewrite Rle_bool_true.
 apply refl_equal.
 rewrite Rabs_mult.
 rewrite (Rabs_pos_eq (bpow (- FLX_exp prec ex))).
-change R1 with (bpow 0).
+change 1%R with (bpow 0).
 rewrite <- (Zplus_opp_r (FLX_exp prec ex)).
 rewrite bpow_plus.
 apply Rmult_le_compat_r.
@@ -320,7 +320,7 @@ rewrite Rle_bool_false.
 apply F2R_0.
 rewrite Rabs_mult.
 rewrite (Rabs_pos_eq (bpow (- FTZ_exp ex))).
-change R1 with (bpow 0).
+change 1%R with (bpow 0).
 rewrite <- (Zplus_opp_r (FTZ_exp ex)).
 rewrite bpow_plus.
 apply Rmult_lt_compat_r.
diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v
index 939002cf..44db6c35 100644
--- a/flocq/Core/Fcore_Raux.v
+++ b/flocq/Core/Fcore_Raux.v
@@ -403,7 +403,7 @@ Definition Z2R n :=
   match n with
   | Zpos p => P2R p
   | Zneg p => Ropp (P2R p)
-  | Z0 => R0
+  | Z0 => 0%R
   end.
 
 Theorem P2R_INR :
@@ -432,10 +432,13 @@ Theorem Z2R_IZR :
   forall n, Z2R n = IZR n.
 Proof.
 intro.
-case n ; intros ; simpl.
+case n ; intros ; unfold Z2R.
 apply refl_equal.
+rewrite <- positive_nat_Z, <- INR_IZR_INZ.
 apply P2R_INR.
+change (IZR (Zneg p)) with (Ropp (IZR (Zpos p))).
 apply Ropp_eq_compat.
+rewrite <- positive_nat_Z, <- INR_IZR_INZ.
 apply P2R_INR.
 Qed.
 
@@ -1193,7 +1196,7 @@ unfold Ztrunc.
 case Rlt_bool_spec ; intro H.
 apply refl_equal.
 rewrite (Rle_antisym _ _ Hx H).
-fold (Z2R 0).
+change 0%R with (Z2R 0).
 rewrite Zceil_Z2R.
 apply Zfloor_Z2R.
 Qed.
@@ -1304,7 +1307,7 @@ unfold Zaway.
 case Rlt_bool_spec ; intro H.
 apply refl_equal.
 rewrite (Rle_antisym _ _ Hx H).
-fold (Z2R 0).
+change 0%R with (Z2R 0).
 rewrite Zfloor_Z2R.
 apply Zceil_Z2R.
 Qed.
@@ -1456,7 +1459,7 @@ Definition bpow e :=
   match e with
   | Zpos p => Z2R (Zpower_pos r p)
   | Zneg p => Rinv (Z2R (Zpower_pos r p))
-  | Z0 => R1
+  | Z0 => 1%R
   end.
 
 Theorem Z2R_Zpower_pos :
@@ -1532,13 +1535,13 @@ Qed.
 Theorem bpow_opp :
   forall e : Z, (bpow (-e) = /bpow e)%R.
 Proof.
-intros e; destruct e.
-simpl; now rewrite Rinv_1.
-now replace (-Zpos p)%Z with (Zneg p) by reflexivity.
-replace (-Zneg p)%Z with (Zpos p) by reflexivity.
+intros [|p|p].
+apply eq_sym, Rinv_1.
+now change (-Zpos p)%Z with (Zneg p).
+change (-Zneg p)%Z with (Zpos p).
 simpl; rewrite Rinv_involutive; trivial.
-generalize (bpow_gt_0 (Zpos p)).
-simpl; auto with real.
+apply Rgt_not_eq.
+apply (bpow_gt_0 (Zpos p)).
 Qed.
 
 Theorem Z2R_Zpower_nat :
@@ -1872,7 +1875,7 @@ apply bpow_ge_0.
 Qed.
 
 Theorem ln_beta_mult_bpow :
-  forall x e, x <> R0 ->
+  forall x e, x <> 0%R ->
   (ln_beta (x * bpow e) = ln_beta x + e :>Z)%Z.
 Proof.
 intros x e Zx.
@@ -1895,7 +1898,7 @@ Qed.
 
 Theorem ln_beta_le_bpow :
   forall x e,
-  x <> R0 ->
+  x <> 0%R ->
   (Rabs x < bpow e)%R ->
   (ln_beta x <= e)%Z.
 Proof.
@@ -2044,20 +2047,19 @@ destruct Hex as (Hex0,Hex1); [now apply Rgt_not_eq|].
 assert (Haxy : (Rabs (x + y) < bpow (ex + 1))%R).
 { rewrite bpow_plus1.
   apply Rlt_le_trans with (2 * bpow ex)%R.
-  - apply Rle_lt_trans with (2 * Rabs x)%R.
-    + rewrite Rabs_right.
-      { apply Rle_trans with (x + x)%R; [now apply Rplus_le_compat_l|].
-        rewrite Rabs_right.
-        { rewrite Rmult_plus_distr_r.
-          rewrite Rmult_1_l.
-          now apply Rle_refl. }
-        now apply Rgt_ge. }
-      apply Rgt_ge.
-      rewrite <- (Rplus_0_l 0).
-      now apply Rplus_gt_compat.
-    + now apply Rmult_lt_compat_l; intuition.
-  - apply Rmult_le_compat_r; [now apply bpow_ge_0|].
-    now change 2%R with (Z2R 2); apply Z2R_le. }
+  - rewrite Rabs_pos_eq.
+    apply Rle_lt_trans with (2 * Rabs x)%R.
+    + rewrite Rabs_pos_eq.
+      replace (2 * x)%R with (x + x)%R by ring.
+      now apply Rplus_le_compat_l.
+      now apply Rlt_le.
+    + apply Rmult_lt_compat_l with (2 := Hex1).
+      exact Rlt_0_2.
+    + rewrite <- (Rplus_0_l 0).
+      now apply Rlt_le, Rplus_lt_compat.
+  - apply Rmult_le_compat_r.
+    now apply bpow_ge_0.
+    now apply (Z2R_le 2). }
 assert (Haxy2 : (bpow (ex - 1) <= Rabs (x + y))%R).
 { apply (Rle_trans _ _ _ Hex0).
   rewrite Rabs_right; [|now apply Rgt_ge].
diff --git a/flocq/Core/Fcore_float_prop.v b/flocq/Core/Fcore_float_prop.v
index 8199ede6..a183bf0a 100644
--- a/flocq/Core/Fcore_float_prop.v
+++ b/flocq/Core/Fcore_float_prop.v
@@ -136,7 +136,7 @@ Qed.
 (** Sign facts *)
 Theorem F2R_0 :
   forall e : Z,
-  F2R (Float beta 0 e) = R0.
+  F2R (Float beta 0 e) = 0%R.
 Proof.
 intros e.
 unfold F2R. simpl.
@@ -145,7 +145,7 @@ Qed.
 
 Theorem F2R_eq_0_reg :
   forall m e : Z,
-  F2R (Float beta m e) = R0 ->
+  F2R (Float beta m e) = 0%R ->
   m = Z0.
 Proof.
 intros m e H.
diff --git a/flocq/Core/Fcore_generic_fmt.v b/flocq/Core/Fcore_generic_fmt.v
index 21e51890..668b4da2 100644
--- a/flocq/Core/Fcore_generic_fmt.v
+++ b/flocq/Core/Fcore_generic_fmt.v
@@ -252,7 +252,7 @@ apply Rmult_1_r.
 Qed.
 
 Theorem scaled_mantissa_0 :
-  scaled_mantissa 0 = R0.
+  scaled_mantissa 0 = 0%R.
 Proof.
 apply Rmult_0_l.
 Qed.
@@ -667,7 +667,7 @@ Theorem round_bounded_small_pos :
   forall x ex,
   (ex <= fexp ex)%Z ->
   (bpow (ex - 1) <= x < bpow ex)%R ->
-  round x = R0 \/ round x = bpow (fexp ex).
+  round x = 0%R \/ round x = bpow (fexp ex).
 Proof.
 intros x ex He Hx.
 unfold round, scaled_mantissa.
@@ -751,19 +751,19 @@ now apply sym_eq.
 Qed.
 
 Theorem round_0 :
-  round 0 = R0.
+  round 0 = 0%R.
 Proof.
 unfold round, scaled_mantissa.
 rewrite Rmult_0_l.
-fold (Z2R 0).
+change 0%R with (Z2R 0).
 rewrite Zrnd_Z2R.
 apply F2R_0.
 Qed.
 
 Theorem exp_small_round_0_pos :
   forall x ex,
- (bpow (ex - 1) <= x < bpow ex)%R ->
-   round x =R0 -> (ex <= fexp ex)%Z .
+  (bpow (ex - 1) <= x < bpow ex)%R ->
+  round x = 0%R -> (ex <= fexp ex)%Z .
 Proof.
 intros x ex H H1.
 case (Zle_or_lt ex (fexp ex)); trivial; intros V.
@@ -771,7 +771,7 @@ contradict H1.
 apply Rgt_not_eq.
 apply Rlt_le_trans with (bpow (ex-1)).
 apply bpow_gt_0.
-apply  (round_bounded_large_pos); assumption.
+apply (round_bounded_large_pos); assumption.
 Qed.
 
 Theorem generic_format_round_pos :
@@ -931,7 +931,7 @@ rewrite <- Ropp_0.
 now apply Ropp_lt_contravar.
 now apply Ropp_le_contravar.
 (* . 0 <= y *)
-apply Rle_trans with R0.
+apply Rle_trans with 0%R.
 apply F2R_le_0_compat. simpl.
 rewrite <- (Zrnd_Z2R rnd 0).
 apply Zrnd_le...
@@ -1020,7 +1020,7 @@ Qed.
 Theorem exp_small_round_0 :
   forall rnd {Hr : Valid_rnd rnd} x ex,
   (bpow (ex - 1) <= Rabs x < bpow ex)%R ->
-   round rnd x =R0 -> (ex <= fexp ex)%Z .
+   round rnd x = 0%R -> (ex <= fexp ex)%Z .
 Proof.
 intros rnd Hr x ex H1 H2.
 generalize Rabs_R0.
@@ -1177,7 +1177,7 @@ rewrite <- (Rmult_0_l (bpow (- canonic_exp x))).
 apply Rmult_le_compat_r with (2 := Hx).
 apply bpow_ge_0.
 rewrite <- H.
-change R0 with (Z2R 0).
+change 0%R with (Z2R 0).
 now rewrite Zfloor_Z2R, Zceil_Z2R.
 Qed.
 
@@ -1212,7 +1212,7 @@ rewrite <- (Rmult_0_l (bpow (- canonic_exp x))).
 apply Rmult_le_compat_r with (2 := Hx).
 apply bpow_ge_0.
 rewrite <- H.
-change R0 with (Z2R 0).
+change 0%R with (Z2R 0).
 now rewrite Zfloor_Z2R, Zceil_Z2R.
 Qed.
 
@@ -1296,7 +1296,7 @@ Theorem round_DN_small_pos :
   forall x ex,
   (bpow (ex - 1) <= x < bpow ex)%R ->
   (ex <= fexp ex)%Z ->
-  round Zfloor x = R0.
+  round Zfloor x = 0%R.
 Proof.
 intros x ex Hx He.
 rewrite <- (F2R_0 beta (canonic_exp x)).
@@ -1552,7 +1552,7 @@ Qed.
 
 Lemma canonic_exp_le_bpow :
   forall (x : R) (e : Z),
-  x <> R0 ->
+  x <> 0%R ->
   (Rabs x < bpow e)%R ->
   (canonic_exp x <= fexp e)%Z.
 Proof.
@@ -1578,7 +1578,7 @@ Context { valid_rnd : Valid_rnd rnd }.
 
 Theorem ln_beta_round_ge :
   forall x,
-  round rnd x <> R0 ->
+  round rnd x <> 0%R ->
   (ln_beta beta x <= ln_beta beta (round rnd x))%Z.
 Proof with auto with typeclass_instances.
 intros x.
@@ -1597,7 +1597,7 @@ Qed.
 
 Theorem canonic_exp_round_ge :
   forall x,
-  round rnd x <> R0 ->
+  round rnd x <> 0%R ->
   (canonic_exp x <= canonic_exp (round rnd x))%Z.
 Proof with auto with typeclass_instances.
 intros x Zr.
@@ -1807,7 +1807,7 @@ rewrite Zceil_floor_neq.
 rewrite Z2R_plus.
 simpl.
 apply Ropp_lt_cancel.
-apply Rplus_lt_reg_l with R1.
+apply Rplus_lt_reg_l with 1%R.
 replace (1 + -/2)%R with (/2)%R by field.
 now replace (1 + - (Z2R (Zfloor x) + 1 - x))%R with (x - Z2R (Zfloor x))%R by ring.
 apply Rlt_not_eq.
@@ -1866,7 +1866,7 @@ rewrite Z2R_abs, Z2R_minus.
 replace (Z2R (Znearest x) - Z2R n)%R with (- (x - Z2R (Znearest x)) + (x - Z2R n))%R by ring.
 apply Rle_lt_trans with (1 := Rabs_triang _ _).
 simpl.
-replace R1 with (/2 + /2)%R by field.
+replace 1%R with (/2 + /2)%R by field.
 apply Rplus_le_lt_compat with (2 := Hd).
 rewrite Rabs_Ropp.
 apply Znearest_N.
diff --git a/flocq/Core/Fcore_rnd_ne.v b/flocq/Core/Fcore_rnd_ne.v
index 1f265406..2d67e709 100644
--- a/flocq/Core/Fcore_rnd_ne.v
+++ b/flocq/Core/Fcore_rnd_ne.v
@@ -370,7 +370,7 @@ destruct (Rle_or_lt (round beta fexp Zfloor x) 0) as [Hr|Hr].
 rewrite (Rle_antisym _ _ Hr).
 unfold scaled_mantissa.
 rewrite Rmult_0_l.
-change R0 with (Z2R 0).
+change 0%R with (Z2R 0).
 now rewrite (Ztrunc_Z2R 0).
 rewrite <- (round_0 beta fexp Zfloor).
 apply round_le...
diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v
index 28d2bc35..3bc0eac3 100644
--- a/flocq/Core/Fcore_ulp.v
+++ b/flocq/Core/Fcore_ulp.v
@@ -18,6 +18,7 @@ COPYING file for more details.
 *)
 
 (** * Unit in the Last Place: our definition using fexp and its properties, successor and predecessor *)
+Require Import Reals Psatz.
 Require Import Fcore_Raux.
 Require Import Fcore_defs.
 Require Import Fcore_rnd.
@@ -2002,7 +2003,7 @@ rewrite Hx in Hfx; contradict Hfx; auto with real.
 intros H.
 apply Rle_trans with (1:=error_le_half_ulp _ _).
 apply Rmult_le_compat_l.
-auto with real.
+apply Rlt_le, pos_half_prf.
 apply ulp_le.
 rewrite Hx; rewrite (Rabs_left1 x), Rabs_left; try assumption.
 apply Ropp_le_contravar.
@@ -2018,7 +2019,7 @@ case (Rle_or_lt 0 (round beta fexp Zceil x)).
 intros H; destruct H.
 apply Rle_trans with (1:=error_le_half_ulp _ _).
 apply Rmult_le_compat_l.
-auto with real.
+apply Rlt_le, pos_half_prf.
 apply ulp_le_pos; trivial.
 case (Rle_or_lt 0 x); trivial.
 intros H1; contradict H.
@@ -2234,21 +2235,7 @@ apply generic_format_0.
 left; apply Rlt_le_trans with (1:=H).
 rewrite V1,V2; right; field.
 (* *)
-assert (T: (u < (u + succ u) / 2 < succ u)%R).
-split.
-apply Rmult_lt_reg_l with 2%R.
-now auto with real.
-apply Rplus_lt_reg_l with (-u)%R.
-apply Rle_lt_trans with u;[right; ring|idtac].
-apply Rlt_le_trans with (1:=V).
-right; field.
-apply Rmult_lt_reg_l with 2%R.
-now auto with real.
-apply Rplus_lt_reg_l with (-succ u)%R.
-apply Rle_lt_trans with u;[right; field|idtac].
-apply Rlt_le_trans with (1:=V).
-right; ring.
-(* *)
+assert (T: (u < (u + succ u) / 2 < succ u)%R) by lra.
 destruct T as (T1,T2).
 apply Rnd_N_pt_monotone with F v ((u + succ u) / 2)%R...
 apply round_N_pt...
diff --git a/flocq/Prop/Fprop_Sterbenz.v b/flocq/Prop/Fprop_Sterbenz.v
index 7260d2e1..4e74f889 100644
--- a/flocq/Prop/Fprop_Sterbenz.v
+++ b/flocq/Prop/Fprop_Sterbenz.v
@@ -133,7 +133,7 @@ assert (Hy0: (0 <= y)%R).
 apply Rplus_le_reg_r with y.
 apply Rle_trans with x.
 now rewrite Rplus_0_l.
-now rewrite Rmult_plus_distr_r, Rmult_1_l in Hxy2.
+now replace (y + y)%R with (2 * y)%R by ring.
 rewrite Rabs_pos_eq with (1 := Hy0).
 rewrite Rabs_pos_eq.
 unfold Rmin.
diff --git a/flocq/Prop/Fprop_div_sqrt_error.v b/flocq/Prop/Fprop_div_sqrt_error.v
index 9d29001d..422b6b64 100644
--- a/flocq/Prop/Fprop_div_sqrt_error.v
+++ b/flocq/Prop/Fprop_div_sqrt_error.v
@@ -103,7 +103,7 @@ apply Rlt_le_trans with (Rabs x * 1)%R.
 apply Rmult_lt_compat_l.
 now apply Rabs_pos_lt.
 apply Rlt_le_trans with (1 := Heps1).
-change R1 with (bpow 0).
+change 1%R with (bpow 0).
 apply bpow_le.
 generalize (prec_gt_0 prec).
 clear ; omega.
@@ -191,7 +191,7 @@ apply Rsqr_le_abs_1.
 apply Rle_trans with (1 := Rabs_triang _ _).
 rewrite Rabs_R1.
 apply Rplus_le_reg_l with (-1)%R.
-rewrite <- Rplus_assoc, Rplus_opp_l, Rplus_0_l.
+replace (-1 + (1 + Rabs eps))%R with (Rabs eps) by ring.
 apply Rle_trans with (1 := Heps1).
 rewrite Rabs_pos_eq.
 apply Rmult_le_reg_l with 2%R.
@@ -256,8 +256,7 @@ replace (prec+(Fexp fr+Fexp fr))%Z with (Fexp fr + (prec+Fexp fr))%Z by ring.
 rewrite bpow_plus, Rmult_assoc.
 apply Rmult_lt_compat_l.
 apply bpow_gt_0.
-apply Rmult_lt_reg_l with 2%R.
-auto with real.
+apply Rmult_lt_reg_l with (1 := Rlt_0_2).
 apply Rle_lt_trans with (Rabs (F2R fr + sqrt x)).
 right; field.
 apply Rle_lt_trans with (1:=Rabs_triang _ _).
@@ -273,7 +272,7 @@ rewrite <- Hr1; auto.
 apply Rlt_le_trans with (bpow (prec + Fexp fr)+ Rabs (sqrt x))%R.
 now apply Rplus_lt_compat_r.
 (* . *)
-rewrite Rmult_plus_distr_r, Rmult_1_l.
+replace (2 * bpow (prec + Fexp fr))%R with (bpow (prec + Fexp fr) + bpow (prec + Fexp fr))%R by ring.
 apply Rplus_le_compat_l.
 assert (sqrt x <> 0)%R.
 apply Rgt_not_eq.
diff --git a/flocq/Prop/Fprop_plus_error.v b/flocq/Prop/Fprop_plus_error.v
index 950ca267..41c2f031 100644
--- a/flocq/Prop/Fprop_plus_error.v
+++ b/flocq/Prop/Fprop_plus_error.v
@@ -157,7 +157,7 @@ Lemma round_plus_eq_zero_aux :
   (canonic_exp beta fexp x <= canonic_exp beta fexp y)%Z ->
   format x -> format y ->
   (0 <= x + y)%R ->
-  round beta fexp rnd (x + y) = R0 ->
+  round beta fexp rnd (x + y) = 0%R ->
   (x + y = 0)%R.
 Proof with auto with typeclass_instances.
 intros x y He Hx Hy Hp Hxy.
@@ -202,11 +202,11 @@ Context { valid_rnd : Valid_rnd rnd }.
 Theorem round_plus_eq_zero :
   forall x y,
   format x -> format y ->
-  round beta fexp rnd (x + y) = R0 ->
+  round beta fexp rnd (x + y) = 0%R ->
   (x + y = 0)%R.
 Proof with auto with typeclass_instances.
 intros x y Hx Hy.
-destruct (Rle_or_lt R0 (x + y)) as [H1|H1].
+destruct (Rle_or_lt 0 (x + y)) as [H1|H1].
 (* . *)
 revert H1.
 destruct (Zle_or_lt (canonic_exp beta fexp x) (canonic_exp beta fexp y)) as [H2|H2].
diff --git a/flocq/Prop/Fprop_relative.v b/flocq/Prop/Fprop_relative.v
index 585b71da..276ccd3b 100644
--- a/flocq/Prop/Fprop_relative.v
+++ b/flocq/Prop/Fprop_relative.v
@@ -44,7 +44,7 @@ Proof with auto with typeclass_instances.
 intros x b Hb0 Hxb.
 destruct (Req_dec x 0) as [Hx0|Hx0].
 (* *)
-exists R0.
+exists 0%R.
 split.
 now rewrite Rabs_R0.
 rewrite Hx0, Rmult_0_l.
@@ -71,7 +71,7 @@ Proof with auto with typeclass_instances.
 intros x b Hb0 Hxb.
 destruct (Req_dec x 0) as [Hx0|Hx0].
 (* *)
-exists R0.
+exists 0%R.
 split.
 now rewrite Rabs_R0.
 rewrite Hx0, Rmult_0_l.
@@ -588,7 +588,7 @@ rewrite Rabs_right;[assumption|apply Rle_ge; now left].
 exists eps; exists 0%R.
 split;[assumption|split].
 rewrite Rabs_R0; apply Rmult_le_pos.
-auto with real.
+apply Rlt_le, pos_half_prf.
 apply bpow_ge_0.
 split;[apply Rmult_0_r|idtac].
 now rewrite Rplus_0_r.
@@ -596,13 +596,14 @@ now rewrite Rplus_0_r.
 exists 0%R; exists (round beta (FLT_exp emin prec) (Znearest choice) x - x)%R.
 split.
 rewrite Rabs_R0; apply Rmult_le_pos.
-auto with real.
+apply Rlt_le, pos_half_prf.
 apply bpow_ge_0.
 split.
 apply Rle_trans with (/2*ulp beta (FLT_exp emin prec) x)%R.
 apply error_le_half_ulp.
 now apply FLT_exp_valid.
-apply Rmult_le_compat_l; auto with real.
+apply Rmult_le_compat_l.
+apply Rlt_le, pos_half_prf.
 rewrite ulp_neq_0.
 2: now apply Rgt_not_eq.
 apply bpow_le.
@@ -650,7 +651,7 @@ destruct (Rtotal_order x 0) as [Nx|[Zx|Px]].
   { apply (Rmult_le_reg_l 2 _ _ Rlt_0_2).
     rewrite Rmult_0_r, Rinv_r; [exact Rle_0_1|].
     apply Rgt_not_eq, Rlt_gt, Rlt_0_2. }
-  exists R0; exists R0; rewrite Zx; split; [|split; [|split]].
+  exists 0%R; exists 0%R; rewrite Zx; split; [|split; [|split]].
   { now rewrite Rabs_R0; apply Rmult_le_pos; [|apply bpow_ge_0]. }
   { now rewrite Rabs_R0; apply Rmult_le_pos; [|apply bpow_ge_0]. }
   { now rewrite Rmult_0_l. }
-- 
cgit