proposition: Theorem generic_format_truncate : forall m e l, (0 <= m)%Z -> let '(m', e', l') := truncate (m, e, l) in format (F2R (Float beta m' e')).
proof: Proof. intros m e l Hm. unfold truncate. set (k := (fexp (Zdigits beta m + e) - e)%Z). case Zlt_bool_spec ; intros Hk. unfold truncate_aux. apply generic_format_F2R. intros Hd. unfold cexp. rewrite mag_F2R_Zdigits with (1 := Hd). rewrite Zdigits_div_Zpower with (1 := Hm). replace (Zdigits beta m - k + (e + k))%Z with (Zdigits beta m + e)%Z by ring. unfold k. ring_simplify. apply Z.le_refl. split. now apply Zlt_le_weak. apply Znot_gt_le. contradict Hd. apply Zdiv_small. apply conj with (1 := Hm). rewrite <- Z.abs_eq with (1 := Hm). apply Zpower_gt_Zdigits. apply Zlt_le_weak. now apply Z.gt_lt. destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm']. apply generic_format_F2R. unfold cexp. rewrite mag_F2R_Zdigits. 2: now apply Zgt_not_eq. unfold k in Hk. clear -Hk. lia. rewrite <- Hm', F2R_0. apply generic_format_0. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket