proposition: Lemma div_UP_correct : forall p x y, ((is_real_ub x /\ is_pos_real y) \/ (is_real_lb x /\ is_neg_real y)) -> valid_ub (div_UP p x y) = true /\ le_upper (Xdiv (toX x) (toX y)) (toX (div_UP p x y)).
proof: Proof. intros p x y. unfold div_UP, is_real_ub, is_real_lb, is_pos_real, is_neg_real. intros HH. split. now rewrite valid_ub_next_up. revert HH. rewrite valid_ub_correct, valid_lb_correct. unfold classify. rewrite classify_spec. rewrite <- B2SF_Prim2B. rewrite 3!toX_Prim2B. intros HH. rewrite next_up_equiv, div_equiv. destruct (Prim2B y) as [sy|sy| |sy my ey By] eqn:Hy. { destruct HH as [[_ HH]|[_ HH]] ; now elim (Rlt_irrefl 0). } { now destruct HH as [[_ HH]|[_ HH]]. } { now destruct HH as [[_ HH]|[_ HH]]. } unfold Xdiv', Xbind2. simpl. rewrite is_zero_correct_float. rewrite FtoR_split. destruct (Prim2B x) as [sx|sx| |sx mx ex Bx] eqn:Hx ; try easy. { simpl. unfold Rdiv at 1 ; rewrite Rmult_0_l. clear ; lra. } { destruct sx, sy ; try easy ; simpl in HH |- *. destruct HH as [[HH _]|[_ HH]] ; try easy. apply Rle_not_lt with (2 := HH). apply Rlt_le, Generic_proof.FtoR_Rpos. destruct HH as [[_ HH]|[HH _]] ; try easy. apply Rle_not_lt with (2 := HH). apply Rlt_le, Generic_proof.FtoR_Rneg. } clear HH. set (b_mxy := Bdiv _ _ _). generalize (Bsucc_correct _ _ Hprec Hmax b_mxy). assert (Hd: B2R (B754_finite sy my ey By) <> 0%R). { destruct sy. now apply Rlt_not_eq, Float_prop.F2R_lt_0. now apply Rgt_not_eq, Float_prop.F2R_gt_0. } generalize (Bdiv_correct _ _ Hprec Hmax mode_NE (B754_finite sx mx ex Bx) (B754_finite sy my ey By) Hd). 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 B2R_BtoX by easy. revert Hb. simpl Rdiv. 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. destruct sx, sy ; try easy. apply Rdiv_neg_compat. now apply Float_prop.F2R_le_0. now apply Float_prop.F2R_gt_0. apply Rmult_le_pos_neg. now apply Float_prop.F2R_ge_0. apply Rlt_le, Rinv_lt_0_compat. now apply Float_prop.F2R_lt_0. } intros H. apply Ropp_le_contravar in H. rewrite Ropp_involutive in H. rewrite <- (SF2B'_B2SF b_mxy), H1. change (BtoX (Bsucc _)) with (Xreal (FtoR radix2 true (shift_pos (Z.to_pos FloatOps.prec) 1 - 1) (emax - FloatOps.prec))). apply Rnot_lt_le. intros H'. apply (Rle_not_lt _ _ H). clear -H'. rewrite FtoR_split in H'. eapply Rlt_le_trans. 2: { apply Generic_fmt.round_le. now apply FLT.FLT_exp_valid. apply Generic_fmt.valid_rnd_N. apply Rlt_le. exact H'. } rewrite Generic_fmt.round_generic. 2: apply Generic_fmt.valid_rnd_N. apply Rcomplements.Rminus_lt_0. rewrite <- Float_prop.F2R_bpow. rewrite <- Operations.F2R_opp. rewrite <- Operations.F2R_minus. now apply Float_prop.F2R_gt_0. apply FLT.generic_format_FLT. now eexists. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig