proposition: Fact ex17 x y : Monotone_exp phi -> generic_format r phi x -> generic_format r phi y -> generic_format r phi (round r phi (Znearest choice) (x + y) - (x + y))%R.
proof: Proof. intros mPhi Hx Hy. assert (forall x1 y1, (cexp r phi x1 <= cexp r phi y1)%Z -> generic_format r phi x1 -> generic_format r phi y1 -> generic_format r phi (round r phi (Znearest choice) (x1 + y1) - (x1 + y1))%R). 2 : destruct (Z_le_dec (cexp r phi x) (cexp r phi y)%Z) as [xLy|yLx]. 2: apply H; auto. 2 : replace (x + y) with (y + x); try lra. 2 : apply H; try lia; auto. clear x y Hx Hy. intros x y He Hx Hy. set (rnd := round r phi (Znearest choice)). destruct (Req_dec (rnd (x + y) - (x + y)) 0) as [xpyZ | xpyNZ]. rewrite xpyZ. apply generic_format_0. unfold generic_format in Hx, Hy. set (mx := Ztrunc (_ _ _ x)) in *. set (ex := cexp _ _ x) in *. set (my := Ztrunc (_ _ _ y)) in *. set (ey := cexp _ _ y) in *. pose (f := {| Fnum := mx + my * r ^ (ey - ex); Fexp := ex |} : float r). assert (Hxy: (x + y)%R = F2R f). rewrite Hx, Hy, <- F2R_plus. unfold Fplus; simpl; rewrite Zle_imp_le_bool with (1 := He); auto. rewrite Hxy. destruct (ex16 {| Fnum := mx + my * r ^ (ey - ex); Fexp := ex |} (Znearest choice) (valid_rnd_N choice)) as [m Hm]. simpl in Hm. unfold rnd, f; rewrite Hm. rewrite <-F2R_minus, Fminus_same_exp. apply generic_format_F2R. intros HH. apply mPhi. apply mag_le_abs. apply F2R_neq_0; auto. replace x with (-(y - (x + y)))%R by ring. rewrite Rabs_Ropp. assert (HRN : Rnd_N_pt (generic_format r phi) (x + y) (round r phi (Znearest choice) (x + y))). apply round_N_pt; auto. rewrite <- Fminus_same_exp, F2R_minus, <- Hm. fold f; rewrite <- Hxy. destruct HRN as [_ PN]; auto. Qed.
imports: Psatz ZArith Reals Flocq(FTZ Core Operations)