proposition: Lemma round_round_minus_aux3 : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), round_round_plus_hyp fexp1 fexp2 -> forall x y, 0 < y -> y <= x -> generic_format beta fexp1 x -> generic_format beta fexp1 y -> round_round_eq fexp1 fexp2 choice1 choice2 (x - y).
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hyx Fx Fy. assert (Px := Rlt_le_trans 0 y x Py Hyx). unfold round_round_eq. destruct (Req_dec y x) as [Hy|Hy]. - rewrite Hy; replace (x - x) with 0 by ring. rewrite round_0. + reflexivity. + now apply valid_rnd_N. - assert (Hyx' : y < x); [lra|]. destruct (Zle_or_lt (mag y) (fexp1 (mag x) - 2)) as [Hly|Hly]. + destruct (Zle_or_lt (mag y) (fexp1 (mag (x - y)) - 2)) as [Hly'|Hly']. * now apply round_round_minus_aux2. * { rewrite (round_generic beta fexp2). - reflexivity. - now apply valid_rnd_N. - assert (Hf1 : (fexp1 (mag (x - y)) - 1 <= mag y)%Z) by lia. now apply (round_round_minus_aux1 fexp1). } + rewrite (round_generic beta fexp2). * reflexivity. * now apply valid_rnd_N. * assert (Hf1 : (fexp1 (mag x) - 1 <= mag y)%Z) by lia. now apply (round_round_minus_aux0 fexp1). Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ