proposition: Lemma div2_correct : forall x, sensible_format = true -> (1 / 256 <= Rabs (toR x))%R -> toX (div2 x) = Xdiv (toX x) (Xreal 2).
proof: Proof. intros x _. unfold toR, toX, toF. rewrite <-!B2SF_Prim2B. unfold div2. rewrite div_equiv. set (bx := Prim2B x). set (b2 := Prim2B 2). case bx => [sx|sx| |sx mx ex Hmex]; clear x bx; try (simpl; change R0 with 0%R; rewrite Rabs_R0; intro H; exfalso; lra); [ ]. pose (bx := B754_finite sx mx ex Hmex). intro Hx. unfold Xdiv, Xdiv'; rewrite is_zero_false; [ |lra]. elim (Bdiv2_correct bx eq_refl). fold b2. set (x2 := Bdiv _ _ _). intros Rx2 [Fx2 _]; revert Rx2 Fx2. rewrite Generic_fmt.round_generic. 2:{ now apply Generic_fmt.valid_rnd_N. } 2:{ unfold Rdiv; change (/ 2)%R with (bpow radix2 (-1)). apply mult_bpow_exact_FLT. { apply generic_format_B2R. } rewrite Z.le_sub_le_add_l, <-Z.le_sub_le_add_r; simpl. apply mag_ge_bpow. unfold B2R. revert Hx. rewrite <-FtoR_split. apply Rle_trans. compute; lra. } unfold B2SF at 2, FtoX. unfold B2R at 2, bx; rewrite <-FtoR_split => <-. case x2 => [sx2|sx2| |sx2 mx2 ex2 Hmex2]; [reflexivity|intro H; discriminate H..|intros _]. now unfold B2R; rewrite <-FtoR_split. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig