proposition: Theorem discri_fp_test : Rabs (d-(b*b-a*c)) <= 2* ulp_flt d.
proof: Proof. Proof with auto with typeclass_instances. 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_can 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. now apply format_dp. destruct (format_is_pff_format_can 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. now 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 (round_NE_is_pff_round radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero (p+q)) as (fv,(Hfv, (Hfv',Hfv''))). rewrite make_bound_Emin in Hfv''; try assumption. replace (--emin)%Z with emin in Hfv'' by lia. destruct (round_NE_is_pff_round radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero (3*Rabs (FtoR radix2 ft))) as (fu,(Hfu, (Hfu',Hfu''))). rewrite make_bound_Emin in Hfu''; try assumption. replace (--emin)%Z with emin in Hfu'' 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_discri2. 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. cut ((FtoR radix2 fd = 0 \/ (Rabs (FtoR radix2 fd - (FtoR radix2 fb * FtoR radix2 fb - FtoR radix2 fa * FtoR radix2 fc)) <= 2 * Fulp (make_bound radix2 prec emin) 2 (Z.abs_nat prec) fd))). intros M; case M; try easy. intros KK; contradict Zd; rewrite <- Hfd; easy. apply discri16 with fp fq ft fdp fdq fs fu fv; try assumption. apply make_bound_p; lia. change 4%nat with (Z.abs_nat 4). apply Zabs_nat_le; lia. intros _; apply FcanonicBound with radix2; try assumption. intros _; apply FcanonicBound with radix2; try assumption. unfold radix2 in Hfb; simpl in Hfb; rewrite Hfb. case (Req_dec b 0); intros Zb. now left. right; apply Rle_trans with (bpow (emin + 3 * prec-1)). rewrite bpow_powerRZ; right; f_equal. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. rewrite inj_abs; lia. apply Rle_trans with (bpow (emin + 3 * prec)). apply bpow_le; lia. apply U1; auto with real. unfold radix2 in Hfa, Hfc; simpl in Hfa, Hfc; rewrite Hfa, Hfc. case (Req_dec (a*c) 0); intros Zac. now left. right; apply Rle_trans with (bpow (emin + 3 * prec - 1)). rewrite bpow_powerRZ; right; f_equal. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. rewrite inj_abs; lia. apply Rle_trans with (2:=U2 Zac); auto with real. apply bpow_le; lia. rewrite <- Hfb in Hfp'; assumption. rewrite <- Hfa, <- Hfc in Hfq'; assumption. generalize Hft'. unfold p; rewrite <- Hfp''; unfold q; now rewrite <- Hfq''. generalize Hfv'. unfold p; rewrite <- Hfp''; unfold q; now rewrite <- Hfq''. intros Y. assert (Y' : d = round_flt (p - q)). unfold d; rewrite Rle_bool_true; try easy. now rewrite <- Hfv'', <- Hft'', <- Hfu''. 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. replace 2%Z with (radix_val radix2) by easy. rewrite Hfdp; unfold dp; now rewrite <- Hfb, Hfp''. 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. now rewrite <- Hfv'', <- Hft'', <- Hfu''. 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