proposition: Lemma pff_round_is_round_N: forall r f, Closest b beta r f -> exists (choice:Z->bool), FtoR beta f = round beta (FLT_exp (-dExp b) p) (Znearest choice) r.
proof: Proof. Proof with auto with typeclass_instances. intros r f Hf. generalize (radix_gt_1 beta); intros M. assert (M':1 < Z.abs_nat p). apply Nat2Z.inj_lt; simpl. rewrite inj_abs; lia. pose (d := round beta (FLT_exp (-dExp b) p) Zfloor r). pose (u := round beta (FLT_exp (-dExp b) p) Zceil r). case (Rle_or_lt ((d+u)/2) r); intros L. destruct L as [L|L]. exists (fun _ => true). rewrite <- pff_round_N_is_round. apply trans_eq with (FtoR beta (RND_Max b beta (Z.abs_nat p) r)). apply ClosestMaxEq with b r (RND_Min b beta (Z.abs_nat p) r); try assumption. apply RND_Min_correct; assumption. apply RND_Max_correct; assumption. rewrite pff_round_DN_is_round; fold d. rewrite pff_round_UP_is_round; fold u. apply Rmult_lt_reg_r with (/2)%R. apply pos_half_prf. apply Rlt_le_trans with (1:=L). right; simpl; field. rewrite pff_round_N_is_round. rewrite pff_round_UP_is_round; fold u. apply sym_eq, round_N_eq_UP... apply FLT_exp_valid. unfold Prec_gt_0; auto with zarith. case (ClosestMinOrMax b beta r f); try assumption; intros LL. exists (fun _ => false). rewrite round_N_middle. rewrite <- pff_round_DN_is_round. apply (MinUniqueP b beta r); try assumption. apply RND_Min_correct; assumption. fold d; fold u; rewrite <- L; field. exists (fun _ => true). rewrite round_N_middle. rewrite <- pff_round_UP_is_round. apply (MaxUniqueP b beta r); try assumption. apply RND_Max_correct; assumption. fold d; fold u; rewrite <- L; field. exists (fun _ => true). rewrite <- pff_round_N_is_round. apply trans_eq with (FtoR beta (RND_Min b beta (Z.abs_nat p) r)). apply ClosestMinEq with b r (RND_Max b beta (Z.abs_nat p) r); try assumption. apply RND_Min_correct; assumption. apply RND_Max_correct; assumption. rewrite pff_round_DN_is_round; fold d. rewrite pff_round_UP_is_round; fold u. apply Rmult_lt_reg_r with (/2)%R. apply pos_half_prf. apply Rle_lt_trans with (2:=L). right; simpl; field. rewrite pff_round_N_is_round. rewrite pff_round_DN_is_round; fold d. apply sym_eq, round_N_eq_DN... apply FLT_exp_valid. unfold Prec_gt_0; auto with zarith. Qed.
imports: Coq(Lia) Pff Core