proposition: Theorem Axpy_aux1_aux1 : Fnormal radix b t -> Fcanonic radix b u -> (0 < u)%R -> (4 * Rabs t <= Rabs u)%R -> (Rabs (FtoRradix a * FtoRradix x - FtoRradix t) <= / 4 * Fulp b radix precision (FPred b radix precision u))%R.
proof: Proof. intros H1 H2 H3 H4. cut (Fcanonic radix b t); [ intros H5 | left; auto ]. apply Rle_trans with (/ 2 * Fulp b radix precision t)%R. 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 t)%R. unfold FtoRradix in |- *; apply ClosestUlp; auto with real arith zarith. apply Rle_trans with (/ 2 * (/ 4 * Fulp b radix precision u))%R. apply Rmult_le_compat_l; auto with real arith. apply Rmult_le_reg_l with 4%R; auto with real arith. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith. ring_simplify (1 * Fulp b radix precision u)%R. cut (Fbounded b (Float (Fnum t) (Z.succ (Z.succ (Fexp t))))); [ intros H6 | idtac ]. 2: elim H1; intros H7 H8; elim H7; intros H9 H10. 2: repeat (split; simpl in |- *; auto with zarith). apply Rle_trans with (Fulp b radix precision (Float (Fnum t) (Z.succ (Z.succ (Fexp t))))). right; unfold Fulp in |- *. replace (Fnormalize radix b precision t) with t; [ idtac | apply FcanonicUnique with (radix := radix) (b := b) (precision := precision); auto with real zarith ]. 2: apply FnormalizeCanonic; auto with zarith. 2: apply sym_eq; apply FnormalizeCorrect; auto with real zarith. replace (Fnormalize radix b precision (Float (Fnum t) (Z.succ (Z.succ (Fexp t))))) with (Float (Fnum t) (Z.succ (Z.succ (Fexp t)))). replace (Fexp (Float (Fnum t) (Z.succ (Z.succ (Fexp t))))) with (Z.succ (Z.succ (Fexp t))); [ idtac | simpl in |- *; auto ]. replace (Z.succ (Z.succ (Fexp t))) with (2 + Fexp t)%Z; [ rewrite powerRZ_add | unfold Z.succ in |- * ]; auto with zarith real. f_equal; simpl; unfold radix; ring_simplify; easy. apply FcanonicUnique with (radix := radix) (b := b) (precision := precision); auto with real arith zarith. 2: apply FnormalizeCanonic; auto with zarith. 2: apply sym_eq; apply FnormalizeCorrect; auto with real zarith. elim H1; intros H7 H8. left; repeat (split; simpl in |- *; auto with zarith). rewrite FulpFabs with b radix precision (Float (Fnum t) (Z.succ (Z.succ (Fexp t)))); auto with zarith. rewrite FulpFabs with b radix precision u; auto with zarith. apply LeFulpPos; auto with zarith real. now apply absFBounded. now apply absFBounded. unfold FtoRradix in |- *; rewrite Fabs_correct; auto with real zarith. apply Rabs_pos. replace (FtoR radix (Fabs (Float (Fnum t) (Z.succ (Z.succ (Fexp t)))))) with (Z.abs (Fnum t) * powerRZ radix (Z.succ (Z.succ (Fexp t))))%R; [ idtac | unfold FtoR in |- *; simpl in |- *; auto ]. replace (Z.succ (Z.succ (Fexp t))) with (2 + Fexp t)%Z; [ rewrite powerRZ_add | unfold Z.succ in |- * ]; auto with zarith real. replace (powerRZ radix 2) with 4%R; [ idtac | simpl; unfold radix; ring_simplify; easy ]. rewrite Rmult_comm; rewrite Rmult_assoc. replace (powerRZ radix (Fexp t) * Z.abs (Fnum t))%R with (Rabs (FtoRradix t)); [ unfold FtoRradix in |- *; repeat rewrite Fabs_correct; auto with real zarith | idtac ]. unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with zarith; unfold FtoR in |- *; simpl in |- *; ring. apply Rmult_le_reg_l with 2%R; auto with arith real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with arith real. ring_simplify (1 * (/ 4 * Fulp b radix precision u))%R. apply Rle_trans with (/ 4 * (2 * Fulp b radix precision (FPred b radix precision u)))%R; [ apply Rmult_le_compat_l; auto with real arith | right; ring ]. apply FulpFPredLe; auto with arith zarith real. Qed.
imports: Reals ZArith List PeanoNat Psatz