proposition: Theorem float_absolute_inv_n : forall c p d x xi zi, ABS (rounding_float (Znearest c) p d x) xi -> float_absolute_n_helper p d xi zi = true -> BND (rounding_float (Znearest c) p d x - x) zi.
proof: Proof. Proof with auto with typeclass_instances. intros c p d x xi zi Hx Hb. assert (H: (Rabs (rounding_float (Znearest c) p d x - x) <= bpow radix2 (float_ulp p d (Fnum (upper xi)) (Fexp (upper xi)) - 1))%R). replace (float_ulp p d (Fnum (upper xi)) (Fexp (upper xi))) with (FLT_exp d (Zpos p) (if Z.eq_dec (Fnum (upper xi)) Z0 then d else (Fexp (upper xi) + Zpos (digits (pos_of_Z (Z.abs (Fnum (upper xi))))))%Z)). apply float_absolute_inv_n_whole. apply Rle_lt_trans with (1 := proj2 (proj2 Hx)). unfold float2R. case Z.eq_dec ; intros Zx. rewrite Zx, F2R_0. apply bpow_gt_0. rewrite digits2_digits. rewrite Zpos_pos_of_Z. rewrite Zdigits_abs, Zplus_comm. rewrite <- mag_F2R_Zdigits with (1 := Zx). destruct mag as (ex,Ex) ; simpl. apply Rle_lt_trans with (1 := RRle_abs _). apply Ex. contradict Zx. apply eq_0_F2R with (1 := Zx). clear -Zx ; zify ; lia. unfold float_ulp. case Z.eq_dec ; intros Zx. rewrite Zx. unfold FLT_exp. clear ; zify ; lia. revert Zx. case Fnum ; simpl ; [|easy|easy]. intros H. now elim H. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fle2_correct _ _ H1). clear H1. intro H1. generalize (Fle2_correct _ _ H2). clear H2. intro H2. split. apply Rle_trans with (1 := H1). unfold float2R. rewrite (F2R_Zopp _ 1%Z). rewrite F2R_bpow. apply Ropp_le_cancel. rewrite Ropp_involutive. apply (Rle_trans _ _ _ (Rabs_idem _)). now rewrite Rabs_Ropp. apply Rle_trans with (2 := H2). unfold float2R. rewrite F2R_bpow. now apply (Rle_trans _ _ _ (Rabs_idem _)). 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