proposition: Lemma error_flt_correct_aux : forall prec mode emin p xi x, contains (convert xi) x -> contains (convert (error_flt prec mode emin p xi)) (Xerror_flt mode emin p x) /\ contains (convert (error_flt prec mode emin p xi)) (Xreal 0).
proof: Proof. intros prec mode emin p [|xl xu] [|xr]; try easy; [now unfold convert; case (_ && _)|]. cbn -[error_aux]. case_eq (F.valid_lb xl); [| simpl; lra]. case_eq (F.valid_ub xu); [| simpl; lra]. simpl. intros Vu Vl [Hl Hu]. generalize (abs_correct_aux xl xu xr). unfold convert. rewrite Vu, Vl. set (xu' := F.max (F.neg xl) xu). intros Hr. assert (Vu' : F.valid_ub xu' = true). { apply F'.max_valid_ub; [| easy]. now rewrite F'.valid_ub_neg. } simple refine (let Hx := Hr _ in _). now split. clearbody xu' Hx. clear -Hx Vu'. destruct F.real eqn:Ru'. 2: easy. case Z.eqb_spec. 2: easy. intros R2. cbv [andb]. apply F'.real_correct in Ru'. rewrite Ru' in Hx. simpl in Hx. set (e := FLT.FLT_exp emin (Z.pos p) (F.StoZ (F.mag xu'))). refine (_ (error_aux_correct_aux prec mode (FLT.FLT_exp emin (Z.pos p)) e xr _ _)). now destruct error_aux. now apply FLT.FLT_exp_valid. unfold Ulp.ulp. case Req_bool_spec ; intros Hxr. { destruct (@FLT.negligible_exp_FLT emin (Z.pos p) eq_refl) as [n [-> H]]. unfold e, FLT.FLT_exp. rewrite Z.max_r by lia. apply bpow_le, Z.le_max_r. } apply bpow_le, Generic_fmt.cexp_le_bpow ; try easy. apply FLT.FLT_exp_monotone. apply Rle_lt_trans with (1 := Hx). rewrite <- (Rabs_pos_eq (F.toR xu')). 2: apply Rle_trans with (2 := Hx), Rabs_pos. generalize (F.mag_correct xu'). unfold bpow. now rewrite R2. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval