proposition: Lemma round_plus_small_id_aux: forall f h, format f -> (bpow (prec+emin) <= f) -> 0 < f -> Rabs h <= /4* ulp_flt f -> round_flt (f+h) = f.
proof: Proof. Proof with auto with typeclass_instances. intros f h Ff H1 H2 Hh. case (Rle_or_lt 0 h); intros H3;[destruct H3|idtac]. rewrite Rabs_right in Hh. 2: now apply Rle_ge, Rlt_le. apply round_N_eq_DN_pt with (f+ ulp_flt f)... pattern f at 2; rewrite <- (round_DN_plus_eps_pos radix2 (FLT_exp emin prec) f) with (eps:=h); try assumption. apply round_DN_pt... now left. split. now left. apply Rle_lt_trans with (1:=Hh). rewrite <- (Rmult_1_l (ulp_flt f)) at 2. apply Rmult_lt_compat_r. rewrite ulp_neq_0; try now apply Rgt_not_eq. apply bpow_gt_0. lra. rewrite <- (round_UP_plus_eps_pos radix2 (FLT_exp emin prec) f) with (eps:=h); try assumption. apply round_UP_pt... now left. split; trivial. apply Rle_trans with (1:=Hh). rewrite <- (Rmult_1_l (ulp_flt f)) at 2. apply Rmult_le_compat_r. apply ulp_ge_0. lra. apply Rplus_lt_reg_l with (-f); ring_simplify. apply Rlt_le_trans with (/2*ulp_flt f). 2: right; field. apply Rle_lt_trans with (1:=Hh). apply Rmult_lt_compat_r. rewrite ulp_neq_0; try now apply Rgt_not_eq. apply bpow_gt_0. lra. rewrite <- H, Rplus_0_r. apply round_generic... rewrite Rabs_left in Hh; try assumption. assert (0 < pred_flt f). apply Rlt_le_trans with (bpow emin). apply bpow_gt_0. apply pred_ge_gt... apply generic_format_FLT_bpow... apply Z.le_refl. apply Rlt_le_trans with (2:=H1). apply bpow_lt. unfold Prec_gt_0 in prec_gt_0_; lia. assert (M:(prec + emin +1 <= mag radix2 f)%Z). apply mag_ge_bpow. replace (prec+emin+1-1)%Z with (prec+emin)%Z by ring. rewrite Rabs_right; try assumption. apply Rle_ge; now left. assert (T1:(ulp_flt (pred_flt f) = ulp_flt f) \/ ( ulp_flt (pred_flt f) = /2* ulp_flt f /\ f = bpow (mag radix2 f -1))). generalize H; rewrite pred_eq_pos; [idtac|now left]. unfold pred_pos; case Req_bool_spec; intros K HH. right; split; try assumption. rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. apply trans_eq with (bpow (mag radix2 f- prec -1)). apply f_equal. unfold cexp. apply trans_eq with (FLT_exp emin prec (mag radix2 f -1)%Z). apply f_equal. unfold FLT_exp. rewrite Z.max_l by lia. apply mag_unique. rewrite Rabs_right. split. apply Rplus_le_reg_l with (bpow (mag radix2 f -1-prec)). ring_simplify. apply Rle_trans with (bpow (mag radix2 f - 1 - 1) + bpow (mag radix2 f - 1 - 1)). apply Rplus_le_compat_r. apply bpow_le. unfold Prec_gt_0 in prec_gt_0_; lia. apply Rle_trans with (bpow 1*bpow (mag radix2 f - 1 - 1)). change (bpow 1) with 2. right; ring. rewrite <- bpow_plus. apply Rle_trans with (bpow (mag radix2 f -1)). apply bpow_le; lia. rewrite <- K; now right. rewrite <- K. apply Rplus_lt_reg_l with (-f+bpow (mag radix2 f-1-prec)); ring_simplify. apply bpow_gt_0. apply Rle_ge. rewrite K at 1. apply Rplus_le_reg_l with (bpow (mag radix2 f - 1 - prec)). ring_simplify. apply bpow_le. unfold Prec_gt_0 in prec_gt_0_; lia. unfold FLT_exp. rewrite Z.max_l by lia. ring. replace (/2) with (bpow (-1)) by reflexivity. rewrite ulp_neq_0; try now apply Rgt_not_eq. rewrite <- bpow_plus. apply f_equal. unfold cexp, FLT_exp. rewrite Z.max_l by lia. ring. left. assert (bpow (mag radix2 f -1) < f). destruct (mag radix2 f); simpl in *. destruct a. now apply Rgt_not_eq. rewrite Rabs_right in H0. destruct H0; try assumption. contradict H0. now apply sym_not_eq. apply Rle_ge; now left. assert (bpow (mag radix2 f -1) + ulp_flt (bpow (mag radix2 f-1)) <= f). rewrite <- succ_eq_pos;[idtac|apply bpow_ge_0]. apply succ_le_lt... apply generic_format_FLT_bpow... unfold Prec_gt_0 in prec_gt_0_;lia. rewrite ulp_bpow in H4. unfold FLT_exp in H4. rewrite Z.max_l in H4 by lia. replace (mag radix2 f - 1 + 1 - prec)%Z with (mag radix2 f - prec)%Z in H4 by ring. rewrite ulp_neq_0; try now apply Rgt_not_eq. rewrite ulp_neq_0 at 2; try now apply Rgt_not_eq. unfold cexp. apply f_equal; apply f_equal. replace (ulp_flt f) with (bpow (mag radix2 f -prec)). apply mag_unique. rewrite Rabs_right. split. apply Rplus_le_reg_l with (bpow (mag radix2 f -prec)). ring_simplify. apply Rle_trans with (2:=H4); right; ring. apply Rlt_trans with f. apply Rplus_lt_reg_l with (-f+bpow (mag radix2 f - prec)). ring_simplify. apply bpow_gt_0. apply Rle_lt_trans with (1:=RRle_abs _). apply bpow_mag_gt. apply Rle_ge. apply Rplus_le_reg_l with (bpow (mag radix2 f - prec)). ring_simplify. left; apply Rle_lt_trans with (2:=H0). apply bpow_le. unfold Prec_gt_0 in prec_gt_0_;lia. rewrite ulp_neq_0; try now apply Rgt_not_eq. unfold cexp, FLT_exp. rewrite Z.max_l. reflexivity. lia. assert (T: (ulp_flt (pred_flt f) = ulp_flt f \/ (ulp_flt (pred_flt f) = / 2 * ulp_flt f /\ - h < / 4 * ulp_flt f)) \/ (ulp_flt (pred_flt f) = / 2 * ulp_flt f /\ f = bpow (mag radix2 f - 1) /\ - h = / 4 * ulp_flt f) ). destruct T1. left; now left. case Hh; intros P. left; right. split; try apply H0; assumption. right. split; try split; try apply H0; assumption. clear T1. destruct T. apply round_N_eq_UP_pt with (pred_flt f)... rewrite <- (round_DN_minus_eps_pos radix2 (FLT_exp emin prec) f) with (eps:=-h); try assumption. replace (f--h) with (f+h) by ring. apply round_DN_pt... split. auto with real. apply Rle_trans with (1:=Hh). apply Rle_trans with (/2*ulp_flt f). apply Rmult_le_compat_r. apply ulp_ge_0. lra. case H0. intros Y; rewrite Y. rewrite <- (Rmult_1_l (ulp_flt f)) at 2. apply Rmult_le_compat_r. apply ulp_ge_0. lra. intros Y; rewrite (proj1 Y); now right. replace (f+h) with (pred_flt f + (f-pred_flt f+h)) by ring. pattern f at 4; rewrite <- (round_UP_pred_plus_eps_pos radix2 (FLT_exp emin prec) f) with (eps:=(f - pred_flt f + h)); try assumption. apply round_UP_pt... replace (f-pred_flt f) with (ulp_flt (pred_flt f)). split. apply Rplus_lt_reg_l with (-h); ring_simplify. case H0; [intros Y|intros (Y1,Y2)]. apply Rle_lt_trans with (1:=Hh). rewrite Y. rewrite <- (Rmult_1_l (ulp_flt f)) at 2. apply Rmult_lt_compat_r. rewrite ulp_neq_0;[apply bpow_gt_0|now apply Rgt_not_eq]. lra. apply Rlt_le_trans with (1:=Y2). rewrite Y1. apply Rmult_le_compat_r. apply ulp_ge_0. lra. apply Rplus_le_reg_l with (-ulp_flt (pred_flt f)); ring_simplify. now left. rewrite pred_eq_pos; try now left. pattern f at 2; rewrite <- (pred_pos_plus_ulp radix2 (FLT_exp emin prec) f)... ring. apply Rplus_lt_reg_l with (-f); ring_simplify. apply Rle_lt_trans with (-(/2 * ulp_flt (pred_flt f))). right. apply trans_eq with ((pred_flt f - f) / 2). field. rewrite pred_eq_pos; try now left. pattern f at 2; rewrite <- (pred_pos_plus_ulp radix2 (FLT_exp emin prec) f)... field. replace h with (--h) by ring. apply Ropp_lt_contravar. case H0;[intros Y|intros (Y1,Y2)]. apply Rle_lt_trans with (1:=Hh). rewrite Y. apply Rmult_lt_compat_r. rewrite ulp_neq_0; try apply bpow_gt_0; now apply Rgt_not_eq. lra. apply Rlt_le_trans with (1:=Y2). rewrite Y1. right; field. elim H0; intros T1 (T2,T3); clear H0. assert (pred_flt f = bpow (mag radix2 f - 1) - bpow (mag radix2 f - 1 -prec)). rewrite pred_eq_pos; try now left. unfold pred_pos; case Req_bool_spec. intros _; rewrite <- T2. apply f_equal, f_equal. unfold FLT_exp. rewrite Z.max_l. ring. lia. intros Y; now contradict T2. assert (round radix2 (FLT_exp emin prec) Zfloor (f+h) = pred_flt f). replace (f+h) with (f-(-h)) by ring. apply round_DN_minus_eps_pos... split. auto with real. rewrite T3, T1. apply Rmult_le_compat_r. apply ulp_ge_0. lra. assert (round radix2 (FLT_exp emin prec) Zceil (f+h) = f). replace (f+h) with (pred_flt f + /2*ulp_flt (pred_flt f)). apply round_UP_pred_plus_eps_pos... split. apply Rmult_lt_0_compat. lra. rewrite ulp_neq_0; try now apply Rgt_not_eq. apply bpow_gt_0. rewrite <- (Rmult_1_l (ulp_flt (pred_flt f))) at 2. apply Rmult_le_compat_r. apply ulp_ge_0. lra. rewrite T1, H0, <- T2. replace h with (--h) by ring; rewrite T3. replace (bpow (mag radix2 f - 1 - prec)) with (/2*ulp_flt f). field. replace (/2) with (bpow (-1)) by reflexivity. rewrite T2 at 1. rewrite ulp_bpow, <- bpow_plus. apply f_equal; unfold FLT_exp. rewrite Z.max_l. ring. lia. assert ((Z.even (Zfloor (scaled_mantissa radix2 (FLT_exp emin prec) (f + h)))) = false). replace (Zfloor (scaled_mantissa radix2 (FLT_exp emin prec) (f + h))) with (Zpower radix2 prec -1)%Z. unfold Zminus; rewrite Z.even_add. rewrite Z.even_opp. rewrite Z.even_pow. reflexivity. unfold Prec_gt_0 in prec_gt_0_; lia. apply eq_IZR. rewrite <- scaled_mantissa_DN... 2: rewrite H4; assumption. rewrite H4. unfold scaled_mantissa. rewrite bpow_opp. rewrite <- ulp_neq_0; try now apply Rgt_not_eq. rewrite T1. rewrite Rinv_mult_distr. 2: apply Rgt_not_eq; lra. 2: apply Rgt_not_eq; rewrite ulp_neq_0; try apply bpow_gt_0. 2: now apply Rgt_not_eq. rewrite Rinv_involutive. 2: apply Rgt_not_eq; lra. rewrite T2 at 2. rewrite ulp_bpow. rewrite <- bpow_opp. unfold FLT_exp at 2. rewrite Z.max_l by lia. replace 2 with (bpow 1) by reflexivity. rewrite <- bpow_plus. rewrite H0. rewrite Rmult_minus_distr_r, <- 2!bpow_plus. rewrite minus_IZR. apply f_equal2. rewrite IZR_Zpower. apply f_equal. ring. unfold Prec_gt_0 in prec_gt_0_; lia. apply trans_eq with (bpow 0). reflexivity. apply f_equal. ring. rewrite round_N_middle. rewrite H5. rewrite H6. reflexivity. rewrite H5, H4. pattern f at 1; rewrite <- (pred_pos_plus_ulp radix2 (FLT_exp emin prec) f); try assumption. ring_simplify. rewrite <- pred_eq_pos;[idtac|now left]. rewrite T1. replace h with (--h) by ring. rewrite T3. field. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)