proposition: Lemma format_REM_aux: forall x y : R, format x -> format y -> (0 <= x)%R -> (0 < y)%R -> ((0 < x/y < /2)%R -> rnd (x/y) = 0%Z) -> format (x - IZR (rnd (x/y))*y).
proof: Proof. Proof with auto with typeclass_instances. intros x y Fx Fy Hx Hy rnd_small. pose (n:=rnd (x / y)). assert (Hn:(IZR n = round beta (FIX_exp 0) rnd (x/y))%R). unfold round, FIX_exp, cexp, scaled_mantissa, F2R; simpl. now rewrite 2!Rmult_1_r. assert (H:(0 <= n)%Z). apply le_IZR; rewrite Hn; simpl. apply Rle_trans with (round beta (FIX_exp 0) rnd 0). right; apply sym_eq, round_0... apply round_le... apply Fourier_util.Rle_mult_inv_pos; assumption. case (Zle_lt_or_eq 0 n); try exact H. clear H; intros H. case (Zle_lt_or_eq 1 n). lia. clear H; intros H. set (ex := cexp beta fexp x). set (ey := cexp beta fexp y). set (mx := Ztrunc (scaled_mantissa beta fexp x)). set (my := Ztrunc (scaled_mantissa beta fexp y)). case (Zle_or_lt ey ex); intros Hexy. assert (H0:(x-IZR n *y = F2R (Float beta (mx*beta^(ex-ey) - n*my) ey))%R). unfold Rminus; rewrite Rplus_comm. replace (IZR n) with (F2R (Float beta n 0)). rewrite Fx, Fy. fold mx my ex ey. rewrite <- F2R_mult. rewrite <- F2R_opp. rewrite <- F2R_plus. unfold Fplus. simpl. rewrite Zle_imp_le_bool with (1 := Hexy). f_equal; f_equal; ring. unfold F2R; simpl; ring. fold n; rewrite H0. apply generic_format_F2R. rewrite <- H0; intros H3. apply monotone_exp. apply mag_le_abs. rewrite H0; apply F2R_neq_0; easy. apply Rmult_le_reg_l with (/Rabs y)%R. apply Rinv_0_lt_compat. apply Rabs_pos_lt. now apply Rgt_not_eq. rewrite Rinv_l. 2: apply Rgt_not_eq, Rabs_pos_lt. 2: now apply Rgt_not_eq. rewrite <- Rabs_Rinv. 2: now apply Rgt_not_eq. rewrite <- Rabs_mult. replace (/y * (x - IZR n *y))%R with (-(IZR n - x/y))%R. rewrite Rabs_Ropp. rewrite Hn. apply Rle_trans with (1:= error_le_ulp beta (FIX_exp 0) _ _). rewrite ulp_FIX. simpl; apply Rle_refl. field. now apply Rgt_not_eq. absurd (1 < n)%Z; try easy. apply Zle_not_lt. apply le_IZR; simpl; rewrite Hn. apply round_le_generic... apply generic_format_FIX. exists (Float beta 1 0); try easy. unfold F2R; simpl; ring. apply Rmult_le_reg_r with y; try easy. unfold Rdiv; rewrite Rmult_assoc. rewrite Rinv_l, Rmult_1_r, Rmult_1_l. 2: now apply Rgt_not_eq. assert (mag beta x < mag beta y)%Z. case (Zle_or_lt (mag beta y) (mag beta x)); try easy. intros J; apply monotone_exp in J; clear -J Hexy. unfold ex, ey, cexp in Hexy; lia. left; apply lt_mag with beta; easy. intros Hn'; fold n; rewrite <- Hn'. rewrite Rmult_1_l. case Hx; intros Hx'. assert (J:(0 < x/y)%R). apply Fourier_util.Rlt_mult_inv_pos; assumption. apply sterbenz... assert (H0:(Rabs (1 - x/y) < 1)%R). rewrite Hn', Hn. apply Rlt_le_trans with (ulp beta (FIX_exp 0) (round beta (FIX_exp 0) rnd (x / y)))%R. apply error_lt_ulp_round... now apply Rgt_not_eq. rewrite ulp_FIX. rewrite <- Hn, <- Hn'. apply Rle_refl. apply Rabs_lt_inv in H0. split; apply Rmult_le_reg_l with (/y)%R; try now apply Rinv_0_lt_compat. unfold Rdiv; rewrite <- Rmult_assoc. rewrite Rinv_l. 2: now apply Rgt_not_eq. rewrite Rmult_1_l, Rmult_comm; fold (x/y)%R. case (Rle_or_lt (/2) (x/y)); try easy. intros K. elim Zlt_not_le with (1 := H). apply Zeq_le. apply rnd_small. now split. apply Ropp_le_cancel; apply Rplus_le_reg_l with 1%R. apply Rle_trans with (1-x/y)%R. 2: right; unfold Rdiv; ring. left; apply Rle_lt_trans with (2:=proj1 H0). right; field. now apply Rgt_not_eq. rewrite <- Hx', Rminus_0_l. now apply generic_format_opp. clear H; intros H; fold n; rewrite <- H. now rewrite Rmult_0_l, Rminus_0_r. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error