proposition: Theorem rel_of_fix_float_n : forall c p d xn x zi, FIX x xn -> rel_of_fix_float_n_helper p d xn zi = true -> REL (rounding_float (Znearest c) p d x) x zi.
proof: Proof. Proof with auto with typeclass_instances. intros c p d xn x zi ((mx, ex), (Hx1, Hx2)) Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Zle_bool_imp_le _ _ H1). clear H1. intro H1. generalize (Fle2_correct _ _ H2). unfold float2R. simpl. rewrite (F2R_Zopp _ 1%Z), F2R_bpow. clear H2. intro H2. generalize (Fle2_correct _ _ H3). unfold float2R. simpl. rewrite F2R_bpow. clear H3. intro H3. destruct (Rle_or_lt (Rabs x) (bpow radix2 (d + Zpos p))) as [He|He]. rewrite round_generic... exists 0%R. repeat split. apply Rle_trans with (1 := H2). rewrite <- Ropp_0. apply Ropp_le_contravar. apply bpow_ge_0. apply Rle_trans with (2 := H3). apply bpow_ge_0. now rewrite Rplus_0_r, Rmult_1_r. apply generic_format_FLT_FIX... rewrite <- Hx1. apply generic_format_F2R. intros _. now apply Z.le_trans with xn. exists ((rounding_float (Znearest c) p d x - x) / x)%R. assert (Rabs ((rounding_float (Znearest c) p d x - x) / x) <= bpow radix2 (- Zpos p))%R. apply float_relative_n_whole. apply Rlt_le. apply Rlt_trans with (2 := He). apply bpow_lt. pattern (d + Zpos p)%Z at 2 ; rewrite <- Zplus_0_r. now apply Zplus_lt_compat_l. repeat split. apply Rle_trans with (1 := H2). apply Ropp_le_cancel. rewrite Ropp_involutive. apply Rle_trans with (2 := H). rewrite <- Rabs_Ropp. apply Rabs_idem. apply Rle_trans with (2 := H3). apply Rle_trans with (2 := H). apply Rabs_idem. field. intros H0. apply Rlt_not_le with (1 := He). rewrite H0, Rabs_R0. apply bpow_ge_0. Qed.
imports: Coq(Bool ZArith Reals Lia) Flocq(Core Digits Round Relative) Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round