proposition: Theorem RoundLeGeneral : forall (p : float) (z : R), Fbounded b p -> Closest b radix z p -> (Rabs p <= Rabs z * / (1 - powerRZ radix (- precision)) + powerRZ radix (Z.pred (- dExp b)) * / (1 - powerRZ radix (- precision)))%R.
proof: Proof. intros p z Hp H. cut (0 < 1 - powerRZ radix (- precision))%R; [ intros H1 | idtac ]. 2: apply Rplus_lt_reg_r with (powerRZ radix (- precision)). 2: ring_simplify. 2: change 1%R with (powerRZ radix 0). 2: apply Rlt_powerRZ ; [ now apply IZR_lt | lia ]. apply Rmult_le_reg_l with (1 - powerRZ radix (- precision))%R; auto. ring_simplify ((1 - powerRZ radix (- precision)) * Rabs p)%R. apply Rle_trans with (Rabs z * ((1 - powerRZ radix (- precision)) * / (1 - powerRZ radix (- precision))) + powerRZ radix (Z.pred (- dExp b)) * ((1 - powerRZ radix (- precision)) * / (1 - powerRZ radix (- precision))))%R; [ idtac | right; ring; ring ]. repeat rewrite Rinv_r; auto with real. ring_simplify. apply Rplus_le_reg_l with (- powerRZ radix (Z.pred (- dExp b)))%R. ring_simplify. apply Rle_trans with (Rabs p + - (Rabs p * powerRZ radix (- precision) + powerRZ radix (Z.pred (- dExp b))))%R; [ right; ring | idtac ]. apply Rle_trans with (Rabs p + - (/ radix * Fulp b radix precision p))%R. apply Rplus_le_compat_l; apply Ropp_le_contravar. apply Rmult_le_reg_l with (IZR radix); auto with real zarith. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real zarith. rewrite Rmult_1_l. apply Rle_trans with (Rabs p * (powerRZ radix 1 * powerRZ radix (- precision)) + powerRZ radix 1 * powerRZ radix (Z.pred (- dExp b)))%R; [ idtac | right; simpl in |- *; ring ]. repeat rewrite <- powerRZ_add; auto with zarith real. replace (1 + - precision)%Z with (Z.succ (- precision)); auto with zarith. replace (1 + Z.pred (- dExp b))%Z with (- dExp b)%Z; auto with zarith. apply FulpLeGeneral; auto. unfold Z.pred in |- *; auto with zarith. apply Rplus_le_reg_l with (- Rabs z + / radix * Fulp b radix precision p)%R. ring_simplify. apply Rle_trans with (Rabs (p - z)). apply Rle_trans with (Rabs p - Rabs z)%R; [ right; ring | apply Rabs_triang_inv ]. rewrite <- Rabs_Ropp. replace (- (p - z))%R with (z - p)%R; [ idtac | ring ]. apply Rmult_le_reg_l with (IZR radix); auto with real zarith. apply Rle_trans with (Fulp b radix precision p * (radix * / radix))%R; [ rewrite Rinv_r; auto with real zarith | right; ring ]. rewrite Rmult_1_r. now apply ClosestUlp. Qed.
imports: Reals ZArith List PeanoNat Psatz