proposition: Lemma round_at_exp_aux_correct : forall mode e2 sign m1 e1 pos, valid_mantissa m1 -> FtoX (toF (round_at_exp_aux mode e2 sign m1 e1 pos)) = FtoX (Fround_at_exp mode (EtoZ e2) (@Generic.Ufloat radix sign (MtoP m1) (EtoZ e1) pos)).
proof: Proof. intros mode p' sign m1 e1 pos Hm1. apply f_equal. unfold round_at_exp_aux. rewrite exponent_cmp_correct. rewrite exponent_sub_correct. rewrite exponent_zero_correct. unfold Fround_at_exp. unfold radix. case_eq (EtoZ p' - EtoZ e1)%Z ; unfold Z.compare. intros Hd. destruct (adjust_mantissa_correct mode m1 pos sign Hm1) as (H1,H2). now rewrite toF_float, H1. intros dp Hd. rewrite exponent_cmp_correct, mantissa_digits_correct, exponent_sub_correct; try easy. rewrite Hd; simpl Z.compare. case Pos.compare_spec. - intros Hc. rewrite <- mantissa_shrp_correct with (z := (exponent_sub p' e1)); try easy; last 2 first. - now rewrite exponent_sub_correct. - rewrite shift_correct, Z.pow_pos_fold. rewrite <- Hc, <- digits_conversion. destruct (Zdigits_correct Carrier.radix (Z.pos (MtoP m1))). now lia. - destruct need_change_zero; try easy. - destruct mantissa_one_correct as [Ho1 Ho2]. now rewrite toF_float, Ho1. - now apply toF_zero. - intros Hc. rewrite fun_if with (f := toF). destruct mantissa_one_correct as [Ho1 Ho2]. now rewrite toF_zero, toF_float, Ho1. - intros Hc. refine ( _ (mantissa_shr_correct dp m1 (exponent_sub p' e1) pos Hm1 _ _)); last 2 first. - now rewrite exponent_sub_correct. - rewrite shift_correct, Z.pow_pos_fold. - assert (He: (Zpos dp <= Zpos ( count_digits Carrier.radix (MtoP m1)) -1)%Z) by lia. generalize (Zpower_le Carrier.radix _ _ He). rewrite <- digits_conversion. destruct (Zdigits_correct Carrier.radix (Z.pos (MtoP m1))). now lia. 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). now rewrite Ha, <- Hl. 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