proposition: Theorem shr_fexp_truncate : forall m e l, (0 <= m)%Z -> shr_fexp m e l = let '(m', e', l') := truncate radix2 fexp (m, e, l) in (shr_record_of_loc m' l', e').
proof: Proof. intros m e l Hm. case_eq (truncate radix2 fexp (m, e, l)). intros (m', e') l'. unfold shr_fexp. rewrite Zdigits2_Zdigits. case_eq (fexp (Zdigits radix2 m + e) - e)%Z. intros He. unfold truncate. rewrite He. simpl. intros H. now inversion H. intros p Hp. assert (He: (e <= fexp (Zdigits radix2 m + e))%Z). clear -Hp ; lia. destruct (inbetween_float_ex radix2 m e l) as (x, Hx). generalize (inbetween_shr x m e l (fexp (Zdigits radix2 m + e) - e) Hm Hx). assert (Hx0 : (0 <= x)%R). apply Rle_trans with (F2R (Float radix2 m e)). now apply F2R_ge_0. exact (proj1 (inbetween_float_bounds _ _ _ _ _ Hx)). case_eq (shr (shr_record_of_loc m l) e (fexp (Zdigits radix2 m + e) - e)). intros mrs e'' H3 H4 H1. generalize (truncate_correct radix2 _ x m e l Hx0 Hx (or_introl _ He)). rewrite H1. intros (H2,_). rewrite <- Hp, H3. assert (e'' = e'). change (snd (mrs, e'') = snd (fst (m',e',l'))). rewrite <- H1, <- H3. unfold truncate. now rewrite Hp. rewrite H in H4 |- *. apply (f_equal (fun v => (v, _))). destruct (inbetween_float_unique _ _ _ _ _ _ _ H2 H4) as (H5, H6). rewrite H5, H6. case mrs. now intros m0 [|] [|]. intros p Hp. unfold truncate. rewrite Hp. simpl. intros H. now inversion H. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative