proposition: Lemma rndG_conversion_aux : forall rexp f, float2R (round rdir rexp f) = Generic_fmt.round radix2 rexp rndG (float2R f).
proof: Proof. Proof with auto with typeclass_instances. intros rexp (m, e). unfold float2R. simpl. destruct m as [|m|m]. rewrite 2!F2R_0, round_0... unfold round. simpl. generalize (hrndG_conversion (rpos rdir) (rpos_good _) rexp m e). unfold Generic_fmt.round, rndG. simpl. rewrite Rcompare_Gt. intros H. rewrite <- H. case round_pos. intros [|n] z ; simpl. unfold float2R. now rewrite 2!F2R_0. apply refl_equal. unfold scaled_mantissa. apply Rmult_lt_0_compat. now apply F2R_gt_0. apply bpow_gt_0. unfold round. simpl. change (Zneg m) with (- Zpos m)%Z. rewrite F2R_Zopp. generalize (hrndG_conversion (rneg rdir) (rneg_good _) rexp m e). unfold Generic_fmt.round, rndG. simpl. rewrite Rcompare_Lt. rewrite cexp_opp. rewrite scaled_mantissa_opp. rewrite Ropp_involutive. rewrite F2R_Zopp. intros H. rewrite <- H. case round_pos. intros [|n] z ; simpl. unfold float2R. rewrite 2!F2R_0. now rewrite Ropp_0. now rewrite <- Fopp2_correct. rewrite scaled_mantissa_opp. apply Ropp_lt_gt_0_contravar. unfold scaled_mantissa. apply Rmult_lt_0_compat. now apply F2R_gt_0. apply bpow_gt_0. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux