proposition: Lemma mult_error_FLX_aux: forall x y, format x -> format y -> (round beta (FLX_exp prec) rnd (x * y) - (x * y) <> 0)%R -> exists f:float beta, (F2R f = round beta (FLX_exp prec) rnd (x * y) - (x * y))%R /\ (cexp (F2R f) <= Fexp f)%Z /\ (Fexp f = cexp x + cexp y)%Z.
proof: Proof. Proof with auto with typeclass_instances. intros x y Hx Hy Hz. set (f := (round beta (FLX_exp prec) rnd (x * y))). destruct (Req_dec (x * y) 0) as [Hxy0|Hxy0]. contradict Hz. rewrite Hxy0. rewrite round_0... ring. destruct (mag beta (x * y)) as (exy, Hexy). specialize (Hexy Hxy0). destruct (mag beta (f - x * y)) as (er, Her). specialize (Her Hz). destruct (mag beta x) as (ex, Hex). assert (Hx0: (x <> 0)%R). contradict Hxy0. now rewrite Hxy0, Rmult_0_l. specialize (Hex Hx0). destruct (mag beta y) as (ey, Hey). assert (Hy0: (y <> 0)%R). contradict Hxy0. now rewrite Hxy0, Rmult_0_r. specialize (Hey Hy0). assert (Hc1: (cexp (x * y)%R - prec <= cexp x + cexp y)%Z). unfold cexp, FLX_exp. rewrite mag_unique with (1 := Hex). rewrite mag_unique with (1 := Hey). rewrite mag_unique with (1 := Hexy). cut (exy - 1 < ex + ey)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (1 := proj1 Hexy). rewrite Rabs_mult. rewrite bpow_plus. apply Rmult_le_0_lt_compat. apply Rabs_pos. apply Rabs_pos. apply Hex. apply Hey. assert (Hc2: (cexp x + cexp y <= cexp (x * y)%R)%Z). unfold cexp, FLX_exp. rewrite mag_unique with (1 := Hex). rewrite mag_unique with (1 := Hey). rewrite mag_unique with (1 := Hexy). cut ((ex - 1) + (ey - 1) < exy)%Z. generalize (prec_gt_0 prec). clear ; lia. apply (lt_bpow beta). apply Rle_lt_trans with (2 := proj2 Hexy). rewrite Rabs_mult. rewrite bpow_plus. apply Rmult_le_compat. apply bpow_ge_0. apply bpow_ge_0. apply Hex. apply Hey. assert (Hr: ((F2R (Float beta (- (Ztrunc (scaled_mantissa beta (FLX_exp prec) x) * Ztrunc (scaled_mantissa beta (FLX_exp prec) y)) + rnd (scaled_mantissa beta (FLX_exp prec) (x * y)) * beta ^ (cexp (x * y)%R - (cexp x + cexp y))) (cexp x + cexp y))) = f - x * y)%R). rewrite Hx at 6. rewrite Hy at 6. rewrite <- F2R_mult. simpl. unfold f, round, Rminus. rewrite <- F2R_opp, Rplus_comm, <- F2R_plus. unfold Fplus. simpl. now rewrite Zle_imp_le_bool with (1 := Hc2). exists (Float beta (- (Ztrunc (scaled_mantissa beta (FLX_exp prec) x) * Ztrunc (scaled_mantissa beta (FLX_exp prec) y)) + rnd (scaled_mantissa beta (FLX_exp prec) (x * y)) * beta ^ (cexp (x * y)%R - (cexp x + cexp y))) (cexp x + cexp y)). split;[assumption|split]. rewrite Hr. simpl. clear Hr. apply Z.le_trans with (cexp (x * y)%R - prec)%Z. unfold cexp, FLX_exp. apply Zplus_le_compat_r. rewrite mag_unique with (1 := Hexy). apply mag_le_bpow with (1 := Hz). replace (bpow (exy - prec)) with (ulp beta (FLX_exp prec) (x * y)). apply error_lt_ulp... rewrite ulp_neq_0; trivial. unfold cexp. now rewrite mag_unique with (1 := Hexy). apply Hc1. reflexivity. Qed.
imports: Coq(ZArith Reals Lia) Core Operations Plus_error