proposition: Theorem tBounded_aux: exists v:float, Fbounded bo v /\ (FtoRradix v=uh-z)%R.
proof: Proof. case (Req_dec (ph+b)%R 0);intros H1. exists (Fopp z); split. apply oppBounded; elim zDef; auto. unfold FtoRradix; rewrite Fopp_correct; replace (FtoR radix uh) with 0%R;[ring|idtac]. apply trans_eq with (FtoR radix (Fzero (-(dExp bo)))). rewrite FzeroisReallyZero; auto. apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply FboundedFzero. rewrite FzeroisReallyZero; rewrite <- H1; auto. case (Rle_or_lt (Rabs pl) (/4*Rabs (ph+b))); intros H2. exists (Fminus radix uh z). split;[idtac|unfold FtoRradix; apply Fminus_correct; auto]. apply Sterbenz; auto. elim uhDef; auto. elim zDef; auto. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (FtoR radix z);[right; simpl; field; auto with real|idtac]. rewrite <- (Rabs_right (FtoR radix z)). 2: apply Rle_ge; generalize zPos; auto with real. apply Rle_trans with (Rabs (a*x+b) / (1 - powerRZ radix (Z.succ (- p)) / 2))%R. apply ClosestRoundeLeNormal with bo; auto with zarith. assert (0 < 1 - powerRZ radix (Z.succ (- p)) / 2)%R. apply UnMoinsPos; auto with zarith. apply Rmult_le_reg_l with (1 - powerRZ radix (Z.succ (- p)) / 2)%R; auto with real. apply Rle_trans with (Rabs (a*x+b));[right; field; auto with real|idtac]. assert (0 < 2 - powerRZ radix (Z.succ (- p)))%R; auto with real. replace (2 - powerRZ radix (Z.succ (- p)))%R with (2*(1 - powerRZ radix (Z.succ (- p)) / 2))%R; auto with real. replace 0%R with (2*0)%R; auto with real. field; auto with real. replace (a*x+b)%R with ((ph+b)+pl)%R;[idtac|rewrite plDef; ring]. apply Rle_trans with (Rabs (ph+b)+Rabs pl)%R;[apply Rabs_triang|idtac]. apply Rle_trans with (Rabs (ph+b)+/ 4 * Rabs (ph + b))%R;auto with real. assert (0 < 4)%R;[apply Rmult_lt_0_compat; auto with real|idtac]. apply Rle_trans with (5/4*(Rabs (ph+b)))%R;[right; field; auto with real|idtac]. apply Rle_trans with (5/4*(Rabs (FtoR radix uh) * (1 + powerRZ radix (Z.succ (- p)) / 2)))%R. apply Rmult_le_compat_l. apply Rlt_le; unfold Rdiv;apply Rmult_lt_0_compat; auto with real. apply ClosestRoundeGeNormal with bo; auto with zarith. fold FtoRradix; apply Rle_trans with ((5/4*(1 + powerRZ radix (Z.succ (- p)) / 2))*Rabs uh)%R; [right; ring|idtac]. rewrite <- Rmult_assoc with (r3:=uh). pattern (FtoRradix uh) at 2; rewrite <- (Rabs_right uh). 2: apply Rle_ge; generalize uhPos; auto with real. apply Rmult_le_compat_r; auto with real. apply Rabs_pos. apply Rmult_le_reg_l with 8%R; [apply Rmult_lt_0_compat; auto with real|idtac]. apply Rle_trans with (10+5*powerRZ radix (Z.succ (- p)))%R;[right; field; auto with real|idtac]. apply Rle_trans with (16-8*powerRZ radix (Z.succ (- p)))%R;[idtac|right; field; auto with real]. apply Rplus_le_reg_l with (-10+8* powerRZ radix (Z.succ (- p)))%R. ring_simplify. apply Rle_trans with (13* /4)%R. apply Rmult_le_compat_l; auto with real. apply Rle_trans with (powerRZ radix (Z.succ (- 3))); unfold Z.succ; auto with zarith real. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. simpl; ring_simplify (radix*1)%R. apply Rle_Rinv; auto with real. rewrite <- mult_IZR; apply IZR_le. apply Z.le_trans with (2*2)%Z. auto with zarith. apply Zmult_le_compat; auto with zarith. apply Rmult_le_reg_l with 4%R; auto with real. apply Rle_trans with 13%R;[right; field; auto with real|idtac]. apply Rle_trans with 24%R; auto with real zarith. right; ring. simpl; fold FtoRradix. rewrite <- (Rabs_right z);[idtac|apply Rle_ge; generalize zPos; auto with real]. rewrite <- (Rabs_right uh);[idtac|apply Rle_ge; generalize uhPos; auto with real]. assert (0 < 1 - powerRZ radix (Z.succ (- p)) / 2)%R. apply UnMoinsPos; auto with zarith. assert (0 < 4)%R;[apply Rmult_lt_0_compat; auto with real|idtac]. assert (0 < 3)%R;[apply Rlt_trans with 2%R; auto with real|idtac]. apply Rle_trans with (Rabs (ph+b) / (1 - powerRZ radix (Z.succ (- p)) / 2))%R. unfold FtoRradix; apply ClosestRoundeLeNormal with bo; auto with zarith. apply Rmult_le_reg_l with (1 - powerRZ radix (Z.succ (- p)) / 2)%R; auto with real. apply Rle_trans with (Rabs (ph+b));[right; field; auto with real|idtac]. replace (2 - powerRZ radix (Z.succ (- p)))%R with (2* (1 - powerRZ radix (Z.succ (- p)) / 2))%R;[idtac|field]. apply prod_neq_R0; auto with real. apply Rle_trans with ((4/3)*(Rabs (a*x+b)))%R. apply Rmult_le_reg_l with (3/4)%R. unfold Rdiv; apply Rmult_lt_0_compat; auto with real. apply Rplus_le_reg_l with (/4*Rabs (ph + b))%R. apply Rle_trans with (Rabs (ph+b));[right; field; auto with real|idtac]. apply Rle_trans with (/4*Rabs (ph+b)+Rabs (a*x+b))%R;[idtac|right; field; auto with real]. pattern (ph+b)%R at 1; replace (ph+b)%R with (-(pl)+(a*x+b))%R;[idtac|rewrite plDef; ring]. apply Rle_trans with (Rabs (-pl)+Rabs (a*x+b))%R; [apply Rabs_triang|rewrite Rabs_Ropp; auto with real]. apply Rle_trans with (4/3*(Rabs z * (1 + powerRZ radix (Z.succ (- p)) / 2)))%R. apply Rmult_le_compat_l; auto with real. apply Rlt_le; unfold Rdiv; apply Rmult_lt_0_compat; auto with real. unfold FtoRradix; apply ClosestRoundeGeNormal with bo; auto with zarith. apply Rle_trans with ((4 / 3 * (1 + powerRZ radix (Z.succ (- p)) / 2))*(Rabs z))%R; [right; ring|idtac]. rewrite <- Rmult_assoc with (r3:=Rabs z). apply Rmult_le_compat_r; auto with real. apply Rabs_pos. apply Rmult_le_reg_l with 6%R; [apply Rmult_lt_0_compat; auto with real|idtac]. apply Rle_trans with (8+4*powerRZ radix (Z.succ (- p)))%R;[right; field; auto with real|idtac]. apply Rle_trans with (12-6*powerRZ radix (Z.succ (- p)))%R;[idtac|right; field; auto with real]. apply Rplus_le_reg_l with (-8+6* powerRZ radix (Z.succ (- p)))%R. ring_simplify. apply Rle_trans with (10* /4)%R. apply Rmult_le_compat_l; auto with real. apply Rle_trans with (powerRZ radix (Z.succ (- 3))); unfold Z.succ; auto with zarith real. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. simpl; ring_simplify (radix*1)%R; auto with real zarith. apply Rle_Rinv; auto with real. rewrite <- mult_IZR; apply IZR_le. apply Z.le_trans with (2*2)%Z. auto with zarith. apply Zmult_le_compat; auto with zarith. apply Rmult_le_reg_l with 4%R; auto with real. apply Rle_trans with 10%R;[right; field; auto with real|idtac]. apply Rle_trans with 16%R; auto with real zarith. right; ring. assert (K:(Fexp a+Fexp x < Fexp ph)%Z). elim errorBoundedMult with bo radix p (Closest bo radix) a x ph; auto with zarith. 2: apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; intros pl' T; elim T; intros H3 T'; elim T'; intros H4 H5; clear T T'. rewrite <- H5. apply ClosestErrorExpStrict with bo radix p (a*x)%R; auto with zarith. elim phDef; auto. fold FtoRradix; contradict H2. apply Rle_not_lt; rewrite plDef; rewrite <- H3; rewrite H2. rewrite Rabs_R0; apply Rle_trans with (/4*0)%R; auto with real. apply Rmult_le_compat_l; auto with real. apply Rabs_pos. assert (K':(-dExp bo < Fexp ph)%Z); auto with zarith. assert (Rabs (ph+b) < 2* powerRZ radix (Fexp ph))%R. apply Rmult_lt_reg_l with (/4)%R; auto with real. assert (0 < 4)%R; auto with real. apply Rlt_le_trans with (1:=H2). apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (Fulp bo radix p ph). rewrite plDef; unfold FtoRradix; apply ClosestUlp; auto with zarith. rewrite CanonicFulp; auto with zarith. unfold FtoR; right; simpl; field; auto with real. left; auto. assert (Fexp ph -1 <= Fexp b)%Z. apply Z.le_trans with (Fexp (Float (Zpos (vNum bo)-2*radix) (Fexp ph -1))); [simpl; auto with zarith|idtac]. assert (0 < Zpos (vNum bo)-2*radix )%Z. assert (2*radix < Zpos (vNum bo))%Z; auto with zarith. rewrite pGivesBound; apply Z.le_lt_trans with (Zpower_nat radix 2); auto with zarith. unfold Zpower_nat; simpl (nat_rect _ _ _ _). ring_simplify (radix*1)%Z; apply Zmult_le_compat_r; auto with zarith. apply Zpower_nat_monotone_lt; lia. apply Fcanonic_Rle_Zle with radix bo p; auto with zarith. left; split;[split|idtac]; auto with zarith. unfold Fnum. apply Z.le_lt_trans with (Z.abs (Zpos (vNum bo) - 2 * radix)); lia. simpl; lia. apply Z.le_trans with (Z.abs (radix * (Zpos (vNum bo) - 2 * radix))); auto with zarith. rewrite Zabs_Zmult; repeat rewrite Z.abs_eq; auto with zarith. apply Z.le_trans with (2* (Zpos (vNum bo) - 2 * radix))%Z; auto with zarith. apply Zplus_le_reg_l with (4*radix)%Z. apply Z.le_trans with (Zpos (vNum bo)+ Zpos (vNum bo))%Z; auto with zarith. assert (4*radix <= Zpos (vNum bo))%Z; auto with zarith. rewrite pGivesBound; apply Z.le_trans with (Zpower_nat radix 3); auto with zarith. unfold Zpower_nat; simpl (nat_rect _ _ _ _). ring_simplify (radix*1)%Z; rewrite Zmult_assoc; apply Zmult_le_compat_r. apply Z.le_trans with (2*radix)%Z; auto with zarith; lia. lia. apply Zpower_nat_monotone_le; lia. fold FtoRradix; apply Rplus_le_reg_l with (2*powerRZ radix (Fexp ph))%R. apply Rle_trans with (Rabs (ph + b)+Rabs b)%R; auto with real. apply Rle_trans with (Rabs ph). 2: pattern (FtoRradix ph) at 1; replace (FtoRradix ph) with ((ph+b)+-b)%R;[idtac|ring]. 2:apply Rle_trans with (Rabs (ph + b) + Rabs (-b))%R; [apply Rabs_triang| rewrite Rabs_Ropp; auto with real]. unfold FtoRradix; repeat rewrite <- Fabs_correct; auto. unfold FtoR, Fabs. simpl (Fexp (Float (Zpos (vNum bo) - 2 * radix) (Fexp ph - 1))). simpl (Fexp (Float (Z.abs (Fnum (Float (Zpos (vNum bo) - 2 * radix) (Fexp ph - 1)))) (Fexp ph - 1))). replace (Fnum (Float (Z.abs (Fnum (Float (Zpos (vNum bo) - 2 * radix) (Fexp ph - 1)))) (Fexp ph - 1))) with (Z.abs (Zpos (vNum bo) - 2 * radix)); auto with zarith. simpl (Fnum (Float (Z.abs (Fnum ph)) (Fexp ph))). simpl (Fexp (Float (Z.abs (Fnum ph)) (Fexp ph))). apply Rle_trans with ((2+ ( Z.abs (Zpos (vNum bo) - 2 * radix))/radix)*powerRZ radix (Fexp ph))%R. unfold Zminus; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; ring_simplify (radix*1)%R. right; field; auto with real zarith. apply IZR_neq; auto with zarith. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rmult_le_reg_l with radix; auto with real zarith. apply IZR_lt; lia. apply Rle_trans with (IZR (Zpos (vNum bo))). rewrite Z.abs_eq; auto with zarith. unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; rewrite mult_IZR. right; simpl; field; try apply IZR_neq; auto with real zarith. elim Nph; intros. apply Rle_trans with (IZR (Z.abs (radix * Fnum ph))); auto with real zarith. apply IZR_le; auto. right; rewrite Zabs_Zmult; rewrite mult_IZR; rewrite Z.abs_eq; auto with zarith real. assert (exists uh':float, (FtoRradix uh'=ph+b)%R /\ (Fbounded bo uh') /\ (Fexp uh'=Fexp ph-1)%Z). unfold FtoRradix; apply BoundedL with p (Fplus radix ph b); auto with zarith. simpl; apply Zmin_Zle; auto with zarith. apply Fplus_correct; auto with zarith. fold FtoRradix; apply Rlt_le_trans with (1:=H). apply Rle_trans with (powerRZ radix (Fexp ph+1)); [rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl|apply Rle_powerRZ; auto with real zarith]. 2: apply IZR_le; lia. ring_simplify (radix*1)%R; rewrite Rmult_comm; apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply IZR_le; lia. elim H3; clear H3; intros uh' T; elim T; intros H5 T'; elim T'; intros H6 H7; clear T T'. assert (FtoRradix uh=uh'). unfold FtoRradix; apply sym_eq. apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; rewrite H5; auto. elim errorBoundedMult with bo radix p (Closest bo radix) a x ph; auto with zarith. 2: apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; intros pl' T; elim T; intros H8 T'; elim T'; intros H9 H10; clear T T'. elim LeExpRound2 with bo radix p (Fexp a+Fexp x)%Z (Fplus radix (Fplus radix ph pl') b) z; auto with zarith. 2: rewrite Fplus_correct; auto with zarith;rewrite Fplus_correct; auto with zarith. 2: fold FtoRradix; rewrite H8. 2: ring_simplify (ph + (a * x - ph) + b)%R; auto with real. 2: simpl; apply Zmin_Zle; lia. fold FtoRradix; intros z' T; elim T; intros H15 T'; elim T'; intros H16 H17; clear T T'. cut ( exists v : float, (FtoRradix v = uh - z)%R /\ Fbounded bo v /\ (Fexp v=Fexp a+Fexp x)%Z). intros T; elim T; intros v T1; elim T1; intros T2 T3; elim T3; intros; exists v; split; auto. unfold FtoRradix; apply BoundedL with p (Fminus radix uh' z'); auto with zarith. simpl; apply Zmin_Zle; auto with zarith. rewrite Fminus_correct; auto with zarith; fold FtoRradix; rewrite <- H3; rewrite H16; auto with real. apply Rlt_le_trans with (powerRZ radix (Fexp ph)); [idtac|apply Rle_powerRZ; auto with real zarith]. fold FtoRradix; rewrite H3; rewrite H5. replace (ph+b-z)%R with ((a*x+b-z)+-pl)%R;[idtac|rewrite plDef; ring]. apply Rle_lt_trans with (Rabs (a*x+b-z)+Rabs (-pl))%R;[apply Rabs_triang|rewrite Rabs_Ropp]. apply Rmult_lt_reg_l with 2%R; auto with real zarith. apply Rle_lt_trans with (2 * Rabs (a * x + b - z) + S 1*Rabs pl)%R;[right; ring|idtac]. apply Rlt_le_trans with (powerRZ radix (Fexp ph)+powerRZ radix (Fexp ph))%R; [idtac|simpl;right; ring]. cut (2 * Rabs (a * x + b - z) < powerRZ radix (Fexp ph))%R;[intros I1|idtac]. cut (2 * Rabs (pl) <= powerRZ radix (Fexp ph))%R;[intros I2; auto with real|idtac]. apply Rle_trans with (Fulp bo radix p ph). rewrite plDef; unfold FtoRradix; apply ClosestUlp; auto with zarith. rewrite CanonicFulp; auto with zarith real. right; unfold FtoR; simpl; ring. left; auto. apply Rle_lt_trans with (Fulp bo radix p z). unfold FtoRradix; apply ClosestUlp; auto with zarith. rewrite CanonicFulp; auto with zarith real. 2: left; auto. 2: apply IZR_le; lia. unfold FtoR; simpl; ring_simplify (1*powerRZ radix (Fexp z))%R. apply Rlt_powerRZ; auto with real zarith. apply IZR_lt; lia. apply Z.le_lt_trans with (Fexp ph-1)%Z; auto with zarith. assert (Fbounded bo (Float (3*radix) (Fexp ph-1))). split; [idtac|simpl; auto with zarith]. apply Z.le_lt_trans with (Z.abs (3*radix)); auto with zarith. rewrite Zabs_Zmult; repeat rewrite Z.abs_eq; auto with zarith. rewrite pGivesBound; apply Z.lt_le_trans with (Zpower_nat radix 3); auto with zarith. unfold Zpower_nat; simpl (nat_rect _ _ _ _)%Z. rewrite Zmult_comm; ring_simplify (radix*1)%Z; apply Zmult_lt_compat_l. auto with zarith. apply Z.lt_le_trans with (2*2)%Z. auto with zarith. apply Z.le_trans with (2*radix)%Z; auto with zarith. apply Zpower_nat_monotone_le; lia. apply Z.le_trans with (Fexp (Float (3*radix) (Fexp ph-1))); auto with zarith. apply Z.le_trans with (Fexp (Fnormalize radix bo p (Float (3*radix) (Fexp ph-1)))). apply Fcanonic_Rle_Zle with radix bo p; auto with zarith. left; auto. apply FnormalizeCanonic; auto with zarith. rewrite FnormalizeCorrect; auto. apply Rle_trans with (FtoR radix (Float (3 * radix) (Fexp ph - 1))); [idtac|rewrite <- Fabs_correct; auto; unfold FtoR]. 2: simpl; rewrite Z.abs_eq; auto with zarith real. 2: apply Z.le_trans with (3*radix)%Z; auto with zarith. apply RoundAbsMonotoner with bo p (Closest bo radix) (a*x+b)%R; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. replace (a*x+b)%R with ((ph+b)+pl)%R;[idtac|rewrite plDef; ring]. apply Rle_trans with (Rabs (ph+b)+Rabs pl)%R;[apply Rabs_triang|idtac]. apply Rle_trans with (2 * powerRZ radix (Fexp ph)+/2*powerRZ radix (Fexp ph))%R; [apply Rplus_le_compat; auto with real|idtac]. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (Fulp bo radix p ph). rewrite plDef; unfold FtoRradix; apply ClosestUlp; auto with zarith. rewrite CanonicFulp; auto with zarith. unfold FtoR; right; simpl; field; auto with real. left; auto. apply Rle_trans with ((2+/2)*powerRZ radix (Fexp ph))%R;[right; ring|idtac]. apply Rle_trans with (3*powerRZ radix (Fexp ph))%R; [idtac|right; unfold FtoR; simpl; unfold Zminus; rewrite powerRZ_add; auto with real zarith]. 2: simpl; ring_simplify (radix*1)%R. 2: replace (IZR (match radix with | Z0 => 0%Z | Zpos y' => Zpos ((y' + xO y')) | Zneg y' => Zneg ((y' + xO y')) end)) with (3*radix)%R;[field; auto with real zarith|idtac]. 2: apply IZR_neq; lia. 2: apply trans_eq with (IZR (3*radix)); auto with real zarith; rewrite mult_IZR; simpl; ring. 2: apply IZR_neq; lia. apply Rmult_le_compat_r. apply powerRZ_le, IZR_lt; lia. lra. apply FcanonicLeastExp with radix bo p; auto with zarith. rewrite FnormalizeCorrect; auto with real zarith. apply FnormalizeCanonic; auto with zarith. assert (0 < pPred (vNum bo))%Z. apply pPredMoreThanOne with radix p; auto with zarith. assert (Fbounded bo (Float (pPred (vNum bo)) (Fexp a+Fexp x+p))). split; simpl; auto with zarith. rewrite Z.abs_eq;[unfold pPred|idtac]; auto with zarith. apply Z.le_trans with (Fexp (Float (pPred (vNum bo)) (Fexp a+Fexp x+p))); auto with zarith. apply Fcanonic_Rle_Zle with radix bo p; auto with zarith. left; auto. left; split; auto. simpl; rewrite Zabs_Zmult; repeat rewrite Z.abs_eq; auto with zarith. apply Z.le_trans with (2* pPred (vNum bo))%Z; auto with zarith. unfold pPred, Z.pred; apply Zplus_le_reg_l with 2%Z. apply Z.le_trans with (Zpos (vNum bo) + Zpos (vNum bo))%Z; auto with zarith. assert (2 <= Zpos (vNum bo))%Z; auto with zarith. rewrite pGivesBound; apply Z.le_trans with (Zpower_nat radix 1); auto with zarith. unfold Zpower_nat; simpl; auto with zarith. apply Zpower_nat_monotone_le; lia. apply Rle_trans with (FtoR radix (Float (pPred (vNum bo)) (Fexp a + Fexp x + p))). 2: right; rewrite <- Fabs_correct; auto; unfold FtoR; simpl; rewrite Z.abs_eq; auto with real zarith. apply RoundAbsMonotoner with bo p (Closest bo radix) (a*x)%R; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. rewrite Rabs_mult; unfold FtoRradix; repeat rewrite <- Fabs_correct; auto. unfold FtoR; simpl; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. apply Rle_trans with (Z.abs (Fnum a) * (powerRZ radix (Fexp a) * powerRZ radix (Fexp x) * Z.abs (Fnum x)))%R;[right; ring|idtac]. apply Rmult_le_compat; auto with real zarith. apply IZR_le; auto with zarith. apply Rle_trans with (0*Z.abs (Fnum x))%R; auto with real. apply Rmult_le_compat_r; auto with real zarith. apply IZR_le; auto with zarith. apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith; apply powerRZ_lt, IZR_lt; lia. elim Fa; intros; unfold pPred; apply IZR_le; auto with real zarith. apply Rmult_le_compat_l; auto with real zarith. apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith; apply powerRZ_lt, IZR_lt; lia. apply Rle_trans with (IZR (Zpos (vNum bo))). apply IZR_le; elim Fx; intros; lia. rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz