proposition: Theorem Axpy_aux3 : Fcanonic radix b u -> Fsubnormal radix b t -> (0 < u)%R -> Fexp (FPred b radix precision u) = (- dExp b)%Z -> (Z.succ (- dExp b) <= Fexp u)%Z -> (Rabs (y1 - y) + Rabs (a1 * x1 - a * x) < / 4 * Fulp b radix precision (FPred b radix precision u))%R -> MinOrMax radix b (a1 * x1 + y1) u.
proof: Proof. intros H1 H2 H3 H4 H5 H6. case (Rle_or_lt u (a1 * x1 + y1)); intros H7. apply MinOrMax2 with precision; auto with zarith real; fold FtoRradix in |- *. replace (a1 * x1 + y1 - FtoRradix u)%R with (y1 - y + (a1 * x1 - a * x) + (a * x - t + (t + y - u)))%R; [ idtac | ring ]. apply Rlt_le_trans with (/ 4 * powerRZ radix (- dExp b) + (/ 2 * powerRZ radix (- dExp b) + / 2 * Fulp b radix precision u))%R. apply Rle_lt_trans with (Rabs (y1 - FtoRradix y + (a1 * x1 - FtoRradix a * FtoRradix x)) + Rabs (FtoRradix a * FtoRradix x - FtoRradix t + (FtoRradix t + FtoRradix y - FtoRradix u)))%R; [ apply Rabs_triang | idtac ]. apply Rlt_le_trans with (/ 4 * powerRZ radix (- dExp b) + Rabs (FtoRradix a * FtoRradix x - FtoRradix t + (FtoRradix t + FtoRradix y - FtoRradix u)))%R; [ apply Rplus_lt_compat_r | apply Rplus_le_compat_l ]. apply Rle_lt_trans with (Rabs (y1 - FtoRradix y) + Rabs (a1 * x1 - FtoRradix a * FtoRradix x))%R; [ apply Rabs_triang | idtac ]. apply Rlt_le_trans with (1 := H6); unfold Fulp in |- *. replace (Fexp (Fnormalize radix b precision (FPred b radix precision u))) with (- dExp b)%Z; auto with real zarith. replace (Fnormalize radix b precision (FPred b radix precision u)) with (FPred b radix precision u); auto with zarith. apply FcanonicUnique with (radix := radix) (b := b) (precision := precision); auto with real zarith. apply FPredCanonic; auto with zarith. apply FnormalizeCanonic; auto with zarith. apply FBoundedPred; auto with zarith. apply sym_eq; apply FnormalizeCorrect; auto with zarith. apply Rle_trans with (Rabs (FtoRradix a * FtoRradix x - FtoRradix t) + Rabs (FtoRradix t + FtoRradix y - FtoRradix u))%R; [ apply Rabs_triang | apply Rplus_le_compat ]. apply Rmult_le_reg_l with 2%R; [ idtac | rewrite <- Rmult_assoc; rewrite Rinv_r ]; auto with arith real. ring_simplify; apply Rle_trans with (Fulp b radix precision t); [ unfold FtoRradix in |- *; apply ClosestUlp; auto with zarith | unfold Fulp in |- * ]. replace (Fexp (Fnormalize radix b precision t)) with (- dExp b)%Z; auto with real zarith. replace (Fnormalize radix b precision t) with t. elim H2; auto with zarith. apply FcanonicUnique with (radix := radix) (b := b) (precision := precision); auto with real zarith. right; auto. apply FnormalizeCanonic; auto with zarith. apply sym_eq; apply FnormalizeCorrect; auto with zarith. apply Rmult_le_reg_l with 2%R; [ idtac | rewrite <- Rmult_assoc; rewrite Rinv_r ]; auto with arith real. ring_simplify (1 * Fulp b radix precision u)%R; unfold FtoRradix in |- *; apply ClosestUlp; auto with zarith. apply Rmult_le_reg_l with 4%R; auto with arith real. apply Rle_trans with (powerRZ radix (-dExp b) * 3 + Fulp b radix precision u * 2)%R. right; simpl; field; auto with real. apply Rle_trans with (Fulp b radix precision u * 2 + Fulp b radix precision u * 2)%R; [ apply Rplus_le_compat_r | idtac ]; auto with real arith. apply Rle_trans with (3 * powerRZ radix (- dExp b))%R; [ right;ring | idtac ]. apply Rle_trans with (4 * powerRZ radix (- dExp b))%R; auto with arith zarith real. apply Rmult_le_compat_r. now apply powerRZ_le, IZR_lt. now apply IZR_le. unfold Fulp in |- *; replace 2%R with (powerRZ radix 1); [ idtac | simpl in |- *; auto with zarith real ]. replace 4%R with (powerRZ radix 2); [ idtac | simpl; unfold pow, radix; ring ]. repeat rewrite <- powerRZ_add; auto with zarith real. replace (2 + - dExp b)%Z with (Z.succ (- dExp b) + 1)%Z; [ apply Rle_powerRZ | unfold Z.succ in |- * ]; auto with zarith real. replace (Fnormalize radix b precision u) with u; auto with zarith arith. apply FcanonicUnique with (radix := radix) (b := b) (precision := precision); auto with real zarith. apply FnormalizeCanonic; auto with zarith. apply sym_eq; apply FnormalizeCorrect; auto with zarith. lra. case (Rle_or_lt (t + y) u); intros H8. apply Axpy_aux2; auto. apply sym_eq; unfold FtoRradix in |- *; apply ExactSum_Near with b precision; auto with zarith. elim H2; intuition. cut (forall v w : R, (v <= w)%R -> v <> w -> (v < w)%R); [ intros V | idtac ]. 2: intros V W H' H'1; case H'; auto with real. 2: intros H'2; absurd (V = W); auto with real. apply V. apply Rmult_le_reg_l with 2%R; auto with real arith. apply Rle_trans with (Fulp b radix precision u); [ unfold FtoRradix in |- *; apply ClosestUlp; auto with zarith | idtac ]. replace (powerRZ 2%Z (- dExp b)) with (Fulp b radix precision (FPred b radix precision u)). apply FulpFPredLe; auto with zarith. unfold Fulp in |- *; replace (Fnormalize radix b precision (FPred b radix precision u)) with (FPred b radix precision u). rewrite H4; auto with zarith real. apply FcanonicUnique with (radix := radix) (b := b) (precision := precision); auto with real zarith. apply FPredCanonic; auto with zarith. apply FnormalizeCanonic; auto with zarith. apply FBoundedPred; auto with zarith. apply sym_eq; apply FnormalizeCorrect; auto with zarith. replace (powerRZ 2%Z (- dExp b)) with (Fulp b radix precision (FPred b radix precision u)). 2: unfold Fulp in |- *; replace (Fnormalize radix b precision (FPred b radix precision u)) with (FPred b radix precision u). 2: rewrite H4; auto with zarith real. rewrite Rabs_left1; auto with real. 2: apply Rplus_le_reg_l with (FtoRradix u); unfold FtoRradix, radix in |- *. 2: ring_simplify; auto with real zarith. case (Req_dec (- (FtoR 2 t + FtoR 2 y - FtoR 2 u)) (Fulp b radix precision (FPred b radix precision u))); auto. intros W; contradict uDef. replace (FtoRradix t + FtoRradix y)%R with (FtoRradix (FPred b radix precision u)); auto with real. cut (FtoRradix u <> FPred b radix precision u); [ intros V' | idtac ]. contradict V'. cut (ProjectorP b radix (Closest b radix)); [ unfold ProjectorP in |- *; intros W' | idtac ]. apply sym_eq; apply W'; auto with zarith real. apply FBoundedPred; auto with zarith. apply RoundedProjector; apply ClosestRoundedModeP with precision; auto with zarith. apply not_eq_sym; apply Rlt_dichotomy_converse; left. unfold FtoRradix in |- *; apply FPredLt; auto with zarith. apply Rplus_eq_reg_l with (Fulp b radix precision (FPred b radix precision u)). rewrite Rplus_comm; unfold FtoRradix in |- *; rewrite FpredUlpPos; auto with zarith. rewrite <- W; unfold FtoRradix, radix in |- *; ring. apply FcanonicUnique with (radix := radix) (b := b) (precision := precision); auto with real zarith. apply FPredCanonic; auto with zarith. apply FnormalizeCanonic; auto with zarith. apply FBoundedPred; auto with zarith. apply sym_eq; apply FnormalizeCorrect; auto with zarith. apply MinOrMax1 with precision; auto with zarith; fold FtoRradix in |- *. rewrite Rabs_left1. 2: apply Rplus_le_reg_l with (FtoRradix u). 2: ring_simplify; auto with real. apply Rle_lt_trans with (y - y1 + (t - a1 * x1) - (t + y - u))%R; [ right; ring | idtac ]. apply Rlt_le_trans with (Rabs (y - y1 + (t - a1 * x1))). cut (forall u v : R, (0 < v)%R -> (u - v < Rabs u)%R); [ intros V; apply V | idtac ]. apply Rplus_lt_reg_r with (FtoRradix u). ring_simplify; auto with real. intros v w H'1. apply Rlt_le_trans with v; auto with real. unfold Rminus in |- *; apply Rlt_le_trans with (v + -0)%R; [ auto with real | right; ring ]. apply RRle_abs. replace (FtoRradix y - y1 + (FtoRradix t - a1 * x1))%R with (- (y1 - FtoRradix y + (a1 * x1 - a * x) + (a * x - t)))%R; [ idtac | ring ]. rewrite Rabs_Ropp. apply Rle_trans with (Rabs (y1 - FtoRradix y + (a1 * x1 - FtoRradix a * FtoRradix x)) + Rabs (FtoRradix a * FtoRradix x - FtoRradix t))%R; [ apply Rabs_triang | idtac ]. apply Rmult_le_reg_l with 2%R; auto with real arith. apply Rle_trans with (2 * Rabs (y1 - FtoRradix y + (a1 * x1 - FtoRradix a * FtoRradix x)) + 2 * Rabs (FtoRradix a * FtoRradix x - FtoRradix t))%R; [ right; ring | idtac ]. apply Rle_trans with (Fulp b radix precision (FPred b radix precision u) + Fulp b radix precision (FPred b radix precision u))%R; [ idtac | right; simpl; ring ]. apply Rplus_le_compat. apply Rle_trans with (2 * (/ 4 * Fulp b radix precision (FPred b radix precision u)))%R; auto with real. apply Rle_trans with (2 * (Rabs (y1 - FtoRradix y) + Rabs (a1 * x1 - FtoRradix a * FtoRradix x)))%R; [ apply Rmult_le_compat_l; auto with real arith; apply Rabs_triang | idtac ]. apply Rmult_le_compat_l; auto with real arith. apply Rle_trans with (1 * Fulp b radix precision (FPred b radix precision u))%R; [ rewrite <- Rmult_assoc; apply Rmult_le_compat_r | right; ring ]; auto with real arith zarith. unfold Fulp in |- *; auto with real zarith. now apply powerRZ_le, IZR_lt. lra. apply Rle_trans with (Fulp b radix precision t); [ unfold FtoRradix in |- *; apply ClosestUlp; auto with zarith | unfold Fulp in |- * ]. apply Rle_powerRZ; auto with zarith real. replace (Fnormalize radix b precision t) with t; [ elim H2; intros H9 H10; elim H10; intros H11 H12; rewrite H11 | idtac ]. 2: apply sym_eq; apply FcanonicFnormalizeEq; auto with zarith; right; auto. replace (Fnormalize radix b precision (FPred b radix precision u)) with (FPred b radix precision u); [ rewrite H4; auto with zarith | idtac ]. apply sym_eq; apply FcanonicFnormalizeEq; auto with zarith. apply FPredCanonic; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz