proposition: Theorem format_REM : forall rnd : R -> Z, Valid_rnd rnd -> forall x y : R, ((Rabs (x/y) < /2)%R -> rnd (x/y)%R = 0%Z) -> format x -> format y -> format (x - IZR (rnd (x/y)%R) * y).
proof: Proof. Proof with auto with typeclass_instances. assert (H: forall rnd : R -> Z, Valid_rnd rnd -> forall x y : R, ((Rabs (x/y) < /2)%R -> rnd (x/y)%R = 0%Z) -> format x -> format y -> (0 < y)%R -> format (x - IZR (rnd (x/y)%R) * y)). intros rnd valid_rnd x y Hrnd Fx Fy Hy. case (Rle_or_lt 0 x); intros Hx. apply format_REM_aux; try easy. intros K. apply Hrnd. rewrite Rabs_pos_eq. apply K. apply Rlt_le, K. replace (x - IZR (rnd (x/y)) * y)%R with (- (-x - IZR (Zrnd_opp rnd (-x/y)) * y))%R. apply generic_format_opp. apply format_REM_aux; try easy... now apply generic_format_opp. apply Ropp_le_cancel; rewrite Ropp_0, Ropp_involutive; now left. replace (- x / y)%R with (- (x/y))%R by (unfold Rdiv; ring). intros K. unfold Zrnd_opp. rewrite Ropp_involutive, Hrnd. easy. rewrite Rabs_left. apply K. apply Ropp_lt_cancel. now rewrite Ropp_0. unfold Zrnd_opp. replace (- (- x / y))%R with (x / y)%R by (unfold Rdiv; ring). rewrite opp_IZR. ring. intros rnd valid_rnd x y Hrnd Fx Fy. case (Rle_or_lt 0 y); intros Hy. destruct Hy as [Hy|Hy]. now apply H. now rewrite <- Hy, Rmult_0_r, Rminus_0_r. replace (IZR (rnd (x/y)) * y)%R with (IZR ((Zrnd_opp rnd) ((x / -y))) * -y)%R. apply H; try easy... replace (x / - y)%R with (- (x/y))%R. intros K. unfold Zrnd_opp. rewrite Ropp_involutive, Hrnd. easy. now rewrite <- Rabs_Ropp. field; now apply Rlt_not_eq. now apply generic_format_opp. apply Ropp_lt_cancel; now rewrite Ropp_0, Ropp_involutive. unfold Zrnd_opp. replace (- (x / - y))%R with (x/y)%R. rewrite opp_IZR. ring. field; now apply Rlt_not_eq. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error