proposition: Lemma round_round_mult_aux : forall (fexp1 fexp2 : Z -> Z), round_round_mult_hyp fexp1 fexp2 -> forall x y, generic_format beta fexp1 x -> generic_format beta fexp1 y -> generic_format beta fexp2 (x * y).
proof: Proof. intros fexp1 fexp2 Hfexp x y Fx Fy. destruct (Req_dec x 0) as [Zx|Zx]. - rewrite Zx. rewrite Rmult_0_l. now apply generic_format_0. - destruct (Req_dec y 0) as [Zy|Zy]. + rewrite Zy. rewrite Rmult_0_r. now apply generic_format_0. + revert Fx Fy. unfold generic_format. unfold cexp. set (mx := Ztrunc (scaled_mantissa beta fexp1 x)). set (my := Ztrunc (scaled_mantissa beta fexp1 y)). unfold F2R; simpl. intros Fx Fy. set (fxy := Float beta (mx * my) (fexp1 (mag x) + fexp1 (mag y))). assert (Hxy : x * y = F2R fxy). { unfold fxy, F2R; simpl. rewrite bpow_plus. rewrite mult_IZR. rewrite Fx, Fy at 1. ring. } apply generic_format_F2R' with (f := fxy); [now rewrite Hxy|]. intros _. unfold cexp, fxy; simpl. destruct Hfexp as (Hfexp1, Hfexp2). now destruct (mag_mult_disj x y Zx Zy) as [Lxy|Lxy]; rewrite Lxy. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ