proposition: Theorem float_absolute_n : forall c p d x xi zi, ABS 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). destruct (Req_dec x 0) as [Hx0|Hx0]. rewrite Hx0, round_0, Rminus_0_r, Rabs_R0... apply bpow_ge_0. replace (bpow radix2 (float_ulp p d (Fnum (upper xi)) (Fexp (upper xi)) - 1)) with (/2 * ulp radix2 (FLT_exp d (Zpos p)) (upper xi))%R. apply Rle_trans with (/2 * ulp radix2 (FLT_exp d (Zpos p)) x)%R. apply error_le_half_ulp... apply Rmult_le_compat_l. apply Rlt_le. apply Rinv_0_lt_compat. now apply IZR_lt. rewrite <- ulp_abs. apply ulp_le_pos... apply Rabs_pos. apply Hx. assert (Hm0: (Fnum (upper xi)) <> Z0). assert (Hx1 := Rabs_no_R0 _ Hx0). contradict Hx1. apply Rle_antisym. replace 0%R with (float2R (upper xi)). apply Hx. clear -Hx1. destruct (upper xi). simpl in Hx1. rewrite Hx1. apply float2_zero. apply Rabs_pos. rewrite ulp_neq_0. 2: now apply F2R_neq_0. rewrite <- (bpow_plus radix2 (-1)). unfold Zminus. rewrite (Zplus_comm _ (-1)). apply (f_equal (fun e => bpow radix2 (-1 + e))). clear -Hm0. destruct (upper xi) as (m, e). unfold cexp, float2R. rewrite mag_F2R with (1 := Hm0). rewrite <- Zdigits_mag with (1 := Hm0). simpl. rewrite <- Zdigits_abs. rewrite Zplus_comm. destruct m as [|m|m] ; unfold Z.abs. now elim Hm0. now rewrite <- digits2_digits. now rewrite <- digits2_digits. 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