proposition: Lemma div_DN_correct : forall p x y, ((is_real_ub x /\ is_neg_real y) \/ (is_real_lb x /\ is_pos_real y)) -> valid_lb (div_DN p x y) = true /\ le_lower (toX (div_DN p x y)) (Xdiv (toX x) (toX y)).
proof: Proof. intros p x y. unfold div_DN, is_real_ub, is_real_lb, is_pos_real, is_neg_real. intros HH. split. now rewrite valid_lb_next_down. 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_down_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. apply Ropp_le_contravar. unfold Rdiv at 2 ; rewrite Rmult_0_l. clear ; lra. } { destruct sx, sy ; try easy ; cbn in HH |- *. destruct HH as [[HH _]|[_ HH]] ; try easy. apply Rle_not_lt with (2 := HH). apply Rlt_le, Generic_proof.FtoR_Rneg. destruct HH as [[_ HH]|[HH _]] ; try easy. apply Rle_not_lt with (2 := HH). apply Rlt_le, Generic_proof.FtoR_Rpos. } clear HH. set (b_mxy := Bdiv _ _ _). generalize (Bpred_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 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 (B2R_BtoX (B754_finite _ _ _ _)) by easy. revert Hb. simpl Rdiv. 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. destruct sx, sy ; try easy. apply Rmult_le_neg_neg. now apply Float_prop.F2R_le_0. apply Rlt_le, Rinv_lt_0_compat. now apply Float_prop.F2R_lt_0. apply Rdiv_pos_compat. now apply Float_prop.F2R_ge_0. now apply Float_prop.F2R_gt_0. } intros H. rewrite <- (SF2B'_B2SF b_mxy), H1. change (BtoX (Bpred _)) with (Xreal (FtoR radix2 false (shift_pos (Z.to_pos FloatOps.prec) 1 - 1) (emax - FloatOps.prec))). apply Ropp_le_contravar. apply Rnot_lt_le. intros H'. apply (Rle_not_lt _ _ H). clear -H'. rewrite FtoR_split in H'. eapply Rle_lt_trans. { 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_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