proposition: Theorem Underf_Err1: forall (a' a:float), vNum b=vNum b' -> (dExp b <= dExp b')%Z -> (Fbounded b' a') -> (Closest b radix a' a) -> (Underf_Err a a' (FtoRradix a') (/2)%R).
proof: Proof. intros. unfold Underf_Err. split; auto. split; auto. case (Zle_or_lt (- dExp b)%Z (Fexp a')); intros. cut (FtoRradix a'=a);[intros H4|idtac]. rewrite H4; split; auto with real. ring_simplify (a-a)%R; rewrite Rabs_R0; apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b p (Closest b radix); auto. apply ClosestRoundedModeP with p; auto with zarith. elim H1; intros; split; auto. rewrite H; auto. split. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (powerRZ radix (- dExp b));[idtac|simpl; right; field; auto with real]. replace (a-a')%R with (-(a'-a))%R;[rewrite Rabs_Ropp|ring]. apply Rle_trans with (Fulp b radix p a). unfold FtoRradix; apply ClosestUlp; auto with zarith. unfold Fulp; apply Rle_powerRZ; try apply IZR_le; auto with real zarith. apply Z.le_trans with (Fexp (firstNormalPos radix b p));[idtac|unfold firstNormalPos; simpl; auto with zarith]. apply Fcanonic_Rle_Zle with radix b p; auto with zarith. apply FnormalizeCanonic; auto with zarith; elim H2; auto. left; apply firstNormalPosNormal; auto with zarith. rewrite (Rabs_right ((FtoR radix (firstNormalPos radix b p)))). rewrite FnormalizeCorrect; auto with zarith. apply RoundAbsMonotoner with b p (Closest b radix) (FtoRradix a'); auto. apply ClosestRoundedModeP with p; auto with zarith. assert (Fnormal radix b (firstNormalPos radix b p)); [apply firstNormalPosNormal; auto with zarith| elim H4; auto]. unfold FtoRradix; rewrite <- Fabs_correct; auto. unfold firstNormalPos, Fabs, FtoR; simpl. apply Rle_trans with (powerRZ radix p * powerRZ radix (Fexp a'))%R. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. elim H1; intros; apply Rle_trans with (IZR (Zpos (vNum b'))); auto with real zarith. apply IZR_le; auto with zarith. rewrite <- H; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. unfold nNormMin; rewrite Zpower_nat_Z_powerRZ. repeat rewrite <- powerRZ_add; try apply IZR_neq; auto with real zarith. apply Rle_powerRZ; try apply IZR_le; lia. apply Rle_ge; apply LeFnumZERO; auto. unfold firstNormalPos, nNormMin; simpl; auto with zarith. apply Zpower_NR0; lia. intros ; absurd (Fexp a' < - dExp b)%Z; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz