proposition: Theorem truncate_FIX_correct : forall x m e l, inbetween_float beta m e x l -> (e <= emin)%Z \/ l = loc_Exact -> let '(m', e', l') := truncate_FIX (m, e, l) in inbetween_float beta m' e' x l' /\ (e' = cexp beta (FIX_exp emin) x \/ (l' = loc_Exact /\ generic_format beta (FIX_exp emin) x)).
proof: Proof. intros x m e l H1 H2. unfold truncate_FIX. set (k := (emin - e)%Z). set (p := Zpower beta k). unfold cexp, FIX_exp. generalize (Zlt_cases 0 k). case (Zlt_bool 0 k) ; intros Hk. split. now apply inbetween_float_new_location. clear H2. left. unfold k. ring. split. exact H1. unfold k in Hk. destruct H2 as [H2|H2]. left. lia. right. split. exact H2. rewrite H2 in H1. inversion_clear H1. rewrite H. apply generic_format_F2R. unfold cexp. lia. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket