proposition: Theorem float_absolute_wide_ne : forall p d x xi zi, ABS x xi -> float_absolute_wide_ne_helper p d xi zi = true -> BND (rounding_float rndNE p d x - x) zi.
proof: Proof. Proof with auto with typeclass_instances. intros p d x xi zi Hx Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H4). generalize (andb_prop _ _ Hb). clear Hb. intros (Hb,H3). generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Zle_bool_imp_le _ _ H1). clear H1. intro H1. generalize (Fle2_correct _ _ H2). unfold float2R. simpl. clear H2. intro H2. generalize (Fle2_correct _ _ H3). unfold float2R. simpl. rewrite (F2R_Zopp _ 1%Z), F2R_bpow. clear H3. intro H3. generalize (Fle2_correct _ _ H4). unfold float2R. simpl. rewrite F2R_bpow. clear H4. intro H4. set (e := (float_ulp p d (Fnum (upper xi)) (Fexp (upper xi)) - 2)%Z) in H2, H3, H4. cut (Rabs (rounding_float rndNE p d x - x) <= bpow radix2 e)%R. split. apply Rle_trans with (1 := H3). apply Ropp_le_cancel. rewrite Ropp_involutive. apply Rle_trans with (2 := H). rewrite <- Rabs_Ropp. apply Rabs_idem. apply Rle_trans with (2 := H4). apply Rle_trans with (2 := H). apply Rabs_idem. destruct Hx as (_,(_,Hx)). clear H3 H4 zi. induction (upper xi). induction Fnum ; simpl. assert (x = 0%R) as ->. rewrite float2_zero in Hx. apply Rabs_le_inv in Hx. apply Rle_antisym with (1 := proj2 Hx). now rewrite <- Ropp_0. rewrite round_0... rewrite Rminus_0_r. rewrite Rabs_R0. apply bpow_ge_0. simpl in e, H1. assert (H9: (e = Fexp + Zpos (digits p0) - Zpos p - 2)%Z). unfold e, FLT_exp. rewrite Zmax_inf_l. exact (refl_equal _). generalize (Zgt_pos_0 (digits p0)). lia. destruct (Rle_or_lt (bpow radix2 (Fexp + Zpos (digits p0) - 1)) (Rabs x)). rewrite float_absolute_ne_sym. replace (rounding_float rndNE p d (Rabs x)) with (bpow radix2 (Fexp + Zpos (digits p0) - 1)). rewrite Rabs_left1. rewrite Ropp_minus_distr. apply Rle_trans with (F2R (Float radix2 (Zpos (xI (shift_pos p 1))) e) - bpow radix2 (Fexp + Zpos (digits p0) - 1))%R. unfold Rminus. apply Rplus_le_compat_r. exact (Rle_trans _ _ _ Hx H2). rewrite H9. rewrite <- F2R_bpow. change (Float2 (Zpos (shift_pos p 1)~1) (Fexp + Zpos (digits p0) - Zpos p - 2) - Float2 1 (Fexp + Zpos (digits p0) - 1) <= bpow radix2 (Fexp + Zpos (digits p0) - Zpos p - 2))%R. rewrite <- Fminus2_correct. unfold Fminus2, Fshift2. simpl. clear H H9 H2 e H1 Hx xi x d. assert (Fexp + Zpos (digits p0) - Zpos p - 2 - (Fexp + Zpos (digits p0) - 1) = Zneg (p + 1))%Z as ->. rewrite <- Zneg_plus_distr. rewrite <- (Zopp_neg p). ring. assert (Zpos (xI (shift_pos p 1)) - Zpos (shift_pos (p + 1) 1) = 1)%Z as ->. rewrite Zpos_xI. rewrite 2!shift_pos_correct. rewrite Zpower_pos_is_exp. change (Z.pow_pos 2 1) with 2%Z. ring. unfold float2R. rewrite F2R_bpow. apply Rle_refl. apply Rplus_le_reg_r with (Rabs x). unfold Rminus. now rewrite Rplus_assoc, Rplus_opp_l, Rplus_0_r, Rplus_0_l. apply eq_sym, Rle_antisym. cut (bpow radix2 (Fexp + Zpos (digits p0) - 1) = Generic_fmt.round radix2 (FLT_exp d (Zpos p)) rndNE (F2R (Float radix2 (Zpos (xI (shift_pos p 1))) e)) :>R). intros ->. apply round_le... exact (Rle_trans _ _ _ Hx H2). change (F2R (Float radix2 (Zpos (shift_pos p 1)~1) e)) with (float2R (Float2 (Zpos (shift_pos p 1)~1) e)). rewrite <- (rndG_conversion roundNE_cs). unfold round, round_pos. simpl. cut (FLT_exp d (Zpos p) (e + Zpos (Pos.succ (digits (shift_pos p 1)))) = e + 2)%Z. intros ->. replace (e + 2 - e)%Z with 2%Z by ring. unfold shr, shr_aux, shift_pos. simpl. rewrite iter_nat_of_P. destruct (ZL4 p) as (p1,H3). rewrite H3. simpl. rewrite H9. replace (Fexp + Zpos (digits p0) - Zpos p - 2 + 2)%Z with (Fexp + Zpos (digits p0) - Zpos p)%Z by ring. destruct (Psucc_pred p) as [H4|H4]. rewrite H4. rewrite H4 in H3. injection H3. intro H5. rewrite <- H5. now rewrite <- F2R_bpow. rewrite <- F2R_bpow. change (F2R (Float radix2 1 (Fexp + Zpos (digits p0) - 1))) with (float2R (Float2 1 (Fexp + Zpos (digits p0) - 1))). rewrite <- (float2_shl_correct 1 (Fexp + Zpos (digits p0) - 1)%Z (Pos.pred p)). simpl. unfold shift_pos. rewrite iter_nat_of_P. rewrite <- H4 in H3. rewrite nat_of_P_succ_morphism in H3. injection H3. intro H5. rewrite H5. apply (f_equal (fun v => float2R (Float2 _ v))). rewrite <- H4 at 2. rewrite Zpos_succ_morphism. unfold Z.succ. ring. rewrite H9. rewrite Zpos_succ_morphism. rewrite (digits2_digits (shift_pos p 1)). rewrite shift_pos_correct, Zmult_1_r. change (Z.pow_pos 2 p) with (Zpower 2 (Zpos p)). rewrite Zdigits_Zpower by easy. unfold Z.succ. replace (Fexp + Zpos (digits p0) - Zpos p - 2 + (Zpos p + 1 + 1))%Z with (Fexp + Zpos (digits p0))%Z by ring. unfold FLT_exp. rewrite Zmax_inf_l. ring. generalize (Zgt_pos_0 (digits p0)). lia. rewrite <- (round_generic radix2 (FLT_exp d (Zpos p)) rndNE (bpow radix2 (Fexp + Zpos (digits p0) - 1))). apply round_le... apply generic_format_bpow. unfold FLT_exp. rewrite Zmax_inf_l. generalize (Zgt_pos_0 p). lia. generalize (Zgt_pos_0 (digits p0)). lia. replace e with (FLT_exp d (Zpos p) (Fexp + Zpos (digits p0) - 1) - 1)%Z. now apply float_absolute_n_whole. unfold e, FLT_exp. assert (H3 := Zgt_pos_0 (digits p0)). assert (H4 := Zgt_pos_0 p). repeat rewrite Zmax_inf_l ; lia. elim Rlt_not_le with (2 := Hx). apply Rlt_le_trans with (Float2 0 Fexp). now apply F2R_lt. unfold float2R. rewrite F2R_0. apply Rabs_pos. 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