proposition: Lemma hombnd_rnd : forall m M u v b B, hombnd m M u v b B -> hombnd (Rmin m M) M (round radix2 fexp ZnearestE u) v (round_err b B) B.
proof: Proof. Proof with auto with typeclass_instances. intros m M u v b B [Ho1 [Ho2 Ho]]. unfold hombnd, round_err. rewrite F2R_plus, F2R_mult, F2R_plus. split. apply Rplus_le_le_0_compat with (2 := Ho1). apply Rmult_le_pos. apply Rplus_le_le_0_compat with (1 := Ho1). now apply Rle_trans with (1 := Rle_0_1). now apply F2R_ge_0. apply (conj Ho2). intros H. specialize (Ho (Rle_trans _ _ _ H (Rmin_l _ _))). destruct Ho as [Ho3 Ho4]. refine (conj _ Ho4). replace (round radix2 fexp ZnearestE u - v)%R with ((round radix2 fexp ZnearestE u - u) + (u - v))%R by ring. rewrite Rmult_plus_distr_r. apply Rle_trans with (1 := Rabs_triang _ _). apply Rplus_le_compat with (2 := Ho3). apply Rle_trans with (1 := error_le_half_ulp _ _ _ _). apply Rmult_le_reg_l with 2%R. apply Rlt_0_2. rewrite <- (Rmult_assoc 2), Rinv_r, Rmult_1_l by apply Rgt_not_eq, Rlt_0_2. assert (HM : (0 <= M)%R). apply Rle_trans with (2 := Rmin_r m M). apply Rle_trans with (2 := H). apply bpow_ge_0. assert (H' : (0 <= (F2R b + F2R B) * M)%R). apply Rmult_le_pos with (2 := HM). apply Rplus_le_le_0_compat with (1 := Ho1). now apply Rle_trans with (1 := Rle_0_1). apply Rle_trans with (ulp radix2 fexp ((F2R b + F2R B) * M)). apply ulp_le... rewrite Rabs_pos_eq with (1 := H'). rewrite Rmult_plus_distr_r. replace u with (u - v + v)%R by ring. apply Rle_trans with (1 := Rabs_triang _ _). now apply Rplus_le_compat. replace (2 * ((F2R b + F2R B) * F2R {| Fnum := 1; Fexp := - prec |} * M))%R with ((F2R b + F2R B) * M * bpow radix2 (1 - prec))%R. rewrite <- (Rabs_pos_eq _ H') at 2. apply ulp_FLT_le. rewrite Rabs_pos_eq with (1 := H'). apply Rle_trans with (1 := H). apply Rle_trans with (1 := Rmin_r _ _). rewrite <- (Rmult_1_l M) at 1. rewrite <- (Rplus_0_l 1). apply Rmult_le_compat_r with (1 := HM). now apply Rplus_le_compat. unfold Zminus. rewrite bpow_plus. change (bpow radix2 1) with 2%R. rewrite F2R_bpow. ring. Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)