proposition: Lemma Fround_at_prec_correct : forall beta mode prec s m1 e1 pos x, (0 < x)%R -> inbetween_float beta (Zpos m1) e1 x (convert_location_inv pos) -> ( (Zpos (count_digits beta m1) < Zpos prec)%Z -> pos = pos_Eq ) -> FtoX (Fround_at_prec mode prec (@Ufloat beta s m1 e1 pos)) = Xreal (round beta mode prec (if s then Ropp x else x)).
proof: Proof. Proof with auto with typeclass_instances. intros beta mode prec s m1 e1 pos x Hx Hl Hp. unfold round. rewrite round_trunc_sign_any_correct with (choice := mode_choice mode) (m := Zpos m1) (e := e1) (l := convert_location_inv pos)... unfold Round.truncate, Round.truncate_aux, FLX_exp. replace (Zdigits beta (Zpos m1) + e1 - Zpos prec - e1)%Z with (Zdigits beta (Zpos m1) - Zpos prec)%Z by ring. replace (Rlt_bool (if s then (-x)%R else x) 0) with s. unfold Fround_at_prec. case_eq (Zpos (count_digits beta m1) - Zpos prec)%Z. intros Hd. apply (f_equal Xreal). rewrite FtoR_split. rewrite adjust_mantissa_correct. rewrite digits_conversion, Hd. easy. intros d Hd. rewrite digits_conversion, Hd. rewrite shift_correct, Zmult_1_l. fold (Zpower beta (Zpos d)). unfold Z.div, Zmod. assert (Zpower beta (Zpos d) > 0)%Z. apply Z.lt_gt. now apply Zpower_gt_0. generalize (Z_div_mod (Zpos m1) (Zpower beta (Zpos d)) H). clear H. case Z.div_eucl. intros q r (Hq, Hr). cut (0 < q)%Z. clear -Hr. case q ; try easy. clear q. intros q _. apply (f_equal Xreal). rewrite FtoR_split. rewrite adjust_mantissa_correct. simpl. apply (f_equal (fun v => F2R (Defs.Float beta (cond_Zopp s (mode_choice mode s (Zpos q) v)) (e1 + Zpos d)))). rewrite <- (Zmult_1_l (Zpower_pos beta d)). rewrite <- shift_correct. apply adjust_pos_correct ; rewrite shift_correct, Zmult_1_l. now apply (Zpower_gt_1 beta (Zpos d)). exact Hr. clear -Hd Hq Hr. apply Zmult_lt_reg_r with (Zpower beta (Zpos d)). now apply Zpower_gt_0. apply Zplus_lt_reg_r with r. simpl (0 * Zpower beta (Zpos d) + r)%Z. rewrite Zmult_comm, <- Hq. apply Z.lt_le_trans with (1 := proj2 Hr). fold (Z.abs (Zpos m1)). apply Zpower_le_Zdigits. rewrite <- Hd. rewrite <- digits_conversion. now apply Zlt_minus_simpl_swap. intros d Hd. rewrite digits_conversion, Hd. rewrite Hp. simpl. rewrite FtoR_split. now destruct mode. apply Z.lt_sub_0. now rewrite Hd. clear -Hx. apply sym_eq. case s. apply Rlt_bool_true. rewrite <- Ropp_0. now apply Ropp_lt_contravar. apply Rlt_bool_false. now apply Rlt_le. clear. intros x m l Hx. case mode ; simpl. now apply inbetween_int_UP_sign. now apply inbetween_int_DN_sign. now apply inbetween_int_ZR_sign with (l := l). now apply inbetween_int_NE_sign with (x := x). case s. rewrite Rabs_Ropp, Rabs_pos_eq. exact Hl. now apply Rlt_le. rewrite Rabs_pos_eq. exact Hl. now apply Rlt_le. rewrite digits_conversion. unfold FLX_exp. destruct (Zle_or_lt (Zpos prec) (Zpos (count_digits beta m1))) as [H|H]. left. clear -H ; lia. right. now rewrite Hp. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic