proposition: Theorem generic_round_generic : forall x, generic_format fexp1 x -> generic_format fexp1 (round fexp2 rnd x).
proof: Proof. Proof with auto with typeclass_instances. intros x Gx. apply generic_format_abs_inv. apply generic_format_abs in Gx. revert rnd valid_rnd x Gx. refine (round_abs_abs _ (fun x y => generic_format fexp1 x -> generic_format fexp1 y) _). intros rnd valid_rnd x [Hx|Hx] Gx. generalize (mag_generic_gt _ x (Rgt_not_eq _ _ Hx) Gx). unfold cexp. destruct (mag beta x) as (ex,Ex) ; simpl. specialize (Ex (Rgt_not_eq _ _ Hx)). intros He'. rewrite Rabs_pos_eq in Ex by now apply Rlt_le. destruct (Zle_or_lt ex (fexp2 ex)) as [He|He]. destruct (round_bounded_small_pos fexp2 rnd x ex He Ex) as [Hr|Hr]. rewrite Hr. apply generic_format_0. rewrite Hr. apply generic_format_bpow'... apply Zlt_le_weak. apply valid_exp_large with ex... destruct (Zle_or_lt (cexp fexp2 x) (cexp fexp1 x)) as [He''|He'']. rewrite round_generic... rewrite Gx. apply generic_format_F2R. fold (round fexp1 Ztrunc x). intros Zx. unfold cexp at 1. rewrite mag_round_ZR... contradict Zx. apply eq_0_F2R with (1 := Zx). destruct (round_bounded_large_pos fexp2 rnd x ex He Ex) as (Hr1,[Hr2|Hr2]). apply generic_format_F2R. intros Zx. fold (round fexp2 rnd x). unfold cexp at 1. rewrite mag_unique_pos with (1 := conj Hr1 Hr2). rewrite <- mag_unique_pos with (1 := Ex). now apply Zlt_le_weak. rewrite Hr2. apply generic_format_bpow'... now apply Zlt_le_weak. rewrite <- Hx, round_0... apply generic_format_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop