proposition: Theorem mult_error_FLT : forall x y, format x -> format y -> (x * y <> 0 -> bpow (emin + 2*prec - 1) <= Rabs (x * y))%R -> format (round beta (FLT_exp emin prec) rnd (x * y) - (x * y))%R.
proof: Proof. Proof with auto with typeclass_instances. intros x y Hx Hy Hxy. set (f := (round beta (FLT_exp emin prec) rnd (x * y))). destruct (Req_dec (f - x * y) 0) as [Hr0|Hr0]. rewrite Hr0. apply generic_format_0. destruct (Req_dec (x * y) 0) as [Hxy'|Hxy']. unfold f. rewrite Hxy'. rewrite round_0... ring_simplify (0 - 0)%R. apply generic_format_0. specialize (Hxy Hxy'). destruct (mult_error_FLX_aux beta prec rnd x y) as ((m,e),(H1,(H2,H3))). now apply generic_format_FLX_FLT with emin. now apply generic_format_FLX_FLT with emin. rewrite <- (round_FLT_FLX beta emin). assumption. apply Rle_trans with (2:=Hxy). apply bpow_le. generalize (prec_gt_0 prec). clear ; lia. rewrite <- (round_FLT_FLX beta emin) in H1. 2:apply Rle_trans with (2:=Hxy). 2:apply bpow_le ; generalize (prec_gt_0 prec) ; clear ; lia. unfold f; rewrite <- H1. apply generic_format_F2R. intros _. simpl in H2, H3. unfold cexp, FLT_exp. case (Zmax_spec (mag beta (F2R (Float beta m e)) - prec) emin); intros (M1,M2); rewrite M2. apply Z.le_trans with (2:=H2). unfold cexp, FLX_exp. apply Z.le_refl. rewrite H3. unfold cexp, FLX_exp. assert (Hxy0:(x*y <> 0)%R). contradict Hr0. unfold f. rewrite Hr0. rewrite round_0... ring. assert (Hx0: (x <> 0)%R). contradict Hxy0. now rewrite Hxy0, Rmult_0_l. assert (Hy0: (y <> 0)%R). contradict Hxy0. now rewrite Hxy0, Rmult_0_r. destruct (mag beta x) as (ex,Ex) ; simpl. specialize (Ex Hx0). destruct (mag beta y) as (ey,Ey) ; simpl. specialize (Ey Hy0). cut (emin + 2 * prec -1 < ex + ey)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (1:=Hxy). rewrite Rabs_mult, bpow_plus. apply Rmult_le_0_lt_compat; try apply Rabs_pos. apply Ex. apply Ey. Qed.
imports: Coq(ZArith Reals Lia) Core Operations Plus_error