proposition: Theorem round_plus_F2R : forall x y, format x -> format y -> (x <> 0)%R -> exists m, round beta fexp rnd (x+y) = F2R (Float beta m (cexp (x / IZR beta))).
proof: Proof. Proof with auto with typeclass_instances. intros x y Fx Fy Zx. case (Zle_or_lt (mag beta (x/IZR beta)) (mag beta y)); intros H1. pose (e:=cexp (x / IZR beta)). destruct (ex_shift x e) as (nx, Hnx); try exact Fx. apply monotone_exp. rewrite <- (mag_minus1 x Zx); lia. destruct (ex_shift y e) as (ny, Hny); try assumption. apply monotone_exp... destruct (round_repr_same_exp beta fexp rnd (nx+ny) e) as (n,Hn). exists n. fold e. rewrite <- Hn; f_equal. rewrite Hnx, Hny; unfold F2R; simpl; rewrite plus_IZR; ring. unfold F2R; simpl. destruct (ex_shift (round beta fexp rnd (x + y)) (cexp (x/IZR beta))) as (n,Hn). apply generic_format_round... apply Z.le_trans with (cexp (x+y)). apply monotone_exp. rewrite <- mag_minus1 by easy. rewrite <- (mag_abs beta (x+y)). assert (U: (Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y) = Rabs x - Rabs y)%R). assert (V: forall x y, (Rabs y <= Rabs x)%R -> (Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y) = Rabs x - Rabs y)%R). clear; intros x y. case (Rle_or_lt 0 y); intros Hy. case Hy; intros Hy'. case (Rle_or_lt 0 x); intros Hx. intros _; rewrite (Rabs_pos_eq y) by easy. rewrite (Rabs_pos_eq x) by easy. left; apply Rabs_pos_eq. now apply Rplus_le_le_0_compat. rewrite (Rabs_pos_eq y) by easy. rewrite (Rabs_left x) by easy. intros H; right; split. now apply Rgt_not_eq. rewrite Rabs_left1. ring. apply Rplus_le_reg_l with (-x)%R; ring_simplify; assumption. intros _; left. now rewrite <- Hy', Rabs_R0, 2!Rplus_0_r. case (Rle_or_lt 0 x); intros Hx. rewrite (Rabs_left y) by easy. rewrite (Rabs_pos_eq x) by easy. intros H; right; split. now apply Rlt_not_eq. rewrite Rabs_pos_eq. ring. apply Rplus_le_reg_l with (-y)%R; ring_simplify; assumption. intros _; left. rewrite (Rabs_left y) by easy. rewrite (Rabs_left x) by easy. rewrite Rabs_left1. ring. lra. apply V; left. apply lt_mag with beta. now apply Rabs_pos_lt. rewrite <- mag_minus1 in H1; try assumption. rewrite 2!mag_abs; lia. destruct U as [U|U]. rewrite U; apply Z.le_trans with (mag beta x). lia. rewrite <- mag_abs. apply mag_le. now apply Rabs_pos_lt. apply Rplus_le_reg_l with (-Rabs x)%R; ring_simplify. apply Rabs_pos. destruct U as (U',U); rewrite U. rewrite <- mag_abs. apply mag_minus_lb. now apply Rabs_pos_lt. now apply Rabs_pos_lt. rewrite 2!mag_abs. assert (mag beta y < mag beta x - 1)%Z. now rewrite (mag_minus1 x Zx). lia. apply cexp_round_ge... apply round_plus_neq_0... contradict H1; apply Zle_not_lt. rewrite <- (mag_minus1 x Zx). replace y with (-x)%R. rewrite mag_opp; lia. lra. now exists n. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative