proposition: Theorem Veltkamp_Even: (choice = fun z => negb (Z.even z)) -> hx = round_flt_s x.
proof: Proof. Proof with auto with typeclass_instances. intros Hchoice. 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_NE_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero (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_NE_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero (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_NE_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero (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 VeltkampEven with beta (make_bound beta prec emin) (Z.abs_nat s) (Z.abs_nat prec) fx fp fq fhx as (hx', (H1,H2)); 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'', <- Hchoice; assumption. rewrite Hfp'', Hfq'', <- Hchoice; assumption. unfold hx; rewrite Hchoice, <- Hfhx'', <- H1. apply trans_eq with (FtoR beta (RND_EvenClosest (make_bound beta (prec-s) emin) beta (Z.abs_nat (prec-s)) x)). generalize (EvenClosestUniqueP (make_bound beta (prec-s) emin) beta (Z.abs_nat (prec-s))); unfold UniqueP; intros T. apply T with x; clear T. apply radix_gt_1. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. rewrite <- Hfx. replace (Z.abs_nat (prec-s)) with (Z.abs_nat prec - Z.abs_nat s)%nat. replace (make_bound beta (prec - s) emin) with (Bound (Pos.of_succ_nat (Peano.pred (Z.abs_nat (Zpower_nat beta (Z.abs_nat prec - Z.abs_nat s))))) (dExp (make_bound beta prec emin))). exact H2. generalize (make_bound_Emin beta (prec-s) _ emin_neg). generalize (make_bound_p beta (prec-s) emin). destruct (make_bound beta (prec-s) emin) as (l1,l2). simpl; intros H3 H4; f_equal. apply Pos2Z.inj. rewrite H3; try lia. replace (Z.abs_nat (prec - s)) with (Z.abs_nat prec - Z.abs_nat s)%nat. rewrite <- (p'GivesBound beta (make_bound beta prec emin) (Z.abs_nat s) (Z.abs_nat prec)) at 2. simpl; easy. apply radix_gt_1. apply Nat2Z.inj. rewrite inj_minus; repeat rewrite inj_abs; lia. apply N2Z.inj. rewrite H4. rewrite Zabs2N.id_abs. now apply Z.abs_neq. apply Nat2Z.inj. rewrite inj_abs; lia. apply RND_EvenClosest_correct. apply radix_gt_1. apply Nat2Z.inj_lt. rewrite inj_abs; simpl; lia. apply make_bound_p; lia. rewrite pff_round_NE_is_round; try lia. f_equal; f_equal. rewrite make_bound_Emin; lia. apply make_bound_p; lia. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat