proposition: Theorem discri_correct_test : Rabs (d-(b*b-a*c)) <= 2* ulp_flt d.
proof: Proof. Proof with auto with typeclass_instances. case (Req_dec (b*b) 0); intros Zbb. unfold d, p; rewrite Zbb, round_0... rewrite Rplus_0_l, Rminus_0_l, Rabs_Ropp. rewrite Rle_bool_true. rewrite round_NE_opp. rewrite ulp_opp. rewrite round_generic... 2: apply generic_format_round... apply Rle_trans with (Rabs (-(q-a*c))). right; f_equal; ring. rewrite Rabs_Ropp. apply Rle_trans with (1:=error_le_half_ulp_round _ _ _ _). fold q; apply Rmult_le_compat_r. apply ulp_ge_0. lra. apply Rle_trans with (1:=RRle_abs _). rewrite <- (Rmult_1_l (Rabs _)) at 1. apply Rmult_le_compat_r. apply Rabs_pos. lra. case (Req_dec (a*c) 0); intros Zac. unfold d, q; rewrite Zac, round_0... rewrite Rplus_0_r, 2!Rminus_0_r. rewrite Rle_bool_true. rewrite round_generic... 2: apply generic_format_round... apply Rle_trans with (1:=error_le_half_ulp_round _ _ _ _). fold p; apply Rmult_le_compat_r. apply ulp_ge_0. lra. apply Rle_trans with (1:=RRle_abs _). rewrite <- (Rmult_1_l (Rabs _)) at 1. apply Rmult_le_compat_r. apply Rabs_pos. lra. case (Req_dec (p-q) 0); intros Zpq. assert (H:d = round_flt (dp - dq)). unfold d; case (Rle_bool_spec _ _); intros H. contradict Zd. unfold d; rewrite Rle_bool_true; try assumption. rewrite Zpq, round_0... rewrite Zpq, round_0... rewrite Rplus_0_l, round_generic... apply generic_format_round... replace d with (round_flt (b * b - a * c)). apply Rle_trans with (1:=error_le_half_ulp_round _ _ _ _). apply Rmult_le_compat_r. apply ulp_ge_0. lra. rewrite H; f_equal. unfold dp, dq; apply trans_eq with (b * b - a * c - (p-q)). rewrite Zpq; ring. ring. assert (G: (3 * Rabs (p - q) < p + q /\ round_flt (dp - dq) = dp-dq) \/ ((3 * Rabs (p - q) < p + q) -> round_flt (dp - dq) <> dp-dq)). case (Req_dec (round_flt (dp - dq)) (dp-dq)); intros G1; case (Rlt_or_le (3 * Rabs (p - q)) (p+q)); intros G2. left; now split. right; intros G3; contradict G2; apply Rlt_not_le; easy. now right. now right. destruct G as [(G1,G2)|G]. unfold d; rewrite Rle_bool_false... rewrite G2. replace (round_flt (p - q)) with (p-q). replace ((p - q + (dp - dq))) with (b * b - a * c). 2: unfold dp, p, dq, q; ring. apply Rle_trans with (1:=error_le_half_ulp_round _ _ _ _). apply Rmult_le_compat_r. apply ulp_ge_0. lra. apply sym_eq, round_generic... apply sterbenz... apply generic_format_round... apply generic_format_round... split. apply Rmult_le_reg_l with 4%R. lra. apply Rplus_le_reg_l with (q-3*p). apply Rle_trans with (p+q);[idtac|right; ring]. apply Rlt_le, Rle_lt_trans with (2:=G1). rewrite <- Rabs_Ropp. apply Rle_trans with (3*(-(p-q))). right; field. apply Rmult_le_compat_l; [lra|apply RRle_abs]. apply Rmult_le_reg_l with 2%R. lra. apply Rplus_le_reg_l with (p-3*q). apply Rle_trans with (p+q);[idtac|right; ring]. apply Rlt_le, Rle_lt_trans with (2:=G1). apply Rle_trans with (3*(p-q)). right; field. apply Rmult_le_compat_l; [lra|apply RRle_abs]. assert (precisionNotZero : (1 < prec)%Z) by lia. destruct (format_is_pff_format radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero a) as (fa,(Hfa,Hfa')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. destruct (format_is_pff_format radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero b) as (fb,(Hfb,Hfb')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. destruct (format_is_pff_format radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero c) as (fc,(Hfc,Hfc')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. destruct (round_NE_is_pff_round radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero (b*b)) as (fp,(Hfp, (Hfp',Hfp''))). rewrite make_bound_Emin in Hfp''; try assumption. replace (--emin)%Z with emin in Hfp'' by lia. destruct (round_NE_is_pff_round radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero (a*c)) as (fq,(Hfq, (Hfq',Hfq''))). rewrite make_bound_Emin in Hfq''; try assumption. replace (--emin)%Z with emin in Hfq'' by lia. destruct (format_is_pff_format radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero dp) as (fdp,(Hfdp,Hfdp')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. apply format_dp. destruct (format_is_pff_format radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero dq) as (fdq,(Hfdq,Hfdq')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. apply format_dq. destruct (round_NE_is_pff_round radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero (p-q)) as (ft,(Hft, (Hft',Hft''))). rewrite make_bound_Emin in Hft''; try assumption. replace (--emin)%Z with emin in Hft'' by lia. destruct (round_NE_is_pff_round radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero (dp-dq)) as (fs,(Hfs, (Hfs',Hfs''))). rewrite make_bound_Emin in Hfs''; try assumption. replace (--emin)%Z with emin in Hfs'' by lia. destruct (format_is_pff_format_can radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero d) as (fd,(Hfd,Hfd')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. apply format_d_discri1. assert (K: (1 < Z.abs_nat prec)%nat). replace 1%nat with (Z.abs_nat 1) by easy. apply Zabs_nat_lt; lia. rewrite <- Hfd, <- Hfb, <- Hfa, <- Hfc. apply Rle_trans with (2 * Fulp (make_bound radix2 prec emin) 2 (Z.abs_nat prec) fd)%R. apply discri with fp fq ft fdp fdq fs; try assumption. apply make_bound_p; lia. apply FcanonicBound with radix2; try assumption. apply FcanonicBound with radix2; try assumption. apply FcanonicBound with radix2; try assumption. apply FcanonicBound with radix2; try assumption. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. assert (emin < Pff.Fexp fd)%Z; try lia. apply FloatFexp_gt with radix2 (make_bound radix2 prec emin) prec; try assumption. apply make_bound_p; lia. apply FcanonicBound with radix2; try assumption. rewrite Hfd. apply U4_discri1; assumption. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. assert (emin < Pff.Fexp ft)%Z; try lia. apply FloatFexp_gt with radix2 (make_bound radix2 prec emin) prec; try assumption. apply make_bound_p; lia. now apply FcanonicBound with radix2. rewrite Hft''. apply Rle_trans with (2:=U3_discri1 Zbb Zac Zpq). apply bpow_le; lia. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. rewrite inj_abs;[idtac|lia]. replace 2%Z with (radix_val radix2) by easy. rewrite Hfb. apply Rle_trans with (2:=U1 Zbb). rewrite <- bpow_powerRZ. apply bpow_le; simpl (radix_val radix2); lia. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. rewrite inj_abs;[idtac|lia]. replace 2%Z with (radix_val radix2) by easy. rewrite Hfa, Hfc. apply Rle_trans with (2:=U2 Zac). rewrite <- bpow_powerRZ. apply bpow_le; simpl (radix_val radix2); lia. replace 2%Z with (radix_val radix2) by easy. right; apply CanonicGeNormal with prec; try assumption. apply make_bound_p; lia. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. rewrite Hfp''. apply abs_round_ge_generic... apply generic_format_FLT_bpow... lia. apply Rle_trans with (2:=U1 Zbb). apply bpow_le; lia. replace 2%Z with (radix_val radix2) by easy. right; apply CanonicGeNormal with prec; try assumption. apply make_bound_p; lia. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. rewrite Hfq''. apply abs_round_ge_generic... apply generic_format_FLT_bpow... lia. apply Rle_trans with (2:=U2 Zac). apply bpow_le; lia. intros C; right. replace 2%Z with (radix_val radix2) by easy. apply CanonicGeNormal with prec; try assumption. apply make_bound_p; lia. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. rewrite Hfs''. apply U5_discri1; try assumption. apply G. unfold p, q; rewrite <- Hfp'', <- Hfq''; easy. replace 2%Z with (radix_val radix2) by easy. apply CanonicGeNormal with prec; try assumption. apply make_bound_p; lia. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. rewrite Hfd. apply Rle_trans with (2:=U4_discri1 Zbb Zac Zpq). apply bpow_le; lia. rewrite <- Hfb in Hfp'; assumption. rewrite <- Hfa, <- Hfc in Hfq'; assumption. intros Y. assert (Y' : d = round_flt (p - q)). unfold d; rewrite Rle_bool_true; try easy. unfold p; rewrite <- Hfp''; unfold q; rewrite <- Hfq''. easy. apply EvenClosestCompatible with (p-q) (RND_EvenClosest (make_bound radix2 prec emin) radix2 (Z.abs_nat prec) (p-q)); try easy. apply make_bound_p; lia. apply RND_EvenClosest_correct; try easy. apply make_bound_p; lia. unfold p; rewrite <- Hfp''; unfold q; now rewrite <- Hfq''. replace 2%Z with (radix_val radix2) by easy. rewrite Hfd, Y'. rewrite pff_round_NE_is_round; try easy. 2: apply make_bound_p; lia. 2: apply FcanonicBound with radix2; try assumption. rewrite make_bound_Emin; try assumption. now replace (--emin)%Z with emin by lia. intros _; generalize Hft'. unfold p; rewrite <- Hfp''; unfold q; now rewrite <- Hfq''. intros _; replace 2%Z with (radix_val radix2) by easy. rewrite Hfdp; unfold dp; now rewrite <- Hfb, Hfp''. intros _; replace 2%Z with (radix_val radix2) by easy. rewrite Hfdq; unfold dq; now rewrite <- Hfa, <- Hfc, Hfq''. intros _; generalize Hfs'. now rewrite <- Hfdp, <- Hfdq. intros Y. assert (Y' : d = round_flt (round_flt (p - q) + round_flt (dp - dq))). unfold d; rewrite Rle_bool_false; try easy. unfold p; rewrite <- Hfp''; unfold q; rewrite <- Hfq''. easy. apply EvenClosestCompatible with (FtoR radix2 ft+FtoR radix2 fs) (RND_EvenClosest (make_bound radix2 prec emin) radix2 (Z.abs_nat prec) (FtoR radix2 ft+FtoR radix2 fs)); try easy. apply make_bound_p; lia. apply RND_EvenClosest_correct; try easy. apply make_bound_p; lia. replace 2%Z with (radix_val radix2) by easy. rewrite Hfd, Y'. rewrite pff_round_NE_is_round; try easy. 2: apply make_bound_p; lia. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. now rewrite Hfs'', Hft''. apply FcanonicBound with radix2; try assumption. right; f_equal. replace 2%Z with (radix_val radix2) by easy. rewrite Fulp_ulp; try easy. 2: apply make_bound_p; lia. rewrite make_bound_Emin; try assumption. now replace (--emin)%Z with emin by lia. apply FcanonicBound with radix2; try assumption. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat