proposition: Theorem RoundedModeUlp : forall P, RoundedModeP b radix P -> forall (p : R) (q : float), P p q -> (Rabs (p - q) < Fulp q)%R.
proof: Proof. intros P H' p q H'0. case (Req_dec p q); intros Eq1. rewrite <- Eq1. replace (p - p)%R with 0%R; [ idtac | ring ]. rewrite Rabs_R0; auto. unfold Fulp, FtoRradix, FtoR in |- *; simpl in |- *; auto with real arith. apply powerRZ_lt, IZR_lt; auto with zarith. case H'. intros H'1 H'2; elim H'2; intros H'3 H'4; elim H'4; intros H'5 H'6; case H'5 with (1 := H'0); clear H'5 H'4 H'2; intros H'5. rewrite Rabs_right; auto. cut (Fbounded b q); [ intros B0 | case H'5; auto ]. apply Rlt_le_trans with (2 := FulpSuc q B0). apply Rplus_lt_reg_l with (r := FtoR radix q). repeat rewrite Rplus_minus; auto. case (Rle_or_lt (FNSucc b radix precision q) p); auto. intros H'2; absurd (FNSucc b radix precision q <= q)%R; auto. apply Rgt_not_le; red in |- *; unfold FtoRradix in |- *; auto with real arith. apply FNSuccLt; auto with zarith. case H'5; auto. intros H'4 H'7; elim H'7; intros H'8 H'9; apply H'9; clear H'7; auto. apply (FcanonicBound radix b); auto with zarith. apply FNSuccCanonic; auto with zarith. apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix q). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; apply isMin_inv1 with (1 := H'5); auto. rewrite Rabs_left1; auto. rewrite Ropp_minus_distr; auto. cut (Fbounded b q); [ intros B0 | case H'5; auto ]. apply Rlt_le_trans with (2 := FulpPred q B0). apply Ropp_lt_cancel; repeat rewrite Rminus_0_l. apply Rplus_lt_reg_l with (r := FtoR radix q). repeat rewrite Rplus_minus; auto. case (Rle_or_lt p (FNPred b radix precision q)); auto. intros H'2; absurd (q <= FNPred b radix precision q)%R; auto. apply Rgt_not_le; red in |- *; unfold FtoRradix in |- *; auto with real arith. apply FNPredLt; auto with zarith. case H'5; auto. intros H'4 H'7; elim H'7; intros H'8 H'9; apply H'9; clear H'7; auto. apply (FcanonicBound radix b); auto with arith. apply FNPredCanonic; auto with zarith. intros H1; apply Rplus_lt_compat_l; auto with real; apply Ropp_lt_contravar; unfold Rminus in |- *; auto with real. apply Rplus_le_reg_l with (r := FtoR radix q). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; apply isMax_inv1 with (1 := H'5). Qed.
imports: Reals ZArith List PeanoNat Psatz