proposition: Theorem Bpred_pos'_correct : (2 < emax)%Z -> forall x, (0 < B2R x)%R -> Bpred_pos' x = Bpred x.
proof: Proof. intros Hp x Fx. assert (B2R (Bpred_pos' x) = pred_pos radix2 fexp (B2R x) /\ is_finite (Bpred_pos' x) = true /\ Bsign (Bpred_pos' x) = false) as [H1 [H2 H3]]. { generalize (Bfrexp_correct x). destruct x as [sx|sx| |sx mx ex Bx] ; try elim (Rlt_irrefl _ Fx). intros Hfrexpx. assert (Hsx : sx = false). { apply gt_0_F2R in Fx. revert Fx. now case sx. } clear Fx. rewrite Hsx in Hfrexpx |- *; clear Hsx sx. specialize (Hfrexpx (eq_refl _)). simpl in Hfrexpx; rewrite B2R_SF2B in Hfrexpx. destruct Hfrexpx as (Hfrexpx_bounds, (Hfrexpx_eq, Hfrexpx_exp)). apply Hp. unfold Bpred_pos', Bfrexp. simpl (snd (_, snd _)). rewrite Hfrexpx_exp. set (x' := B754_finite _ _ _ _). set (xr := F2R _). assert (Nzxr : xr <> 0%R). { now apply F2R_neq_0. } assert (Hulp := Bulp_correct x' (eq_refl _)). rewrite <- (Bulp'_correct Hp x') in Hulp by easy. assert (Hldexp := Bldexp_correct mode_NE Bone (fexp (mag radix2 xr - 1))). rewrite Bone_correct, Rmult_1_l in Hldexp. assert (Fbpowxr : generic_format radix2 fexp (bpow radix2 (fexp (mag radix2 xr - 1)))). { apply generic_format_bpow, Z.max_lub. - unfold Prec_gt_0 in prec_gt_0_; lia. - apply Z.le_max_r. } assert (H : Rlt_bool (Rabs (round radix2 fexp (round_mode mode_NE) (bpow radix2 (fexp (mag radix2 xr - 1))))) (bpow radix2 emax) = true); [|rewrite H in Hldexp; clear H]. { apply Rlt_bool_true; rewrite round_generic; [|apply valid_rnd_round_mode|apply Fbpowxr]. rewrite Rabs_pos_eq; [|apply bpow_ge_0]; apply bpow_lt. apply Z.max_lub_lt. 2: apply emin_lt_emax. apply (Zplus_lt_reg_r _ _ (prec + 1)); ring_simplify. rewrite Z.add_1_r; apply Zle_lt_succ, mag_le_bpow. - exact Nzxr. - apply (Rlt_le_trans _ (bpow radix2 emax)). + change xr with (B2R x'); apply abs_B2R_lt_emax. + apply bpow_le; unfold Prec_gt_0 in prec_gt_0_; lia. } set (d := if (mx~0 =? _)%positive then _ else _). assert (Hminus := Bminus_correct mode_NE x' d (eq_refl _)). assert (Fd : is_finite d = true). { unfold d; case (_ =? _)%positive. - now rewrite (proj1 (proj2 Hldexp)), is_finite_Bone. - now rewrite (proj1 (proj2 Hulp)). } specialize (Hminus Fd). assert (Px : (0 <= B2R x')%R). { unfold B2R, x', F2R; simpl. now apply Rmult_le_pos; [apply IZR_le|apply bpow_ge_0]. } assert (Pd : (0 <= B2R d)%R). { unfold d; case (_ =? _)%positive. - rewrite (proj1 Hldexp). now rewrite round_generic; [apply bpow_ge_0|apply valid_rnd_N|]. - rewrite (proj1 Hulp); apply ulp_ge_0. } assert (Hdlex : (B2R d <= B2R x')%R). { unfold d; case (_ =? _)%positive. - rewrite (proj1 Hldexp). rewrite round_generic; [|now apply valid_rnd_N|now simpl]. apply (Rle_trans _ (bpow radix2 (mag radix2 xr - 1))). + apply bpow_le, Z.max_lub. * unfold Prec_gt_0 in prec_gt_0_; lia. * apply (Zplus_le_reg_r _ _ 1); ring_simplify. apply mag_ge_bpow. replace (_ - 1)%Z with emin by ring. now change xr with (B2R x'); apply abs_B2R_ge_emin. + rewrite <-(Rabs_pos_eq _ Px). now change xr with (B2R x'); apply bpow_mag_le. - rewrite (proj1 Hulp); apply ulp_le_id. + assert (B2R x' <> 0%R); [exact Nzxr|lra]. + apply generic_format_B2R. } assert (H : Rlt_bool (Rabs (round radix2 fexp (round_mode mode_NE) (B2R x' - B2R d))) (bpow radix2 emax) = true); [|rewrite H in Hminus; clear H]. { apply Rlt_bool_true. rewrite <-round_NE_abs; [|now apply FLT_exp_valid]. rewrite Rabs_pos_eq; [|lra]. apply (Rle_lt_trans _ (B2R x')). - apply round_le_generic; [now apply FLT_exp_valid|now apply valid_rnd_N| |lra]. apply generic_format_B2R. - apply (Rle_lt_trans _ _ _ (Rle_abs _)), abs_B2R_lt_emax. } rewrite (proj1 Hminus). rewrite (proj1 (proj2 Hminus)). rewrite (proj2 (proj2 Hminus)). split; [|split; [reflexivity|now case (Rcompare_spec _ _); [lra| |]]]. unfold pred_pos, d. case (Pos.eqb_spec _ _); intro Hd; case (Req_bool_spec _ _); intro Hpred. + rewrite (proj1 Hldexp). rewrite (round_generic _ _ _ _ Fbpowxr). change xr with (B2R x'). replace (_ - _)%R with (pred_pos radix2 fexp (B2R x')). * rewrite round_generic; [reflexivity|now apply valid_rnd_N|]. apply generic_format_pred_pos; [now apply FLT_exp_valid|apply generic_format_B2R|]. change xr with (B2R x') in Nzxr; lra. * now unfold pred_pos; rewrite Req_bool_true. + exfalso; apply Hpred. assert (Hmx : IZR (Z.pos mx) = bpow radix2 (prec - 1)). { apply (Rmult_eq_reg_l 2); [|lra]; rewrite <-mult_IZR. change (2 * Z.pos mx)%Z with (Z.pos mx~0); rewrite Hd. rewrite shift_pos_correct, Z.mul_1_r. change (IZR (Z.pow_pos _ _)) with (bpow radix2 (Z.pos (Z.to_pos prec))). rewrite Z2Pos.id; [|exact prec_gt_0_]. change 2%R with (bpow radix2 1); rewrite <-bpow_plus. f_equal; ring. } unfold x' at 1; unfold B2R at 1; unfold F2R; simpl. rewrite Hmx, <-bpow_plus; f_equal. apply (Z.add_reg_l 1); ring_simplify; symmetry; apply mag_unique_pos. unfold F2R; simpl; rewrite Hmx, <-bpow_plus; split. * right; f_equal; ring. * apply bpow_lt; lia. + rewrite (proj1 Hulp). assert (H : ulp radix2 fexp (B2R x') = bpow radix2 (fexp (mag radix2 (B2R x') - 1))); [|rewrite H; clear H]. { unfold ulp; rewrite Req_bool_false; [|now simpl]. unfold cexp; f_equal. assert (H : (mag radix2 (B2R x') <= emin + prec)%Z). { assert (Hcm : canonical_mantissa mx ex = true). { now generalize Bx; unfold bounded; rewrite Bool.andb_true_iff. } apply (canonical_canonical_mantissa false) in Hcm. revert Hcm; fold emin; unfold canonical, cexp; simpl. change (F2R _) with (B2R x'); intro Hex. apply Z.nlt_ge; intro H'; apply Hd. apply Pos2Z.inj_pos; rewrite shift_pos_correct, Z.mul_1_r. apply eq_IZR; change (IZR (Z.pow_pos _ _)) with (bpow radix2 (Z.pos (Z.to_pos prec))). rewrite Z2Pos.id; [|exact prec_gt_0_]. change (Z.pos mx~0) with (2 * Z.pos mx)%Z. rewrite Z.mul_comm, mult_IZR. apply (Rmult_eq_reg_r (bpow radix2 (ex - 1))); [|apply Rgt_not_eq, bpow_gt_0]. change 2%R with (bpow radix2 1); rewrite Rmult_assoc, <-!bpow_plus. replace (1 + _)%Z with ex by ring. unfold B2R at 1, F2R in Hpred; simpl in Hpred; rewrite Hpred. change (F2R _) with (B2R x'); rewrite Hex. unfold fexp, FLT_exp; rewrite Z.max_l; [f_equal; ring|lia]. } now unfold fexp, FLT_exp; do 2 (rewrite Z.max_r; [|lia]). } replace (_ - _)%R with (pred_pos radix2 fexp (B2R x')). * rewrite round_generic; [reflexivity|apply valid_rnd_N|]. apply generic_format_pred_pos; [now apply FLT_exp_valid| |change xr with (B2R x') in Nzxr; lra]. apply generic_format_B2R. * now unfold pred_pos; rewrite Req_bool_true. + rewrite (proj1 Hulp). replace (_ - _)%R with (pred_pos radix2 fexp (B2R x')). * rewrite round_generic; [reflexivity|now apply valid_rnd_N|]. apply generic_format_pred_pos; [now apply FLT_exp_valid|apply generic_format_B2R|]. change xr with (B2R x') in Nzxr; lra. * now unfold pred_pos; rewrite Req_bool_false. } assert (is_finite x = true /\ Bsign x = false) as [H4 H5]. { clear -Fx. destruct x as [| | |sx mx ex Hx] ; try elim Rlt_irrefl with (1 := Fx). repeat split. destruct sx. elim Rlt_not_le with (1 := Fx). now apply F2R_le_0. easy. } generalize (Bpred_correct x H4). rewrite Rlt_bool_true ; cycle 1. { apply Rlt_le_trans with 0%R. rewrite <- Ropp_0. apply Ropp_lt_contravar. apply bpow_gt_0. apply pred_ge_0. now apply FLT_exp_valid. exact Fx. apply generic_format_B2R. } intros [H7 [H8 H9]]. apply eq_sym. apply B2R_Bsign_inj ; try easy. rewrite H7, H1. apply pred_eq_pos. now apply Rlt_le. rewrite H9, H3. rewrite is_finite_strict_B2R by now apply Rgt_not_eq. now rewrite H5. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative