proposition: Theorem ClosestUlp : forall (p : R) (q : float), Closest b radix p q -> (2 * Rabs (p - q) <= Fulp b radix precision q)%R.
proof: Proof. intros p q H'. case (Req_dec p q); intros Eqpq. rewrite Eqpq. replace (Rabs (q - q)) with 0%R; [ rewrite Rmult_0_r | replace (q - q)%R with 0%R; try ring; rewrite Rabs_right; auto with real ]. unfold Fulp in |- *; apply Rlt_le; auto with real arith. apply powerRZ_lt, IZR_lt; lia. replace (2 * Rabs (p - q))%R with (Rabs (p - q) + Rabs (p - q))%R; [ idtac | simpl in |- *; ring ]. case ClosestMinOrMax with (1 := H'); intros H'1. apply Rle_trans with (Rabs (p - q) + Rabs (FNSucc b radix precision q - p))%R. apply Rplus_le_compat_l. rewrite <- (Rabs_Ropp (p - q)). rewrite Ropp_minus_distr. elim H'; auto. intros H'0 H'2; apply H'2; auto. apply FcanonicBound with (radix := radix); auto with zarith arith. apply FNSuccCanonic; auto with zarith. rewrite Rabs_right. rewrite Rabs_right. replace (p - q + (FNSucc b radix precision q - p))%R with (FNSucc b radix precision q - q)%R; [ idtac | ring ]. unfold FtoRradix in |- *; apply FulpSuc; auto. case H'1; auto. apply Rge_minus; apply Rle_ge; auto with real zarith. case MinMax with (3 := pGivesBound) (r := p) (p := q); auto with zarith. intros H'0 H'2; elim H'2; intros H'3 H'4; apply H'3; clear H'2; auto. apply Rge_minus; apply Rle_ge; auto with real. apply isMin_inv1 with (1 := H'1). apply Rle_trans with (Rabs (p - q) + Rabs (p - FNPred b radix precision q))%R. apply Rplus_le_compat_l. rewrite <- (Rabs_Ropp (p - q)); rewrite <- (Rabs_Ropp (p - FNPred b radix precision q)). repeat rewrite Ropp_minus_distr. elim H'; auto. intros H'0 H'2; apply H'2; auto. apply FcanonicBound with (radix := radix); auto with zarith. apply FNPredCanonic; auto with zarith. rewrite <- (Rabs_Ropp (p - q)); rewrite Ropp_minus_distr. rewrite Rabs_right. rewrite Rabs_right. replace (q - p + (p - FNPred b radix precision q))%R with (q - FNPred b radix precision q)%R; [ idtac | ring ]. unfold FtoRradix in |- *; apply FulpPred; auto. case H'1; auto. apply Rge_minus; apply Rle_ge; auto with real. case MaxMin with (3 := pGivesBound) (r := p) (p := q); auto with zarith. intros H'0 H'2; elim H'2; intros H'3 H'4; apply H'3; clear H'2; auto. apply Rge_minus; apply Rle_ge; auto with real. apply isMax_inv1 with (1 := H'1). Qed.
imports: Reals ZArith List PeanoNat Psatz