proposition: Theorem Axpy_opt : forall (a1 x1 y1 : R) (a x y t u : float), (Fbounded b a) -> (Fbounded b x) -> (Fbounded b y) -> (Fbounded b t) -> (Fbounded b u) -> (Closest b radix (a * x) t) -> (Closest b radix (t + y) u) -> (Fcanonic radix b u) -> (Fcanonic radix b t) -> ((5 + 4 * (powerRZ radix (- precision))) * / (1 - powerRZ radix (- precision)) * (Rabs (a * x) + (powerRZ radix (Z.pred (- dExp b)))) <= Rabs y)%R -> (Rabs (y1 - y) + Rabs (a1 * x1 - a * x) <= (powerRZ radix (Z.pred (Z.pred (- precision)))) * (1 - powerRZ radix (Z.succ (- precision))) * Rabs y + - (powerRZ radix (Z.pred (Z.pred (- precision))) * Rabs (a * x)) + - powerRZ radix (Z.pred (Z.pred (- dExp b))))%R -> (MinOrMax radix b (a1 * x1 + y1) u).
proof: Proof. intros a1 x1 y1 a x y t u Fa Fx Fy Ft Fu tDef uDef Cu Ct H1 H2. apply Axpy_tFlessu with a x y t; auto. cut (0 < 1 - powerRZ radix (- precision))%R; [ intros H'1 | idtac ]. 2: apply Rplus_lt_reg_r with (powerRZ radix (- precision)). 2: ring_simplify (powerRZ radix (- precision) + 0)%R. 2: ring_simplify (powerRZ radix (- precision) + (1 - powerRZ radix (- precision)))%R. 2: replace 1%R with (powerRZ radix 0); [ auto with real zarith | simpl in |- *; auto ]. cut (0 < 1 + powerRZ radix (- precision))%R; [ intros H'2 | idtac ]. 2: apply Rlt_le_trans with 1%R; auto with real. 2: apply Rle_trans with (1 + 0)%R; auto with real zarith. cut ((5 + 4 * powerRZ radix (- precision)) * Rabs t <= Rabs y)%R; [ intros H3 | idtac ]. apply Rplus_le_reg_l with (- Rabs (FtoRradix u))%R. ring_simplify (- Rabs (FtoRradix u) + Rabs (FtoRradix u))%R. apply Rle_trans with (- ((Rabs y + - Rabs t) * / (1 + powerRZ radix (- precision))) + 4 * Rabs (FtoRradix t))%R; [ apply Rplus_le_compat_r; apply Ropp_le_contravar | idtac ]. apply Rle_trans with (Rabs (FtoRradix y + FtoRradix t) * / (1 + powerRZ radix (- precision)))%R. apply Rmult_le_compat_r; auto with real zarith. rewrite <- (Rabs_Ropp (FtoRradix t)). apply Rle_trans with (Rabs (FtoRradix y) - Rabs (- FtoRradix t))%R; [ right; ring | idtac ]. replace (FtoRradix y + FtoRradix t)%R with (FtoRradix y - - FtoRradix t)%R; [ apply Rabs_triang_inv | ring ]. case Cu; intros H4. apply Rmult_le_reg_l with (1 + powerRZ radix (- precision))%R; auto. apply Rle_trans with (Rabs (FtoRradix y + FtoRradix t) * ((1 + powerRZ radix (- precision)) * / (1 + powerRZ radix (- precision))))%R; [ right; ring; ring | idtac ]. rewrite Rinv_r; auto with real. ring_simplify (Rabs (FtoRradix y + FtoRradix t) * 1)%R. rewrite Rmult_plus_distr_r. apply Rle_trans with (Rabs u + / radix * Fulp b radix precision u)%R. apply Rplus_le_reg_l with (- Rabs u)%R. apply Rle_trans with (/ radix * Fulp b radix precision u)%R; [idtac|right; ring]. apply Rle_trans with (Rabs (FtoRradix y + FtoRradix t - FtoRradix u)). apply Rle_trans with (Rabs (FtoRradix y + FtoRradix t) - Rabs (FtoRradix u))%R; [ right; ring | apply Rabs_triang_inv ]. apply Rmult_le_reg_l with (IZR radix); auto with real zarith. apply Rle_trans with (Fulp b radix precision u * (radix * / radix))%R; [ rewrite Rinv_r; auto with real zarith | right; ring ]. ring_simplify (Fulp b radix precision u * 1)%R. unfold FtoRradix in |- *; apply ClosestUlp; auto with real zarith. rewrite Rplus_comm; auto. rewrite Rmult_1_l; apply Rplus_le_compat_l. apply Rmult_le_reg_l with (IZR radix); auto with real zarith. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real zarith. ring_simplify (1 * Fulp b radix precision u)%R. apply Rle_trans with (Rabs (FtoRradix u) * powerRZ radix (Z.succ (- precision)))%R. unfold FtoRradix in |- *; apply FulpLe2; auto with zarith. replace (Fnormalize radix b precision u) with u; [ idtac | apply FcanonicUnique with (radix := radix) (precision := precision) (b := b) ]; auto with zarith real. apply FnormalizeCanonic; auto with zarith. apply sym_eq; apply FnormalizeCorrect; auto with zarith. unfold Z.succ in |- *; rewrite powerRZ_add; auto with zarith real; simpl in |- *; auto with zarith real; right; ring. replace (FtoRradix y + FtoRradix t)%R with (FtoRradix u); auto with real. apply Rle_trans with (Rabs (FtoRradix u) * 1)%R; [ apply Rmult_le_compat_l | right; ring ]; auto with real. apply Rabs_pos. pattern 1%R at 2 in |- *; replace 1%R with (/ 1)%R; auto with real zarith. apply Rle_Rinv; auto with real zarith. pattern 1%R at 1 in |- *; replace 1%R with (1 + 0)%R; auto with real zarith. apply Rplus_le_compat_l. now apply powerRZ_le, IZR_lt. unfold FtoRradix in |- *; apply plusExact1 with b precision; auto with real zarith. rewrite Rplus_comm; auto. elim H4; intros H5 H6; elim H6; intros H7 H8; rewrite H7; apply Zmin_Zle; elim Fy; elim Ft; auto with zarith. apply Rle_trans with (((5 + 4 * powerRZ radix (- precision)) * Rabs (FtoRradix t) + - Rabs (FtoRradix y)) * / (1 + powerRZ radix (- precision)))%R. right; replace 5%R with (1 + 4)%R by ring. replace (4 * Rabs (FtoRradix t))%R with (4 * Rabs (FtoRradix t) * ((1 + powerRZ radix (- precision)) * / (1 + powerRZ radix (- precision))))%R. ring; ring. rewrite Rinv_r; auto with real; ring. apply Rle_trans with (0 * / (1 + powerRZ radix (- precision)))%R; [ apply Rmult_le_compat_r; auto with real | right; ring ]. apply Rplus_le_reg_l with (Rabs (FtoRradix y)). apply Rle_trans with ((5 + 4 * powerRZ radix (- precision)) * Rabs (FtoRradix t))%R; [ right; ring | ring_simplify (Rabs (FtoRradix y) + 0)%R ]; auto. apply Rle_trans with (2 := H1). rewrite Rmult_assoc. apply Rmult_le_compat_l; auto with real arith. apply Rle_trans with (5 + 4 * 0)%R; auto with real arith. ring_simplify (5 + 4 * 0)%R; auto with real arith. apply Rplus_le_compat_l; apply Rmult_le_compat_l. now apply IZR_le. now apply powerRZ_le, IZR_lt. apply Rle_trans with (Rabs (FtoRradix a * FtoRradix x) * / (1 - powerRZ radix (- precision)) + powerRZ radix (Z.pred (- dExp b)) * / (1 - powerRZ 2%Z (- precision)))%R; [ idtac | right; simpl; unfold radix; ring ]. unfold FtoRradix in |- *; apply RoundLeGeneral; auto with real zarith. now apply Rplus_le_compat_l, powerRZ_le, IZR_lt. ring_simplify. apply Rlt_powerRZ; auto with zarith; now apply IZR_lt. apply Rle_lt_trans with (1 := H2). apply UlpFlessuGe2 with t; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz