proposition: Lemma Bdiv2_correct x : is_finite x = true -> let x2 := Bdiv mode_NE x (Prim2B 2) in B2R x2 = Generic_fmt.round radix2 (FLT.FLT_exp (3 - emax - FloatOps.prec) FloatOps.prec) (round_mode mode_NE) (B2R x / 2) /\ is_finite x2 = true /\ Bsign x2 = Bsign x /\ (Rabs (B2R x2) <= Rabs (B2R x))%R.
proof: Proof. set (b2 := Prim2B 2). assert (Hb2 : { H | b2 = B754_finite false 4503599627370496 (-51) H }). { now compute; eexists. } assert (Nz2 : B2R b2 <> 0%R). { compute; lra. } case x => [sx|sx| |sx mx ex Hmex]; [ |intro H; discriminate H..| ]; intros _ x2. { unfold x2. elim Hb2 => Hb2f ->. simpl; unfold Rdiv; rewrite Rabs_R0, Rmult_0_l. rewrite Generic_fmt.round_0; [ |now apply Generic_fmt.valid_rnd_N]. now split; [ |split; [ |split; [case sx|right]]]. } generalize (Bdiv_correct _ _ Hprec Hmax mode_NE (B754_finite sx mx ex Hmex) b2 Nz2). fold x2. set (fexp := FLT.FLT_exp _ _). set (m := round_mode _). set (rx := B2R (B754_finite sx mx ex _)). replace (B2R _) with 2%R; [ |compute; lra]. cut ((Rabs (Generic_fmt.round radix2 fexp m (rx / 2)) <= Rabs rx)%R). { intro Hrx2rx. rewrite Rlt_bool_true. 2:{ generalize (abs_B2R_lt_emax _ _ (B754_finite false mx ex Hmex)). apply Rle_lt_trans. revert Hrx2rx. unfold rx, B2R; rewrite <-!FtoR_split. now rewrite !Generic_proof.FtoR_abs. } simpl. intros [-> [Fx2 Sx2]]. split; [reflexivity|split; [exact Fx2|split; [ |exact Hrx2rx]]]. now rewrite Sx2; [case sx|revert Fx2; case x2]. } case (Rlt_or_le rx 0) => Hrx. { rewrite (Rabs_left1 rx); [ |now apply Rlt_le]. rewrite Rabs_left1. { apply Ropp_le_contravar. rewrite <-(Generic_fmt.round_generic radix2 fexp m rx) at 1. { apply Generic_fmt.round_le. { now apply FLT.FLT_exp_valid. } { now apply Generic_fmt.valid_rnd_N. } lra. } apply generic_format_B2R. } rewrite <-(Generic_fmt.round_0 radix2 fexp m). apply Generic_fmt.round_le. { now apply FLT.FLT_exp_valid. } { now apply Generic_fmt.valid_rnd_N. } lra. } rewrite (Rabs_pos_eq _ Hrx). rewrite Rabs_pos_eq. { rewrite <-(Generic_fmt.round_generic radix2 fexp m rx) at 2. { apply Generic_fmt.round_le. { now apply FLT.FLT_exp_valid. } { now apply Generic_fmt.valid_rnd_N. } lra. } apply generic_format_B2R. } rewrite <-(Generic_fmt.round_0 radix2 fexp m). apply Generic_fmt.round_le. { now apply FLT.FLT_exp_valid. } { now apply Generic_fmt.valid_rnd_N. } lra. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig