proposition: Theorem float_of_fix_flt : forall rdir {Hrnd : Valid_rnd rdir}, forall x : R, forall d1 d2 : Z, forall p1 p2 : positive, FIX x d1 -> FLT x p1 -> Zle_bool d2 d1 && Zle_bool (Zpos p1) (Zpos p2) = true -> rounding_float rdir p2 d2 x = x.
proof: Proof. Proof with auto with typeclass_instances. intros rdir Hrnd x d1 d2 p1 p2 (f1,(Hx1,Hx2)) (f2,(Hx3,Hx4)) Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Zle_bool_imp_le _ _ H1). clear H1. intro H1. generalize (Zle_bool_imp_le _ _ H2). clear H2. intro H2. apply round_generic... destruct f1 as (m1, e1). destruct f2 as (m2, e2). destruct (Z.eq_dec m2 0) as [Hm|Hm]. rewrite <- Hx3. unfold float2R. rewrite Hm, F2R_0. apply generic_format_0. assert (mag radix2 (F2R (Float radix2 m2 e2)) <= Zpos p2 + e2)%Z. rewrite mag_F2R with (1 := Hm). apply Zplus_le_compat_r. apply Z.le_trans with (2 := H2). apply bpow_lt_bpow with radix2. destruct (mag radix2 (IZR m2)) as (n2, Hn). simpl. specialize (Hn (IZR_neq _ _ Hm)). apply Rle_lt_trans with (1 := proj1 Hn). rewrite <- abs_IZR. now apply IZR_lt. destruct (Zle_or_lt e1 e2) as [He|He]. rewrite <- Hx3. apply generic_format_F2R. intros _ ; simpl. apply Z.max_lub. clear -H ; lia. apply Z.le_trans with (1 := H1). now apply Z.le_trans with e1. rewrite <- Hx1. apply generic_format_F2R. intros _ ; simpl. apply Z.max_lub. unfold float2R in Hx1. simpl in Hx1. rewrite Hx1, <- Hx3. unfold float2R. simpl. lia. now apply Z.le_trans with d1. Qed.
imports: Coq(Bool ZArith Reals Lia) Flocq(Core Digits Round Relative) Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round