proposition: Theorem Dekker: (radix=2)%Z \/ (Nat.Even t) -> ((-dExp b <= Fexp x+Fexp y)%Z -> (x*y=r+t4)%R) /\ (Rabs (x*y-(r+t4)) <= (7/2)*powerRZ radix (-(dExp b)))%R.
proof: Proof. intros. case (Zle_or_lt (-dExp b) (Fexp x+Fexp y)); intros. cut (x * y = r + t4)%R; [intros; split; auto|idtac]. rewrite H1; ring_simplify ( (r + t4) - (r + t4))%R; rewrite Rabs_R0. apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith. unfold Rdiv; apply Rmult_lt_0_compat; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply trans_eq with (r-(Fopp t4))%R;[idtac|unfold FtoRradix; rewrite Fopp_correct; ring]. unfold FtoRradix; apply Dekker1 with b t p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 (Fopp t1) (Fopp t2) (Fopp t3); auto; try rewrite Fopp_correct; fold FtoRradix. replace (r-x1y1)%R with (-(-r+x1y1))%R;[apply ClosestOpp; auto|ring]. replace (-t1-x1y2)%R with (-(t1+x1y2))%R;[apply ClosestOpp; auto|ring]. replace (-t2-x2y1)%R with (-(t2+x2y1))%R;[apply ClosestOpp; auto|ring]. replace (-t3-x2y2)%R with (-(t3+x2y2))%R;[apply ClosestOpp; auto|ring]. split. intros; absurd (Fexp x + Fexp y < - dExp b)%Z; auto with zarith. replace (r+t4)%R with (r-(Fopp t4))%R;[idtac|unfold FtoRradix; rewrite Fopp_correct; ring]. unfold FtoRradix; apply Dekker2 with t p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 (Fopp t1) (Fopp t2) (Fopp t3); auto; try rewrite Fopp_correct; fold FtoRradix. replace (r-x1y1)%R with (-(-r+x1y1))%R;[apply ClosestOpp; auto|ring]. replace (-t1-x1y2)%R with (-(t1+x1y2))%R;[apply ClosestOpp; auto|ring]. replace (-t2-x2y1)%R with (-(t2+x2y1))%R;[apply ClosestOpp; auto|ring]. replace (-t3-x2y2)%R with (-(t3+x2y2))%R;[apply ClosestOpp; auto|ring]. Qed.
imports: Reals ZArith List PeanoNat Psatz