New definitions for ulp, pred, succ. And all the corresponding modifications.

src/Appli/Fappli_rnd_odd.v

@@ -935,13 +935,9 @@ case K2; clear K2; intros K2.
 case (Rle_or_lt  x m); intros Y;[destruct Y|idtac].
 (* . *)
 apply trans_eq with (F2R d).
-apply round_N_DN_betw with (F2R u)...
+apply betw_eq_N_DN' with (F2R u)...
 apply DN_odd_d_aux; split; try left; assumption.
 apply UP_odd_d_aux; split; try left; assumption.
-split.
-apply round_ge_generic...
-apply generic_format_fexpe_fexp, Hd.
-apply Hd.
 assert (o <= (F2R d + F2R u) / 2)%R.
 apply round_le_generic...
 apply Fm.
@@ -950,10 +946,7 @@ destruct H1; trivial.
 apply P.
 now apply Rlt_not_eq.
 trivial.
-apply sym_eq, round_N_DN_betw with (F2R u)...
-split.
-apply Hd.
-exact H0.
+apply sym_eq, betw_eq_N_DN' with (F2R u)...
 (* . *)
 replace o with x.
 reflexivity.
@@ -961,10 +954,9 @@ apply sym_eq, round_generic...
 rewrite H0; apply Fm.
 (* . *)
 apply trans_eq with (F2R u).
-apply round_N_UP_betw with (F2R d)...
+apply betw_eq_N_UP' with (F2R d)...
 apply DN_odd_d_aux; split; try left; assumption.
 apply UP_odd_d_aux; split; try left; assumption.
-split.
 assert ((F2R d + F2R u) / 2 <= o)%R.
 apply round_ge_generic...
 apply Fm.
@@ -973,13 +965,7 @@ destruct H0; trivial.
 apply P.
 now apply Rgt_not_eq.
 rewrite <- H0; trivial.
-apply round_le_generic...
-apply generic_format_fexpe_fexp, Hu.
-apply Hu.
-apply sym_eq, round_N_UP_betw with (F2R d)...
-split.
-exact Y.
-apply Hu.
+apply sym_eq, betw_eq_N_UP' with (F2R d)...
 Qed.
 
 

src/Core/Fcore_FIX.v

@@ -22,6 +22,7 @@ Require Import Fcore_Raux.
 Require Import Fcore_defs.
 Require Import Fcore_rnd.
 Require Import Fcore_generic_fmt.
+Require Import Fcore_ulp.
 Require Import Fcore_rnd_ne.
 
 Section RND_FIX.
@@ -84,4 +85,16 @@ intros ex ey H.
 apply Zle_refl.
 Qed.
 
+Theorem ulp_FIX: forall x, ulp beta FIX_exp x = bpow emin.
+Proof.
+intros x; unfold ulp.
+case Req_bool_spec; intros Zx.
+case (negligible_exp_spec FIX_exp).
+intros (_,T); specialize (T (emin-1)%Z); contradict T.
+unfold FIX_exp; omega.
+intros (n,(H1,_)); rewrite H1; reflexivity.
+reflexivity.
+Qed.
+
+
 End RND_FIX.

src/Core/Fcore_FLT.v

@@ -25,6 +25,7 @@ Require Import Fcore_generic_fmt.
 Require Import Fcore_float_prop.
 Require Import Fcore_FLX.
 Require Import Fcore_FIX.
+Require Import Fcore_ulp.
 Require Import Fcore_rnd_ne.
 
 Section RND_FLT.
@@ -230,6 +231,33 @@ omega.
 apply Zle_refl.
 Qed.
 
+Theorem ulp_FLT_small: forall x, (Rabs x < bpow (emin+prec))%R ->
+    ulp beta FLT_exp x = bpow emin.
+Proof with auto with typeclass_instances.
+intros x Hx.
+unfold ulp; case Req_bool_spec; intros Hx2.
+(* x = 0 *)
+case (negligible_exp_spec FLT_exp).
+intros (_,T); specialize (T (emin-1)%Z); contradict T.
+apply Zle_not_lt; unfold FLT_exp.
+apply Zle_trans with (2:=Z.le_max_r _ _); omega.
+assert (V:FLT_exp emin = emin).
+unfold FLT_exp; apply Z.max_r.
+unfold Prec_gt_0 in prec_gt_0_; omega.
+intros (n,(H1,H2)); rewrite H1, <-V.
+apply f_equal, fexp_negligible_exp_eq...
+omega.
+(* x <> 0 *)
+apply f_equal; unfold canonic_exp, FLT_exp.
+apply Z.max_r.
+assert (ln_beta beta x-1 < emin+prec)%Z;[idtac|omega].
+destruct (ln_beta beta x) as (e,He); simpl.
+apply lt_bpow with beta.
+apply Rle_lt_trans with (2:=Hx).
+now apply He.
+Qed.
+
+
 (** FLT is a nice format: it has a monotone exponent... *)
 Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
 Proof.

src/Core/Fcore_FLX.v

@@ -24,6 +24,7 @@ Require Import Fcore_rnd.
 Require Import Fcore_generic_fmt.
 Require Import Fcore_float_prop.
 Require Import Fcore_FIX.
+Require Import Fcore_ulp.
 Require Import Fcore_rnd_ne.
 
 Section RND_FLX.
@@ -211,6 +212,16 @@ now apply FLXN_format_generic.
 now apply generic_format_FLXN.
 Qed.
 
+Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R.
+Proof.
+unfold ulp; rewrite Req_bool_true; trivial.
+case (negligible_exp_spec FLX_exp).
+intros (H1,H2); now rewrite H1.
+intros (n,(H1,H2)); contradict H2.
+unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega.
+Qed.
+
+
 (** FLX is a nice format: it has a monotone exponent... *)
 Global Instance FLX_exp_monotone : Monotone_exp FLX_exp.
 Proof.

src/Core/Fcore_FTZ.v

@@ -23,6 +23,7 @@ Require Import Fcore_defs.
 Require Import Fcore_rnd.
 Require Import Fcore_generic_fmt.
 Require Import Fcore_float_prop.
+Require Import Fcore_ulp.
 Require Import Fcore_FLX.
 
 Section RND_FTZ.
@@ -194,6 +195,21 @@ apply Zle_refl.
 omega.
 Qed.
 
+Theorem ulp_FTZ_0: ulp beta FTZ_exp 0 = bpow (emin+prec-1).
+Proof with auto with typeclass_instances.
+unfold ulp; rewrite Req_bool_true; trivial.
+case (negligible_exp_spec FTZ_exp).
+intros (_,T); specialize (T (emin-1)%Z); contradict T.
+apply Zle_not_lt; unfold FTZ_exp; unfold Prec_gt_0 in prec_gt_0_.
+rewrite Zlt_bool_true; omega.
+assert (V:(FTZ_exp (emin+prec-1) = emin+prec-1)%Z).
+unfold FTZ_exp; rewrite Zlt_bool_true; omega.
+intros (n,(H1,H2)); rewrite H1, <-V.
+apply f_equal, fexp_negligible_exp_eq...
+omega.
+Qed.
+
+
 Section FTZ_round.
 
 (** Rounding with FTZ *)

src/Core/Fcore_Raux.v

@@ -2327,6 +2327,160 @@ Qed.
 
 End cond_Ropp.
 
+
+(** LPO taken from Coquelicot *)
+
+Theorem LPO_min :
+  forall P : nat -> Prop, (forall n, P n \/ ~ P n) ->
+  {n : nat | P n /\ forall i, (i < n)%nat -> ~ P i} + {forall n, ~ P n}.
+Proof.
+assert (Hi: forall n, (0 < INR n + 1)%R).
+  intros N.
+  rewrite <- S_INR.
+  apply lt_0_INR.
+  apply lt_0_Sn.
+intros P HP.
+set (E y := exists n, (P n /\ y = / (INR n + 1))%R \/ (~ P n /\ y = 0)%R).
+assert (HE: forall n, P n -> E (/ (INR n + 1))%R).
+  intros n Pn.
+  exists n.
+  left.
+  now split.
+assert (BE: is_upper_bound E 1).
+  intros x [y [[_ ->]|[_ ->]]].
+  rewrite <- Rinv_1 at 2.
+  apply Rinv_le.
+  exact Rlt_0_1.
+  rewrite <- S_INR.
+  apply (le_INR 1), le_n_S, le_0_n.
+  exact Rle_0_1.
+destruct (completeness E) as [l [ub lub]].
+  now exists 1%R.
+  destruct (HP O) as [H0|H0].
+  exists 1%R.
+  exists O.
+  left.
+  apply (conj H0).
+  rewrite Rplus_0_l.
+  apply sym_eq, Rinv_1.
+  exists 0%R.
+  exists O.
+  right.
+  now split.
+destruct (Rle_lt_dec l 0) as [Hl|Hl].
+  right.
+  intros n Pn.
+  apply Rle_not_lt with (1 := Hl).
+  apply Rlt_le_trans with (/ (INR n + 1))%R.
+  now apply Rinv_0_lt_compat.
+  apply ub.
+  now apply HE.
+left.
+set (N := Zabs_nat (up (/l) - 2)).
+exists N.
+assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R).
+  unfold N.
+  rewrite INR_IZR_INZ.
+  rewrite inj_Zabs_nat.
+  replace (IZR (up (/ l)) - 1)%R with (IZR (up (/ l) - 2) + 1)%R.
+  apply (f_equal (fun v => IZR v + 1)%R).
+  apply Zabs_eq.
+  apply Zle_minus_le_0.
+  apply (Zlt_le_succ 1).
+  apply lt_IZR.
+  apply Rle_lt_trans with (/l)%R.
+  apply Rmult_le_reg_r with (1 := Hl).
+  rewrite Rmult_1_l, Rinv_l by now apply Rgt_not_eq.
+  apply lub.
+  exact BE.
+  apply archimed.
+  rewrite minus_IZR.
+  simpl.
+  ring.
+assert (H: forall i, (i < N)%nat -> ~ P i).
+  intros i HiN Pi.
+  unfold is_upper_bound in ub.
+  refine (Rle_not_lt _ _ (ub (/ (INR i + 1))%R _) _).
+  now apply HE.
+  rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq.
+  apply Rinv_1_lt_contravar.
+  rewrite <- S_INR.
+  apply (le_INR 1).
+  apply le_n_S.
+  apply le_0_n.
+  apply Rlt_le_trans with (INR N + 1)%R.
+  apply Rplus_lt_compat_r.
+  now apply lt_INR.
+  rewrite HN.
+  apply Rplus_le_reg_r with (-/l + 1)%R.
+  ring_simplify.
+  apply archimed.
+destruct (HP N) as [PN|PN].
+  now split.
+elimtype False.
+refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _).
+  intros x [y [[Py ->]|[_ ->]]].
+  destruct (eq_nat_dec y N) as [HyN|HyN].
+  elim PN.
+  now rewrite <- HyN.
+  apply Rinv_le.
+  apply Hi.
+  apply Rplus_le_compat_r.
+  apply Rnot_lt_le.
+  intros Hy.
+  refine (H _ _ Py).
+  apply INR_lt in Hy.
+  clear -Hy HyN.
+  omega.
+  now apply Rlt_le, Rinv_0_lt_compat.
+rewrite S_INR, HN.
+ring_simplify (IZR (up (/ l)) - 1 + 1)%R.
+rewrite <- (Rinv_involutive l) at 2 by now apply Rgt_not_eq.
+apply Rinv_1_lt_contravar.
+rewrite <- Rinv_1.
+apply Rinv_le.
+exact Hl.
+now apply lub.
+apply archimed.
+Qed.
+
+Theorem LPO :
+  forall P : nat -> Prop, (forall n, P n \/ ~ P n) ->
+  {n : nat | P n} + {forall n, ~ P n}.
+Proof.
+intros P HP.
+destruct (LPO_min P HP) as [[n [Pn _]]|Pn].
+left.
+now exists n.
+now right.
+Qed.
+
+
+Lemma LPO_Z : forall P : Z -> Prop, (forall n, P n \/ ~P n) ->
+  {n : Z| P n} + {forall n, ~ P n}.
+Proof.
+intros P H.
+destruct (LPO (fun n => P (Z.of_nat n))) as [J|J].
+intros n; apply H.
+destruct J as (n, Hn).
+left; now exists (Z.of_nat n).
+destruct (LPO (fun n => P (-Z.of_nat n)%Z)) as [K|K].
+intros n; apply H.
+destruct K as (n, Hn).
+left; now exists (-Z.of_nat n)%Z.
+right; intros n; case (Zle_or_lt 0 n); intros M.
+rewrite <- (Zabs_eq n); trivial.
+rewrite <- Zabs2Nat.id_abs.
+apply J.
+rewrite <- (Zopp_involutive n).
+rewrite <- (Z.abs_neq n).
+rewrite <- Zabs2Nat.id_abs.
+apply K.
+omega.
+Qed.
+
+
+
 (** A little tactic to simplify terms of the form [bpow a * bpow b]. *)
 Ltac bpow_simplify :=
   (* bpow ex * bpow ey ~~> bpow (ex + ey) *)

src/Core/Fcore_rnd_ne.v

@@ -191,7 +191,8 @@ rewrite Rmult_plus_distr_r.
 rewrite Z2R_Zpower, <- bpow_plus.
 ring_simplify (ex - fexp ex + fexp ex)%Z.
 rewrite Hu2, Hud.
-unfold ulp, canonic_exp.
+rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq].
+unfold canonic_exp.
 rewrite ln_beta_unique with beta x ex.
 unfold F2R.
 simpl. ring.
@@ -223,7 +224,8 @@ specialize (H ex).
 omega.
 (* - xu < bpow ex *)
 revert Hud.
-unfold ulp, F2R.
+rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq].
+unfold F2R.
 rewrite Hd, Hu.
 unfold canonic_exp.
 rewrite ln_beta_unique with beta (F2R xu) ex.

src/Prop/Fprop_div_sqrt_error.v

@@ -136,7 +136,10 @@ rewrite Rabs_Ropp.
 replace (bpow (Fexp fr)) with (ulp beta (FLX_exp prec) (F2R fr)).
 rewrite <- Hr1.
 apply ulp_error_f...
-unfold ulp; apply f_equal.
+apply Rmult_integral_contrapositive_currified; try apply Rinv_neq_0_compat; assumption.
+rewrite ulp_neq_0.
+2: now rewrite <- Hr1.
+apply f_equal.
 now rewrite Hr2, <- Hr1.
 replace (prec+(Fexp fr+Fexp fy))%Z with ((prec+Fexp fy)+Fexp fr)%Z by ring.
 rewrite bpow_plus.
@@ -247,7 +250,9 @@ apply Rabs_pos.
 apply Rle_trans with (/2*ulp beta  (FLX_exp prec) (F2R fr))%R.
 rewrite <- Hr1.
 apply ulp_half_error_f...
-right; unfold ulp; apply f_equal.
+right; rewrite ulp_neq_0.
+2: now rewrite <- Hr1.
+apply f_equal.
 rewrite Hr2, <- Hr1; trivial.
 rewrite Rmult_assoc, Rmult_comm.
 replace (prec+(Fexp fr+Fexp fr))%Z with (Fexp fr + (prec+Fexp fr))%Z by ring.

src/Prop/Fprop_mult_error.v

@@ -127,7 +127,8 @@ rewrite ln_beta_unique with (1 := Hexy).
 apply ln_beta_le_bpow with (1 := Hz).
 replace (bpow (exy - prec)) with (ulp beta (FLX_exp prec) (x * y)).
 apply ulp_error...
-unfold ulp, canonic_exp.
+rewrite ulp_neq_0; trivial.
+unfold canonic_exp.
 now rewrite ln_beta_unique with (1 := Hexy).
 apply Hc1.
 reflexivity.

src/Prop/Fprop_relative.v

@@ -113,16 +113,15 @@ Theorem relative_error :
   forall x,
   (bpow emin <= Rabs x)%R ->
   (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs x)%R.
-Proof.
+Proof with auto with typeclass_instances.
 intros x Hx.
-apply Rlt_le_trans with (ulp beta fexp x)%R.
-now apply ulp_error.
-unfold ulp, canonic_exp.
 assert (Hx': (x <> 0)%R).
-intros H.
-apply Rlt_not_le with (2 := Hx).
-rewrite H, Rabs_R0.
-apply bpow_gt_0.
+intros T; contradict Hx; rewrite T, Rabs_R0.
+apply Rlt_not_le, bpow_gt_0.
+apply Rlt_le_trans with (ulp beta fexp x)%R.
+now apply ulp_error...
+rewrite ulp_neq_0; trivial.
+unfold canonic_exp.
 destruct (ln_beta beta x) as (ex, He).
 simpl.
 specialize (He Hx').
@@ -197,14 +196,13 @@ Theorem relative_error_round :
   (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs (round beta fexp rnd x))%R.
 Proof with auto with typeclass_instances.
 intros Hp x Hx.
+assert (Hx': (x <> 0)%R).
+intros T; contradict Hx; rewrite T, Rabs_R0.
+apply Rlt_not_le, bpow_gt_0.
 apply Rlt_le_trans with (ulp beta fexp x)%R.
 now apply ulp_error.
-assert (Hx': (x <> 0)%R).
-intros H.
-apply Rlt_not_le with (2 := Hx).
-rewrite H, Rabs_R0.
-apply bpow_gt_0.
-unfold ulp, canonic_exp.
+rewrite ulp_neq_0; trivial.
+unfold canonic_exp.
 destruct (ln_beta beta x) as (ex, He).
 simpl.
 specialize (He Hx').
@@ -268,7 +266,8 @@ intros H.
 apply Rlt_not_le with (2 := Hx).
 rewrite H, Rabs_R0.
 apply bpow_gt_0.
-unfold ulp, canonic_exp.
+rewrite ulp_neq_0; trivial.
+unfold canonic_exp.
 destruct (ln_beta beta x) as (ex, He).
 simpl.
 specialize (He Hx').
@@ -359,7 +358,8 @@ intros H.
 apply Rlt_not_le with (2 := Hx).
 rewrite H, Rabs_R0.
 apply bpow_gt_0.
-unfold ulp, canonic_exp.
+rewrite ulp_neq_0; trivial.
+unfold canonic_exp.
 destruct (ln_beta beta x) as (ex, He).
 simpl.
 specialize (He Hx').
@@ -685,7 +685,8 @@ apply Rle_trans with (/2*ulp beta (FLT_exp emin prec) x)%R.
 apply ulp_half_error.
 now apply FLT_exp_valid.
 apply Rmult_le_compat_l; auto with real.
-unfold ulp.
+rewrite ulp_neq_0.
+2: now apply Rgt_not_eq.
 apply bpow_le.
 unfold FLT_exp, canonic_exp.
 rewrite Zmax_right.