proposition: Theorem Bsucc_correct : forall x, is_finite x = true -> 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) = Bsign x && is_finite_strict x)%bool else B2SF (Bsucc x) = S754_infinity false.
proof: Proof. intros [sx|sx| | [|] mx ex Bx] Hx ; try easy ; clear Hx. - simpl. change fexp with (FLT_exp emin prec). rewrite succ_0, ulp_FLT_0 by easy. rewrite Rlt_bool_true. repeat split ; cycle 1. now case sx. apply F2R_bpow. apply bpow_lt. apply emin_lt_emax. - change (B2R (B754_finite _ _ _ _)) with (F2R (Fopp (Float radix2 (Zpos mx) ex))). rewrite F2R_opp, succ_opp. rewrite Rlt_bool_true ; cycle 1. { apply Rle_lt_trans with 0%R. 2: apply bpow_gt_0. rewrite <- Ropp_0. apply Ropp_le_contravar. apply pred_ge_0. now apply FLT_exp_valid. now apply F2R_gt_0. apply generic_format_canonical. now apply (canonical_bounded false). } simpl. rewrite B2R_SF2B, is_finite_SF2B, Bsign_SF2B. generalize (binary_round_correct mode_ZR true (xO mx - 1) (ex - 1)). set (z := binary_round _ _ _ _). rewrite F2R_cond_Zopp. simpl. rewrite round_ZR_opp. rewrite round_ZR_DN by now apply F2R_ge_0. assert (H: F2R (Float radix2 (Zpos (xO mx - 1)) (ex - 1)) = (F2R (Float radix2 (Zpos mx) ex) - F2R (Float radix2 1 (ex - 1)))%R). { rewrite (F2R_change_exp _ (ex - 1) _ ex) by apply Z.le_pred_l. rewrite <- F2R_minus, Fminus_same_exp. apply F2R_eq. replace (ex - (ex - 1))%Z with 1%Z by ring. now rewrite Zmult_comm. } rewrite Rlt_bool_true. + intros [_ [H1 [H2 H3]]]. split. 2: now split. rewrite H1, H. apply f_equal. apply round_DN_minus_eps_pos. now apply FLT_exp_valid. now apply F2R_gt_0. apply (generic_format_B2R (B754_finite false mx ex Bx)). split. now apply F2R_gt_0. rewrite F2R_bpow. change fexp with (FLT_exp emin prec). destruct (ulp_FLT_pred_pos radix2 emin prec (F2R (Float radix2 (Zpos mx) ex))) as [Hu|[Hu1 Hu2]]. * apply (generic_format_B2R (B754_finite false mx ex Bx)). * now apply F2R_ge_0. * rewrite Hu. rewrite ulp_canonical. apply bpow_le. apply Z.le_pred_l. easy. now apply (canonical_bounded false). * rewrite Hu2. rewrite ulp_canonical. rewrite <- (Zmult_1_r radix2). change (_ / _)%R with (bpow radix2 ex * bpow radix2 (-1))%R. rewrite <- bpow_plus. apply Rle_refl. easy. now apply (canonical_bounded false). + rewrite Rabs_Ropp, Rabs_pos_eq. eapply Rle_lt_trans. 2: apply bounded_lt_emax with (1 := Bx). apply Rle_trans with (F2R (Float radix2 (Zpos (xO mx - 1)) (ex - 1))). apply round_DN_pt. now apply FLT_exp_valid. rewrite H. rewrite <- (Rminus_0_r (F2R _)) at 2. apply Rplus_le_compat_l. apply Ropp_le_contravar. now apply F2R_ge_0. apply round_DN_pt. now apply FLT_exp_valid. apply generic_format_0. now apply F2R_ge_0. - assert (Cx := proj1 (andb_prop _ _ Bx)). apply (canonical_canonical_mantissa false) in Cx. replace (succ _ _ _) with (F2R (Float radix2 (Zpos mx + 1) ex)) ; cycle 1. { unfold succ, B2R. rewrite Rle_bool_true by now apply F2R_ge_0. rewrite ulp_canonical by easy. rewrite <- F2R_bpow. rewrite <- F2R_plus. now rewrite Fplus_same_exp. } simpl. rewrite B2R_SF2B, is_finite_SF2B, Bsign_SF2B. generalize (binary_round_correct mode_UP false (mx + 1) ex). simpl. rewrite round_generic. + rewrite Rabs_pos_eq by now apply F2R_ge_0. case Rlt_bool_spec ; intros Hs. now intros [_ H]. intros H. rewrite B2SF_SF2B. now rewrite (proj2 H). + apply valid_rnd_UP. + destruct (mag radix2 (F2R (Float radix2 (Zpos mx) ex))) as [e He]. rewrite Rabs_pos_eq in He by now apply F2R_ge_0. refine (_ (He _)). 2: now apply F2R_neq_0. clear He. intros He. destruct (F2R_p1_le_bpow _ (Zpos mx) _ _ eq_refl (proj2 He)) as [H|H]. * apply generic_format_F2R. intros _. rewrite Cx at 2. apply cexp_ge_bpow. apply FLT_exp_monotone. rewrite Rabs_pos_eq by now apply F2R_ge_0. rewrite (mag_unique_pos _ _ e). apply He. split. apply Rle_trans with (1 := proj1 He). apply F2R_le. apply Z.le_succ_diag_r. exact H. * simpl in H. rewrite H. apply generic_format_FLT_bpow. easy. apply le_bpow with radix2. apply Rlt_le. apply Rle_lt_trans with (2 := proj2 He). apply generic_format_ge_bpow with fexp. intros e'. apply Z.le_max_r. now apply F2R_gt_0. now apply generic_format_canonical. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative