proposition: Theorem Axpy_tFlessu : 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 -> (4 * Rabs t <= Rabs u)%R -> (Rabs (y1 - y) + Rabs (a1 * x1 - a * x) < / 4 * Fulp b radix precision (FLess b precision u))%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. unfold FLess in |- *; case (Rcase_abs (FtoR 2 u)); fold radix in |- *; intros H3 H2. 2: cut (0 <= u)%R; [ intros H'; case H'; intros H4; clear H' | auto with real ]. 2: apply AxpyPos with precision a x y t; auto. apply MinOrMax_Fopp. replace (- (a1 * x1 + y1))%R with (- a1 * x1 + - y1)%R; [ idtac | ring ]. apply AxpyPos with precision (Fopp a) x (Fopp y) (Fopp t); fold radix FtoRradix in |- *; auto with real zarith. now apply oppBounded. now apply oppBounded. now apply oppBounded. replace (FtoRradix (Fopp a) * FtoRradix x)%R with (- (a * x))%R; [ apply ClosestOpp; auto | unfold FtoRradix in |- *; rewrite Fopp_correct; ring ]. replace (FtoRradix (Fopp t) + FtoRradix (Fopp y))%R with (- (t + y))%R; [ apply ClosestOpp; auto | unfold FtoRradix in |- *; repeat rewrite Fopp_correct; ring ]. now apply FcanonicFopp. now apply FcanonicFopp. unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real. unfold FtoRradix in |- *; repeat rewrite Fopp_correct; repeat rewrite Rabs_Ropp; auto with real. unfold FtoRradix in |- *; repeat rewrite Fopp_correct; rewrite <- (Rabs_Ropp (- a1 * x1 - - FtoR radix a * FtoR radix x)); auto with real. replace (- (- a1 * x1 - - FtoR radix a * FtoR radix x))%R with (a1 * x1 - FtoRradix a * FtoRradix x)%R; [ auto | unfold FtoRradix in |- *; ring ]. rewrite <- Rabs_Ropp. replace (- (- y1 - - FtoR radix y))%R with (y1 - FtoRradix y)%R; [ idtac | unfold FtoRradix in |- *; ring ]. rewrite FPredFopFSucc; auto with zarith. rewrite Fopp_Fopp; auto with zarith. replace (Fulp b radix precision (Fopp (FSucc b radix precision u))) with (Fulp b radix precision (FSucc b radix precision u)); auto. unfold Fulp in |- *; rewrite Fnormalize_Fopp; simpl in |- *; auto with real zarith. apply MinOrMax3 with precision; auto with zarith; fold FtoRradix in |- *. cut (FtoRradix t = 0%R); [ intros H' | idtac ]. cut (FtoRradix y = 0%R); [ intros H5 | idtac ]. replace (a1 * x1 + y1 - FtoRradix u)%R with (y1 - y + (a1 * x1 - a * x) + a * x)%R. 2: rewrite <- H4; rewrite H5; ring. apply Rle_lt_trans with (Rabs (y1 - FtoRradix y + (a1 * x1 - FtoRradix a * FtoRradix x)) + Rabs (FtoRradix a * FtoRradix x))%R; [ apply Rabs_triang | idtac ]. apply Rlt_le_trans with (/ 4 * Fulp b radix precision (FPred b radix precision u) + Rabs (FtoRradix a * FtoRradix x))%R; auto with real. apply Rplus_lt_compat_r; apply Rle_lt_trans with (2 := H2); apply Rabs_triang. apply Rle_trans with (/ 4 * Fulp b radix precision (FPred b radix precision u) + / 2 * Fulp b radix precision (FPred b radix precision u))%R; [ apply Rplus_le_compat_l | idtac ]. replace (FtoRradix a * FtoRradix x)%R with (FtoRradix a * FtoRradix x - t)%R; [ idtac | rewrite H'; ring ]. apply Rmult_le_reg_l with 2%R; auto with real arith. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith. ring_simplify (1 * Fulp b radix precision (FPred b radix precision u))%R; 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 real zarith. replace (Fexp (Fnormalize radix b precision t)) with (- dExp b)%Z. cut (Fbounded b (Fnormalize radix b precision (FPred b radix precision u))); [ intros H6; elim H6; auto | apply FnormalizeBounded; auto with zarith ]. apply FBoundedPred; auto with zarith. replace (Fnormalize radix b precision t) with t. replace t with (Float 0 (- dExp b)); [ simpl in |- *; auto | idtac ]. apply FcanonicUnique with (radix := radix) (precision := precision) (b := b); auto with zarith. right; repeat (split; simpl in |- *; auto with zarith). fold FtoRradix in |- *; rewrite H'; unfold FtoRradix, FtoR in |- *; simpl in |- *; ring. apply FcanonicUnique with (radix := radix) (precision := precision) (b := b); auto with zarith. apply FnormalizeCanonic; auto with zarith. apply sym_eq; apply FnormalizeCorrect; auto with zarith. apply Rle_trans with ((/ 4 + / 2) * Fulp b radix precision (FPred b radix precision u))%R; [ right; ring | idtac ]. apply Rle_trans with (1 * Fulp b radix precision (FPred b radix precision u))%R; [ apply Rmult_le_compat_r | right; ring ]. unfold Fulp in |- *; auto with real zarith. now apply powerRZ_le; apply IZR_lt. lra. cut (ProjectorP b radix (Closest b radix)); [ unfold ProjectorP in |- *; intros V | idtac ]. replace 0%R with (FtoRradix (Float 0 (- dExp b))); [ idtac | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ]. unfold FtoRradix in |- *; apply V; auto. replace (Float 0 (- dExp b)) with u; fold FtoRradix in |- *. replace (FtoRradix y) with (FtoRradix t + FtoRradix y)%R; auto. rewrite H'; ring. apply FcanonicUnique with (radix := radix) (precision := precision) (b := b); auto with zarith. right; repeat (split; simpl in |- *; auto with zarith). fold FtoRradix in |- *; rewrite <- H4; unfold FtoRradix, FtoR in |- *; simpl in |- *; ring. apply RoundedProjector; auto. apply ClosestRoundedModeP with precision; auto with zarith. cut (forall z : R, (Rabs z <= 0)%R -> z = 0%R); [ intros V; apply V | idtac ]. apply Rmult_le_reg_l with 4%R; auto with real arith. apply Rle_trans with (1 := H1); right; rewrite <- H4; auto with real. ring_simplify (4*0)%R; apply Rabs_R0. intros z V; case (Req_dec 0 z); auto with real. intros V'; contradict V. apply Rlt_not_le; apply Rabs_pos_lt; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz