proposition: Lemma mul_UP_correct : forall p x y, ((is_non_neg' x /\ is_non_neg' y) \/ (is_non_pos' x /\ is_non_pos' y) \/ (is_non_pos_real x /\ is_non_neg_real y) \/ (is_non_neg_real x /\ is_non_pos_real y)) -> valid_ub (mul_UP p x y) = true /\ le_upper (Xmul (toX x) (toX y)) (toX (mul_UP p x y)).
proof: Proof. intros p x y. unfold mul_UP, is_non_neg', is_non_pos', is_non_pos_real, is_non_neg_real. intros HH. split. now rewrite valid_ub_next_up. 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. rewrite next_up_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_Rpos. apply Rle_not_lt with (1 := H1). apply Generic_proof.FtoR_Rneg. } 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 := H). apply Generic_proof.FtoR_Rpos. } clear HH. set (b_mxy := Bmult _ _ _). generalize (Bsucc_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 Bsucc. destruct H as [H2 [H3 H4]]. rewrite !B2R_BtoX, H2 by easy. apply Ulp.succ_round_ge_id. now apply FLT.FLT_exp_valid. apply Generic_fmt.valid_rnd_N. } intros Hb H1 _. simpl in H1. destruct xorb eqn:Hs. 2: 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_left1. 2: { apply Generic_fmt.round_le_generic. now apply FLT.FLT_exp_valid. apply Generic_fmt.valid_rnd_N. apply Generic_fmt.generic_format_0. now apply Float_prop.F2R_le_0. } set (v := Defs.F2R _). clearbody v. destruct b_mxy as [|[|]| |] ; try easy. clear. intros H. change (Bsucc _) with (Bopp Bmax_float). rewrite BtoX_Bopp. unfold Bmax_float. rewrite B2R_BtoX by easy. rewrite B2R_SF2B. simpl. apply Ropp_le_contravar in H. rewrite Ropp_involutive in H. eapply Rle_trans. apply (Ulp.succ_round_ge_id radix2 (fexp FloatOps.prec emax) (round_mode mode_NE)). replace (Ropp _) with (Ulp.succ radix2 (fexp FloatOps.prec emax) (-bpow radix2 emax)). { apply Ulp.succ_le with (4 := H). now apply FLT.FLT_exp_valid. apply Generic_fmt.generic_format_round. now apply FLT.FLT_exp_valid. apply Generic_fmt.valid_rnd_N. apply Generic_fmt.generic_format_opp. now apply Generic_fmt.generic_format_bpow. } rewrite Ulp.succ_opp, Ulp.pred_bpow. apply f_equal. 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