proposition: Lemma error_aux_correct_aux : forall prec mode fexp e x, Generic_fmt.Valid_exp fexp -> (Ulp.ulp radix2 fexp x <= bpow radix2 e)%R -> contains (convert (error_aux prec mode e)) (Xreal (Generic_fmt.round radix2 fexp (rnd_of_mode mode) x - x)) /\ contains (convert (error_aux prec mode e)) (Xreal 0).
proof: Proof. intros prec mode fexp e x Ve Hx. unfold error_aux. set (e' := match mode with rnd_NE => Z.pred e | _ => e end). set (err := F.pow2_UP prec (F.ZtoS e')). assert (mode = rnd_NE \/ e' = e) as [-> | ->] by now (destruct mode ; left + right). - destruct (F.pow2_UP_correct prec (F.ZtoS e')) as [Hp1 Hp2]. generalize (F.ZtoS_correct prec e'). fold err in Hp1, Hp2 |- *. simpl. rewrite F'.valid_lb_neg, Hp1, F'.neg_correct. destruct (F.toX err) as [ |er]. easy. intros [Hs|Hs] ; [|easy]. simpl. simple refine (let H := _ in conj H _). 2: { apply Rabs_le in H. apply Rabs_le_inv. apply Rle_trans with (2 := H). rewrite Rabs_R0. apply Rabs_pos. } apply Rabs_le_inv. apply Rle_trans with (2 := Hp2). eapply Rle_trans. now apply Ulp.error_le_half_ulp. rewrite Rmult_1_l. apply Rle_trans with (bpow radix2 (e - 1)). 2: now apply bpow_le. unfold Z.sub. rewrite Zplus_comm, bpow_plus. apply Rmult_le_compat_l with (2 := Hx). apply bpow_ge_0. - destruct (F.pow2_UP_correct prec (F.ZtoS e)) as [Hp1 Hp2]. generalize (F.ZtoS_correct prec e). fold err in Hp1, Hp2 |- *. assert (Hp3 := F'.valid_lb_neg err). rewrite Hp1 in Hp3. destruct (F.toX err) as [ |er] eqn:He. { intros _. destruct mode ; simpl ; rewrite ?Hp1, ?Hp3, ?F'.valid_lb_zero, ?F'.valid_ub_zero ; simpl ; rewrite ?F'.neg_correct, ?F.zero_correct, He ; simpl ; try easy ; repeat split ; try apply Rle_refl. apply Rle_0_minus. now apply Generic_fmt.round_UP_pt. apply Rle_minus. now apply Generic_fmt.round_DN_pt. } intros [Hs|Hs] ; [|easy]. assert (- er <= Generic_fmt.round radix2 fexp (rnd_of_mode mode) x - x <= er)%R. { apply Rabs_le_inv. eapply Rle_trans. apply Ulp.error_le_ulp. exact Ve. apply valid_rnd_of_mode. apply Rle_trans with (2 := Hp2). rewrite Rmult_1_l. apply Rle_trans with (1 := Hx). now apply bpow_le. } assert (H1 := Rabs_le _ _ H). assert (H2 := Rle_trans _ _ _ (Rabs_pos _) H1). destruct mode ; simpl ; rewrite ?Hp1, ?Hp3, ?F'.valid_lb_zero, ?F'.valid_ub_zero ; simpl ; rewrite ?F'.neg_correct, ?F.zero_correct, He ; simpl ; split ; try apply Rabs_le_inv ; try split ; try rewrite Rabs_R0 ; try easy ; try apply Rle_refl ; try apply H. apply Rle_0_minus. now apply Generic_fmt.round_UP_pt. apply Rle_minus. now apply Generic_fmt.round_DN_pt. rewrite <- Ropp_0. now apply Ropp_le_contravar. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval