proposition: Lemma ErrFMA_correct: a*x+y = r1+r2+r3.
proof: Proof. Proof with auto with typeclass_instances. destruct V1_Und1 as [HZ|Und1']. assert (HZ1: u1 = 0). unfold u1; rewrite HZ; apply round_0... rewrite HZ; unfold r3; ring_simplify. unfold gamma, alpha2, beta2, beta1, alpha1. rewrite HZ1; replace u2 with 0. rewrite Rplus_0_r, Rplus_0_l; rewrite 2!round_generic with (x:=y)... replace r1 with y. replace (y-y) with 0 by ring. rewrite Rplus_0_r, round_0... rewrite Rplus_0_r, round_0... ring. unfold r1; rewrite HZ. rewrite Rplus_0_l, round_generic... unfold u2; rewrite HZ, HZ1; ring. assert (precisionNotZero : (1 < prec)%Z) by lia. replace (r1+r2+r3) with (r1+gamma+alpha2). 2: unfold r3; ring. assert (J1: format u2). replace (u2) with (-(u1-(a*x))) by (unfold u2; ring). apply generic_format_opp. apply mult_error_FLT... assert (J2: format alpha2). replace (alpha2) with (-(alpha1-(y+u2))) by (unfold alpha2; ring). apply generic_format_opp. apply plus_error... assert (J3: format beta2). replace (beta2) with (-(beta1-(u1+alpha1))) by (unfold beta2; ring). apply generic_format_opp. apply plus_error... apply generic_format_round... apply generic_format_round... 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 alpha2) as (fal2,(Hfal2,Hfal2')). 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 beta2) as (fbe2,(Hfbe2,Hfbe2')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. rewrite <- Hfa, <- Hfx, <- Hfy, <- Hfal2. 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+u2)) as (fal1,(Hfal1, (Hfal1',Hfal1''))). rewrite make_bound_Emin in Hfal1''; try assumption. replace (--emin)%Z with emin in Hfal1'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (u1+alpha1)) as (fbe1,(Hfbe1, (Hfbe1',Hfbe1''))). rewrite make_bound_Emin in Hfbe1''; try assumption. replace (--emin)%Z with emin in Hfbe1'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (beta1-r1)) as (ff,(Hff, (Hff',Hff''))). rewrite make_bound_Emin in Hff''; try assumption. replace (--emin)%Z with emin in Hff'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (FtoR beta ff+beta2)) as (fga,(Hfga, (Hfga',Hfga''))). rewrite make_bound_Emin in Hfga''; try assumption. replace (--emin)%Z with emin in Hfga'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (gamma+alpha2)) 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 gamma; rewrite <- Hff'', <- Hfga''. apply FmaErr with (make_bound beta prec emin) (Z.abs_nat prec) (fun r f => f = RND_Closest (make_bound beta prec emin) beta (Z.abs_nat prec) choice r) fu1 fu2 fal1 fbe1 fbe2 ff; try assumption. apply radix_gt_1. apply make_bound_p; lia. replace 3%nat with (Z.abs_nat 3). apply Zabs_nat_le; lia. now unfold Z.abs_nat, Pos.to_nat. intros r f H. rewrite H. apply RND_Closest_correct. replace 1%nat with (Z.abs_nat 1) by easy. apply Zabs_nat_lt; lia. apply make_bound_p; lia. intros x1 x2 g1 g2 K1 K2 K3. rewrite K1, K2, K3; easy. rewrite Hfal1''; fold alpha1. case V1_Und2; intros V;[now right|left]. apply FloatFexp_gt with beta (make_bound beta prec emin) prec. apply make_bound_p; lia. lia. apply FcanonicBound with (1:=Hfal1). rewrite Hfal1''; fold alpha1. now rewrite make_bound_Emin, Z.opp_involutive. rewrite Hfu1''; fold u1. case V1_Und3; intros V;[now right|left]. apply FloatFexp_gt with beta (make_bound beta prec emin) prec. apply make_bound_p; lia. lia. apply FcanonicBound with (1:=Hfu1). rewrite Hfu1''; fold u1. now rewrite make_bound_Emin, Z.opp_involutive. rewrite Hfbe1''; fold beta1. case V1_Und4; intros V;[now right|left]. apply FloatFexp_gt with beta (make_bound beta prec emin) prec. apply make_bound_p; lia. lia. apply FcanonicBound with (1:=Hfbe1). rewrite Hfbe1''; fold beta1. rewrite make_bound_Emin, Z.opp_involutive; try assumption. apply Rle_trans with (2:=V); right. f_equal; ring. rewrite Hfr1''; fold r1. case V1_Und5; intros V;[now right|left]. apply CanonicGeNormal with prec; try assumption. apply make_bound_p; lia. rewrite Hfr1''; fold r1. rewrite make_bound_Emin, Z.opp_involutive; try assumption. apply underf_mult_aux' with beta prec; try assumption. apply make_bound_p; lia. rewrite Hfa, Hfx. apply Rle_trans with (2:=Und1'). rewrite make_bound_Emin, Z.opp_involutive. now right. lia. rewrite Hfa, Hfx; apply Hfu1'. now rewrite Hfu2, Hfa, Hfx, Hfu1''. rewrite Hfy, Hfu2; apply Hfal1'. now rewrite Hfal2, Hfy, Hfu2, Hfal1''. now rewrite Hfbe2, Hfu1'', Hfal1'', Hfbe1''. rewrite Hfbe1'', Hfr1''; apply Hff'. rewrite Hfbe2; apply Hfga'. apply FcanonicUnique with (4:=Hfr1) (precision:=Z.abs_nat prec). apply radix_gt_1. apply sym_not_eq, Nat.lt_neq. apply absolu_lt_nz; lia. apply make_bound_p; lia. apply RND_Closest_canonic. replace 1%nat with (Z.abs_nat 1) by easy. apply Zabs_nat_lt; lia. apply make_bound_p; lia. rewrite Hfr1''. rewrite Hfa, Hfx, Hfy. rewrite pff_round_N_is_round; try assumption. f_equal; f_equal. rewrite make_bound_Emin; try easy; ring. apply make_bound_p; lia. rewrite Hfu1'', Hfal1''; fold u1; fold alpha1. apply FcanonicUnique with (4:=Hfbe1) (precision:=Z.abs_nat prec). apply radix_gt_1. apply sym_not_eq, Nat.lt_neq. apply absolu_lt_nz; lia. apply make_bound_p; lia. apply RND_Closest_canonic. replace 1%nat with (Z.abs_nat 1) by easy. apply Zabs_nat_lt; lia. apply make_bound_p; lia. rewrite pff_round_N_is_round; try assumption. rewrite Hfbe1''. f_equal; f_equal. rewrite make_bound_Emin; try easy; ring. apply make_bound_p; lia. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat