proposition: Theorem float_relative_inv_n : forall c p d x xi zi, ABS (rounding_float (Znearest c) p d x) xi -> float_relative_inv_n_helper p d xi zi = true -> REL (rounding_float (Znearest c) p d x) x zi.
proof: Proof. Proof with auto with typeclass_instances. intros c p d x xi zi Hx Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Flt2_correct _ _ H1). unfold float2R. simpl. rewrite F2R_bpow. clear H1. intro H1. generalize (Fle2_correct _ _ H2). unfold float2R. simpl. rewrite (F2R_Zopp _ 1%Z), F2R_bpow. clear H2. intro H2. generalize (Fle2_correct _ _ H3). unfold float2R. simpl. rewrite F2R_bpow. clear H3. intro H3. exists ((rounding_float (Znearest c) p d x - x) / x)%R. split. assert (Rabs ((rounding_float (Znearest c) p d x - x) / x) <= bpow radix2 (- Zpos p))%R. apply float_relative_inv_n_whole. apply Rlt_le_trans with (1 := H1). apply Hx. split. apply Rle_trans with (1 := H2). apply Ropp_le_cancel. rewrite Ropp_involutive. apply Rle_trans with (2 := H). rewrite <- Rabs_Ropp. apply Rabs_idem. apply Rle_trans with (2 := H3). apply Rle_trans with (2 := H). apply Rabs_idem. field. intros H. apply Rlt_not_le with (1 := H1). apply Rle_trans with (1 := proj1 (proj2 Hx)). rewrite H, round_0, Rabs_R0... apply bpow_ge_0. 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