proposition: Theorem truncate_correct' : forall x m e l, (0 <= x)%R -> inbetween_float beta m e x l -> (e <= cexp beta fexp x)%Z \/ l = loc_Exact -> let '(m', e', l') := truncate (m, e, l) in inbetween_float beta m' e' x l' /\ (e' = cexp beta fexp x \/ (l' = loc_Exact /\ format x)).
proof: Proof. intros x m e l [Hx|Hx] H1 H2. - destruct (Zle_or_lt e (fexp (Zdigits beta m + e))) as [H3|H3]. + generalize (truncate_correct_partial x m e l Hx H1 H3). destruct (truncate (m, e, l)) as [[m' e'] l']. intros [H4 H5]. apply (conj H4). now left. + destruct H2 as [H2|H2]. generalize (truncate_correct_partial' x m e l Hx H1 H2). destruct (truncate (m, e, l)) as [[m' e'] l']. intros [H4 H5]. apply (conj H4). now left. rewrite H2 in H1 |- *. simpl. generalize (Zlt_cases 0 (fexp (Zdigits beta m + e) - e)). destruct Zlt_bool. intros H. apply False_ind. lia. intros _. apply (conj H1). right. repeat split. inversion_clear H1. rewrite H. apply generic_format_F2R. intros Zm. unfold cexp. rewrite mag_F2R_Zdigits with (1 := Zm). now apply Zlt_le_weak. - assert (Hm: m = 0%Z). cut (m <= 0 < m + 1)%Z. lia. assert (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R as Hx'. apply inbetween_float_bounds with (1 := H1). rewrite <- Hx in Hx'. split. apply le_0_F2R with (1 := proj1 Hx'). apply gt_0_F2R with (1 := proj2 Hx'). rewrite Hm, <- Hx in H1 |- *. clear -H1. destruct H1 as [_ | l' [H _] _]. + assert (exists e', truncate (Z0, e, loc_Exact) = (Z0, e', loc_Exact)). unfold truncate, truncate_aux. case Zlt_bool. rewrite Zdiv_0_l, Zmod_0_l. eexists. apply f_equal. unfold new_location. now case Z.even. now eexists. destruct H as [e' H]. rewrite H. split. constructor. apply eq_sym, F2R_0. right. repeat split. apply generic_format_0. + rewrite F2R_0 in H. elim Rlt_irrefl with (1 := H). Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket