proposition: Theorem Veltkamp: exists choice': Z->bool , hx = round beta (FLT_exp emin (prec-s)) (Znearest choice') x.
proof: Proof. Proof with auto with typeclass_instances. assert (precisionNotZero : (1 < prec)%Z) by lia. destruct (format_is_pff_format beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero x) as (fx,(Hfx,Hfx')). rewrite make_bound_Emin; try assumption. replace (--emin)%Z with emin by lia; assumption. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (x*(bpow s+1))) as (fp,(Hfp, (Hfp',Hfp''))). rewrite make_bound_Emin in Hfp''; try assumption. replace (--emin)%Z with emin in Hfp'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (x-p)) as (fq,(Hfq, (Hfq',Hfq''))). rewrite make_bound_Emin in Hfq''; try assumption. replace (--emin)%Z with emin in Hfq'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (q+p)) as (fhx,(Hfhx, (Hfhx',Hfhx''))). rewrite make_bound_Emin in Hfhx''; try assumption. replace (--emin)%Z with emin in Hfhx'' by lia. destruct Veltkamp with beta (make_bound beta prec emin) (Z.abs_nat s) (Z.abs_nat prec) fx fp fq fhx as (H1,(hx', (H2,(H3,H4)))); try assumption. apply radix_gt_1. apply make_bound_p; lia. replace 2%nat with (Z.abs_nat 2) by easy. apply Zabs_nat_le; lia. apply Nat2Z.inj_le. rewrite inj_abs; lia. rewrite Hfx; rewrite inj_abs; try lia. rewrite bpow_powerRZ in Hfp'; exact Hfp'. rewrite Hfx, Hfp''; assumption. rewrite Hfp'', Hfq''; assumption. destruct pff_round_is_round_N with beta (make_bound beta (prec-s) emin) (Z.abs_nat (prec-s)) (FtoR beta fx) hx' as (choice',M). rewrite Zabs2Nat.id. apply make_bound_p; lia. rewrite inj_abs; simpl; lia. unfold make_bound. replace (Z.to_pos (beta ^ (prec - s))) with (Pos.of_succ_nat (Init.Nat.pred (Z.abs_nat (Zpower_nat beta (Z.abs_nat prec - Z.abs_nat s))))). replace (Z.abs_N emin) with (dExp (make_bound beta prec emin)) by easy. exact H3. apply Zpos_eq_iff. apply trans_eq with (Zpower_nat beta (Z.abs_nat prec - Z.abs_nat s)). rewrite <- p''GivesBound with (b:=make_bound beta prec emin) at 2. simpl; auto. apply radix_gt_1. rewrite Zpower_Zpower_nat,Z2Pos.id. f_equal; apply sym_eq, Zabs2Nat.inj_sub; lia. apply Zpower_nat_less. apply radix_gt_1. lia. exists choice'. unfold hx; rewrite <- Hfhx'', <- H2, M. f_equal; try easy. f_equal. rewrite make_bound_Emin; lia. rewrite inj_abs; simpl; lia. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat