proposition: Lemma pff_round_NE_is_round: forall (r:R), (FtoR beta (RND_EvenClosest b beta (Z.abs_nat p) r) = round beta (FLT_exp (-dExp b) p) rndNE r).
proof: Proof. intros. assert (Rnd_NE_pt beta (FLT_exp (-dExp b) p) r (round beta (FLT_exp (-dExp b) p) rndNE r)). apply round_NE_pt; auto with zarith. apply FLT_exp_valid. unfold Prec_gt_0; auto with zarith. apply exists_NE_FLT. now right. unfold Rnd_NE_pt, Rnd_NG_pt, Rnd_N_pt, NE_prop in H. destruct H as ((H1,H2),H3). destruct (format_is_pff_format _ H1) as (f,(Hf1,Hf2)). rewrite <- Hf1. apply sym_eq. eapply (EvenClosestUniqueP b beta (Z.abs_nat p)). apply radix_gt_1. lia. exact pGivesBound. split. split; auto; intros g Hg. rewrite Hf1. apply H2. apply pff_format_is_format; auto. case (Req_dec (FtoR beta (Fnormalize beta b (Z.abs_nat p) f)) 0%R); intros L. left. unfold FNeven, Feven, Even. exists 0%Z. rewrite Zmult_0_r. apply eq_IZR. apply Rmult_eq_reg_l with (powerRZ beta (Pff.Fexp (Fnormalize beta b (Z.abs_nat p) f)))%R. rewrite Rmult_0_r. rewrite <- L; unfold FtoR; simpl; ring. apply powerRZ_NOR; auto with zarith real. apply Rgt_not_eq. apply IZR_lt; apply radix_gt_0. destruct H3. destruct H as (g,(Hg1,(Hg2,Hg3))). left. unfold FNeven, Feven. apply equiv_RNDs_aux. replace (Pff.Fnum (Fnormalize beta b (Z.abs_nat p) f)) with (Fnum g); try assumption. replace g with (Float beta (Pff.Fnum (Fnormalize beta b (Z.abs_nat p) f)) (Pff.Fexp (Fnormalize beta b (Z.abs_nat p) f))). easy. apply canonical_unique with (FLT_exp (- dExp b) p). 2: assumption. apply pff_canonic_is_canonic. apply FnormalizeCanonic. 2-3: lia. 2: auto with real. apply radix_gt_1. exact L. rewrite <- Hg1, <- Hf1. rewrite <- FnormalizeCorrect with beta b (Z.abs_nat p) f; auto with zarith. unfold F2R, FtoR; simpl. rewrite bpow_powerRZ. reflexivity. apply radix_gt_1. right; intros q (Hq1,Hq2). rewrite Hf1. apply H. split. apply pff_format_is_format; auto. intros g Hg. destruct (format_is_pff_format _ Hg) as (v,(Hv1,Hv2)). rewrite <- Hv1. apply Hq2; auto. apply RND_EvenClosest_correct with (3 := pGivesBound). apply radix_gt_1. lia. Qed.
imports: Coq(Lia) Pff Core