proposition: Theorem Fplus_correct : forall x y, let '(m, e, l) := Fplus x y in (l = loc_Exact \/ e <= cexp beta fexp (F2R x + F2R y))%Z /\ inbetween_float beta m e (F2R x + F2R y) l.
proof: Proof. intros [m1 e1] [m2 e2]. unfold Fplus. case Zeq_bool_spec ; intros Hm1. { rewrite Hm1. split. now left. rewrite F2R_0, Rplus_0_l. now constructor 1. } case Zeq_bool_spec ; intros Hm2. { rewrite Hm2. split. now left. rewrite F2R_0, Rplus_0_r. now constructor 1. } set (p1 := (Zdigits beta m1 + e1)%Z). set (p2 := (Zdigits beta m2 + e2)%Z). set (e := Z.min (Z.max e1 e2) (fexp (Z.max p1 p2 - 1))). case Zle_bool_spec ; intros Hp ; cycle 1. { rewrite <- F2R_plus. destruct Operations.Fplus as [m' e']. split. now left. now constructor 1. } set (z := (F2R _ + F2R _)%R). assert (Hz: (e <= cexp beta fexp z)%Z). { apply Z.le_trans with (fexp (Z.max p1 p2 - 1)). apply Z.le_min_r. unfold cexp. apply monotone_exp. unfold z. revert Hp. unfold p1, p2. rewrite <- 2!mag_F2R_Zdigits by easy. clear -Hm1 Hm2. destruct (Zle_or_lt (mag beta (F2R (Float beta m1 e1))) (mag beta (F2R (Float beta m2 e2)))) as [Hp'|Hp']. - rewrite Z.max_r by easy. rewrite Z.abs_neq by (clear -Hp'; lia). rewrite Rplus_comm. intros H. apply mag_plus_ge. now apply F2R_neq_0. clear -H ; lia. - rewrite Z.max_l, Z.abs_eq by (clear -Hp'; lia). intros H. apply mag_plus_ge. now apply F2R_neq_0. clear -H ; lia. } case Zlt_bool_spec ; intros He. - assert (He': (e <= e2)%Z) by (clear -He ; lia). generalize (Fplus_core_correct m2 e2 m1 e1 e He'). rewrite Rplus_comm. fold z. destruct Fplus_core as [m' l]. refine (fun H => conj _ H). now right. - assert (He': (e <= e1)%Z) by (clear -He ; lia). generalize (Fplus_core_correct m1 e1 m2 e2 e He'). fold z. destruct Fplus_core as [m' l]. refine (fun H => conj _ H). now right. Qed.
imports: Coq(ZArith Reals Lia) Core Bracket Operations Round