proposition: Lemma round_round_mult_beta_odd : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), (forall ex, (fexp2 ex <= fexp1 ex)%Z) -> forall x y, generic_format beta fexp1 x -> generic_format beta fexp1 y -> round_round_eq beta fexp1 fexp2 choice1 choice2 (x * y).
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Fx Fy. unfold round_round_eq. destruct (Rlt_or_le x 0) as [Sx|Sx]; destruct (Rlt_or_le y 0) as [Sy|Sy]. - replace (x * y) with ((- x) * (- y)); [|ring]. assert (Px : 0 <= - x); [lra|]. assert (Py : 0 <= - y); [lra|]. apply generic_format_opp in Fx. apply generic_format_opp in Fy. now apply round_round_mult_beta_odd_aux2. - replace (x * y) with (- ((- x) * y)); [|ring]. assert (Px : 0 <= - x); [lra|]. apply generic_format_opp in Fx. do 3 rewrite round_N_opp. apply Ropp_eq_compat. now apply round_round_mult_beta_odd_aux2. - replace (x * y) with (- (x * (- y))); [|ring]. assert (Py : 0 <= - y); [lra|]. apply generic_format_opp in Fy. do 3 rewrite round_N_opp. apply Ropp_eq_compat. now apply round_round_mult_beta_odd_aux2. - now apply round_round_mult_beta_odd_aux2. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)