proposition: Theorem Dekker2_aux: (FtoRradix x <>0) -> (FtoRradix y <>0) -> (radix=2)%Z \/ (Nat.Even t) -> (Rabs (x*y-(r-t4)) <= (7/2)*powerRZ radix (-(dExp b)))%R.
proof: Proof. intros P1 P2. intros; generalize dExpPrim; intros. elim (NormalbPrim x); auto. intros x' T; elim T; intros Nx' T'; elim T'; intros Hx' Ex'; clear T T'. elim (NormalbPrim y); auto. intros y' T; elim T; intros Ny' T'; elim T'; intros Hy' Ey'; clear T T'. assert (MM:(-(dExp b') <= Fexp x'+Fexp y')%Z). unfold b'; simpl; rewrite dExpPrimEq; auto with zarith. generalize Underf_Err2; intros T. elim T with b radix t b' (x*y)%R r; auto with zarith; clear T. intros r' T; elim T; intros H1 H2; clear T. elim Veltkampb' with x p q hx tx; auto. 2: apply FcanonicBound with radix; auto. intros H4 T; elim T; intros H5 T'; elim T'; intros H6 H7; clear T T'. elim Veltkampb' with y p' q' hy ty; auto. 2: apply FcanonicBound with radix; auto. intros H8 T; elim T; intros H9 T'; elim T'; intros H10 H11; clear T T'. assert (TotalP (Closest b' radix)). apply ClosestTotal with t; auto with zarith. unfold TotalP in H3. elim (H3 (hx * hy)%R); intros x1y1' H12. elim (H3 (hx * ty)%R); intros x1y2' H13. elim (H3 (tx * hy)%R); intros x2y1' H14. elim (H3 (tx * ty)%R); intros x2y2' H15. elim (H3 (r' - x1y1')%R); intros t1' H16. elim (H3 (t1' - x1y2')%R); intros t2' H17. elim (H3 (t2' - x2y1')%R); intros t3' H18. elim (H3 (t3' - x2y2')%R); intros t4' H19. rewrite <- Hx'; rewrite <- Hy'; unfold FtoRradix. rewrite DekkerN with radix b' t x' y' p q hx tx p' q' hy ty x1y1' x1y2' x2y1' x2y2' r' t1' t2' t3' t4'; auto with zarith. 2: fold FtoRradix; rewrite Hx'; auto. 2: fold FtoRradix; rewrite Hx'; auto. 2: fold FtoRradix; rewrite Hx'; auto. 2: fold FtoRradix; rewrite Hy'; auto. 2: fold FtoRradix; rewrite Hy'; auto. 2: fold FtoRradix; rewrite Hy'; auto. 2: fold FtoRradix; rewrite Hx'; rewrite Hy'; auto. fold FtoRradix. replace (r' - t4' - (r - t4))%R with (-(r-r')+((t4-t4')))%R;[idtac|ring]. apply Rle_trans with (1:=Rabs_triang (-(r-r'))%R ((t4-t4'))%R). apply Rle_trans with ((3/4)*powerRZ radix (- dExp b) +(11/4)*powerRZ radix (- dExp b))%R; [idtac|right; field; apply prod_neq_R0; auto with real; apply prod_neq_R0; auto with real]. apply Rplus_le_compat. rewrite Rabs_Ropp; auto with real. elim H1; intros G1 G2; elim G2; intros G3 G4; elim G4; intros G5 G6. unfold FtoRradix; apply Rle_trans with (1:=G5); right; ring. cut (2 <= s);[intros Sle|unfold s; apply SLe; auto]. cut (s <= t-2);[intros Sge|unfold s; apply SGe; auto]. cut (s+s <= t+1)%Z;[intros s2le|unfold s; apply s2Le; auto]. cut (t <=s+s)%Z;[intros s2ge|unfold s; apply s2Ge; auto]. generalize VeltkampU; intros V. elim V with radix b' s t x' p q hx tx; auto. 2: left; auto. 2: fold FtoRradix; rewrite Hx'; auto. 2: fold FtoRradix; rewrite Hx'; auto. 2: fold FtoRradix; rewrite Hx'; auto. intros MX1 T; elim T; intros MX2 T'; clear T; elim T'; intros T1 T2; clear T'. elim T1; intros Chx' T1'; elim T1'; intros MX3 T1''; elim T1''; intros MX4 MX5; clear T1 T1' T1''. lapply MX5; auto; clear MX5; intros MX5. elim T2; intros Ctx' T1'; elim T1'; intros MX6 T1''; elim T1''; intros MX7 MX8; clear T2 T1' T1''. elim V with radix b' s t y' p' q' hy ty; auto. 2: left; auto. 2: fold FtoRradix; rewrite Hy'; auto. 2: fold FtoRradix; rewrite Hy'; auto. 2: fold FtoRradix; rewrite Hy'; auto. intros MY1 T; elim T; intros MY2 T'; clear T; elim T'; intros T1 T2; clear T'. elim T1; intros Chy' T1'; elim T1'; intros MY3 T1''; elim T1''; intros MY4 MY5; clear T1 T1' T1''. lapply MY5; auto; clear MY5; intros MY5. elim T2; intros Cty' T1'; elim T1'; intros MY6 T1''; elim T1''; intros MY7 MY8; clear T2 T1' T1'' V. generalize Boundedt1; intros V. elim V with radix b' s t x' Chx' Ctx' y' Chy' Cty' r' (Fminus radix (Fmult x' y') r'); auto with zarith real; clear V. 2: fold FtoRradix; rewrite Hy';rewrite Hx'; auto. 2:rewrite Fminus_correct; auto with zarith; rewrite Fmult_correct; auto with zarith; ring. 2:rewrite MX6; rewrite MX3; exact MX2. 2:rewrite MY6; rewrite MY3; exact MY2. 2:rewrite MX6; replace (FtoR radix tx) with (FtoR radix x'-FtoR radix hx)%R; auto with real. 2:rewrite MX2; ring. 2:rewrite MY6; replace (FtoR radix ty) with (FtoR radix y'-FtoR radix hy)%R; auto with real. 2:rewrite MY2; ring. intros Ct1' T; elim T; intros M11 T'; elim T'; intros M12 M13; clear T T'. generalize Boundedt2; intros V. elim V with radix b' s t x' Chx' Ctx' y' Chy' Cty' r' (Fminus radix (Fmult x' y') r'); auto with zarith real; clear V. 2: fold FtoRradix; rewrite Hy';rewrite Hx'; auto. 2:rewrite Fminus_correct; auto with zarith; rewrite Fmult_correct; auto with zarith; ring. 2:rewrite MX6; rewrite MX3; exact MX2. 2:rewrite MY6; rewrite MY3; exact MY2. 2:rewrite MX6; replace (FtoR radix tx) with (FtoR radix x'-FtoR radix hx)%R; auto with real. 2:rewrite MX2; ring. 2:rewrite MY6; replace (FtoR radix ty) with (FtoR radix y'-FtoR radix hy)%R; auto with real. 2:rewrite MY2; ring. intros Ct2' T; elim T; intros M21 T'; elim T'; intros M22 M23; clear T T'. generalize Boundedt3; intros V. elim V with radix b' s t x' Chx' Ctx' y' Chy' Cty' r' (Fminus radix (Fmult x' y') r'); auto with zarith real; clear V. 2: fold FtoRradix; rewrite Hy';rewrite Hx'; auto. 2:rewrite Fminus_correct; auto with zarith; rewrite Fmult_correct; auto with zarith; ring. 2:rewrite MX6; rewrite MX3; exact MX2. 2:rewrite MY6; rewrite MY3; exact MY2. 2:rewrite MX6; replace (FtoR radix tx) with (FtoR radix x'-FtoR radix hx)%R; auto with real. 2:rewrite MX2; ring. 2:rewrite MY6; replace (FtoR radix ty) with (FtoR radix y'-FtoR radix hy)%R; auto with real. 2:rewrite MY2; ring. intros Ct3' T; elim T; intros M31 T'; elim T'; intros M32 M33; clear T T'. generalize Boundedt4_aux; intros V. elim V with radix b' s t x' Chx' Ctx' y' Chy' Cty' r' ; auto with zarith real; clear V. 2: fold FtoRradix; rewrite Hy';rewrite Hx'; auto. 2:rewrite MX6; rewrite MX3; exact MX2. 2:rewrite MY6; rewrite MY3; exact MY2. intros Ct4' T; elim T; intros M41 T'; elim T'; intros M42 M43; clear T T'. elim Boundedx1y1_aux with radix b' s t x' Chx' y' Chy'; auto with zarith. intros Cx1y1' T; elim T; intros O1 T'; elim T'; intros O2 O3 ; clear T T'. elim Boundedx1y2_aux with radix b' s t x' Chx' y' Cty'; auto with zarith. intros Cx1y2' T; elim T; intros O4 T'; elim T'; intros O5 O6; clear T T'. elim Boundedx2y1_aux with radix b' s t x' Ctx' y' Chy'; auto with zarith. intros Cx2y1' T; elim T; intros O7 T'; elim T'; intros O8 O9; clear T T'. assert (tmp:forall (f:float) (i:nat), (i <= t) -> (Fbounded (Bound (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (i))))) (dExp b')) f) -> (Fbounded b' f)). intros f i J1 J2; elim J2; intros J3 J4; split; auto with zarith. apply Z.lt_le_trans with (1:=J3). apply Z.le_trans with (Zpower_nat radix i);[idtac|unfold b'; simpl; rewrite pGivesBound; auto with zarith]. simpl. apply Z.le_trans with (Z_of_nat (nat_of_P (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (i))))))). unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with zarith. rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith. rewrite Nat.lt_succ_pred with 0 (Z.abs_nat (Zpower_nat radix (i))); auto with zarith. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply Zpower_NR0; auto with zarith. cut ( 0 < Z.abs_nat (Zpower_nat radix (i)))%Z; auto with zarith. simpl; rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply Zpower_nat_less; lia. apply Zpower_NR0; lia. apply Zpower_nat_monotone_le; lia. elim Boundedx2y2 with radix b' t x' y' p q Chx' Ctx' p' q' Chy' Cty'; auto with zarith. 2: fold FtoRradix; rewrite Hx'; auto. 2: fold FtoRradix; rewrite Hx'; auto. 2:apply ClosestCompatible with (1:=H6); auto. 2:apply tmp with (t-s); auto with zarith. 2:apply ClosestCompatible with (1:=H7); auto with real. 2: fold FtoRradix; rewrite Hx'; auto with real. 2:apply tmp with s; auto with zarith. 2: fold FtoRradix; rewrite Hy'; auto. 2: fold FtoRradix; rewrite Hy'; auto. 2:apply ClosestCompatible with (1:=H10); auto. 2:apply tmp with (t-s); auto with zarith. 2:fold FtoRradix; rewrite Hy'; apply ClosestCompatible with (1:=H11); auto with real. 2:apply tmp with s; auto with zarith. intros Cx2y2' T; elim T; intros O10 T'; elim T'; intros O11 O12; clear T T' tmp. assert (ZZ:RoundedModeP b' radix (Closest b' radix)). apply ClosestRoundedModeP with t; auto with zarith. assert (K1':FtoRradix x1y1'=Cx1y1'). unfold FtoRradix; apply sym_eq; apply RoundedModeProjectorIdemEq with b' t (Closest b' radix); auto with zarith. rewrite O1; rewrite MY3; rewrite MX3; auto. assert (K1:FtoRradix Ct1'=t1'). unfold FtoRradix; apply RoundedModeProjectorIdemEq with b' t (Closest b' radix); auto with zarith. rewrite M11; replace (FtoR radix Chx' * FtoR radix Chy')%R with (FtoRradix x1y1'); auto. rewrite <- O1; auto. assert (K2':FtoRradix x1y2'=Cx1y2'). unfold FtoRradix; apply sym_eq; apply RoundedModeProjectorIdemEq with b' t (Closest b' radix); auto with zarith. rewrite O4; rewrite MY6; rewrite MX3; auto. assert (K2:FtoRradix Ct2'=t2'). unfold FtoRradix; apply RoundedModeProjectorIdemEq with b' t (Closest b' radix); auto with zarith. rewrite M21; rewrite <- M11; fold FtoRradix; rewrite K1. replace (Chx' * Cty')%R with (FtoRradix x1y2'); auto. unfold FtoRradix; rewrite <- O4; auto. assert (K3':FtoRradix x2y1'=Cx2y1'). unfold FtoRradix; apply sym_eq; apply RoundedModeProjectorIdemEq with b' t (Closest b' radix); auto with zarith. rewrite O7; rewrite MY3; rewrite MX6; auto. assert (K3:FtoRradix Ct3'=t3'). unfold FtoRradix; apply RoundedModeProjectorIdemEq with b' t (Closest b' radix); auto with zarith. rewrite M31; rewrite <- M21; fold FtoRradix; rewrite K2. replace (Ctx' * Chy')%R with (FtoRradix x2y1'); auto. unfold FtoRradix; rewrite <- O7; auto. assert (K4':FtoRradix x2y2'=Cx2y2'). unfold FtoRradix; apply sym_eq; apply RoundedModeProjectorIdemEq with b' t (Closest b' radix); auto with zarith. rewrite O10; rewrite MX6; rewrite MY6; auto. assert (K4:FtoRradix Ct4'=t4'). unfold FtoRradix; apply RoundedModeProjectorIdemEq with b' t (Closest b' radix); auto with zarith. rewrite M41; rewrite <- M31; fold FtoRradix; rewrite K3. replace (Ctx' * Cty')%R with (FtoRradix x2y2'); auto. unfold FtoRradix; rewrite <- O10; auto. rewrite <- K4. cut (Underf_Err b radix b' t4 Ct4' (t3-x2y2)%R (11/4)). unfold FtoRradix; intros G; elim G; intros G1 G2; elim G2; intros G3 G4; elim G4; auto with real. replace (11/4)%R with (9/4+/2)%R; [idtac|field; apply prod_neq_R0; auto with real; apply prod_neq_R0; auto with real]. unfold FtoRradix; apply Underf_Err3_bis with t Ct3' Cx2y2' (t2-x2y1)%R (tx*ty)%R; auto with zarith. replace (9/4)%R with (7/4+/2)%R;[idtac| field; apply prod_neq_R0; auto with real; apply prod_neq_R0; auto with real]. unfold FtoRradix; apply Underf_Err3_bis with t Ct2' Cx2y1' (t1-x1y2)%R (tx*hy)%R; auto with zarith. replace (7/4)%R with (5/4+/2)%R;[idtac| field; apply prod_neq_R0; auto with real; apply prod_neq_R0; auto with real]. unfold FtoRradix; apply Underf_Err3_bis with t Ct1' Cx1y2' (r-x1y1)%R (hx*ty)%R; auto with zarith. replace (5/4)%R with ((3/4)+/2)%R;[idtac| field; apply prod_neq_R0; auto with real; apply prod_neq_R0; auto with real]. unfold FtoRradix; apply Underf_Err3_bis with t r' Cx1y1' (x*y)%R (hx*hy)%R; auto with zarith. cut (hx*hy=FtoRradix Cx1y1')%R. intros P; rewrite P; unfold FtoRradix; apply Underf_Err1 with t; auto with zarith. fold FtoRradix; rewrite <- P; auto. rewrite <- K1'; unfold FtoRradix; rewrite <- MX3; rewrite <- MY3; rewrite <- O1; auto. apply Rmult_le_reg_l with (IZR 4); auto with real zarith; simpl. apply Rle_trans with (IZR 5);[simpl; right; field; auto with real|idtac]. repeat apply prod_neq_R0; auto with real. apply Rle_trans with (IZR 28); [auto with real zarith|simpl; right; ring]. rewrite M11; rewrite <- O1; auto with real. rewrite M13; apply rExp with radix b' s; auto. fold FtoRradix; rewrite Hx'; rewrite Hy'; auto. cut (hx*ty=FtoRradix Cx1y2')%R. intros P; rewrite P; unfold FtoRradix; apply Underf_Err1 with t; auto with zarith. fold FtoRradix; rewrite <- P; auto. unfold FtoRradix; rewrite O4; rewrite MX3; rewrite MY6; auto with real. apply Rmult_le_reg_l with (IZR 4); auto with real zarith; simpl. apply Rle_trans with (IZR 7);[simpl; right; field; auto with real|idtac]. repeat apply prod_neq_R0; auto with real. apply Rle_trans with (IZR 28); [auto with real zarith|simpl; right; ring]. rewrite M21; rewrite M11; rewrite O4; ring. cut (tx*hy=FtoRradix Cx2y1')%R. intros P; rewrite P; unfold FtoRradix; apply Underf_Err1 with t; auto with zarith. fold FtoRradix; rewrite <- P; auto. unfold FtoRradix; rewrite O7; rewrite MX6; rewrite MY3; auto with real. apply Rmult_le_reg_l with (IZR 4); auto with real zarith; simpl. apply Rle_trans with (IZR 9);[simpl; right; field; auto with real|idtac]. repeat apply prod_neq_R0; auto with real. apply Rle_trans with (IZR 28); [auto with real zarith|simpl; right; ring]. rewrite M21; rewrite M31; rewrite O7; ring. cut (tx*ty=FtoRradix Cx2y2')%R. intros P; rewrite P; unfold FtoRradix; apply Underf_Err1 with t; auto with zarith. fold FtoRradix; rewrite <- P; auto. unfold FtoRradix; rewrite O10; rewrite MX6; rewrite MY6; auto with real. apply Rmult_le_reg_l with (IZR 4); auto with real zarith; simpl. apply Rle_trans with (IZR 11);[simpl; right; field; auto with real|idtac]. repeat apply prod_neq_R0; auto with real. apply Rle_trans with (IZR 28); [auto with real zarith|simpl; right; ring]. rewrite M41; rewrite M31; rewrite O10; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz