proposition: Lemma sub_DN_correct : forall p x y, valid_lb x = true -> valid_ub y = true -> (valid_lb (sub_DN p x y) = true /\ le_lower (toX (sub_DN p x y)) (Xsub (toX x) (toX y))).
proof: Proof. intros p x y. unfold sub_DN. intros Vx Vy; split; [now rewrite valid_lb_next_down| ]; revert Vx Vy. rewrite valid_ub_correct, valid_lb_correct. unfold classify. rewrite !classify_spec. unfold toX, toF. rewrite <-!B2SF_Prim2B. rewrite next_down_equiv, sub_equiv. case_eq (Prim2B x); [intros sx|intros [ | ]| |intros sx mx ex Be]; intro Hx; try (intros H; discriminate H); intros _. { rewrite Xsub_split. rewrite Xadd_0_l. case_eq (Prim2B y); [intros [ | ]|intros [ | ]| |intros sy my ey By]; intro Hy; try (intros H; discriminate H); intros _; try (replace (SF64add _ _) with (Prim2SF y); [rewrite Hy]); try (now simpl); [case sx; compute; lra..| ]. rewrite <-Generic_proof.Fneg_correct. apply le_lower_pred_finite. } { now intros _; case Prim2B; [intros [ | ]|intros [ | ]| | ]. } { now simpl. } case_eq (Prim2B y); [intros sy|intros [ | ]| |intros sy my ey By]; intro Hy; try (intros H; discriminate H); intros _. { rewrite Xsub_split. rewrite <-Generic_proof.Fneg_correct. rewrite Xadd_0_r. apply le_lower_pred_finite. } { now case sx. } { now simpl. } rewrite <-Hx, <-Hy. set (b_x := Prim2B x). set (b_y := Prim2B y). set (b_xmy := Bminus _ _ _). generalize (Bpred_correct _ _ Hprec Hmax b_xmy). assert (Fx : is_finite b_x = true). { now unfold b_x; rewrite Hx. } assert (Fy : is_finite b_y = true). { now unfold b_y; rewrite Hy. } generalize (Bminus_correct _ _ Hprec Hmax mode_NE b_x b_y Fx Fy). fold b_xmy. assert (Hrx : B2R b_x = FtoR radix2 sx mx ex). { now unfold b_x, B2R; rewrite Hx, <-FtoR_split. } assert (Hry : B2R b_y = FtoR radix2 sy my ey). { now unfold b_y, B2R; rewrite Hy, <-FtoR_split. } case Rlt_bool_spec => Hb. { intros [Rxmy [Fxmy Sxmy]]. intro H; generalize (H Fxmy); clear H. case Rlt_bool; [ |now intros ->]. set (b_s := Bpred _). case_eq b_s; [intro ss..| |intros ss ms es Hes]; intro Hs. { intros [Rs _]; revert Rs; simpl => ->. rewrite Rxmy, Hrx, Hry. unfold b_x, b_y; rewrite Hx, Hy. apply Ropp_le_contravar. apply Ulp.pred_round_le_id. { now apply FLT.FLT_exp_valid. } now apply Generic_fmt.valid_rnd_N. } { now case ss. } { now simpl. } intros [Rs _]; revert Rs; simpl. rewrite <-FtoR_split => ->. rewrite Rxmy, Hrx, Hry. unfold b_x, b_y; rewrite Hx, Hy. apply Ropp_le_contravar. apply Ulp.pred_round_le_id. { now apply FLT.FLT_exp_valid. } now apply Generic_fmt.valid_rnd_N. } change (binary_overflow _ _ _ _) with (S754_infinity (Bsign b_x)). intros [Hxmy Sxy] _. revert Hxmy. case_eq b_xmy; [intro sxmy..| |intros sxmy mxmy exmy Hexmy]; intro Hxmy; try (intro H; discriminate H); [simpl]. case sxmy; [now simpl| ]. unfold FtoX. unfold le_lower, le_upper. intro H; inversion H as (Hsx); clear H. assert (Hsx' : Bsign b_x = sx). { now unfold b_x; rewrite Hx. } assert (Hsy' : Bsign b_y = sy). { now unfold b_y; rewrite Hy. } revert Hsx Sxy. rewrite !Hsx', Hsy'. intro Hsx''; rewrite <-Hsx'', <-(Bool.negb_involutive false); intro Hsy''. apply ssrbool.negb_inj in Hsy''. revert Hb; rewrite Hrx, Hry, <-Hsx'', <-Hsy''. unfold negb. set (sum := (_ - _)%R). rewrite Rabs_pos_eq. 2:{ set (fexp := SpecFloat.fexp _ _). set (rnd := round_mode _). rewrite <-(Generic_fmt.round_0 radix2 fexp rnd). apply Generic_fmt.round_le. { now apply FLT.FLT_exp_valid. } { now apply Generic_fmt.valid_rnd_N. } unfold sum. generalize (Generic_proof.FtoR_Rpos radix2 mx ex). generalize (Generic_proof.FtoR_Rneg radix2 my ey). lra. } unfold round_mode. set (c := fun _ => _). change (SpecFloat.fexp _ _) with (FLT.FLT_exp (3 - emax - FloatOps.prec) FloatOps.prec). elim (Relative.error_N_FLT radix2 (3 - emax - FloatOps.prec) _ Hprec c sum). intros eps [eta [Heps [Heta [Hepseta ->]]]]. intro Hb. case (Req_dec eta 0) => Heta0. { revert Hb. rewrite Heta0, Rplus_0_r. unfold b_x, b_y; rewrite Hx, Hy. intro Hb. apply Ropp_le_contravar. apply Rle_trans with (bpow radix2 emax / (1 + eps))%R. 2: { apply (Rmult_le_reg_r (1 + eps)). { revert Heps; compute; case Rcase_abs; lra. } rewrite <-Hsx'', <-Hsy''; unfold negb; fold sum. unfold Rdiv; rewrite Rmult_assoc, Rinv_l, ?Rmult_1_r; [exact Hb| ]. revert Heps; compute; case Rcase_abs; lra. } apply (Rmult_le_reg_r (1 + eps)). { generalize (Rabs_le_inv _ _ Heps); compute; lra. } unfold Rdiv; rewrite Rmult_assoc, Rinv_l, ?Rmult_1_r. 2:{ generalize (Rabs_le_inv _ _ Heps); compute; lra. } apply Rle_trans with (FtoR radix2 false (9007199254740992 - 1) 971 * (1 + /2 * bpow radix2 (-FloatOps.prec + 1)))%R. 2:{ compute; lra. } apply Rmult_le_compat_l; [compute; lra| ]. apply Rplus_le_compat_l. generalize (Rabs_le_inv _ _ Heps); intros [_ H]; exact H. } revert Hb. elim (Rmult_integral _ _ Hepseta); [ |lra]; intros ->. rewrite Rplus_0_r, Rmult_1_r. unfold b_x, b_y; rewrite Hx, Hy, <-Hsx'', <-Hsy''. intro H. apply Ropp_le_contravar. unfold negb; fold sum. apply (Rplus_le_reg_r eta). revert H; apply Rle_trans. generalize (Rabs_le_inv _ _ Heta). compute; lra. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig