proposition: Lemma avg_half_sub_correct_aux: forall u v, format u -> format v -> u <= v -> (0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) -> 0 < Rabs ((u+v)/2) < bpow emin -> 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 x y a av. intros u v Fu Fv uLev same_sign. pose (b:=(u+v)/2); fold b. intros (H1,H2). apply generic_format_FIX_FLT,FIX_format_generic in Fu. apply generic_format_FIX_FLT,FIX_format_generic in Fv. destruct Fu as [[nu eu] J1 J2]. destruct Fv as [[nv ev] J3 J4]; simpl in J2, J4. assert (b = IZR (nu+nv) * bpow (emin-1)). unfold b; rewrite J1, J3; unfold F2R; rewrite J2,J4; simpl. unfold Zminus; rewrite bpow_plus, plus_IZR. change (bpow (-(1))) with (/2). field. assert (Z.abs (nu+nv) = 1)%Z. cut (0 < Z.abs (nu+nv) < 2)%Z. lia. split; apply lt_IZR; simpl; rewrite abs_IZR; apply Rmult_lt_reg_l with (bpow (emin-1)); try apply bpow_gt_0. rewrite Rmult_0_r. apply Rlt_le_trans with (1:=H1). right; rewrite H, Rabs_mult. rewrite (Rabs_right (bpow (emin -1))). ring. apply Rle_ge, bpow_ge_0. apply Rle_lt_trans with (Rabs b). right; rewrite H, Rabs_mult. rewrite (Rabs_right (bpow (emin -1))). ring. apply Rle_ge, bpow_ge_0. apply Rlt_le_trans with (1:=H2). right; unfold Zminus; rewrite bpow_plus. change (bpow (-(1))) with (/2). field. assert (((nu=0)/\ (nv=1)) \/ ((nu=-1)/\(nv=0)))%Z. assert (nu <= nv)%Z. apply le_IZR. apply Rmult_le_reg_r with (bpow emin). apply bpow_gt_0. apply Rle_trans with u. right; rewrite J1,J2; reflexivity. apply Rle_trans with (1:=uLev). right; rewrite J3,J4; reflexivity. case same_sign; intros (L1,L2). rewrite J1 in L1; apply Fnum_ge_0 in L1; simpl in L1. rewrite J3 in L2; apply Fnum_ge_0 in L2; simpl in L2. left. rewrite Z.abs_eq in H0. lia. lia. rewrite J1 in L1; apply Fnum_le_0 in L1; simpl in L1. rewrite J3 in L2; apply Fnum_le_0 in L2; simpl in L2. right. rewrite Z.abs_neq in H0. lia. lia. assert (G1:(round_flt (bpow emin/2) = 0)). replace (bpow emin /2) with (bpow (emin-1)). unfold round, scaled_mantissa. rewrite cexp_FLT_FIX. unfold cexp, FIX_exp; simpl. rewrite <- bpow_plus. replace (bpow (emin - 1 + - emin)) with (/2). replace (ZnearestE (/ 2)) with 0%Z. unfold F2R; simpl; ring. unfold Znearest. replace (Zfloor (/2)) with 0%Z. rewrite Rcompare_Eq. reflexivity. simpl; ring. apply sym_eq, Zfloor_imp. simpl; lra. ring_simplify (emin-1+-emin)%Z; reflexivity. apply Rgt_not_eq, Rlt_gt, bpow_gt_0. rewrite Rabs_right. apply bpow_lt. unfold Prec_gt_0 in prec_gt_0_; lia. apply Rle_ge, bpow_ge_0. unfold Zminus; rewrite bpow_plus. reflexivity. case H3; intros (T1,T2). unfold b, avg_half_sub. rewrite J1,J3,J2,J4,T1,T2; unfold F2R; simpl. rewrite Rmult_0_l, Rmult_1_l, 2!Rplus_0_l. unfold Rminus; rewrite Ropp_0, Rplus_0_r. rewrite (round_generic _ _ _ (bpow (emin)))... 2: apply generic_format_FLT_bpow... 2: lia. rewrite G1. rewrite round_0... rewrite Rplus_0_l, Rabs_Ropp. rewrite Rabs_right. 2: apply Rle_ge, Rmult_le_pos. 2: apply bpow_ge_0. 2: lra. apply Rle_trans with ((3*ulp_flt (bpow emin / 2))/2);[idtac|right; unfold Rdiv; ring]. unfold Rdiv; apply Rmult_le_compat_r. lra. apply Rle_trans with (3*bpow emin). apply Rle_trans with (1*bpow emin). right; ring. apply Rmult_le_compat_r. apply bpow_ge_0. now apply IZR_le. apply Rmult_le_compat_l. now apply IZR_le. rewrite ulp_neq_0. 2: apply Rmult_integral_contrapositive_currified. 2: apply Rgt_not_eq, bpow_gt_0. 2: apply Rinv_neq_0_compat, Rgt_not_eq; lra. apply bpow_le. unfold cexp, FLT_exp. apply Z.le_max_r. unfold b, avg_half_sub. rewrite J1,J3,J2,J4,T1,T2; unfold F2R; simpl. rewrite Rmult_0_l, Rplus_0_r. replace (0 - _ * bpow emin) with (bpow emin) by ring. rewrite (round_generic _ _ _ (bpow emin))... 2: apply generic_format_FLT_bpow... 2: lia. rewrite G1. replace (_ * bpow emin + 0) with (-bpow emin) by ring. rewrite round_generic... 2: apply generic_format_opp. 2: apply generic_format_FLT_bpow... 2: lia. replace (- bpow emin - _ * bpow emin / 2) with (-(bpow emin/2)) by field. rewrite Rabs_Ropp. rewrite Rabs_right. replace (_ * bpow emin / 2) with (-(bpow emin/2)) by field. rewrite ulp_opp. apply Rle_trans with ((3*ulp_flt (bpow emin / 2))/2);[idtac|right; unfold Rdiv; ring]. unfold Rdiv; apply Rmult_le_compat_r. lra. apply Rle_trans with (3*bpow emin). apply Rle_trans with (1*bpow emin). right; ring. apply Rmult_le_compat_r. apply bpow_ge_0. now apply IZR_le. apply Rmult_le_compat_l. now apply IZR_le. rewrite ulp_neq_0. 2: apply Rmult_integral_contrapositive_currified. 2: apply Rgt_not_eq, bpow_gt_0. 2: apply Rinv_neq_0_compat, Rgt_not_eq; lra. apply bpow_le. unfold cexp, FLT_exp. apply Z.le_max_r. apply Rle_ge, Rmult_le_pos. apply bpow_ge_0. lra. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)