proposition: Lemma mul_DN_correct : forall p x y, ((is_non_neg_real x /\ is_non_neg_real y) \/ (is_non_pos_real x /\ is_non_pos_real y) \/ (is_non_neg' x /\ is_non_pos' y) \/ (is_non_pos' x /\ is_non_neg' y)) -> (valid_lb (mul_DN p x y) = true /\ le_lower (toX (mul_DN p x y)) (Xmul (toX x) (toX y))).
proof: Proof. intros p x y. unfold mul_DN, is_non_neg', is_non_pos', is_non_pos_real, is_non_neg_real. intros HH. split. now rewrite valid_lb_next_down. revert HH. rewrite 2!valid_ub_correct, 2!valid_lb_correct. unfold classify. rewrite 2!classify_spec. rewrite <- 2!B2SF_Prim2B. rewrite 3!toX_Prim2B. intros HH. unfold le_lower. rewrite next_down_equiv, mul_equiv. destruct (Prim2B x) as [sx|sx| |sx mx ex Bx] eqn:Hx ; try easy. { clear HH. destruct (Prim2B y) as [sy|sy| |sy my ey By] ; try easy ; simpl ; rewrite Rmult_0_l ; lra. } { destruct (Prim2B y) as [sy|sy| |sy my ey By] ; try easy ; simpl. now destruct sx, sy ; try easy ; simpl in HH |- * ; intuition. destruct sx, sy ; try easy ; simpl in HH |- * ; intuition. apply Rle_not_lt with (1 := H1). apply Generic_proof.FtoR_Rneg. apply Rle_not_lt with (1 := H1). apply Generic_proof.FtoR_Rpos. } destruct (Prim2B y) as [sy|sy| |sy my ey By] eqn:Hy ; try easy. simpl ; rewrite Rmult_0_r ; lra. simpl ; destruct xorb eqn:Hs ; simpl ; try easy. { destruct sx, sy ; try easy ; simpl in HH |- * ; intuition. apply Rle_not_lt with (1 := H0). apply Generic_proof.FtoR_Rneg. apply Rle_not_lt with (1 := H0). apply Generic_proof.FtoR_Rpos. } clear HH. set (b_mxy := Bmult _ _ _). generalize (Bpred_correct _ _ Hprec Hmax b_mxy). generalize (Bmult_correct _ _ Hprec Hmax mode_NE (B754_finite sx mx ex Bx) (B754_finite sy my ey By)). fold b_mxy. case Rlt_bool_spec. { intros _ [-> [-> H1]] H. specialize (H eq_refl). destruct Rlt_bool. 2: now destruct Bpred. destruct H as [H2 [H3 H4]]. rewrite !B2R_BtoX, H2 by easy. apply Ropp_le_contravar. apply Ulp.pred_round_le_id. now apply FLT.FLT_exp_valid. apply Generic_fmt.valid_rnd_N. } intros Hb H1 _. simpl in H1. destruct xorb eqn:Hs. now destruct b_mxy as [|[|]| |]. rewrite 2!B2R_BtoX by easy. revert Hb. simpl Xmul. simpl Rmult. rewrite <- Operations.F2R_mult. simpl Operations.Fmult. replace (cond_Zopp sx _ * _)%Z with (Z.pos mx * Z.pos my)%Z. 2: now destruct sx, sy. clear Hs. rewrite Rabs_pos_eq. 2: { apply Generic_fmt.round_ge_generic. now apply FLT.FLT_exp_valid. apply Generic_fmt.valid_rnd_N. apply Generic_fmt.generic_format_0. now apply Float_prop.F2R_ge_0. } set (v := Defs.F2R _). clearbody v. destruct b_mxy as [|[|]| |] ; try easy. clear. intros H. change (Bpred _) with (Bmax_float). rewrite B2R_BtoX by easy. apply Ropp_le_contravar. eapply Rle_trans. 2: apply (Ulp.pred_round_le_id radix2 (fexp FloatOps.prec emax) (round_mode mode_NE)). unfold Bmax_float. rewrite B2R_SF2B. simpl. replace (Defs.F2R _) with (Ulp.pred radix2 (fexp FloatOps.prec emax) (bpow radix2 emax)). { apply Ulp.pred_le with (4 := H). now apply FLT.FLT_exp_valid. now apply Generic_fmt.generic_format_bpow. apply Generic_fmt.generic_format_round. now apply FLT.FLT_exp_valid. apply Generic_fmt.valid_rnd_N. } rewrite Ulp.pred_bpow. unfold Defs.F2R. simpl. rewrite <- mult_IZR, <- minus_IZR. now apply f_equal. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig