Upgrade Flocq to version 2.6.1 from upstream (#71)

We were previously at 2.5.2.  Quoting the NEWS from upstream:

Version 2.6.1:
 - ensured compatibility from Coq 8.4 to 8.8

Version 2.6.0:
 - ensured compatibility from Coq 8.4 to 8.7
 - removed some hypotheses on some lemmas of Fcore_ulp
 - added lemmas to Fprop_plus_error
 - improved examples

Also: in preparation for Coq 8.8, silence warning "compatibility-notation"
when building Flocq, because this warning is on by default in 8.8,
and Flocq triggers it a lot.

7 files changed, 420 insertions, 171 deletions

diff --git a/flocq/Appli/Fappli_double_round.v b/flocq/Appli/Fappli_double_round.v
index 2c4937ab..82f61da3 100644
--- a/flocq/Appli/Fappli_double_round.v
+++ b/flocq/Appli/Fappli_double_round.v
@@ -5,6 +5,7 @@ Require Import Fcore_defs.
 Require Import Fcore_generic_fmt.
 Require Import Fcalc_ops.
 Require Import Fcore_ulp.
+Require Fcore_FLX Fcore_FLT Fcore_FTZ.
 
 Require Import Psatz.
 
@@ -659,7 +660,7 @@ Qed.
 
 Section Double_round_mult_FLX.
 
-Require Import Fcore_FLX.
+Import Fcore_FLX.
 
 Variable prec : Z.
 Variable prec' : Z.
@@ -685,8 +686,8 @@ End Double_round_mult_FLX.
 
 Section Double_round_mult_FLT.
 
-Require Import Fcore_FLX.
-Require Import Fcore_FLT.
+Import Fcore_FLX.
+Import Fcore_FLT.
 
 Variable emin prec : Z.
 Variable emin' prec' : Z.
@@ -718,7 +719,8 @@ End Double_round_mult_FLT.
 
 Section Double_round_mult_FTZ.
 
-Require Import Fcore_FTZ.
+Import Fcore_FLX.
+Import Fcore_FTZ.
 
 Variable emin prec : Z.
 Variable emin' prec' : Z.
@@ -796,7 +798,7 @@ Lemma ln_beta_minus_disj :
    \/ (ln_beta (x - y) = (ln_beta x - 1)%Z :> Z)).
 Proof.
 intros x y Px Py Hln.
-assert (Hxy : y < x); [now apply (ln_beta_lt_pos beta); [| |omega]|].
+assert (Hxy : y < x); [now apply (ln_beta_lt_pos beta); [ |omega]|].
 generalize (ln_beta_minus beta x y Py Hxy); intro Hln2.
 generalize (ln_beta_minus_lb beta x y Px Py Hln); intro Hln3.
 omega.
@@ -1611,7 +1613,7 @@ Qed.
 
 Section Double_round_plus_FLX.
 
-Require Import Fcore_FLX.
+Import Fcore_FLX.
 
 Variable prec : Z.
 Variable prec' : Z.
@@ -1667,8 +1669,8 @@ End Double_round_plus_FLX.
 
 Section Double_round_plus_FLT.
 
-Require Import Fcore_FLX.
-Require Import Fcore_FLT.
+Import Fcore_FLX.
+Import Fcore_FLT.
 
 Variable emin prec : Z.
 Variable emin' prec' : Z.
@@ -1739,8 +1741,8 @@ End Double_round_plus_FLT.
 
 Section Double_round_plus_FTZ.
 
-Require Import Fcore_FLX.
-Require Import Fcore_FTZ.
+Import Fcore_FLX.
+Import Fcore_FTZ.
 
 Variable emin prec : Z.
 Variable emin' prec' : Z.
@@ -2325,7 +2327,7 @@ Qed.
 
 Section Double_round_plus_beta_ge_3_FLX.
 
-Require Import Fcore_FLX.
+Import Fcore_FLX.
 
 Variable prec : Z.
 Variable prec' : Z.
@@ -2385,8 +2387,8 @@ End Double_round_plus_beta_ge_3_FLX.
 
 Section Double_round_plus_beta_ge_3_FLT.
 
-Require Import Fcore_FLX.
-Require Import Fcore_FLT.
+Import Fcore_FLX.
+Import Fcore_FLT.
 
 Variable emin prec : Z.
 Variable emin' prec' : Z.
@@ -2461,8 +2463,8 @@ End Double_round_plus_beta_ge_3_FLT.
 
 Section Double_round_plus_beta_ge_3_FTZ.
 
-Require Import Fcore_FLX.
-Require Import Fcore_FTZ.
+Import Fcore_FLX.
+Import Fcore_FTZ.
 
 Variable emin prec : Z.
 Variable emin' prec' : Z.
@@ -2880,7 +2882,7 @@ Qed.
 
 Section Double_round_sqrt_FLX.
 
-Require Import Fcore_FLX.
+Import Fcore_FLX.
 
 Variable prec : Z.
 Variable prec' : Z.
@@ -2917,8 +2919,8 @@ End Double_round_sqrt_FLX.
 
 Section Double_round_sqrt_FLT.
 
-Require Import Fcore_FLX.
-Require Import Fcore_FLT.
+Import Fcore_FLX.
+Import Fcore_FLT.
 
 Variable emin prec : Z.
 Variable emin' prec' : Z.
@@ -2972,8 +2974,8 @@ End Double_round_sqrt_FLT.
 
 Section Double_round_sqrt_FTZ.
 
-Require Import Fcore_FLX.
-Require Import Fcore_FTZ.
+Import Fcore_FLX.
+Import Fcore_FTZ.
 
 Variable emin prec : Z.
 Variable emin' prec' : Z.
@@ -3318,7 +3320,7 @@ Qed.
 
 Section Double_round_sqrt_beta_ge_4_FLX.
 
-Require Import Fcore_FLX.
+Import Fcore_FLX.
 
 Variable prec : Z.
 Variable prec' : Z.
@@ -3357,8 +3359,8 @@ End Double_round_sqrt_beta_ge_4_FLX.
 
 Section Double_round_sqrt_beta_ge_4_FLT.
 
-Require Import Fcore_FLX.
-Require Import Fcore_FLT.
+Import Fcore_FLX.
+Import Fcore_FLT.
 
 Variable emin prec : Z.
 Variable emin' prec' : Z.
@@ -3414,8 +3416,8 @@ End Double_round_sqrt_beta_ge_4_FLT.
 
 Section Double_round_sqrt_beta_ge_4_FTZ.
 
-Require Import Fcore_FLX.
-Require Import Fcore_FTZ.
+Import Fcore_FLX.
+Import Fcore_FTZ.
 
 Variable emin prec : Z.
 Variable emin' prec' : Z.
@@ -4401,7 +4403,7 @@ Qed.
 
 Section Double_round_div_FLX.
 
-Require Import Fcore_FLX.
+Import Fcore_FLX.
 
 Variable prec : Z.
 Variable prec' : Z.
@@ -4445,8 +4447,8 @@ End Double_round_div_FLX.
 
 Section Double_round_div_FLT.
 
-Require Import Fcore_FLX.
-Require Import Fcore_FLT.
+Import Fcore_FLX.
+Import Fcore_FLT.
 
 Variable emin prec : Z.
 Variable emin' prec' : Z.
@@ -4515,8 +4517,8 @@ End Double_round_div_FLT.
 
 Section Double_round_div_FTZ.
 
-Require Import Fcore_FLX.
-Require Import Fcore_FTZ.
+Import Fcore_FLX.
+Import Fcore_FTZ.
 
 Variable emin prec : Z.
 Variable emin' prec' : Z.
diff --git a/flocq/Core/Fcore_FLT.v b/flocq/Core/Fcore_FLT.v
index 53dc48a7..2258b1d9 100644
--- a/flocq/Core/Fcore_FLT.v
+++ b/flocq/Core/Fcore_FLT.v
@@ -257,32 +257,33 @@ apply Rle_lt_trans with (2:=Hx).
 now apply He.
 Qed.
 
-Theorem ulp_FLT_le: forall x, (bpow (emin+prec) <= Rabs x)%R ->
-  (ulp beta FLT_exp x <= Rabs x * bpow (1-prec))%R.
+Theorem ulp_FLT_le :
+  forall x, (bpow (emin + prec - 1) <= Rabs x)%R ->
+  (ulp beta FLT_exp x <= Rabs x * bpow (1 - prec))%R.
 Proof.
 intros x Hx.
-assert (x <> 0)%R.
-intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt.
-rewrite Z, Rabs_R0; apply bpow_gt_0.
-rewrite ulp_neq_0; try assumption.
+assert (Zx : (x <> 0)%R).
+  intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt.
+  rewrite Z, Rabs_R0; apply bpow_gt_0.
+rewrite ulp_neq_0 with (1 := Zx).
 unfold canonic_exp, FLT_exp.
 destruct (ln_beta beta x) as (e,He).
 apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R.
 rewrite <- bpow_plus.
 right; apply f_equal.
-apply trans_eq with (e-prec)%Z;[idtac|ring].
-simpl; apply Z.max_l.
-assert (emin+prec <= e)%Z; try omega.
-apply le_bpow with beta.
-apply Rle_trans with (1:=Hx).
-left; now apply He.
+replace (e - 1 + (1 - prec))%Z with (e - prec)%Z by ring.
+apply Z.max_l.
+assert (emin+prec-1 < e)%Z; try omega.
+apply lt_bpow with beta.
+apply Rle_lt_trans with (1:=Hx).
+now apply He.
 apply Rmult_le_compat_r.
 apply bpow_ge_0.
 now apply He.
 Qed.
 
-
-Theorem ulp_FLT_ge: forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R.
+Theorem ulp_FLT_gt :
+  forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R.
 Proof.
 intros x; case (Req_dec x 0); intros Hx.
 rewrite Hx, ulp_FLT_small, Rabs_R0, Rmult_0_l; try apply bpow_gt_0.
diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v
index 44db6c35..77235e63 100644
--- a/flocq/Core/Fcore_Raux.v
+++ b/flocq/Core/Fcore_Raux.v
@@ -1842,10 +1842,13 @@ Qed.
 
 Lemma ln_beta_lt_pos :
   forall x y,
-  (0 < x)%R -> (0 < y)%R ->
+  (0 < y)%R ->
   (ln_beta x < ln_beta y)%Z -> (x < y)%R.
 Proof.
-intros x y Px Py.
+intros x y Py.
+case (Rle_or_lt x 0); intros Px.
+intros H.
+now apply Rle_lt_trans with 0%R.
 destruct (ln_beta x) as (ex, Hex).
 destruct (ln_beta y) as (ey, Hey).
 simpl.
@@ -2099,7 +2102,7 @@ assert (Hbeta : (2 <= r)%Z).
 { destruct r as (beta_val,beta_prop).
   now apply Zle_bool_imp_le. }
 intros x y Px Py Hln.
-assert (Oxy : (y < x)%R); [now apply ln_beta_lt_pos; [| |omega]|].
+assert (Oxy : (y < x)%R); [apply ln_beta_lt_pos;[assumption|omega]|].
 destruct (ln_beta x) as (ex,Hex).
 destruct (ln_beta y) as (ey,Hey).
 simpl in Hln |- *.
diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v
index 3bc0eac3..4fdd319e 100644
--- a/flocq/Core/Fcore_ulp.v
+++ b/flocq/Core/Fcore_ulp.v
@@ -43,7 +43,6 @@ now left.
 now right.
 Qed.
 
-
 (** [negligible_exp] is either none (as in FLX) or Some n such that n <= fexp n. *)
 Definition negligible_exp: option Z :=
   match (LPO_Z _ (fun z => Z_le_dec_aux z (fexp z))) with
@@ -272,6 +271,7 @@ Qed.
 
 Lemma not_FTZ_generic_format_ulp:
    (forall x,  F (ulp x)) -> Exp_not_FTZ fexp.
+Proof.
 intros H e.
 specialize (H (bpow (e-1))).
 rewrite ulp_neq_0 in H.
@@ -1483,23 +1483,27 @@ now apply generic_format_opp.
 now apply Ropp_lt_contravar.
 Qed.
 
-
-Theorem lt_succ_le:
+Theorem lt_succ_le :
   forall x y,
-  F x -> F y -> (y <> 0)%R ->
+  (y <> 0)%R ->
   (x <= y)%R ->
   (x < succ y)%R.
 Proof.
-intros x y Fx Fy Zy Hxy.
-case (Rle_or_lt (succ y) x); trivial; intros H.
-absurd (succ y = y)%R.
-apply Rgt_not_eq.
+intros x y Zy Hxy.
+apply Rle_lt_trans with (1 := Hxy).
 now apply succ_gt_id.
-apply Rle_antisym.
-now apply Rle_trans with x.
-apply succ_ge_id.
 Qed.
 
+Theorem pred_lt_le :
+  forall x y,
+  (x <> 0)%R ->
+  (x <= y)%R ->
+  (pred x < y)%R.
+Proof.
+intros x y Zy Hxy.
+apply Rlt_le_trans with (2 := Hxy).
+now apply pred_lt_id.
+Qed.
 
 Theorem succ_pred_aux : forall x, F x -> (0 < x)%R -> succ (pred x)=x.
 Proof.
@@ -1510,17 +1514,15 @@ rewrite succ_eq_pos.
 now apply pred_pos_plus_ulp.
 Qed.
 
-Theorem pred_succ_aux_0 : (pred (succ 0)=0)%R.
+Theorem pred_ulp_0 :
+  pred (ulp 0) = 0%R.
 Proof.
-unfold succ; rewrite Rle_bool_true.
-2: apply Rle_refl.
-rewrite Rplus_0_l.
 rewrite pred_eq_pos.
 2: apply ulp_ge_0.
 unfold ulp; rewrite Req_bool_true; trivial.
 case negligible_exp_spec'.
 (* *)
-intros (H1,H2); rewrite H1.
+intros [H1 _]; rewrite H1.
 unfold pred_pos; rewrite Req_bool_false.
 2: apply Rlt_not_eq, bpow_gt_0.
 unfold ulp; rewrite Req_bool_true; trivial.
@@ -1535,111 +1537,73 @@ apply Rminus_diag_eq, f_equal.
 apply sym_eq, valid_exp; omega.
 Qed.
 
-Theorem pred_succ_aux : forall x, F x -> (0 < x)%R -> pred (succ x)=x.
+Theorem succ_0 :
+  succ 0 = ulp 0.
 Proof.
-intros x Fx Hx.
-rewrite succ_eq_pos;[idtac|now left].
-rewrite pred_eq_pos.
-2: apply Rplus_le_le_0_compat;[now left| apply ulp_ge_0].
-unfold pred_pos.
-case Req_bool_spec; intros H1.
-(* *)
-pose (l:=(ln_beta beta (x+ulp x))).
-rewrite H1 at 1; fold l.
-apply Rplus_eq_reg_r with (ulp x).
-rewrite H1; fold l.
-rewrite (ulp_neq_0 x) at 3.
-2: now apply Rgt_not_eq.
-unfold canonic_exp.
-replace (fexp (ln_beta beta x)) with (fexp (l-1))%Z.
-ring.
-apply f_equal, sym_eq.
-apply Zle_antisym.
-assert (ln_beta beta x - 1 < l - 1)%Z;[idtac|omega].
-apply lt_bpow with beta.
-unfold l; rewrite <- H1.
-apply Rle_lt_trans with x.
-destruct (ln_beta beta x) as (e,He); simpl.
-rewrite <- (Rabs_right x) at 1.
-2: apply Rle_ge; now left.
-now apply He, Rgt_not_eq.
-apply Rplus_lt_reg_l with (-x)%R; ring_simplify.
-rewrite ulp_neq_0.
-apply bpow_gt_0.
-now apply Rgt_not_eq.
-apply le_bpow with beta.
-unfold l; rewrite <- H1.
-apply id_p_ulp_le_bpow; trivial.
-rewrite <- (Rabs_right x) at 1.
-2: apply Rle_ge; now left.
-apply bpow_ln_beta_gt.
-(* *)
-replace (ulp (x+ ulp x)) with (ulp x).
-ring.
-rewrite ulp_neq_0 at 1.
-2: now apply Rgt_not_eq.
-rewrite ulp_neq_0 at 1.
-2: apply Rgt_not_eq, Rlt_gt.
-2: apply Rlt_le_trans with (1:=Hx).
-2: apply Rplus_le_reg_l with (-x)%R; ring_simplify.
-2: apply ulp_ge_0.
-apply f_equal; unfold canonic_exp; apply f_equal.
-apply sym_eq, ln_beta_unique.
-rewrite Rabs_right.
-2: apply Rle_ge; left.
-2: apply Rlt_le_trans with (1:=Hx).
-2: apply Rplus_le_reg_l with (-x)%R; ring_simplify.
-2: apply ulp_ge_0.
-destruct (ln_beta beta x) as (e,He); simpl.
-rewrite Rabs_right in He.
-2: apply Rle_ge; now left.
-split.
-apply Rle_trans with x.
-apply He, Rgt_not_eq; assumption.
-apply Rplus_le_reg_l with (-x)%R; ring_simplify.
-apply ulp_ge_0.
-case (Rle_lt_or_eq_dec (x+ulp x) (bpow e)); trivial.
-apply id_p_ulp_le_bpow; trivial.
-apply He, Rgt_not_eq; assumption.
-intros K; contradict H1.
-rewrite K, ln_beta_bpow.
-apply f_equal; ring.
+unfold succ.
+rewrite Rle_bool_true.
+apply Rplus_0_l.
+apply Rle_refl.
 Qed.
 
+Theorem pred_0 :
+  pred 0 = Ropp (ulp 0).
+Proof.
+rewrite <- succ_0.
+rewrite <- Ropp_0 at 1.
+apply pred_opp.
+Qed.
 
-
-Theorem succ_pred : forall x, F x -> succ (pred x)=x.
+Theorem pred_succ_aux :
+  forall x, F x -> (0 < x)%R ->
+  pred (succ x) = x.
+Proof.
+intros x Fx Hx.
+apply Rle_antisym.
+- apply Rnot_lt_le.
+  intros H.
+  apply succ_le_lt with (1 := Fx) in H.
+  revert H.
+  apply Rlt_not_le.
+  apply pred_lt_id.
+  apply Rgt_not_eq.
+  apply Rlt_le_trans with (1 := Hx).
+  apply succ_ge_id.
+  now apply generic_format_pred, generic_format_succ.
+- apply le_pred_lt with (1 := Fx).
+  now apply generic_format_succ.
+  apply succ_gt_id.
+  now apply Rgt_not_eq.
+Qed.
+
+Theorem succ_pred :
+  forall x, F x ->
+  succ (pred x) = x.
 Proof.
 intros x Fx.
-case (Rle_or_lt 0 x); intros Hx.
-destruct Hx as [Hx|Hx].
+destruct (Rle_or_lt 0 x) as [[Hx|Hx]|Hx].
 now apply succ_pred_aux.
 rewrite <- Hx.
-rewrite pred_eq_opp_succ_opp, succ_opp, Ropp_0.
-rewrite pred_succ_aux_0; ring.
+rewrite pred_0, succ_opp, pred_ulp_0.
+apply Ropp_0.
 rewrite pred_eq_opp_succ_opp, succ_opp.
 rewrite pred_succ_aux.
-ring.
+apply Ropp_involutive.
 now apply generic_format_opp.
 now apply Ropp_0_gt_lt_contravar.
 Qed.
 
-Theorem pred_succ : forall x, F x -> pred (succ x)=x.
+Theorem pred_succ :
+  forall x, F x ->
+  pred (succ x) = x.
 Proof.
 intros x Fx.
-case (Rle_or_lt 0 x); intros Hx.
-destruct Hx as [Hx|Hx].
-now apply pred_succ_aux.
-rewrite <- Hx.
-apply pred_succ_aux_0.
-rewrite succ_eq_opp_pred_opp, pred_opp.
-rewrite succ_pred_aux.
-ring.
+rewrite <- (Ropp_involutive x).
+rewrite succ_opp, pred_opp.
+apply f_equal, succ_pred.
 now apply generic_format_opp.
-now apply Ropp_0_gt_lt_contravar.
 Qed.
 
-
 Theorem round_UP_pred_plus_eps :
   forall x, F x ->
   forall eps, (0 < eps <= if (Rle_bool x 0) then (ulp x)
@@ -2041,26 +2005,16 @@ apply error_le_half_ulp.
 rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption.
 Qed.
 
-
-Theorem pred_le: forall x y,
-   F x -> F y -> (x <= y)%R -> (pred x <= pred y)%R.
+Theorem pred_le :
+  forall x y, F x -> F y -> (x <= y)%R ->
+  (pred x <= pred y)%R.
 Proof.
-intros x y Fx Fy Hxy.
-assert (V:( ((x = 0) /\ (y = 0)) \/ (x <>0 \/ x < y))%R).
-case (Req_dec x 0); intros Zx.
-case Hxy; intros Zy.
-now right; right.
-left; split; trivial; now rewrite <- Zy.
-now right; left.
-destruct V as [(V1,V2)|V].
-rewrite V1,V2; now right.
-apply le_pred_lt; try assumption.
-apply generic_format_pred; try assumption.
-case V; intros V1.
-apply Rlt_le_trans with (2:=Hxy).
-now apply pred_lt_id.
-apply Rle_lt_trans with (2:=V1).
-now apply pred_le_id.
+intros x y Fx Fy [Hxy| ->].
+2: apply Rle_refl.
+apply le_pred_lt with (2 := Fy).
+now apply generic_format_pred.
+apply Rle_lt_trans with (2 := Hxy).
+apply pred_le_id.
 Qed.
 
 Theorem succ_le: forall x y,
@@ -2088,6 +2042,28 @@ rewrite <- (pred_succ x), <- (pred_succ y); try assumption.
 apply pred_le; trivial; now apply generic_format_succ.
 Qed.
 
+Theorem pred_lt :
+  forall x y, F x -> F y -> (x < y)%R ->
+  (pred x < pred y)%R.
+Proof.
+intros x y Fx Fy Hxy.
+apply Rnot_le_lt.
+intros H.
+apply Rgt_not_le with (1 := Hxy).
+now apply pred_le_inv.
+Qed.
+
+Theorem succ_lt :
+  forall x y, F x -> F y -> (x < y)%R ->
+  (succ x < succ y)%R.
+Proof.
+intros x y Fx Fy Hxy.
+apply Rnot_le_lt.
+intros H.
+apply Rgt_not_le with (1 := Hxy).
+now apply succ_le_inv.
+Qed.
+
 (* was lt_UP_le_DN *)
 Theorem le_round_DN_lt_UP :
   forall x y, F y ->
diff --git a/flocq/Flocq_version.v b/flocq/Flocq_version.v
index b01a08f9..72d4fe20 100644
--- a/flocq/Flocq_version.v
+++ b/flocq/Flocq_version.v
@@ -29,4 +29,4 @@ Definition Flocq_version := Eval vm_compute in
       parse t major (minor * 10 + N_of_ascii h - N_of_ascii "0"%char)%N
     | Empty_string => (major * 100 + minor)%N
     end in
-  parse "2.5.2"%string N0 N0.
+  parse "2.6.1"%string N0 N0.
diff --git a/flocq/Prop/Fprop_mult_error.v b/flocq/Prop/Fprop_mult_error.v
index 7c71627b..44448cd6 100644
--- a/flocq/Prop/Fprop_mult_error.v
+++ b/flocq/Prop/Fprop_mult_error.v
@@ -158,7 +158,6 @@ Notation bpow e := (bpow beta e).
 
 Variable emin prec : Z.
 Context { prec_gt_0_ : Prec_gt_0 prec }.
-Variable Hpemin: (emin <= prec)%Z.
 
 Notation format := (generic_format beta (FLT_exp emin prec)).
 Notation cexp := (canonic_exp beta (FLT_exp emin prec)).
@@ -173,7 +172,6 @@ Theorem mult_error_FLT :
   (x*y = 0)%R \/ (bpow (emin + 2*prec - 1) <= Rabs (x * y))%R ->
   format (round beta (FLT_exp emin prec) rnd (x * y) - (x * y))%R.
 Proof with auto with typeclass_instances.
-clear Hpemin.
 intros x y Hx Hy Hxy.
 set (f := (round beta (FLT_exp emin prec) rnd (x * y))).
 destruct (Req_dec (f - x * y) 0) as [Hr0|Hr0].
diff --git a/flocq/Prop/Fprop_plus_error.v b/flocq/Prop/Fprop_plus_error.v
index 41c2f031..9bb5aee8 100644
--- a/flocq/Prop/Fprop_plus_error.v
+++ b/flocq/Prop/Fprop_plus_error.v
@@ -19,6 +19,7 @@ COPYING file for more details.
 
 (** * Error of the rounded-to-nearest addition is representable. *)
 
+Require Import Psatz.
 Require Import Fcore_Raux.
 Require Import Fcore_defs.
 Require Import Fcore_float_prop.
@@ -26,6 +27,7 @@ Require Import Fcore_generic_fmt.
 Require Import Fcore_FIX.
 Require Import Fcore_FLX.
 Require Import Fcore_FLT.
+Require Import Fcore_ulp.
 Require Import Fcalc_ops.
 
 
@@ -267,3 +269,270 @@ rewrite Z2R_plus; ring.
 Qed.
 
 End Fprop_plus_FLT.
+
+Section Fprop_plus_mult_ulp.
+
+Variable beta : radix.
+Notation bpow e := (bpow beta e).
+
+Variable fexp : Z -> Z.
+Context { valid_exp : Valid_exp fexp }.
+Context { monotone_exp : Monotone_exp fexp }.
+Variable rnd : R -> Z.
+Context { valid_rnd : Valid_rnd rnd }.
+
+Notation format := (generic_format beta fexp).
+Notation cexp := (canonic_exp beta fexp).
+
+Lemma ex_shift :
+  forall x e, format x -> (e <= cexp x)%Z ->
+  exists m, (x = Z2R m * bpow e)%R.
+Proof with auto with typeclass_instances.
+intros x e Fx He.
+exists (Ztrunc (scaled_mantissa beta fexp x)*Zpower beta (cexp x -e))%Z.
+rewrite Fx at 1; unfold F2R; simpl.
+rewrite Z2R_mult, Rmult_assoc.
+f_equal.
+rewrite Z2R_Zpower.
+2: omega.
+rewrite <- bpow_plus; f_equal; ring.
+Qed.
+
+Lemma ln_beta_minus1 :
+  forall z, z <> 0%R ->
+  (ln_beta beta z - 1)%Z = ln_beta beta (z / Z2R beta).
+Proof.
+intros z Hz.
+unfold Zminus.
+rewrite <- ln_beta_mult_bpow with (1 := Hz).
+now rewrite bpow_opp, bpow_1.
+Qed.
+
+Theorem round_plus_mult_ulp :
+  forall x y, format x -> format y -> (x <> 0)%R ->
+  exists m, (round beta fexp rnd (x+y) = Z2R m * ulp beta fexp (x/Z2R beta))%R.
+Proof with auto with typeclass_instances.
+intros x y Fx Fy Zx.
+case (Zle_or_lt (ln_beta beta (x/Z2R beta)) (ln_beta beta y)); intros H1.
+pose (e:=cexp (x / Z2R beta)).
+destruct (ex_shift x e) as (nx, Hnx); try exact Fx.
+apply monotone_exp.
+rewrite <- (ln_beta_minus1 x Zx); omega.
+destruct (ex_shift y e) as (ny, Hny); try assumption.
+apply monotone_exp...
+destruct (round_repr_same_exp beta fexp rnd (nx+ny) e) as (n,Hn).
+exists n.
+apply trans_eq with (F2R (Float beta n e)).
+rewrite <- Hn; f_equal.
+rewrite Hnx, Hny; unfold F2R; simpl; rewrite Z2R_plus; ring.
+unfold F2R; simpl.
+rewrite ulp_neq_0; try easy.
+apply Rmult_integral_contrapositive_currified; try assumption.
+apply Rinv_neq_0_compat.
+apply Rgt_not_eq.
+apply radix_pos.
+(* *)
+destruct (ex_shift (round beta fexp rnd (x + y)) (cexp (x/Z2R beta))) as (n,Hn).
+apply generic_format_round...
+apply Zle_trans with (cexp (x+y)).
+apply monotone_exp.
+rewrite <- ln_beta_minus1 by easy.
+rewrite <- (ln_beta_abs beta (x+y)).
+(* . *)
+assert (U: (Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y) = Rabs x - Rabs y)%R).
+assert (V: forall x y, (Rabs y <= Rabs x)%R ->
+   (Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y) = Rabs x - Rabs y)%R).
+clear; intros x y.
+case (Rle_or_lt 0 y); intros Hy.
+case Hy; intros Hy'.
+case (Rle_or_lt 0 x); intros Hx.
+intros _; rewrite (Rabs_pos_eq y) by easy.
+rewrite (Rabs_pos_eq x) by easy.
+left; apply Rabs_pos_eq.
+now apply Rplus_le_le_0_compat.
+rewrite (Rabs_pos_eq y) by easy.
+rewrite (Rabs_left x) by easy.
+intros H; right; split.
+now apply Rgt_not_eq.
+rewrite Rabs_left1.
+ring.
+apply Rplus_le_reg_l with (-x)%R; ring_simplify; assumption.
+intros _; left.
+now rewrite <- Hy', Rabs_R0, 2!Rplus_0_r.
+case (Rle_or_lt 0 x); intros Hx.
+rewrite (Rabs_left y) by easy.
+rewrite (Rabs_pos_eq x) by easy.
+intros H; right; split.
+now apply Rlt_not_eq.
+rewrite Rabs_pos_eq.
+ring.
+apply Rplus_le_reg_l with (-y)%R; ring_simplify; assumption.
+intros _; left.
+rewrite (Rabs_left y) by easy.
+rewrite (Rabs_left x) by easy.
+rewrite Rabs_left1.
+ring.
+lra.
+apply V; left.
+apply ln_beta_lt_pos with beta.
+now apply Rabs_pos_lt.
+rewrite <- ln_beta_minus1 in H1; try assumption.
+rewrite 2!ln_beta_abs; omega.
+(* . *)
+destruct U as [U|U].
+rewrite U; apply Zle_trans with (ln_beta beta x).
+omega.
+rewrite <- ln_beta_abs.
+apply ln_beta_le.
+now apply Rabs_pos_lt.
+apply Rplus_le_reg_l with (-Rabs x)%R; ring_simplify.
+apply Rabs_pos.
+destruct U as (U',U); rewrite U.
+rewrite <- ln_beta_abs.
+apply ln_beta_minus_lb.
+now apply Rabs_pos_lt.
+now apply Rabs_pos_lt.
+rewrite 2!ln_beta_abs.
+assert (ln_beta beta y < ln_beta beta x - 1)%Z.
+now rewrite (ln_beta_minus1 x Zx).
+omega.
+apply canonic_exp_round_ge...
+intros K.
+apply round_plus_eq_zero in K...
+contradict H1; apply Zle_not_lt.
+rewrite <- (ln_beta_minus1 x Zx).
+replace y with (-x)%R.
+rewrite ln_beta_opp; omega.
+lra.
+exists n.
+rewrite ulp_neq_0.
+assumption.
+apply Rmult_integral_contrapositive_currified; try assumption.
+apply Rinv_neq_0_compat.
+apply Rgt_not_eq.
+apply radix_pos.
+Qed.
+
+Context {exp_not_FTZ : Exp_not_FTZ fexp}.
+
+Theorem round_plus_ge_ulp :
+  forall x y, format x -> format y ->
+  round beta fexp rnd (x+y) = 0%R \/
+  (ulp beta fexp (x/Z2R beta) <= Rabs (round beta fexp rnd (x+y)))%R.
+Proof with auto with typeclass_instances.
+intros x y Fx Fy.
+case (Req_dec x 0); intros Zx.
+(* *)
+rewrite Zx, Rplus_0_l.
+rewrite round_generic...
+unfold Rdiv; rewrite Rmult_0_l.
+rewrite Fy at 2.
+unfold F2R; simpl; rewrite Rabs_mult.
+rewrite (Rabs_pos_eq (bpow _)) by apply bpow_ge_0.
+case (Z.eq_dec (Ztrunc (scaled_mantissa beta fexp y)) 0); intros Hm.
+left.
+rewrite Fy, Hm; unfold F2R; simpl; ring.
+right.
+apply Rle_trans with (1*bpow (cexp y))%R.
+rewrite Rmult_1_l.
+rewrite <- ulp_neq_0.
+apply ulp_ge_ulp_0...
+intros K; apply Hm.
+rewrite K, scaled_mantissa_0.
+apply (Ztrunc_Z2R 0).
+apply Rmult_le_compat_r.
+apply bpow_ge_0.
+rewrite <- Z2R_abs.
+apply (Z2R_le 1).
+apply (Zlt_le_succ 0).
+now apply Z.abs_pos.
+(* *)
+destruct (round_plus_mult_ulp x y Fx Fy Zx) as (m,Hm).
+case (Z.eq_dec m 0); intros Zm.
+left.
+rewrite Hm, Zm; simpl; ring.
+right.
+rewrite Hm, Rabs_mult.
+rewrite (Rabs_pos_eq (ulp _ _ _)) by apply ulp_ge_0.
+apply Rle_trans with (1*ulp beta fexp (x/Z2R beta))%R.
+right; ring.
+apply Rmult_le_compat_r.
+apply ulp_ge_0.
+rewrite <- Z2R_abs.
+apply (Z2R_le 1).
+apply (Zlt_le_succ 0).
+now apply Z.abs_pos.
+Qed.
+
+End Fprop_plus_mult_ulp.
+
+Section Fprop_plus_ge_ulp.
+
+Variable beta : radix.
+Notation bpow e := (bpow beta e).
+
+Variable rnd : R -> Z.
+Context { valid_rnd : Valid_rnd rnd }.
+Variable emin prec : Z.
+Context { prec_gt_0_ : Prec_gt_0 prec }.
+
+Theorem round_plus_ge_ulp_FLT : forall x y e,
+  generic_format beta (FLT_exp emin prec) x -> generic_format beta (FLT_exp emin prec) y ->
+  (bpow e <= Rabs x)%R ->
+  round beta (FLT_exp emin prec) rnd (x+y) = 0%R \/
+  (bpow (e - prec) <= Rabs (round beta (FLT_exp emin prec) rnd (x+y)))%R.
+Proof with auto with typeclass_instances.
+intros x y e Fx Fy He.
+assert (Zx: x <> 0%R).
+  contradict He.
+  apply Rlt_not_le; rewrite He, Rabs_R0.
+  apply bpow_gt_0.
+case round_plus_ge_ulp with beta (FLT_exp emin prec) rnd x y...
+intros H; right.
+apply Rle_trans with (2:=H).
+rewrite ulp_neq_0.
+unfold canonic_exp.
+rewrite <- ln_beta_minus1 by easy.
+unfold FLT_exp; apply bpow_le.
+apply Zle_trans with (2:=Z.le_max_l _ _).
+destruct (ln_beta beta x) as (n,Hn); simpl.
+assert (e < n)%Z; try omega.
+apply lt_bpow with beta.
+apply Rle_lt_trans with (1:=He).
+now apply Hn.
+apply Rmult_integral_contrapositive_currified; try assumption.
+apply Rinv_neq_0_compat.
+apply Rgt_not_eq.
+apply radix_pos.
+Qed.
+
+Theorem round_plus_ge_ulp_FLX : forall x y e,
+  generic_format beta (FLX_exp prec) x -> generic_format beta (FLX_exp prec) y ->
+  (bpow e <= Rabs x)%R ->
+  round beta (FLX_exp prec) rnd (x+y) = 0%R \/
+  (bpow (e - prec) <= Rabs (round beta (FLX_exp prec) rnd (x+y)))%R.
+Proof with auto with typeclass_instances.
+intros x y e Fx Fy He.
+assert (Zx: x <> 0%R).
+  contradict He.
+  apply Rlt_not_le; rewrite He, Rabs_R0.
+  apply bpow_gt_0.
+case round_plus_ge_ulp with beta (FLX_exp prec) rnd x y...
+intros H; right.
+apply Rle_trans with (2:=H).
+rewrite ulp_neq_0.
+unfold canonic_exp.
+rewrite <- ln_beta_minus1 by easy.
+unfold FLX_exp; apply bpow_le.
+destruct (ln_beta beta x) as (n,Hn); simpl.
+assert (e < n)%Z; try omega.
+apply lt_bpow with beta.
+apply Rle_lt_trans with (1:=He).
+now apply Hn.
+apply Rmult_integral_contrapositive_currified; try assumption.
+apply Rinv_neq_0_compat.
+apply Rgt_not_eq.
+apply radix_pos.
+Qed.
+
+End Fprop_plus_ge_ulp.