proposition: Theorem Axpy : tv = round radix2 (FLT_exp emin prec) Zfloor (y+a*x) \/ tv = round radix2 (FLT_exp emin prec) Zceil (y+a*x).
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 ta) as (fta,(Hfta,Hfta')). 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 tx) as (ftx,(Hftx,Hftx')). 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 ty) as (fty,(Hfty,Hfty')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. destruct (round_N_is_pff_round radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero choice (ta*tx)) as (fg,(Hfg, (Hfg',Hfg''))). rewrite make_bound_Emin in Hfg''; try assumption. replace (--emin)%Z with emin in Hfg'' by lia. destruct (round_N_is_pff_round radix2 (make_bound radix2 prec emin) prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero choice (ty+FtoR radix2 fg)) as (ftv,(Hftv, (Hftv',Hftv''))). rewrite make_bound_Emin in Hftv''; try assumption. replace (--emin)%Z with emin in Hftv'' by lia. assert (MinOrMax radix2 (make_bound radix2 prec emin) (a*x+y) ftv). unfold radix2 in Hfty, Hftx, Hfta; simpl in Hfty, Hftx, Hfta. apply Axpy_opt with (Z.abs_nat prec) fta ftx fty fg; try assumption. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. now apply FcanonicBound with radix2. now apply FcanonicBound with radix2. now rewrite Hfta, Hftx. now rewrite Rplus_comm, Hfty. rewrite Hfty, Hftx, Hfta. rewrite inj_abs; try lia. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. clear -H1. apply Rle_trans with (2:=H1); right. f_equal. rewrite bpow_powerRZ. unfold Rdiv; simpl; f_equal; ring. f_equal; rewrite bpow_powerRZ. simpl; f_equal; easy. rewrite Hfty, Hfta,Hftx. rewrite inj_abs; try lia. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. clear -H2. apply Rle_trans with (1:=H2); right. rewrite 3!bpow_powerRZ; unfold Z.pred, Z.succ. unfold Rminus; f_equal; f_equal; f_equal. f_equal; f_equal;[ring| f_equal; f_equal; ring]. f_equal; f_equal; ring. ring. unfold tv; rewrite <- Hfg'', <- Hftv''. case H; intros H'; [left|right]. apply trans_eq with (FtoR radix2 (RND_Min (make_bound radix2 prec emin) radix2 (Z.abs_nat prec) (a*x+y))). apply MinUniqueP with (make_bound radix2 prec emin) (a*x+y)%R; try easy. apply RND_Min_correct; try easy. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. rewrite pff_round_DN_is_round. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. rewrite Rplus_comm; easy. apply make_bound_p; lia. lia. apply trans_eq with (FtoR radix2 (RND_Max (make_bound radix2 prec emin) radix2 (Z.abs_nat prec) (a*x+y))). apply MaxUniqueP with (make_bound radix2 prec emin) (a*x+y)%R; try easy. apply RND_Max_correct; try easy. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. rewrite pff_round_UP_is_round. rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia. rewrite Rplus_comm; easy. apply make_bound_p; lia. lia. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat