proposition: Theorem Dekker2: (radix=2)%Z \/ (Nat.Even t) -> (Rabs (x*y-(r-t4)) <= (7/2)*powerRZ radix (-(dExp b)))%R.
proof: Proof. intros. case (Req_dec 0%R x); intros Ny. cut (FtoRradix r=0)%R;[intros Z1|idtac]. cut (FtoRradix t4=0)%R;[intros Z2|idtac]. replace ((x * y - (r - t4)))%R with 0%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. fold FtoRradix; rewrite Z1; rewrite Z2; rewrite <- Ny; ring. cut (FtoRradix hx=0)%R;[intros Z3|idtac]. cut (FtoRradix tx=0)%R;[intros Z4|idtac]. unfold FtoRradix; apply ClosestZero with b t (t3-x2y2)%R; auto with zarith. cut (FtoRradix t3=0)%R;[intros Z5|idtac]. cut (FtoRradix x2y2=0)%R;[intros Z6|idtac]. rewrite Z5; rewrite Z6; ring. unfold FtoRradix; apply ClosestZero with b t (tx*ty)%R; auto with zarith. rewrite Z4; ring. unfold FtoRradix; apply ClosestZero with b t (t2-x2y1)%R; auto with zarith. cut (FtoRradix t2=0)%R;[intros Z5|idtac]. cut (FtoRradix x2y1=0)%R;[intros Z6|idtac]. rewrite Z5; rewrite Z6; ring. unfold FtoRradix; apply ClosestZero with b t (tx*hy)%R; auto with zarith. rewrite Z4; ring. unfold FtoRradix; apply ClosestZero with b t (t1-x1y2)%R; auto with zarith. cut (FtoRradix t1=0)%R;[intros Z5|idtac]. cut (FtoRradix x1y2=0)%R;[intros Z6|idtac]. rewrite Z5; rewrite Z6; ring. unfold FtoRradix; apply ClosestZero with b t (hx*ty)%R; auto with zarith. rewrite Z3; ring. unfold FtoRradix; apply ClosestZero with b t (r-x1y1)%R; auto with zarith. cut (FtoRradix x1y1=0)%R;[intros Z6|idtac]. rewrite Z1; rewrite Z6; ring. unfold FtoRradix; apply ClosestZero with b t (hx*hy)%R; auto with zarith. rewrite Z3; ring. elim VeltkampU with radix b s t x p q hx tx; auto. intros T1 T; elim T; intros H' T'; clear T1 T T'. fold FtoRradix in H'; rewrite Z3 in H'; rewrite <- Ny in H'; auto with real. apply trans_eq with (0+tx)%R; auto with real. unfold s; apply SLe; auto. unfold s; apply SGe; auto. elim Veltkamp with radix b s t x p q hx; auto. 2: apply SLe; auto. 2: apply SGe; auto. 2: apply FcanonicBound with radix; auto. intros T1 T; elim T; intros hy' T'; elim T'; intros G1 T''; elim T''; intros ; clear T1 T T' T''. unfold FtoRradix; rewrite <- G1. apply ClosestZero with (Bound (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (t - s))))) (dExp b)) (t-s) (FtoR radix x)%R; auto with zarith. apply p'GivesBound; auto with zarith. cut (s <= t-2); [unfold s; auto with zarith | apply SGe; auto]. unfold FtoRradix; apply ClosestZero with b t (x*y)%R; auto with zarith. rewrite <- Ny; ring. case (Req_dec 0%R y); intros Nx. cut (FtoRradix r=0)%R;[intros Z1|idtac]. cut (FtoRradix t4=0)%R;[intros Z2|idtac]. replace ((x * y - (r - t4)))%R with 0%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. fold FtoRradix; rewrite Z1; rewrite Z2; rewrite <- Nx; ring. cut (FtoRradix hy=0)%R;[intros Z3|idtac]. cut (FtoRradix ty=0)%R;[intros Z4|idtac]. unfold FtoRradix; apply ClosestZero with b t (t3-x2y2)%R; auto with zarith. cut (FtoRradix t3=0)%R;[intros Z5|idtac]. cut (FtoRradix x2y2=0)%R;[intros Z6|idtac]. rewrite Z5; rewrite Z6; ring. unfold FtoRradix; apply ClosestZero with b t (tx*ty)%R; auto with zarith. rewrite Z4; ring. unfold FtoRradix; apply ClosestZero with b t (t2-x2y1)%R; auto with zarith. cut (FtoRradix t2=0)%R;[intros Z5|idtac]. cut (FtoRradix x2y1=0)%R;[intros Z6|idtac]. rewrite Z5; rewrite Z6; ring. unfold FtoRradix; apply ClosestZero with b t (tx*hy)%R; auto with zarith. rewrite Z3; ring. unfold FtoRradix; apply ClosestZero with b t (t1-x1y2)%R; auto with zarith. cut (FtoRradix t1=0)%R;[intros Z5|idtac]. cut (FtoRradix x1y2=0)%R;[intros Z6|idtac]. rewrite Z5; rewrite Z6; ring. unfold FtoRradix; apply ClosestZero with b t (hx*ty)%R; auto with zarith. rewrite Z4; ring. unfold FtoRradix; apply ClosestZero with b t (r-x1y1)%R; auto with zarith. cut (FtoRradix x1y1=0)%R;[intros Z6|idtac]. rewrite Z1; rewrite Z6; ring. unfold FtoRradix; apply ClosestZero with b t (hx*hy)%R; auto with zarith. rewrite Z3; ring. elim VeltkampU with radix b s t y p' q' hy ty; auto. intros T1 T; elim T; intros H' T'; clear T1 T T'. fold FtoRradix in H'; rewrite Z3 in H'; rewrite <- Nx in H'; auto with real. apply trans_eq with (0+ty)%R; auto with real. unfold s; apply SLe; auto. unfold s; apply SGe; auto. elim Veltkamp with radix b s t y p' q' hy; auto. 2: apply SLe; auto. 2: apply SGe; auto. 2: apply FcanonicBound with radix; auto. intros T1 T; elim T; intros hy' T'; elim T'; intros G1 T''; elim T''; intros ; clear T1 T T' T''. unfold FtoRradix; rewrite <- G1. apply ClosestZero with (Bound (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (t - s))))) (dExp b)) (t-s) (FtoR radix y)%R; auto with zarith. apply p'GivesBound; auto with zarith. cut (s <= t-2); [unfold s; auto with zarith | apply SGe; auto]. unfold FtoRradix; apply ClosestZero with b t (x*y)%R; auto with zarith. rewrite <- Nx; ring. apply Dekker2_aux; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz