proposition: Lemma pff_round_N_is_round: forall choice, forall (r:R), (FtoR beta (RND_Closest b beta (Z.abs_nat p) choice r) = round beta (FLT_exp (-dExp b) p) (Znearest choice) r).
proof: Proof. Proof with auto with typeclass_instances. generalize (radix_gt_1 beta); intros M. intros choice r; apply sym_eq. assert (K:Valid_exp (FLT_exp (- dExp b) p)). apply FLT_exp_valid. unfold Prec_gt_0; auto with zarith. unfold RND_Closest, FtoRradix. rewrite pff_round_DN_is_round. rewrite pff_round_UP_is_round. case (Rle_dec _ _); intros H1. case (Rle_lt_or_eq_dec _ _ H1); intros H2. rewrite pff_round_UP_is_round. apply round_N_eq_UP... rewrite Rabs_right in H2;[idtac| apply Rle_ge, Rle_0_minus, round_UP_pt; easy]. rewrite Rabs_left1 in H2;[idtac| apply Rle_minus, round_DN_pt; easy]. apply Rmult_lt_reg_r with 2%R; try apply Rlt_0_2. unfold Rdiv; rewrite Rmult_assoc, Rinv_l. 2: apply Rgt_not_eq, Rlt_0_2. apply Rplus_lt_reg_l with (-round beta (FLT_exp (- dExp b) p) Zfloor r - r)%R. apply Rle_lt_trans with (round beta (FLT_exp (- dExp b) p) Zceil r - r)%R;[right;ring|idtac]. apply Rlt_le_trans with (1:=H2). right; ring. rewrite round_N_middle. rewrite inj_abs by lia. case (choice _). apply sym_eq, pff_round_UP_is_round. apply sym_eq, pff_round_DN_is_round. rewrite Rabs_right in H2;[idtac| apply Rle_ge, Rle_0_minus, round_UP_pt; easy]. rewrite Rabs_left1 in H2;[idtac| apply Rle_minus, round_DN_pt; easy]. rewrite H2; ring. rewrite pff_round_DN_is_round. apply round_N_eq_DN... apply Rnot_le_lt in H1. rewrite Rabs_left1 in H1;[idtac| apply Rle_minus, round_DN_pt; easy]. rewrite Rabs_right in H1;[idtac| apply Rle_ge, Rle_0_minus, round_UP_pt; easy]. apply Rmult_lt_reg_r with 2%R; try apply Rlt_0_2. unfold Rdiv; rewrite Rmult_assoc, Rinv_l. 2: apply Rgt_not_eq, Rlt_0_2. apply Rplus_lt_reg_l with (-round beta (FLT_exp (- dExp b) p) Zfloor r - r)%R. apply Rle_lt_trans with (-(round beta (FLT_exp (- dExp b) p) Zfloor r - r))%R;[right;ring|idtac]. apply Rlt_le_trans with (1:=H1). right; ring. Qed.
imports: Coq(Lia) Pff Core