proposition: Theorem div_error_FLX : forall rnd { Zrnd : Valid_rnd rnd } x y, format x -> format y -> format (x - round beta (FLX_exp prec) rnd (x/y) * y)%R.
proof: Proof. Proof with auto with typeclass_instances. intros rnd Zrnd x y Hx Hy. destruct (Req_dec y 0) as [Zy|Zy]. now rewrite Zy, Rmult_0_r, Rminus_0_r. destruct (Req_dec (round beta (FLX_exp prec) rnd (x/y)) 0) as [Hr|Hr]. rewrite Hr; ring_simplify (x-0*y)%R; assumption. assert (Zx: x <> R0). contradict Hr. rewrite Hr. unfold Rdiv. now rewrite Rmult_0_l, round_0. destruct (canonical_generic_format _ _ x Hx) as (fx,(Hx1,Hx2)). destruct (canonical_generic_format _ _ y Hy) as (fy,(Hy1,Hy2)). destruct (canonical_generic_format beta (FLX_exp prec) (round beta (FLX_exp prec) rnd (x / y))) as (fr,(Hr1,Hr2)). apply generic_format_round... unfold Rminus; apply generic_format_plus_prec with fx (Fopp (Fmult fr fy)); trivial. intros e; apply Z.le_refl. now rewrite F2R_opp, F2R_mult, <- Hr1, <- Hy1. destruct (relative_error_FLX_ex beta prec (prec_gt_0 prec) rnd (x / y)%R) as (eps,(Heps1,Heps2)). rewrite Heps2. rewrite <- Rabs_Ropp. replace (-(x + - (x / y * (1 + eps) * y)))%R with (x * eps)%R by now field. rewrite Rabs_mult. apply Rlt_le_trans with (Rabs x * 1)%R. apply Rmult_lt_compat_l. now apply Rabs_pos_lt. apply Rlt_le_trans with (1 := Heps1). change 1%R with (bpow 0). apply bpow_le. generalize (prec_gt_0 prec). clear ; lia. rewrite Rmult_1_r. rewrite Hx2, <- Hx1. unfold cexp. destruct (mag beta x) as (ex, Hex). simpl. specialize (Hex Zx). apply Rlt_le. apply Rlt_le_trans with (1 := proj2 Hex). apply bpow_le. unfold FLX_exp. ring_simplify. apply Z.le_refl. replace (Fexp (Fopp (Fmult fr fy))) with (Fexp fr + Fexp fy)%Z. 2: unfold Fopp, Fmult; destruct fr; destruct fy; now simpl. replace (x + - (round beta (FLX_exp prec) rnd (x / y) * y))%R with (y * (-(round beta (FLX_exp prec) rnd (x / y) - x/y)))%R. 2: field; assumption. rewrite Rabs_mult. apply Rlt_le_trans with (Rabs y * bpow (Fexp fr))%R. apply Rmult_lt_compat_l. now apply Rabs_pos_lt. rewrite Rabs_Ropp. replace (bpow (Fexp fr)) with (ulp beta (FLX_exp prec) (F2R fr)). rewrite <- Hr1. apply error_lt_ulp_round... apply Rmult_integral_contrapositive_currified; try apply Rinv_neq_0_compat; assumption. rewrite ulp_neq_0. 2: now rewrite <- Hr1. apply f_equal. now rewrite Hr2, <- Hr1. replace (prec+(Fexp fr+Fexp fy))%Z with ((prec+Fexp fy)+Fexp fr)%Z by ring. rewrite bpow_plus. apply Rmult_le_compat_r. apply bpow_ge_0. rewrite Hy2, <- Hy1 ; unfold cexp, FLX_exp. ring_simplify (prec + (mag beta y - prec))%Z. destruct (mag beta y); simpl. left; now apply a. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error