proposition: Theorem Underf_Err3: forall (x x' y y' z' z:float) (rx ry epsx epsy:R), vNum b=vNum b' -> (dExp b <= dExp b')%Z -> (Underf_Err x x' rx epsx) -> (Underf_Err y y' ry epsy) -> (epsx+epsy <= (powerRZ radix (p-1) -1))%R -> (Fbounded b' z') -> (FtoRradix z'=x'-y')%R -> (Fexp z' <= Fexp x')%Z -> (Fexp z' <= Fexp y')%Z -> (Closest b radix (x-y) z) -> (Underf_Err z z' (x-y) (epsx+epsy)%R).
proof: Proof. intros. unfold Underf_Err. split; auto. split; auto. unfold Underf_Err in H1; unfold Underf_Err in H2. case (Zle_or_lt (- dExp b)%Z (Fexp z')); intros. elim H1; intros V1 T; elim T; intros V2 T'; elim T'; intros V3 V4; clear T T' H1. elim H2; intros W1 T; elim T; intros W2 T'; elim T'; intros W3 W4; clear T T' H2. cut (FtoRradix z=z')%R;[intros H9'; rewrite H9'; split; auto|idtac]. ring_simplify (z'-z')%R; rewrite Rabs_R0. apply Rle_trans with (0* powerRZ radix (- dExp b))%R;[right; ring|apply Rmult_le_compat_r; auto with real zarith]. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (0+0)%R; [right; ring|apply Rplus_le_compat; auto with real]. apply Rmult_le_reg_l with (powerRZ radix (- dExp b))%R; auto with real zarith; ring_simplify (powerRZ radix (- dExp b) * 0)%R; try rewrite Rmult_comm. apply powerRZ_lt, IZR_lt; lia. apply Rle_trans with (2:=V3); auto with real. apply Rabs_pos. apply Rmult_le_reg_l with (powerRZ radix (- dExp b))%R; auto with real zarith; ring_simplify (powerRZ radix (- dExp b) * 0)%R; try rewrite Rmult_comm. apply powerRZ_lt, IZR_lt; lia. apply Rle_trans with (2:=W3); auto with real. apply Rabs_pos. unfold FtoRradix; apply sym_eq. apply RoundedModeProjectorIdemEq with b p (Closest b radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. elim H4; intros; split; try lia. fold FtoRradix; rewrite H5. rewrite <- V4; auto with zarith. rewrite <- W4; auto with zarith real. elim H1; intros V1 T; elim T; intros V2 T'; elim T'; intros V3 V4; clear T T' H1. elim H2; intros W1 T; elim T; intros W2 T'; elim T'; intros W3 W4; clear T T' H2. split;[idtac|intros; absurd (- dExp b <= Fexp z')%Z; auto with zarith]. replace (z-z')%R with (-((x-y)-z)+((x-x')+-(y-y')))%R;[idtac|rewrite H5; ring]. apply Rle_trans with (1:=Rabs_triang (- (x - y - z))%R ((x - x') + - (y - y'))%R). apply Rle_trans with ((Rabs (- (x - y - z))) + (Rabs (x - x') +(Rabs (- (y - y')))))%R; [apply Rplus_le_compat_l; apply Rabs_triang|idtac]. rewrite Rabs_Ropp; rewrite Rabs_Ropp. apply Rle_trans with (0 + ( epsx * powerRZ radix (- dExp b) + epsy * powerRZ radix (- dExp b)))%R;[idtac|right; ring]. apply Rplus_le_compat;[idtac|apply Rplus_le_compat; auto with real]. cut (FtoRradix (Fnormalize radix b p z)=x-y)%R. unfold FtoRradix; rewrite FnormalizeCorrect; auto. fold FtoRradix; intros T; rewrite T; ring_simplify (x - y - (x - y))%R; rewrite Rabs_R0; auto with real. unfold FtoRradix, Rminus; rewrite <- Fopp_correct; auto. apply plusExact1 with b p; auto. elim V1; auto. apply oppBounded; elim W1; auto. rewrite Fopp_correct; auto with real. apply ClosestCompatible with (1:=H8); auto. rewrite FnormalizeCorrect; auto with real. apply FnormalizeBounded; auto with zarith; elim H8; auto. apply Z.le_trans with (-(dExp b))%Z. 2: apply Zmin_Zle. 2: elim V1; intros T1 T2; elim T1; auto. 2: elim W1; intros T1 T2; elim T1; auto. apply Z.le_trans with (Fexp (Float (pPred (vNum b)) (-(dExp b))%Z)); [idtac| simpl; auto with zarith]. apply Fcanonic_Rle_Zle with radix b p; auto with zarith. apply FnormalizeCanonic; auto with zarith; elim H8; auto. apply FcanonicPpred with p; auto with zarith. rewrite (Rabs_right ((FtoR radix (Float (pPred (vNum b)) (- dExp b))))). rewrite FnormalizeCorrect; auto with zarith. apply RoundAbsMonotoner with b p (Closest b radix) (x-y)%R; auto. apply ClosestRoundedModeP with p; auto with zarith. assert (Fcanonic radix b (Float (pPred (vNum b)) (- dExp b))); [apply FcanonicPpred with p; auto with zarith | apply FcanonicBound with radix; auto]. replace (x-y)%R with ((x-x')+-(y-y')+z')%R;[idtac|rewrite H5; ring]. apply Rle_trans with (1:=Rabs_triang (x - x' + - (y - y'))%R z'). apply Rle_trans with ((powerRZ radix (p - 1) - 1)*powerRZ radix (-(dExp b)) + (powerRZ radix p - 1)*powerRZ radix (-(dExp b)-1))%R;[apply Rplus_le_compat|idtac]. apply Rle_trans with (1:=Rabs_triang (x-x')%R (-(y-y'))%R); rewrite Rabs_Ropp. apply Rle_trans with (epsx * powerRZ radix (- dExp b)+ epsy * powerRZ radix (- dExp b))%R; auto with real. apply Rle_trans with ((epsx+epsy) * powerRZ radix (- dExp b))%R;[right; ring|idtac]. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. unfold FtoRradix; rewrite <- Fabs_correct; auto. unfold Fabs, FtoR; simpl. apply Rmult_le_compat; auto with real zarith. apply IZR_le; auto with zarith. apply powerRZ_le, IZR_lt; lia. elim H4; intros. apply Rle_trans with (IZR (Z.pred (Zpos (vNum b')))); auto with real zarith. apply IZR_le; lia. unfold Z.pred, Zminus; rewrite plus_IZR. rewrite <- H; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. apply Rle_powerRZ; try apply IZR_le; auto with real zarith. apply Rle_trans with ((powerRZ radix p - 1) * powerRZ radix (- dExp b))%R. apply Rle_trans with (- powerRZ radix (- dExp b)+powerRZ radix p * powerRZ radix (- dExp b))%R;[idtac|right; ring]. apply Rle_trans with (- powerRZ radix (- dExp b)+ ((powerRZ radix (p - 1)* powerRZ radix (- dExp b)+ (powerRZ radix p*powerRZ radix (- dExp b - 1) - powerRZ radix (- dExp b - 1)))))%R; [right; ring|apply Rplus_le_compat_l]. repeat rewrite <- powerRZ_add; try apply IZR_neq; auto with real zarith. replace ((p + (- dExp b - 1)))%Z with (p - 1 + - dExp b)%Z;[idtac|ring]. apply Rle_trans with (powerRZ radix (p - 1 + - dExp b) + (powerRZ radix (p - 1 + - dExp b) - 0))%R; auto with real zarith. apply Rplus_le_compat_l; unfold Rminus; apply Rplus_le_compat_l; auto with real zarith. apply Ropp_le_contravar. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (2*(powerRZ radix (p - 1 + - dExp b)))%R;[right; ring|idtac]. apply Rle_trans with (radix*(powerRZ radix (p - 1 + - dExp b)))%R; [apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; lia. apply IZR_le; lia. unfold Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; right; field; auto with real zarith. apply IZR_neq; lia. unfold FtoR; simpl. unfold pPred, Z.pred, Zminus; rewrite plus_IZR. rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; simpl; auto with real zarith. apply Rle_ge; apply LeFnumZERO; auto. simpl; apply Zlt_le_weak. apply pPredMoreThanOne with radix p; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz