proposition: Theorem hrndG_conversion : forall rexp m e, float2R (tofloat (round_pos rdir rexp m e)) = Generic_fmt.round radix2 rexp hrndG (F2R (Float radix2 (Zpos m) e)).
proof: Proof. Proof with auto with typeclass_instances. intros rexp m e. assert (He: cexp radix2 rexp (F2R (Float radix2 (Zpos m) e)) = rexp (e + Zpos (digits m))%Z). rewrite digits2_digits. rewrite Zdigits_mag. 2: easy. unfold cexp. rewrite mag_F2R. 2: easy. now rewrite Zplus_comm. unfold round_pos. case_eq (rexp (e + Zpos (digits m)) - e)%Z. intros H. apply sym_eq. apply round_generic... apply generic_format_F2R. intros _ ; simpl. rewrite He. rewrite Zminus_eq with (1 := H). apply Z.le_refl. intros p H. unfold Generic_fmt.round, scaled_mantissa. rewrite He. unfold F2R, float2R. simpl. rewrite Rmult_assoc, <- bpow_plus. assert (rexp (e + Zpos (digits m)) = e + Zpos p)%Z. lia. rewrite H0. ring_simplify (e + -(e + Zpos p))%Z. apply (f_equal (fun m => IZR m * _)%R). unfold hrndG. rewrite (shr_conversion m p). simpl. set (rs := hrndG_aux (Zfloor (IZR (Zpos m) * / IZR (Zpower_pos 2 p))) (IZR (Zpos m) * / IZR (Zpower_pos 2 p))). rewrite (surjective_pairing rs). simpl. assert (H1: rdir (rnd_record_mk (ZtoN (Zfloor (IZR (Zpos m) * / IZR (Zpower_pos 2 p)))) (fst rs) (snd rs)) = true -> (IZR (Zfloor (IZR (Zpos m) * / IZR (Zpower_pos 2 p))) <> IZR (Zpos m) * / IZR (Zpower_pos 2 p))%R). unfold rs, hrndG_aux. destruct (inbetween_spec _ _ (IZR (Zpos m) * / IZR (Zpower_pos 2 p)) (bracket_aux _)) as [H1|l H1 H2]. simpl. intros H2 _. destruct (good_rdir (ZtoN (Zfloor (IZR (Zpos m) * / IZR (Zpower_pos 2 p))))) as (H3, _). now rewrite H2 in H3. intros _. now apply Rlt_not_eq. revert H1. case rdir. intros H1. rewrite Znat.Z_of_N_succ. rewrite Z_of_N_ZtoN. apply sym_eq. apply Zceil_floor_neq. now apply H1. apply Zfloor_lub. now apply (F2R_ge_0 radix2 (Float radix2 (Zpos m) (- (Zpos p)))). intros _. rewrite Z_of_N_ZtoN. apply refl_equal. apply Zfloor_lub. now apply (F2R_ge_0 radix2 (Float radix2 (Zpos m) (- (Zpos p)))). intros p H. apply sym_eq. apply round_generic... apply generic_format_F2R. intros _ ; simpl. rewrite He. generalize (Zlt_neg_0 p). lia. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux