proposition: Theorem Twice_EvenClosest_Round: forall (x:float) (r:R), (-(dExp bo) <= (Fexp x)-1)%Z -> (Fnormal radix bo x) -> (EvenClosest bo radix precision r x) -> (EvenClosest bo radix precision (2*r)%R (Float (Fnum x) (Z.succ (Fexp x)))).
proof: Proof. intros x r U Nx H. assert (x*2=(Float (Fnum x) (Z.succ (Fexp x))))%R. unfold FtoRradix, FtoR, Z.succ; simpl; rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix; ring. elim H; intros H2 H3; elim H2; intros H'1 H'2; split. split; [split; simpl; auto with zarith; apply H'1|idtac]. intros. fold FtoRradix; rewrite <- H0. replace (x*2-2*r)%R with (2*(x-r))%R;[idtac|unfold Rdiv; ring]. rewrite Rabs_mult; rewrite Rabs_right; auto with real. case (Zle_lt_or_eq (-(dExp bo))%Z (Fexp f)); try apply H1; intros L. replace (f-2*r)%R with (2*((Float (Fnum f) (Z.pred (Fexp f)))-r))%R. rewrite Rabs_mult; rewrite Rabs_right with (2)%R. 2: apply Rle_ge; auto with real. apply Rmult_le_compat_l; auto with real. unfold FtoRradix; apply H'2. split; simpl; auto with zarith; apply H1. unfold FtoRradix, FtoR, Z.pred; simpl; rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 2; simpl; unfold radix; field. replace (f-2*r)%R with (-((2*r)-f))%R;[rewrite Rabs_Ropp|ring]. apply Rle_trans with (2:=Rabs_triang_inv (2*r)%R f). rewrite Rabs_mult; rewrite (Rabs_right 2%R); try apply Rle_ge;auto with real. pattern r at 2 in |-*; replace r with (x-(x-r))%R;[idtac|ring]. apply Rle_trans with (2*(Rabs (x)-Rabs (x-r))-Rabs f)%R;[idtac|unfold Rminus; apply Rplus_le_compat_r; apply Rmult_le_compat_l; auto with real]. 2: generalize (Rabs_triang_inv x (x-r)%R); unfold Rminus; auto with real. apply Rplus_le_reg_l with (Rabs f -2*(Rabs (x-r)))%R. apply Rle_trans with (Rabs f);[right;ring|idtac]. apply Rle_trans with (2*(Rabs x)-4*Rabs (x-r))%R;[idtac|right;ring]. apply Rle_trans with (((powerRZ radix precision)-1)*(powerRZ radix ((Fexp x)-1)))%R. unfold FtoRradix; rewrite <- Fabs_correct; auto;unfold Fabs, FtoR; simpl. apply Rmult_le_compat; auto with real zarith. apply IZR_le; auto with zarith. apply powerRZ_le, IZR_lt; auto with zarith. apply Rle_trans with (Z.pred (Zpower_nat radix precision));[rewrite <- pGivesBound|idtac]. apply IZR_le;apply Zle_Zpred; auto with zarith; apply H1. unfold Z.pred; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. rewrite <- L; apply Rle_powerRZ; auto with real zarith. apply Rle_trans with (2*(powerRZ radix (Z.pred precision))*(powerRZ radix (Fexp x))-2*(powerRZ radix (Fexp x)))%R. apply Rle_trans with (((powerRZ radix (precision+1))-4)*(powerRZ radix (Fexp x-1)))%R;[apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; auto with zarith. rewrite powerRZ_add; auto with real zarith; simpl. apply Rplus_le_reg_l with (-(powerRZ radix precision)+4)%R. unfold radix at 5; ring_simplify. apply Rle_trans with (powerRZ radix 2)%R; auto with real zarith. simpl; unfold radix; ring_simplify (2*(2*1))%R; auto with real zarith. apply Rle_powerRZ; auto with real zarith. replace (2*powerRZ radix (Fexp x))%R with (4*powerRZ radix (Fexp x -1))%R. replace 2%R with (powerRZ radix 1%Z);[idtac|apply powerRZ_1]. repeat rewrite <- powerRZ_add; auto with real zarith. replace (1+Z.pred precision+Fexp x)%Z with ((precision+1)+(Fexp x-1))%Z;[idtac|unfold Z.pred; ring]. rewrite powerRZ_add with (n:=(precision+1)%Z);auto with real zarith; right;ring. unfold Zminus; rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 2; simpl; unfold radix; field. unfold Rminus; apply Rplus_le_compat;[rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real|apply Ropp_le_contravar]. unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR, Fabs; simpl. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. apply Rmult_le_reg_l with radix; auto with real zarith. pattern (IZR radix) at 1 in |-*; replace (IZR radix) with (powerRZ radix 1%Z);[idtac|simpl; ring]. rewrite <- powerRZ_add; auto with real zarith; elim Nx; intros. replace (1+Z.pred precision)%Z with (Z_of_nat precision)%Z;[idtac|unfold Z.pred; ring]. apply Rle_trans with (IZR (Zpos (vNum bo)));[rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith|idtac]. apply Rle_trans with (IZR (Z.abs (radix * Fnum x))); auto with real zarith. apply IZR_le; auto. rewrite Zabs_Zmult; rewrite Z.abs_eq; auto with real zarith. rewrite mult_IZR; auto with real. unfold radix; auto with zarith. replace 4%R with (2*2)%R; [rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real|simpl;ring]. replace (x+-r)%R with (-(r-x))%R;[rewrite Rabs_Ropp|ring]. apply Rle_trans with (Fulp bo radix precision x). unfold FtoRradix; apply ClosestUlp; auto. rewrite CanonicFulp; auto with real zarith. right; unfold FtoR, radix; simpl; ring. left; auto. case H3; intros V. left; generalize V; unfold FNeven; rewrite FcanonicFnormalizeEq; auto with zarith. rewrite FcanonicFnormalizeEq; auto with zarith. elim Nx; intros; left; split; auto with zarith. elim H1; intros; split; simpl; auto with zarith. left; auto. right; intros. apply trans_eq with (2*(FtoR radix (Float (Fnum q0) (Z.pred (Fexp q0)))))%R. unfold FtoR, Z.pred; simpl; rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 3; simpl; unfold radix; field. apply trans_eq with (2*(FtoR radix x))%R. 2: unfold FtoR, Z.succ; simpl; rewrite powerRZ_add; auto with real zarith. 2: rewrite powerRZ_1; unfold radix; ring. apply Rmult_eq_compat_l; apply V. replace r with ((2*r)/2)%R;[idtac|field; auto with real]. apply Half_Closest_Round; auto. apply Z.le_trans with (1:=U). fold (Z.pred (Fexp x)); cut (Fexp x <= Fexp q0)%Z; auto with zarith. apply Z.le_trans with (Fexp (Fnormalize radix bo precision q0)). apply Fcanonic_Rle_Zle with radix bo precision; auto with zarith. left; auto. apply FnormalizeCanonic; auto with zarith. elim H1; auto. generalize ClosestMonotone; unfold MonotoneP; intros. repeat rewrite <- Fabs_correct; auto. apply H4 with bo (Rabs r) (Rabs (2*r))%R. rewrite Rabs_mult; rewrite (Rabs_right 2%R); try apply Rle_ge; auto with real. apply Rle_lt_trans with (1*Rabs r)%R;[right;ring|apply Rmult_lt_compat_r; auto with real]. apply Rabs_pos_lt;unfold not;intros. absurd (is_Fzero x). apply FnormalNotZero with radix bo ; auto. apply is_Fzero_rep2 with radix; auto. cut (0 <= FtoR radix x)%R; intros. cut (FtoR radix x <= 0)%R; intros; auto with real. apply RleRoundedLessR0 with bo precision (Closest bo radix) r; auto with real. apply ClosestRoundedModeP with precision; auto. apply RleRoundedR0 with bo precision (Closest bo radix) r; auto with real. apply ClosestRoundedModeP with precision; auto. apply ClosestFabs with precision; auto. apply ClosestFabs with precision; auto. generalize ClosestCompatible; unfold CompatibleP; intros T. apply T with (2*r)%R q0; auto with real zarith. apply sym_eq;apply FnormalizeCorrect; auto. apply FnormalizeBounded; auto with zarith. elim H1; auto. apply FcanonicLeastExp with radix bo precision; auto with zarith. apply sym_eq; apply FnormalizeCorrect; auto. elim H1; auto. apply FnormalizeCanonic; auto with zarith;elim H1; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz