proposition: Lemma avg_half_sub_correct_aux2: forall u v, format u -> format v -> u <= v -> (0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) -> Rabs (avg_half_sub u v -((u+v)/2)) <= 3/2 * ulp_flt ((u+v)/2).
proof: Proof. Proof with auto with typeclass_instances. clear Fx Fy a av x y. intros u v Fu Fv uLev same_sign. pose (b:=(u+v)/2); fold b. assert (T: forall z, Rabs (2*z) = 2* Rabs z). intros z; rewrite Rabs_mult. rewrite Rabs_pos_eq; try reflexivity. apply Rlt_le, Rlt_0_2. destruct uLev as [uLtv|uEqv]. assert (B: u <= v) by now left. assert (K1: b <> 0). unfold b ; lra. assert (Y:(Rabs (round_flt (v - u) - (v-u)) <= ulp_flt b)). apply Rle_trans with (/2*ulp_flt (v-u)). apply error_le_half_ulp... apply Rmult_le_reg_l with (1 := Rlt_0_2). rewrite <- Rmult_assoc, Rinv_r, Rmult_1_l. 2: apply Rgt_not_eq, Rlt_0_2. apply Rle_trans with (ulp_flt (2*b)). case same_sign; intros (T1,T2). apply ulp_le_pos... lra. unfold b ; lra. rewrite <- (ulp_opp _ _ (2*b)). apply ulp_le_pos... lra. unfold b ; lra. rewrite 2!ulp_neq_0; trivial. 2: lra. change 2 with (bpow 1). rewrite <- bpow_plus. apply bpow_le. unfold cexp, FLT_exp. rewrite Rmult_comm, mag_mult_bpow; trivial. rewrite <- Z.add_max_distr_l. replace (mag radix2 b + 1 - prec)%Z with (1 + (mag radix2 b - prec))%Z by ring. apply Z.max_le_compat_l. lia. case (Rle_or_lt (bpow emin) (Rabs b)); intros D. unfold avg_half_sub. case (Rle_or_lt (bpow (prec+emin)) (v-u)); intros H1. cut (round_flt (round_flt (v - u) / 2) = round_flt (v - u) / 2). intros Z; rewrite Z. replace (round_flt (u + round_flt (v - u) / 2) - b) with ((round_flt (u + round_flt (v - u) / 2) - (u + round_flt (v - u) / 2)) +/2*(round_flt (v - u)-(v-u))). 2: unfold b; field. apply Rle_trans with (1:=Rabs_triang _ _). apply Rle_trans with (ulp_flt b+/2*ulp_flt b);[idtac|right; field]. apply Rplus_le_compat. apply Rle_trans with (/2*ulp_flt (u + round_flt (v - u) / 2)). apply error_le_half_ulp... apply Rmult_le_reg_l with (1 := Rlt_0_2). rewrite <- Rmult_assoc, Rinv_r, Rmult_1_l. 2: apply Rgt_not_eq, Rlt_0_2. apply Rle_trans with (2:=FLT_ulp_double _ _ _). apply ulp_le... replace (u + round_flt (v - u) / 2) with (b+/2*(round_flt (v - u) - (v - u))). 2: unfold b; field. rewrite (T b). replace (2 * Rabs b) with (Rabs b + Rabs b) by ring. apply Rle_trans with (1:=Rabs_triang _ _). apply Rplus_le_compat_l. rewrite Rabs_mult. rewrite Rabs_pos_eq. 2: lra. apply Rmult_le_reg_l with (1 := Rlt_0_2). rewrite <- Rmult_assoc, Rinv_r, Rmult_1_l. 2: apply Rgt_not_eq, Rlt_0_2. apply Rle_trans with (1:=Y). apply Rle_trans with (ulp_flt (2*b)). apply ulp_le... rewrite <- (Rmult_1_l (Rabs b)). rewrite (T b). apply Rmult_le_compat_r. apply Rabs_pos. now apply IZR_le. rewrite <- (T b). rewrite <- ulp_abs. apply FLT_ulp_le_id... assert (H:generic_format radix2 (FIX_exp emin) (2*b)). replace (2*b) with (u+v). 2: unfold b; field. apply generic_format_FIX_FLT,FIX_format_generic in Fu. apply generic_format_FIX_FLT,FIX_format_generic in Fv. destruct Fu as [fu J1 J2]. destruct Fv as [fv J3 J4]. apply generic_format_FIX. exists (Float radix2 (Fnum fu+Fnum fv) emin). rewrite J1,J3; unfold F2R; simpl. rewrite J2,J4, plus_IZR; ring. easy. apply FIX_format_generic in H. destruct H as [[n e] J1 J2]. rewrite J1; unfold F2R; rewrite J2. simpl; rewrite Rabs_mult. pattern (bpow emin) at 1; rewrite <- (Rmult_1_l (bpow emin)). rewrite (Rabs_right (bpow emin)). 2: apply Rle_ge, bpow_ge_0. apply Rmult_le_compat_r. apply bpow_ge_0. rewrite <- abs_IZR. apply IZR_le. cut (0 < Z.abs n)%Z. lia. apply Z.abs_pos. intros M; apply K1. apply Rmult_eq_reg_l with 2. 2: apply Rgt_not_eq, Rlt_0_2. rewrite Rmult_0_r, J1, M. apply F2R_0. rewrite Rabs_mult. rewrite Rabs_right. 2: lra. apply Rmult_le_compat_l with (2 := Y). lra. apply round_generic... apply FLT_format_half... apply generic_format_round... apply abs_round_ge_generic... apply generic_format_FLT_bpow... unfold Prec_gt_0 in prec_gt_0_; lia. rewrite Rabs_right; try assumption. apply Rle_ge; left; apply Rplus_lt_reg_l with u; now ring_simplify. cut ((round_flt (v - u)= (v-u))). intros Z; rewrite Z. replace (u + round_flt ((v-u) / 2)) with (b+((round_flt ((v-u) / 2) - (v-u)/2))). 2: unfold b; field. pose (eps:=(round_flt ((v - u) / 2) - (v - u) / 2)%R); fold eps. assert (Rabs eps <= /2*bpow emin). unfold eps. apply Rle_trans with (1:=error_le_half_ulp _ _ _ _)... right; apply f_equal. apply ulp_FLT_small... rewrite Zplus_comm; apply Rle_lt_trans with (2:=H1). rewrite Rabs_pos_eq ; lra. replace (round_flt (b + eps) - b) with ((round_flt (b+eps) -(b+eps)) + eps) by ring. apply Rle_trans with (1:=Rabs_triang _ _). apply Rle_trans with (/2*ulp_flt (b+eps) + /2*bpow emin). apply Rplus_le_compat. apply error_le_half_ulp... assumption. apply Rmult_le_reg_l with (1 := Rlt_0_2). apply Rle_trans with (ulp_flt (b + eps)+bpow emin). right; field. apply Rle_trans with (2*ulp_flt b + ulp_flt b). 2: right; field. apply Rplus_le_compat. apply Rle_trans with (2:=FLT_ulp_double _ _ _). apply ulp_le... rewrite (T b). replace (2 * Rabs b) with (Rabs b + Rabs b) by ring. apply Rle_trans with (1:=Rabs_triang _ _). apply Rplus_le_compat_l. apply Rle_trans with (2:=D). rewrite <- (Rmult_1_l (bpow emin)). apply Rle_trans with (1:=H). apply Rmult_le_compat_r. apply bpow_ge_0. lra. rewrite <- ulp_FLT_small with radix2 emin prec 0... apply ulp_ge_ulp_0... rewrite Rabs_R0; apply bpow_gt_0. apply round_generic... apply FLT_format_plus_small... now apply generic_format_opp. rewrite Rabs_right. now left. apply Rle_ge, Rplus_le_reg_l with u; now ring_simplify. apply avg_half_sub_correct_aux; trivial. split; trivial. now apply Rabs_pos_lt. unfold avg_half_sub,b. rewrite uEqv. replace (v-v) with 0 by ring. rewrite round_0... unfold Rdiv; rewrite Rmult_0_l. rewrite round_0... rewrite Rplus_0_r. rewrite round_generic... replace ((v+v)*/2) with v by field. replace (v-v) with 0 by ring. rewrite Rabs_R0. apply Rmult_le_pos. apply Rmult_le_pos. now apply IZR_le. lra. apply ulp_ge_0. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)