proposition: Lemma ErrFmaAppr_correct: Rabs (r1+r2 -(a*x+y)) <= (3*beta/2+/2) * bpow beta (2-2*prec)%Z * Rabs (r1).
proof: Proof. Proof with auto with typeclass_instances. assert (precisionNotZero : (1 < prec)%Z) by lia. assert (J1: format u2). replace (u2) with (-(u1-(a*x))) by (unfold u2; ring). apply generic_format_opp. apply mult_error_FLT... intros L; case Und1; easy. assert (J2: format v2). replace (v2) with (-(v1-(y+u1))) by (unfold v2; ring). apply generic_format_opp. apply plus_error... apply generic_format_round... assert (G: forall f, Fcanonic beta (make_bound beta prec emin) f -> (FtoR beta f = 0 \/ bpow beta (emin+prec-1)%Z <= Rabs (FtoR beta f)) -> Fnormal beta (make_bound beta prec emin) f \/ FtoR beta f = 0%nat). intros f Hf K; case K; [right|left]. now rewrite H. apply CanonicGeNormal with prec; try easy. apply make_bound_p; lia. rewrite make_bound_Emin; try assumption. apply Rle_trans with (2:=H). apply bpow_le; lia. case Und1; intros Und1'. unfold r2, t1, t2, v2, v1, r1, u2, u1; rewrite Und1'. rewrite round_0... rewrite Rplus_0_l, Rplus_0_r. rewrite (round_generic _ _ _ y)... replace (y-y) with 0 by ring. rewrite Rplus_0_r, Rminus_0_l, Ropp_0, round_0... rewrite Rplus_0_l, round_0... replace (y+0-y) with 0 by ring; rewrite Rabs_R0. apply Rmult_le_pos. 2: apply Rabs_pos. apply Rmult_le_pos; try apply bpow_ge_0. apply Rplus_le_le_0_compat. apply Rmult_le_pos. apply Rmult_le_pos. auto with real. left; apply IZR_lt; apply radix_gt_0. left; apply pos_half_prf. left; apply pos_half_prf. destruct (format_is_pff_format beta (make_bound beta prec emin) prec (make_bound_p beta 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 beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero x) as (fx,(Hfx,Hfx')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. destruct (format_is_pff_format beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero y) as (fy,(Hfy,Hfy')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. destruct (format_is_pff_format beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero u2) as (fu2,(Hfu2,Hfu2')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. destruct (format_is_pff_format beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero v2) as (fv2,(Hfv2,Hfv2')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (a*x+y)) as (fr1,(Hfr1, (Hfr1',Hfr1''))). rewrite make_bound_Emin in Hfr1''; try assumption. replace (--emin)%Z with emin in Hfr1'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (a*x)) as (fu1,(Hfu1, (Hfu1',Hfu1''))). rewrite make_bound_Emin in Hfu1''; try assumption. replace (--emin)%Z with emin in Hfu1'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (y+u1)) as (fv1,(Hfv1, (Hfv1',Hfv1''))). rewrite make_bound_Emin in Hfv1''; try assumption. replace (--emin)%Z with emin in Hfv1'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (v1-r1)) as (ft1,(Hft1, (Hft1',Hft1''))). rewrite make_bound_Emin in Hft1''; try assumption. replace (--emin)%Z with emin in Hft1'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (u2+v2)) as (ft2,(Hft2, (Hft2',Hft2''))). rewrite make_bound_Emin in Hft2''; try assumption. replace (--emin)%Z with emin in Hft2'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (t1+t2)) as (fr2,(Hfr2, (Hfr2',Hfr2''))). rewrite make_bound_Emin in Hfr2''; try assumption. replace (--emin)%Z with emin in Hfr2'' by lia. unfold r1; rewrite <- Hfr1''. unfold r2; rewrite <- Hfr2''. rewrite <- Hfa, <- Hfx, <- Hfy. rewrite bpow_powerRZ. replace prec with (Z.of_nat (Z.abs_nat prec)). 2: rewrite inj_abs; lia. apply ErrFmaApprox with (make_bound beta prec emin) fu1 fu2 fv1 fv2 ft1 ft2; try assumption. apply radix_gt_1. apply make_bound_p; lia. replace 4%nat with (Z.abs_nat 4). apply Zabs_nat_le; lia. now unfold Z.abs_nat, Pos.to_nat. apply G; try assumption. case Und1; intros K1;[left|right]. rewrite Hfu1'', K1, round_0... rewrite Hfu1''. apply abs_round_ge_generic... apply generic_format_bpow. unfold FLT_exp; rewrite Z.max_l; lia. apply Rle_trans with (2:=K1). apply bpow_le; lia. apply G; try assumption. rewrite Hfv1''; apply Und2. apply G; try assumption. rewrite Hfr1''; apply Und3. apply G; try assumption. rewrite Hfr2''; apply Und4. apply G; try assumption. rewrite Hft2''; apply Und5. apply underf_mult_aux' with beta prec; try assumption. apply make_bound_p; assumption. rewrite Hfa, Hfx. apply Rle_trans with (2:=Und1'). apply bpow_le. rewrite make_bound_Emin, Z.opp_involutive; lia. rewrite Hfa, Hfx, Hfy; apply Hfr1'. rewrite Hfa, Hfx; apply Hfu1'. now rewrite Hfu2, Hfa, Hfx, Hfu1''. rewrite Hfu1'', Hfy, Rplus_comm; apply Hfv1'. rewrite Hfv2, Hfu1'', Hfy, Hfv1''. unfold v2; unfold v1; unfold u1; ring. rewrite Hfv1'', Hfr1''; apply Hft1'. rewrite Hfu2, Hfv2; apply Hft2'. rewrite Hft1'', Hft2''; apply Hfr2'. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat