proposition: Lemma round_round_minus_aux : 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 <= x -> 0 <= y -> 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 Nnx Nny Fx Fy. unfold round_round_eq. destruct (Req_dec x 0) as [Zx|Nzx]. - rewrite Zx; unfold Rminus; rewrite Rplus_0_l. do 3 rewrite round_N_opp. rewrite (round_generic beta fexp2). * reflexivity. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). destruct Hexp as (_,(_,(_,Hexp4))). now intros _; apply Hexp4; lia. exact Fy. - destruct (Req_dec y 0) as [Zy|Nzy]. + rewrite Zy; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. rewrite (round_generic beta fexp2). * reflexivity. * now apply valid_rnd_N. * apply (generic_inclusion_mag beta fexp1). destruct Hexp as (_,(_,(_,Hexp4))). now intros _; apply Hexp4; lia. exact Fx. + assert (Px : 0 < x); [lra|]. assert (Py : 0 < y); [lra|]. destruct (Rlt_or_le x y) as [H|H]. * apply Rlt_le in H. replace (x - y) with (- (y - x)) by ring. do 3 rewrite round_N_opp. apply Ropp_eq_compat. now apply round_round_minus_aux3. * now apply round_round_minus_aux3. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ