proposition: Lemma RleRoundedAbs: forall (f:float) (r:R), (Closest bo radix r f) -> (Fnormal radix bo f) -> (-(dExp bo) < Fexp f)%Z -> ((powerRZ radix (p - 1) + - / (2 * radix)) * powerRZ radix (Fexp f) <= Rabs r)%R.
proof: Proof. intros f r H H0 H'0. assert (exists f':float, f'=(Float (nNormMin radix p) (Fexp f))). exists (Float (nNormMin radix p) (Fexp f)); auto. elim H1; clear H1; intros f' H1. assert (Fbounded bo f'). rewrite H1; split; simpl; auto with zarith. rewrite Z.abs_eq. apply ZltNormMinVnum; auto with zarith. apply Zlt_le_weak; apply nNormPos; auto with zarith. assert (Fnormal radix bo f'). split; auto. rewrite H1; simpl; rewrite <- PosNormMin with radix bo p; auto with zarith. assert (f' <= Fabs f)%R. rewrite H1; unfold FtoRradix, FtoR; simpl. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. assert (nNormMin radix p <= Z.abs (Fnum f))%Z; try apply IZR_le; auto with real zarith. apply pNormal_absolu_min with bo; auto with zarith. apply Rle_trans with (f'-powerRZ radix (Z.pred (Fexp f))/2)%R. right; rewrite H1; unfold FtoRradix, FtoR, Z.pred, Zminus; simpl. rewrite powerRZ_add with (n:=Fexp f); try apply IZR_neq; auto with real zarith; simpl; ring_simplify (radix*1)%R. replace (IZR (nNormMin radix p)) with (powerRZ radix (p + -1)). field; try apply IZR_neq; auto with real zarith. unfold nNormMin; rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with real zarith. case (Rle_or_lt (f' - powerRZ radix (Z.pred (Fexp f)) / 2) (Rabs r)); auto; intros I. absurd (Rabs (Fabs f - Rabs r) <= Rabs ((FPred bo radix p f') - Rabs r))%R. 2: assert (K: (Closest bo radix (Rabs r) (Fabs f))). 2: apply ClosestFabs with p; auto with zarith. 2: elim K; intros K1 K2; unfold FtoRradix; apply K2; auto. 2: apply FBoundedPred; auto with zarith. apply Rlt_not_le. rewrite Rabs_left1. rewrite Rabs_right with (Fabs f - Rabs r)%R. apply Rplus_lt_reg_r with (Rabs r+(FPred bo radix p f'))%R. ring_simplify. apply Rlt_le_trans with (2*(f' - powerRZ radix (Z.pred (Fexp f)) / 2))%R. apply Rmult_lt_compat_l; auto with real. apply Rle_trans with (f'+ FPred bo radix p f')%R; auto with real. apply Rle_trans with (2*f'- powerRZ radix (Z.pred (Fexp f)))%R; [right; field; auto with real|idtac]. apply Rplus_le_reg_l with (-f'- FPred bo radix p f'+ powerRZ radix (Z.pred (Fexp f)))%R. ring_simplify. right; apply trans_eq with (FtoRradix (Fminus radix f' (FPred bo radix p f'))). unfold FtoRradix; rewrite Fminus_correct; auto with real zarith. unfold FtoRradix; rewrite FPredDiff3; auto with zarith. rewrite H1; simpl; unfold FtoR; simpl; ring. rewrite H1; auto. rewrite H1; simpl; auto with zarith. rewrite Rplus_comm; auto with real. apply Rle_ge. assert (Rabs r < Fabs f)%R; auto with real. apply Rlt_le_trans with (1:=I). apply Rle_trans with (Fabs f-0)%R; auto with real; unfold Rminus; apply Rplus_le_compat; auto with real zarith. apply Ropp_le_contravar; unfold Rdiv; apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. left; apply Rlt_Rminus; auto. assert ((FPred bo radix p f' <= Rabs r))%R; auto with real. 2: apply Rle_trans with (Rabs r-Rabs r)%R; unfold Rminus; auto with real. case (Rle_or_lt (FPred bo radix p f') (Rabs r)); auto; intros I'. absurd (FPred bo radix p f' < f')%R. 2: unfold FtoRradix; apply FPredLt; auto with zarith. apply Rle_not_lt. apply Rle_trans with (1:=H4). unfold FtoRradix; rewrite Fabs_correct; auto. apply RoundAbsMonotoner with bo p (Closest bo radix) r; auto with zarith real. apply ClosestRoundedModeP with p; auto with zarith. apply FBoundedPred; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz