proposition: Theorem Bsucc'_correct : (2 < emax)%Z -> forall x, is_finite x = true -> Bsucc' x = Bsucc x.
proof: Proof. intros Hp x Fx. destruct x as [sx|sx| |sx mx ex Bx] ; try easy. { generalize (Bldexp_correct mode_NE Bone emin). rewrite Bone_correct, Rmult_1_l. rewrite round_generic. rewrite Rlt_bool_true. simpl. intros [H1 [H2 H3]]. apply B2R_inj. apply is_finite_strict_B2R. rewrite H1. apply Rgt_not_eq. apply bpow_gt_0. easy. rewrite H1. apply eq_sym, F2R_bpow. rewrite Rabs_pos_eq by now apply bpow_ge_0. apply bpow_lt, emin_lt_emax. apply valid_rnd_N. apply generic_format_bpow. unfold fexp. rewrite Z.max_r. apply Z.le_refl. generalize (prec_gt_0 prec). lia. } set (x := B754_finite sx mx ex Bx). assert (H: if Rlt_bool (succ radix2 fexp (B2R x)) (bpow radix2 emax) then B2R (Bsucc' x) = succ radix2 fexp (B2R x) /\ is_finite (Bsucc' x) = true /\ Bsign (Bsucc' x) = sx else B2SF (Bsucc' x) = S754_infinity false). { assert (Hsucc : succ radix2 fexp 0 = bpow radix2 emin). { rewrite succ_0. now apply ulp_FLT_0. } unfold Bsucc', x; destruct sx. + case Rlt_bool_spec; intro Hover. * rewrite B2R_Bopp; simpl (Bopp (B754_finite _ _ _ _)). rewrite is_finite_Bopp. set (ox := B754_finite false mx ex Bx). assert (Hpred := Bpred_correct ox eq_refl). rewrite Bpred_pos'_correct ; cycle 1. exact Hp. now apply F2R_gt_0. rewrite Rlt_bool_true in Hpred. rewrite (proj1 Hpred), (proj1 (proj2 Hpred)). split. rewrite <- succ_opp. simpl. now rewrite <- F2R_opp. apply (conj eq_refl). rewrite Bsign_Bopp, (proj2 (proj2 Hpred)). easy. generalize (proj1 (proj2 Hpred)). now case Bpred. apply Rlt_le_trans with 0%R. rewrite <- Ropp_0. apply Ropp_lt_contravar, bpow_gt_0. apply pred_ge_0. now apply FLT_exp_valid. now apply F2R_gt_0. apply generic_format_B2R. * exfalso; revert Hover; apply Rlt_not_le. apply (Rle_lt_trans _ (succ radix2 fexp 0)). { apply succ_le; [now apply FLT_exp_valid|apply generic_format_B2R| apply generic_format_0|]. unfold B2R, F2R; simpl; change (Z.neg mx) with (- Z.pos mx)%Z. rewrite opp_IZR, <-Ropp_mult_distr_l, <-Ropp_0; apply Ropp_le_contravar. now apply Rmult_le_pos; [apply IZR_le|apply bpow_ge_0]. } rewrite Hsucc; apply bpow_lt. apply emin_lt_emax. + fold x. assert (Hulp := Bulp_correct x (eq_refl _)). assert (Hplus := Bplus_correct mode_NE x (Bulp x) (eq_refl _)). rewrite (proj1 (proj2 Hulp)) in Hplus; specialize (Hplus (eq_refl _)). assert (Px : (0 <= B2R x)%R). { now apply F2R_ge_0. } assert (Hsucc' : (succ radix2 fexp (B2R x) = B2R x + ulp radix2 fexp (B2R x))%R). { now unfold succ; rewrite (Rle_bool_true _ _ Px). } rewrite (proj1 Hulp), <- Hsucc' in Hplus. rewrite round_generic in Hplus; [|apply valid_rnd_N| now apply generic_format_succ; [apply FLT_exp_valid|apply generic_format_B2R]]. rewrite Rabs_pos_eq in Hplus; [|apply (Rle_trans _ _ _ Px), succ_ge_id]. revert Hplus; case Rlt_bool_spec; intros Hover Hplus. * split; [now simpl|split; [now simpl|]]. rewrite (proj2 (proj2 Hplus)); case Rcompare_spec. { intro H; exfalso; revert H. apply Rle_not_lt, (Rle_trans _ _ _ Px), succ_ge_id. } { intro H; exfalso; revert H; apply Rgt_not_eq, Rlt_gt. apply (Rlt_le_trans _ (B2R x)); [|apply succ_ge_id]. now apply Rmult_lt_0_compat; [apply IZR_lt|apply bpow_gt_0]. } now simpl. * now rewrite (proj1 Hplus). } generalize (Bsucc_correct x Fx). revert H. case Rlt_bool_spec ; intros H. intros [H1 [H2 H3]] [H4 [H5 H6]]. apply B2R_Bsign_inj ; try easy. now rewrite H4. rewrite H3, H6. simpl. now case sx. intros H1 H2. apply B2SF_inj. now rewrite H1, H2. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative