proposition: Theorem Dekker_aux: (exists x':float, (FtoRradix x'=tx*ty)%R /\ (Fbounded b x')) -> (x*y=r-t4)%R.
proof: Proof. intros L1. generalize SLe; intros Sle; generalize SGe; intros Sge. generalize s2Le; intros s2le; generalize s2Ge; intros s2ge. generalize VeltkampU; intros V. elim V with radix b s t x p q hx tx; auto. 2: left; auto. intros MX1 T; elim T; intros MX2 T'; clear T; elim T'; intros T1 T2; clear T'. elim T1; intros hx' 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 tx' 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. intros MY1 T; elim T; intros MY2 T'; clear T; elim T'; intros T1 T2; clear T'. elim T1; intros hy' 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 ty' 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 hx' tx' y hy' ty' r (Fminus radix (Fmult x y) r); auto with zarith real; clear V. 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 t1' 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 hx' tx' y hy' ty' r (Fminus radix (Fmult x y) r); auto with zarith real; clear V. 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 t2' 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 hx' tx' y hy' ty' r (Fminus radix (Fmult x y) r); auto with zarith real; clear V. 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 t3' T; elim T; intros M31 T'; elim T'; intros M32 M33; clear T T'. generalize Boundedt4; intros V. elim V with radix b s t x hx' tx' y hy' ty' r ; auto with zarith real; clear V. 2:rewrite MX6; rewrite MX3; exact MX2. 2:rewrite MY6; rewrite MY3; exact MY2. intros t4' T; elim T; intros M41 M42; clear T. cut (FtoRradix t4=r-x*y)%R; auto with real. intros V; rewrite V; ring. apply sym_eq. apply trans_eq with (FtoRradix t4'). unfold FtoRradix; rewrite M41; rewrite MX2; rewrite MY2. rewrite MX3; rewrite MX6; rewrite MY3; rewrite MY6; ring. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. replace (FtoR radix t4') with (t3 - x2y2)%R; auto. replace (FtoRradix t3) with (FtoRradix t3'). replace (FtoRradix x2y2) with (tx*ty)%R. unfold FtoRradix; rewrite M31; rewrite M41. rewrite <- MY6; rewrite <- MX6; ring. elim L1; intros v T; elim T; intros L2 L3. rewrite <- L2; unfold FtoRradix. apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. replace (FtoR radix v) with (tx*ty)%R; auto with real. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. replace (FtoR radix t3') with (t2-x2y1)%R; auto with real. replace (FtoRradix t2) with (FtoRradix t2'). replace (FtoRradix x2y1) with (tx*hy)%R. unfold FtoRradix; rewrite M21; rewrite M31. rewrite <- MX6; rewrite <- MY3; ring. elim Boundedx2y1 with radix b s t x tx' y hy'; auto with zarith. intros v T; elim T; intros L2 L3. apply trans_eq with (FtoR radix v). unfold FtoRradix; rewrite L2; rewrite MX6; rewrite MY3; ring. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. replace (FtoR radix v) with (tx*hy)%R; auto with real. unfold FtoRradix; rewrite L2; rewrite MX6; rewrite MY3; ring. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. replace (FtoR radix t2') with (t1-x1y2)%R; auto with real. replace (FtoRradix t1) with (FtoRradix t1'). replace (FtoRradix x1y2) with (hx*ty)%R. unfold FtoRradix; rewrite M21; rewrite M11. rewrite <- MX3; rewrite <- MY6; ring. elim Boundedx1y2 with radix b s t x hx' y ty'; auto with zarith. intros v T; elim T; intros L2 L3; clear T. apply trans_eq with (FtoR radix v). unfold FtoRradix; rewrite L2; rewrite MY6; rewrite MX3; ring. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. replace (FtoR radix v) with (hx*ty)%R; auto with real. unfold FtoRradix; rewrite L2; rewrite MY6; rewrite MX3; ring. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. replace (FtoR radix t1') with (r-x1y1)%R; auto with real. replace (FtoRradix x1y1) with (hx*hy)%R. unfold FtoRradix; rewrite M11; rewrite MY3; rewrite MX3; ring. elim Boundedx1y1 with radix b s t x hx' y hy'; auto with zarith. intros v T; elim T; intros L2 L3; clear T. apply trans_eq with (FtoR radix v). unfold FtoRradix; rewrite L2; rewrite MY3; rewrite MX3; ring. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. replace (FtoR radix v) with (hx*hy)%R; auto with real. unfold FtoRradix; rewrite L2; rewrite MY3; rewrite MX3; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz