proposition: Theorem next_up_equiv : forall x, Prim2B (next_up x) = Bsucc (Prim2B x).
proof: Proof. intro x. apply B2Prim_inj. rewrite B2Prim_Prim2B. apply Prim2SF_inj. rewrite Prim2SF_B2Prim. rewrite next_up_spec. rewrite <-B2SF_Prim2B. assert (Hsndfrexp : forall x : binary_float prec emax, snd (SFfrexp prec emax (B2SF x)) = snd (Bfrexp x)). { intro x'. generalize (Z_frexp_spec (B2Prim x')). generalize (frexp_equiv (B2Prim x')). case Z.frexp; intros f' e'. rewrite Prim2B_B2Prim, Prim2SF_B2Prim. intros H H'; generalize (f_equal snd H'); generalize (f_equal snd H); simpl. now intros ->. } assert (Hldexp : forall x e, SFldexp prec emax (B2SF x) e = B2SF (Bldexp mode_NE x e)). { intros x' e'. rewrite <-(Prim2B_B2Prim x'), B2SF_Prim2B, <-Z_ldexp_spec. now rewrite <-B2SF_Prim2B, ldexp_equiv. } assert (Hulp : forall x, SFulp prec emax (B2SF x) = B2SF (Bulp' x)). { intro x'. unfold SFulp, Bulp'. now rewrite Hsndfrexp, <-Hldexp. } assert (Hpred_pos : forall x, (0 < B2R x)%R -> SFpred_pos prec emax (B2SF x) = B2SF (Bpred_pos' x)). { intros x' Fx'. unfold SFpred_pos, Bpred_pos'. rewrite Hsndfrexp. set (fe := fexp _ _ _). change (SFone _ _) with (B2SF Bone). rewrite Hldexp, Hulp. case x' as [sx|sx| |sx mx ex Bx]; try easy. unfold B2SF at 1. set (y := Bldexp _ _ _). set (z := Bulp' _). case Pos.eqb. - rewrite <-(Prim2B_B2Prim (B754_finite _ _ _ _)). rewrite <-(Prim2B_B2Prim y). now rewrite <-sub_equiv, !B2SF_Prim2B, sub_spec. - rewrite <-(Prim2B_B2Prim (B754_finite _ _ _ _)). rewrite <-(Prim2B_B2Prim z). now rewrite <-sub_equiv, !B2SF_Prim2B, sub_spec. } case Prim2B as [sx|sx| |sx mx ex Bx]; [reflexivity|now case sx|reflexivity| ]. rewrite <- Bsucc'_correct by easy. unfold SF64succ, SFsucc, B2SF at 1, Bsucc'. case sx. - unfold B2SF at 1, SFopp at 2. rewrite <-(Prim2B_B2Prim (Bpred_pos' _)). rewrite <- opp_equiv, B2SF_Prim2B, opp_spec, Prim2SF_B2Prim. rewrite <- Hpred_pos. easy. now apply Float_prop.F2R_gt_0. - rewrite Hulp. rewrite Bulp'_correct by easy. rewrite <-(Prim2B_B2Prim (B754_finite _ _ _ _)). rewrite <-(Prim2B_B2Prim (Bulp _)). rewrite <-add_equiv, !B2SF_Prim2B, add_spec, !Prim2SF_B2Prim. now unfold SF64add. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN