proposition: Theorem truncate_correct_format : forall m e, m <> Z0 -> let x := F2R (Float beta m e) in generic_format beta fexp x -> (e <= fexp (Zdigits beta m + e))%Z -> let '(m', e', l') := truncate (m, e, loc_Exact) in x = F2R (Float beta m' e') /\ e' = cexp beta fexp x.
proof: Proof. intros m e Hm x Fx He. assert (Hc: cexp beta fexp x = fexp (Zdigits beta m + e)). unfold cexp, x. now rewrite mag_F2R_Zdigits. unfold truncate. rewrite <- Hc. set (k := (cexp beta fexp x - e)%Z). case Zlt_bool_spec ; intros Hk. unfold truncate_aux. rewrite Fx at 1. assert (H: (e + k)%Z = cexp beta fexp x). unfold k. ring. refine (conj _ H). rewrite <- H. apply F2R_eq. replace (scaled_mantissa beta fexp x) with (IZR (Zfloor (scaled_mantissa beta fexp x))). rewrite Ztrunc_IZR. unfold scaled_mantissa. rewrite <- H. unfold x, F2R. simpl. rewrite Rmult_assoc, <- bpow_plus. ring_simplify (e + - (e + k))%Z. clear -Hm Hk. destruct k as [|k|k] ; try easy. simpl. apply Zfloor_div. intros H. generalize (Zpower_pos_gt_0 beta k) (Zle_bool_imp_le _ _ (radix_prop beta)). lia. rewrite scaled_mantissa_generic with (1 := Fx). now rewrite Zfloor_IZR. split. apply refl_equal. unfold k in Hk. lia. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket