proposition: Lemma Fplus_naive_correct : forall sx mx ex sy my ey ez, (ez <= ex)%Z -> (ez <= ey)%Z -> let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in let y := F2R (Float radix2 (cond_Zopp sy (Zpos my)) ey) in F2R (Float radix2 (Fplus_naive sx mx ex sy my ey ez) ez) = (x + y)%R.
proof: Proof. intros sx mx ex sy my ey ez Ex Ey. unfold Fplus_naive, F2R. simpl. generalize (shl_align_correct' mx ex ez Ex). generalize (shl_align_correct' my ey ez Ey). destruct shl_align as [my' ey']. destruct shl_align as [mx' ex']. intros [Hy _]. intros [Hx _]. simpl. rewrite plus_IZR, Rmult_plus_distr_r. generalize (f_equal (cond_Ropp sx) Hx). generalize (f_equal (cond_Ropp sy) Hy). rewrite <- 4!F2R_cond_Zopp. unfold F2R. simpl. now intros -> ->. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative