proposition: Theorem float_enforce : forall rdir {Hrnd : Valid_rnd rdir} p d x xi zi, BND (rounding_float rdir p d x) xi -> enforce_helper (FLT_exp d (Zpos p)) xi zi = true -> BND (rounding_float rdir p d x) zi.
proof: Proof. Proof with auto with typeclass_instances. intros rdir Hrnd p d x xi zi Hx Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fle2_correct _ _ H1). rewrite (rndG_conversion roundUP_cs). clear H1. intro H1. generalize (Fle2_correct _ _ H2). rewrite (rndG_conversion roundDN_cs). clear H2. intro H2. revert Hx. intros (Hx1, Hx2). split. apply Rle_trans with (1 := H1). rewrite <- (round_generic _ _ rndUP _ (generic_format_round radix2 (FLT_exp d (Zpos p)) rdir x)). apply round_le... apply Rle_trans with (2 := H2). rewrite <- (round_generic _ _ rndDN _ (generic_format_round radix2 (FLT_exp d (Zpos p)) rdir x)). apply round_le... 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