proposition: Lemma round_aux_correct : forall mode p sign m1 e1 pos, valid_mantissa m1 -> FtoX (toF (round_aux mode p sign m1 e1 pos)) = FtoX (Fround_at_prec mode (prec p) (@Generic.Ufloat radix sign (MtoP m1) (EtoZ e1) pos)).
proof: Proof. intros mode p' sign m1 e1 pos Hm1. apply f_equal. unfold round_aux. set (p := match exponent_cmp p' exponent_zero with Gt => p' | _ => exponent_one end). assert (Hp: Zpos (prec p') = EtoZ p). unfold p. rewrite exponent_cmp_correct, exponent_zero_correct. unfold prec. case_eq (EtoZ p') ; try easy ; intros ; apply sym_eq ; apply exponent_one_correct. clearbody p. rewrite exponent_cmp_correct. rewrite exponent_sub_correct. rewrite exponent_zero_correct. rewrite mantissa_digits_correct with (1 := Hm1). unfold Fround_at_prec. rewrite Hp. unfold radix. case_eq (Zpos (count_digits Carrier.radix (MtoP m1)) - EtoZ p)%Z ; unfold Z.compare. intros Hd. destruct (adjust_mantissa_correct mode m1 pos sign Hm1) as (H1,H2). rewrite toF_float with (1 := H2). now rewrite H1. intros dp Hd. refine (_ (mantissa_shr_correct dp m1 (exponent_sub (mantissa_digits m1) p) pos Hm1 _ _)). case mantissa_shr. intros sq sl. case Z.div_eucl. intros q r (Hq, (Hl, Vq)). rewrite <- Hq. destruct (adjust_mantissa_correct mode sq sl sign Vq) as (Ha, Va). rewrite toF_float with (1 := Va). rewrite Ha. rewrite exponent_add_correct, exponent_sub_correct, mantissa_digits_correct with (1 := Hm1). now rewrite Hd, Hl. now rewrite exponent_sub_correct, mantissa_digits_correct. rewrite shift_correct, Zmult_1_l. change (Zpower Carrier.radix (Zpos dp) <= Z.abs (Zpos (MtoP m1)))%Z. apply Zpower_le_Zdigits. rewrite <- Hd, <- Hp. rewrite <- digits_conversion. clear ; lia. intros dp Hd. now rewrite toF_float. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig