proposition: Lemma Bnearbyint_correct_aux : forall md sx mx ex (Hx : bounded mx ex = true), let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in let z := SFnearbyint_binary md sx mx ex in valid_binary z = true /\ SF2R radix2 z = (round radix2 (FIX_exp 0) (round_mode md) x) /\ is_finite_SF z = true /\ (is_nan_SF z = false -> sign_SF z = sx).
proof: Proof. intros md sx mx ex Hmxex. simpl. set (mrs' := if (ex <? - prec)%Z then {| shr_m := Z0; shr_r := false; shr_s := true |} else fst (shr {| shr_m := Z.pos mx; shr_r := false; shr_s := false |} ex (- ex))). assert (mrs'_simpl : mrs' = fst (shr {| shr_m := Z.pos mx; shr_r := false; shr_s := false |} ex (- ex))). { unfold mrs'. case Zlt_bool_spec; [ | easy]. intros Hex1. symmetry. apply shr_limit; simpl; [now left |]. apply Z.lt_le_trans with (radix2 ^ prec)%Z. - unfold bounded, canonical_mantissa, fexp in Hmxex. apply andb_prop in Hmxex. destruct Hmxex as [Hmxex _]. apply Zeq_bool_eq in Hmxex. rewrite Zpos_digits2_pos in Hmxex. apply Z.eq_le_incl in Hmxex. apply Z.max_lub_l in Hmxex. assert (Hmx : (Zdigits radix2 (Z.pos mx) <= prec)%Z) by lia. replace (Z.pos mx) with (Z.abs (Z.pos mx)); [| now simpl]. now apply Zpower_gt_Zdigits. - apply Zpower_le. lia. } assert (mrs'_ge_0 : (ex < 0)%Z -> (0 <= shr_m mrs')%Z). { intros Hex. rewrite mrs'_simpl. apply (Z.mul_le_mono_pos_l _ _ (2 ^ (- ex))). apply (Zpower_gt_0 radix2). lia. rewrite Z.mul_0_r. apply le_shr_le. easy. lia. } repeat split; unfold SFnearbyint_binary, SFnearbyint_binary_aux; case Zle_bool_spec; intros Hex0; fold mrs'; auto. - destruct choice_mode eqn:H0; auto. unfold shl_align_fexp. destruct shl_align as [mx''' ex'''] eqn:H1; simpl. unfold bounded, canonical_mantissa in Hmxex. apply andb_prop in Hmxex. destruct Hmxex as [Hmxex Hex']. unfold bounded, canonical_mantissa. assert (A : (fexp (Z.pos (digits2_pos p) + 0) <= 0)%Z). { rewrite Z.add_0_r in *. rewrite Zpos_digits2_pos in *. destruct (le_shr_le mrs' ex (- ex)) as [H2 H3]; [now apply mrs'_ge_0 | lia |]. destruct (le_choice_mode_le md sx (shr_m mrs') (loc_of_shr_record mrs')) as [H4 H5]. rewrite H0 in H4, H5. transitivity (fexp (Zdigits radix2 (shr_m mrs' + 1))); [apply fexp_monotone; apply Zdigits_le; [lia | assumption] | transitivity (fexp ((Zdigits radix2 (shr_m mrs') + 1))); [apply fexp_monotone; apply Zdigits_succ_le; now apply mrs'_ge_0 | transitivity (fexp (Zdigits radix2 ((shr_m {| shr_m := Z.pos mx; shr_r := false; shr_s := false |}) / (2 ^ (- ex))) + 1)); [apply fexp_monotone; apply Zplus_le_compat_r; apply Zdigits_le; simpl; auto | simpl ]]]. - apply Zdiv.Zdiv_le_lower_bound; [lia |]. rewrite Z.mul_comm. rewrite mrs'_simpl. apply le_shr_le; simpl; lia. - transitivity (fexp (Zdigits radix2 (Z.pos mx / 2 ^ 1) + 1)). + apply fexp_monotone. apply Zplus_le_compat_r. apply Zdigits_le. * apply Z.div_pos; lia. * apply Z.opp_pos_neg in Hex0. apply Z.div_le_compat_l; [lia |]. split; [lia |]. apply Z.pow_le_mono_r; lia. + rewrite Zdigits_div_Zpower; [| lia |]. * rewrite Z.sub_add. apply Zeq_bool_eq in Hmxex. unfold fexp in *. rewrite Z.max_lub_iff. split; [| lia]. apply (Zplus_le_reg_l _ _ ex). rewrite Zplus_0_r. rewrite Z.add_sub_assoc. rewrite Z.add_comm. rewrite <-Hmxex at 2. apply Z.le_max_l. * split; [lia |]. replace 1%Z with (Zdigits radix2 (Z.pos 1)); [| easy]. apply Zdigits_le; lia. } refine (_ (shl_align_correct' p 0 (fexp (Z.pos (digits2_pos p) + 0)) _)). + rewrite H1. intros [H2 H3]. rewrite <-H3 in H2. apply andb_true_intro; split. * apply Zeq_bool_true. rewrite H3 at 2. rewrite !Zpos_digits2_pos. rewrite <-!mag_F2R_Zdigits; [| lia | lia]. now apply (f_equal (fun f => fexp (mag radix2 f))). * apply Zle_bool_true. rewrite H3. transitivity 0%Z; [assumption|]. apply Zle_minus_le_0. apply Z.lt_le_incl. apply prec_lt_emax_. + assumption. - symmetry. apply round_generic; auto. + apply valid_rnd_round_mode. + apply generic_format_FIX. exists (Float radix2 (cond_Zopp sx (Z.pos mx) * Z.pow 2 ex) 0); auto. simpl. rewrite <-(Z.sub_0_r ex) at 2. now apply F2R_change_exp. - rewrite round_trunc_sign_any_correct with (choice := choice_mode md) (m := Z.pos mx) (e := ex) (l := loc_Exact). + fold (shr_record_of_loc (Z.pos mx) loc_Exact) in mrs'_simpl. rewrite mrs'_simpl. replace (- ex)%Z with (FIX_exp 0 (Zdigits2 (Z.pos mx) + ex) - ex)%Z; [| auto]. rewrite !shr_truncate; [ | apply FIX_exp_valid | easy ]. destruct truncate as (rec, loc) eqn:H0. destruct rec as (z0, z1) eqn:H1. simpl. rewrite shr_m_shr_record_of_loc. rewrite loc_of_shr_record_of_loc. replace (Rlt_bool (F2R {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}) 0) with sx. * destruct choice_mode as [| p0 | p0] eqn:H2. -- simpl. symmetry. rewrite cond_Zopp_0. apply F2R_0. -- generalize (shl_align_fexp_correct p0 0). destruct shl_align_fexp as (p1, z2). simpl. intros [H3 _]. rewrite !F2R_cond_Zopp. apply f_equal. simpl in H0. rewrite Zlt_bool_true in H0; [| lia]. rewrite Z.add_opp_diag_r in H0. injection H0. intros _ H4 _. now rewrite <-H4. -- destruct (le_choice_mode_le md sx z0 loc) as [H3 _]. rewrite H2 in H3. simpl in H0. rewrite Zlt_bool_true in H0 by lia. injection H0. intros _ _ H4. elim (Zle_not_lt 0 z0). rewrite <- H4. apply Z_div_pos. apply Z.lt_gt, (Zpower_gt_0 radix2). lia. easy. now apply Z.le_lt_trans with (1 := H3). * rewrite F2R_cond_Zopp. apply eq_sym, Rlt_bool_cond_Ropp. now apply F2R_gt_0. + apply FIX_exp_valid. + apply valid_rnd_round_mode. + apply round_mode_choice_mode. + rewrite <-F2R_abs. simpl. rewrite abs_cond_Zopp. simpl. now apply inbetween_Exact. + auto. - destruct choice_mode eqn:H0; [easy | now destruct shl_align_fexp |]. apply mrs'_ge_0 in Hex0. destruct (le_choice_mode_le md sx (shr_m mrs') (loc_of_shr_record mrs')) as [H2 H3]. rewrite H0 in H2, H3. lia. - destruct choice_mode eqn:H0; [easy | now destruct shl_align_fexp | easy]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative