proposition: Theorem Bpred_correct : forall x, is_finite x = true -> if Rlt_bool (- bpow radix2 emax) (pred radix2 fexp (B2R x)) then B2R (Bpred x) = pred radix2 fexp (B2R x) /\ is_finite (Bpred x) = true /\ (Bsign (Bpred x) = Bsign x || negb (is_finite_strict x))%bool else B2SF (Bpred x) = S754_infinity true.
proof: Proof. intros x Fx. assert (Fox : is_finite (Bopp x) = true). { now rewrite is_finite_Bopp. } rewrite <-(Ropp_involutive (B2R x)), <-B2R_Bopp. rewrite pred_opp, Rlt_bool_opp. generalize (Bsucc_correct _ Fox). case (Rlt_bool _ _). - intros (HR, (HF, HS)); unfold Bpred. rewrite B2R_Bopp, HR, is_finite_Bopp. rewrite <-(Bool.negb_involutive (Bsign x)), <-Bool.negb_andb. apply (conj eq_refl). apply (conj HF). rewrite Bsign_Bopp, <-(Bsign_Bopp x), HS. + now rewrite is_finite_strict_Bopp. + now revert Fx; case x. + now revert HF; case (Bsucc _). - now unfold Bpred; case (Bsucc _); intro s; case s. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative