proposition: Lemma Fnearbyint_exact_correct : forall beta mode (x : float beta), FtoX (Fnearbyint_exact mode x) = Xnearbyint mode (FtoX x).
proof: Proof. intros beta mode x. assert (bP := Zle_bool_imp_le _ _ (radix_prop beta)). unfold Fnearbyint_exact, Fround_at_exp. destruct x as [| |b p z]; simpl float_to_ufloat; lazy iota beta; try easy. now generalize (Rnearbyint_IZR mode 0); simpl; intro H; rewrite H. destruct z as [| p1 | n1]; simpl Zminus; lazy iota beta. - now rewrite adjust_mantissa_Eq; simpl; rewrite Rnearbyint_IZR. - now simpl; rewrite Rnearbyint_IZR. rewrite <-digits_conversion, shift1_correct. case Z.compare_spec; intro H. set (x := Float b p _). set (p1 := adjust_pos _ _ _). pose (y := (FtoR beta b p (Z.neg n1))). apply trans_equal with (y := Xreal (IZR (cond_Zopp (Rlt_bool y 0) (mode_choice mode (Rlt_bool y 0) 0 (convert_location_inv p1))))). unfold y; rewrite Rlt_bool_float. now destruct b; destruct mode; simpl; destruct p1. apply (f_equal Xreal). apply sym_equal. assert (V : (1 < beta ^ Z.pos n1)%Z) by now apply Zpower_gt_1. assert (V0 : (1 < IZR (beta ^ Z.pos n1))%R) by now apply IZR_lt. assert (V1 : (Z.pos p < beta ^ Z.pos n1)%Z). generalize (Zdigits_correct beta (Z.pos p)). now rewrite H; intros [_ V3]. assert (V2 : inbetween_int 0 (Rabs y) (convert_location_inv p1)). unfold p1, inbetween_int. rewrite adjust_pos_correct; try lia; last 2 first. - now rewrite Pos2Z.inj_pow, radix_to_pos. - now rewrite Pos2Z.inj_pow, radix_to_pos; lia. simpl; unfold y, p1; rewrite FtoR_abs. rewrite Pos2Z.inj_pow, radix_to_pos. replace 1%R with (0 + IZR (beta ^ Z.pos n1)* (1 / IZR (beta ^ Z.pos n1)))%R; last first. field; last now apply Rlt_neq_sym; lra. apply new_location_correct; try lia. - apply Rdiv_lt_0_compat; try lra. apply inbetween_Exact. simpl. rewrite Z.pow_pos_fold. now field; lra. destruct mode; apply (f_equal IZR). - now eapply inbetween_int_UP_sign. - now eapply inbetween_int_DN_sign. - now eapply inbetween_int_ZR_sign with (l := (convert_location_inv p1)). - now eapply inbetween_int_NE_sign. set (x := Float b p _). set (p1 := pos_Lo). pose (y := (FtoR beta b p (Z.neg n1))). apply trans_equal with (y := Xreal (IZR (cond_Zopp (Rlt_bool y 0) (mode_choice mode (Rlt_bool y 0) 0 (convert_location_inv p1))))). unfold y; rewrite Rlt_bool_float. now destruct b; destruct mode; simpl; destruct p1. apply (f_equal Xreal). apply sym_equal. assert (0 < IZR (Zpos p))%R as V by now apply IZR_lt. assert (V0 : (1 < beta ^ Z.pos n1)%Z) by now apply Zpower_gt_1. assert (V1 : (1 < IZR (beta ^ Z.pos n1))%R) by now apply IZR_lt. assert (V2 : (Z.pos p < beta ^ Z.pos n1)%Z). generalize (Zdigits_correct beta (Z.pos p)). intros [_ V2]. apply Z.lt_trans with (1 := V2). apply Zpower_lt; lia. assert (V3 : inbetween_int 0 (Rabs y) (convert_location_inv p1)). unfold y, p1, inbetween_int. rewrite FtoR_abs. apply inbetween_Inexact; simpl; rewrite Z.pow_pos_fold. - split; try lra. - apply Rdiv_lt_0_compat; lra. - apply Rdiv_gt_mult_pos; try lra. rewrite Rmult_1_r; apply IZR_lt; lia. - rewrite Rcompare_div_l; try lra. replace (IZR (beta ^ Z.pos n1) * ((0 + 1) / 2))%R with (IZR (beta ^ Z.pos n1) / 2)%R; last first. now unfold Rdiv; ring. rewrite Rcompare_div_r; try lra. rewrite <- (mult_IZR 2). rewrite Rcompare_IZR. apply Zcompare_Lt; apply Z.gt_lt. apply Zgt_le_trans with (m := (beta * Zpos p)%Z); last first. now apply Zmult_le_compat_r; lia. apply Zle_gt_trans with (m := (beta ^ (1 + Zdigits beta (Z.pos p)))%Z). now apply Zpower_le; lia. rewrite Zpower_plus, Z.pow_1_r; try lia; last first. now apply Zdigits_ge_0. apply Zmult_gt_compat_l; try lia. generalize (Zdigits_correct beta (Z.pos p)); lia. destruct mode; apply (f_equal IZR). - now eapply inbetween_int_UP_sign. - now eapply inbetween_int_DN_sign. - now eapply inbetween_int_ZR_sign with (l := (convert_location_inv p1)). - now eapply inbetween_int_NE_sign. rewrite Zdiv_eucl_unique. set (q := (_ / _)%Z). set (r := (_ mod _)%Z). assert (Pq : (0 < q)%Z). apply Z.div_str_pos; split; try easy; try lia. generalize (Zdigits_correct beta (Zpos p)); intros [U1 U2]. apply Z.le_trans with (2 := U1). rewrite Pos2Z.inj_pow, radix_to_pos. now apply Zpower_le; lia. assert (Pr : (0 <= r < Z.pos (Z.to_pos beta ^ n1))%Z). now apply Z_mod_lt. revert Pq. case_eq q; try lia; intros q1 Hq1; try lia; intros _. unfold FtoX. rewrite FtoR_split. rewrite adjust_mantissa_correct, adjust_pos_correct; last 2 first. - rewrite Pos2Z.inj_pow, radix_to_pos. now apply Zpower_gt_1. - now apply Pr. unfold F2R; simpl bpow; rewrite Rmult_1_r. pose (ll := new_location (Z.pos (Z.to_pos beta ^ n1)) r loc_Exact). assert (V : inbetween_int q (IZR (Zpos p) / IZR (Z.pow_pos beta n1)) ll). unfold q, inbetween_int, ll. replace (IZR (Z.pos p / Z.pos (Z.to_pos beta ^ n1) + 1))%R with (IZR (Z.pos p / Z.pos (Z.to_pos beta ^ n1)) + IZR (Z.pos (Z.to_pos beta ^ n1)) * (1 / IZR (Z.pos (Z.to_pos beta ^ n1))))%R; last first. rewrite plus_IZR; simpl. field. apply Rlt_neq_sym. now apply IZR_lt. apply new_location_correct; try lia. - apply Rdiv_lt_0_compat; try lra. now apply IZR_lt. - rewrite Pos2Z.inj_pow, radix_to_pos. now apply Zpower_gt_1. apply inbetween_Exact. unfold r. rewrite Pos2Z.inj_pow, radix_to_pos, Z.pow_pos_fold. assert (0 < beta ^ Z.pos n1)%Z. apply Zpower_gt_0; lia. rewrite (Z_div_mod_eq (Z.pos p) (beta ^ Z.pos n1)) at 1; try lia. rewrite plus_IZR, mult_IZR. field. apply Rlt_neq_sym; apply IZR_lt; lia. unfold Fnum; apply sym_equal. rewrite <-(Rlt_bool_float beta b p (Z.neg n1)) at 2 3. destruct mode; unfold Xlift, Rnearbyint, F2R; do 2 eapply f_equal. - apply inbetween_int_UP_sign. now rewrite FtoR_abs, <- Hq1. - apply inbetween_int_DN_sign. now rewrite FtoR_abs, <- Hq1. - apply inbetween_int_ZR_sign with (l := ll). now rewrite FtoR_abs, <- Hq1. - apply inbetween_int_NE_sign with (l := ll). now rewrite FtoR_abs, <- Hq1. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic