proposition: Theorem Fplus_core_correct : forall m1 e1 m2 e2 e, (e <= e1)%Z -> let '(m, l) := Fplus_core m1 e1 m2 e2 e in inbetween_float beta m e (F2R (Float beta m1 e1) + F2R (Float beta m2 e2)) l.
proof: Proof. intros m1 e1 m2 e2 e He1. unfold Fplus_core. case Zlt_bool_spec ; intros He2. - unfold truncate_aux. unfold inbetween_float, F2R. simpl. rewrite 3!plus_IZR. rewrite Rplus_assoc. rewrite 2!Rmult_plus_distr_r. replace (IZR (m1 * Zpower beta (e1 - e)) * bpow e)%R with (IZR m1 * bpow e1)%R. 2: { rewrite mult_IZR, IZR_Zpower by lia. rewrite Rmult_assoc, <- bpow_plus. apply (f_equal (fun v => IZR m1 * bpow v)%R). ring. } rewrite <- 3!(Rplus_comm _ (IZR m1 * bpow e1)). apply inbetween_plus_compat. set (k := (e - e2)%Z). rewrite <- (plus_IZR _ 1). replace e with (e2 + k)%Z by (unfold k ; ring). apply inbetween_float_new_location. exact He2. now constructor 1. - constructor 1. unfold F2R. simpl. rewrite plus_IZR, Rmult_plus_distr_r. rewrite 2!mult_IZR, 2!IZR_Zpower by lia. rewrite 2!Rmult_assoc, <- 2!bpow_plus. apply (f_equal2 (fun v w => IZR m1 * bpow v + IZR m2 * bpow w)%R) ; ring. Qed.
imports: Coq(ZArith Reals Lia) Core Bracket Operations Round