proposition: Theorem Dekker: (radix_val beta=2)%Z \/ (Z.Even prec) -> (x*y=0 \/ bpow (emin + 2 * prec - 1) <= Rabs (x * y) -> (x*y=r+t4)%R) /\ (Rabs (x*y-(r+t4)) <= (7/2)*bpow emin)%R.
proof: Proof. Proof with auto with typeclass_instances. intros HH. case (Req_dec x 0); intros Kx. assert (Kr: r=0). unfold r; rewrite Kx, Rmult_0_l, round_0... assert (Khx: hx=0). unfold hx, qx, px; rewrite Kx, Rmult_0_l, round_0... rewrite Rplus_0_r, Rminus_0_l, Ropp_0, round_0... apply round_0... assert (Kt4: t4=0). unfold t4, t3, t2, t1, x1y1, x1y2, x2y1, x2y2, tx; rewrite Kr, Kx, Khx. rewrite 2!Rmult_0_l, round_0... rewrite Rminus_0_r, Rplus_0_r, round_0... rewrite 2!Rmult_0_l, round_0... rewrite 3!Rplus_0_r, Ropp_0; repeat rewrite round_0... rewrite Kx, Kr, Kt4. split;[intros; ring|idtac]. rewrite Rmult_0_l, Rplus_0_l, Rminus_0_l, Ropp_0, Rabs_R0. apply Rmult_le_pos; try apply bpow_ge_0. apply Rmult_le_pos. apply Fourier_util.Rle_zero_pos_plus1; apply Rmult_le_pos. left; apply Rlt_0_2. apply Fourier_util.Rle_zero_pos_plus1; left; apply Rlt_0_2. left; apply pos_half_prf. case (Req_dec y 0); intros Ky. assert (Kr: r=0). unfold r; rewrite Ky, Rmult_0_r, round_0... assert (Khy: hy=0). unfold hy, qy, py; rewrite Ky, Rmult_0_l, round_0... rewrite Rplus_0_r, Rminus_0_l, Ropp_0, round_0... apply round_0... assert (Kt4: t4=0). unfold t4, t3, t2, t1, x1y1, x1y2, x2y1, x2y2, ty; rewrite Kr, Ky, Khy. rewrite 2!Rmult_0_r, round_0... rewrite Rminus_0_r, Rplus_0_r, round_0... rewrite 2!Rmult_0_r, round_0... rewrite 3!Rplus_0_r, Ropp_0; repeat rewrite round_0... rewrite Ky, Kr, Kt4. split;[intros; ring|idtac]. rewrite Rmult_0_r, Rplus_0_l, Rminus_0_l, Ropp_0, Rabs_R0. apply Rmult_le_pos; try apply bpow_ge_0. apply Rmult_le_pos. apply Fourier_util.Rle_zero_pos_plus1; apply Rmult_le_pos. left; apply Rlt_0_2. apply Fourier_util.Rle_zero_pos_plus1; left; apply Rlt_0_2. left; apply pos_half_prf. assert (precisionNotZero : (1 < prec)%Z) by lia. assert (emin_neg': (emin <= 0)%Z) by lia. destruct (format_is_pff_format_can 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 (fpx,(Hfpx, (Hfpx',Hfpx''))). rewrite make_bound_Emin in Hfpx''; try assumption. replace (--emin)%Z with emin in Hfpx'' 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-px)) as (fqx,(Hfqx, (Hfqx',Hfqx''))). rewrite make_bound_Emin in Hfqx''; try assumption. replace (--emin)%Z with emin in Hfqx'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (qx+px)) as (fhx,(Hfhx, (Hfhx',Hfhx''))). rewrite make_bound_Emin in Hfhx''; try assumption. replace (--emin)%Z with emin in Hfhx'' 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-hx)) as (ftx,(Hftx, (Hftx',Hftx''))). rewrite make_bound_Emin in Hftx''; try assumption. replace (--emin)%Z with emin in Hftx'' by lia. destruct (format_is_pff_format_can beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero y) as (fy,(Hfy,Hfy')). 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 (y*(bpow s+1))) as (fpy,(Hfpy, (Hfpy',Hfpy''))). rewrite make_bound_Emin in Hfpy''; try assumption. replace (--emin)%Z with emin in Hfpy'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (y-py)) as (fqy,(Hfqy, (Hfqy',Hfqy''))). rewrite make_bound_Emin in Hfqy''; try assumption. replace (--emin)%Z with emin in Hfqy'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (qy+py)) as (fhy,(Hfhy, (Hfhy',Hfhy''))). rewrite make_bound_Emin in Hfhy''; try assumption. replace (--emin)%Z with emin in Hfhy'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (y-hy)) as (fty,(Hfty, (Hfty',Hfty''))). rewrite make_bound_Emin in Hfty''; try assumption. replace (--emin)%Z with emin in Hfty'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (hx*hy)) as (fx1y1,(Hfx1y1, (Hfx1y1',Hfx1y1''))). rewrite make_bound_Emin in Hfx1y1''; try assumption. replace (--emin)%Z with emin in Hfx1y1'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (hx*ty)) as (fx1y2,(Hfx1y2, (Hfx1y2',Hfx1y2''))). rewrite make_bound_Emin in Hfx1y2''; try assumption. replace (--emin)%Z with emin in Hfx1y2'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (tx*hy)) as (fx2y1,(Hfx2y1, (Hfx2y1',Hfx2y1''))). rewrite make_bound_Emin in Hfx2y1''; try assumption. replace (--emin)%Z with emin in Hfx2y1'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (tx*ty)) as (fx2y2,(Hfx2y2, (Hfx2y2',Hfx2y2''))). rewrite make_bound_Emin in Hfx2y2''; try assumption. replace (--emin)%Z with emin in Hfx2y2'' 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*y)) as (fr,(Hfr, (Hfr',Hfr''))). rewrite make_bound_Emin in Hfr''; try assumption. replace (--emin)%Z with emin in Hfr'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (-r+x1y1)) as (ft1,(Hft1, (Hft1',Hft1''))). rewrite make_bound_Emin in Hft1''; try assumption. replace (--emin)%Z with emin in Hft1'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (t1+x1y2)) as (ft2,(Hft2, (Hft2',Hft2''))). rewrite make_bound_Emin in Hft2''; try assumption. replace (--emin)%Z with emin in Hft2'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (t2+x2y1)) as (ft3,(Hft3, (Hft3',Hft3''))). rewrite make_bound_Emin in Hft3''; try assumption. replace (--emin)%Z with emin in Hft3'' by lia. destruct (round_N_is_pff_round beta (make_bound beta prec emin) prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero choice (t3+x2y2)) as (ft4,(Hft4, (Hft4',Hft4''))). rewrite make_bound_Emin in Hft4''; try assumption. replace (--emin)%Z with emin in Hft4'' by lia. assert (Hs:(s =(Z.abs_nat prec - Nat.div2 (Z.abs_nat prec))%nat)). unfold s; rewrite inj_minus. assert (TT: (Z.div2 prec = Nat.div2 (Z.abs_nat prec))%Z). rewrite Nat.div2_div, Z.div2_div, Nat2Z.inj_div; simpl. rewrite inj_abs; lia. rewrite <- TT. rewrite inj_abs; try lia. rewrite Z.max_r; try lia. assert (Z.div2 prec <= prec)%Z; try lia. rewrite Z.div2_div; apply Zlt_le_weak. apply Z_div_lt; lia. assert (D:(((- dExp (make_bound beta prec emin) <= Pff.Fexp fx + Pff.Fexp fy)%Z -> (FtoR beta fx * FtoR beta fy = FtoR beta fr + FtoR beta ft4)) /\ Rabs (FtoR beta fx * FtoR beta fy - (FtoR beta fr + FtoR beta ft4)) <= 7 / 2 * powerRZ beta (- dExp (make_bound beta prec emin)))). apply Dekker with (Z.abs_nat prec) fpx fqx fhx ftx fpy fqy fhy fty fx1y1 fx1y2 fx2y1 fx2y2 ft1 ft2 ft3; try assumption. apply radix_gt_1. apply make_bound_p; lia. replace 4%nat with (Z.abs_nat 4) by easy. apply Zabs_nat_le; lia. rewrite Hfx, <- Hs, <- bpow_powerRZ; apply Hfpx'. rewrite Hfx, Hfpx''; apply Hfqx'. rewrite Hfpx'', Hfqx''; apply Hfhx'. rewrite Hfx, Hfhx''; apply Hftx'. rewrite Hfy, <- Hs, <- bpow_powerRZ; apply Hfpy'. rewrite Hfy, Hfpy''; apply Hfqy'. rewrite Hfpy'', Hfqy''; apply Hfhy'. rewrite Hfy, Hfhy''; apply Hfty'. rewrite Hfhx'', Hfhy''; apply Hfx1y1'. rewrite Hfhx'', Hfty''; apply Hfx1y2'. rewrite Hftx'', Hfhy''; apply Hfx2y1'. rewrite Hftx'', Hfty''; apply Hfx2y2'. rewrite Hfx, Hfy; apply Hfr'. rewrite Hfr'', Hfx1y1''; apply Hft1'. rewrite Hft1'', Hfx1y2''; apply Hft2'. rewrite Hft2'', Hfx2y1''; apply Hft3'. rewrite Hft3'', Hfx2y2''; apply Hft4'. rewrite make_bound_Emin; lia. case HH; intros K;[now left|right]. destruct K as (l,Hl). exists (Z.abs_nat l). apply Nat2Z.inj. rewrite inj_mult. rewrite 2!inj_abs; lia. rewrite <- Hfx, <- Hfy. unfold r; rewrite <- Hfr''. unfold t4; rewrite <- Hft4''. destruct D as (D1,D2); split. intros L. apply D1. apply underf_mult_aux' with beta prec; try assumption. apply make_bound_p; assumption. now apply FcanonicBound with beta. now apply FcanonicBound with beta. case L; intros L'. contradict L'. apply Rmult_integral_contrapositive_currified. rewrite Hfx; easy. rewrite Hfy; easy. apply Rle_trans with (2:=L'). right; repeat f_equal. rewrite make_bound_Emin, Z.opp_involutive; lia. apply Rle_trans with (1:=D2). rewrite make_bound_Emin, Z.opp_involutive. 2: lia. rewrite bpow_powerRZ. now right. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat