proposition: Theorem DekkerS2: (radix=2)%Z \/ (Nat.Even t) -> (x*y=r-t4)%R.
proof: Proof. intros H; unfold FtoRradix. case (Req_dec 0%R x); intros Ny. cut (FtoRradix r=0)%R;[intros Z1|idtac]. cut (FtoRradix t4=0)%R;[intros Z2|idtac]. 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. right; auto. elim Veltkamp with radix b s t x p q hx; auto. 2: unfold s; apply SLe; auto. 2: unfold s; apply SGe; auto. 2: elim Cx; 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. elim bimplybplusNorm with radix b s t x; auto. 2: unfold s; apply SLe; auto. 2: unfold s; apply SGe; auto. 2: elim Cx; auto. intros xx T; elim T; intros X1 X2; clear T. rewrite <- X1. assert (Fnormal radix (plusExp t b) y). elim Cy; intros F1 F2; elim F1; intros. split;[split|idtac]; unfold plusExp; simpl; lia. assert (- dExp (plusExp t b) <= Fexp xx + Fexp y)%Z. elim X2; intros F1 F2; elim F1; intros. assert (0 <= Fexp y)%Z; auto with zarith. apply Zplus_le_reg_l with (Fexp x). apply Z.le_trans with (2:=Expoxy). elim Cx; intros F1' F2'; elim F2'; auto with zarith. assert (Closest (plusExp t b) radix (FtoR radix y * (powerRZ radix (t - Nat.div2 t)%nat + 1)) p'). cut (FtoR radix y * (powerRZ radix (t - Nat.div2 t)%nat + 1) = (FtoRradix (Fmult y (Float (Zpower_nat radix (t - Nat.div2 t)%nat + 1) 0))))%R. intros K'; rewrite K'. unfold FtoRradix; apply Closestbbplus with 2 t; auto with zarith. unfold Fmult; simpl. assert (K:Fbounded b y);[elim Cy; auto|elim K; auto with zarith]. fold FtoRradix; rewrite <- K'; auto with real. unfold FtoRradix; rewrite Fmult_correct; auto. unfold FtoR; simpl; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; simpl; ring. assert (Closest (plusExp t b) radix (FtoR radix y - FtoR radix p') q'). rewrite <- Fminus_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fminus; simpl; apply Zmin_Zle. assert (K:Fbounded b y);[elim Cy; auto|elim K; auto with zarith]. assert (K:Fbounded b p');[elim B1; auto|elim K; auto with zarith]. rewrite Fminus_correct; auto. assert (Closest (plusExp t b) radix (FtoR radix q' + FtoR radix p') hy). rewrite <- Fplus_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fplus; simpl; apply Zmin_Zle. assert (K:Fbounded b q');[elim B2; auto|elim K; auto with zarith]. assert (K:Fbounded b p');[elim B1; auto|elim K; auto with zarith]. rewrite Fplus_correct; auto. assert (Closest (plusExp t b) radix (FtoR radix y - FtoR radix hy) ty). rewrite <- Fminus_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fminus; simpl; apply Zmin_Zle. assert (K:Fbounded b y);[elim Cy; auto|elim K; auto with zarith]. assert (K:Fbounded b hy);[elim B3; auto|elim K; auto with zarith]. rewrite Fminus_correct; auto. assert (Closest (plusExp t b) radix (FtoR radix xx * (powerRZ radix (t - Nat.div2 t)%nat + 1)) p). rewrite X1; cut (FtoR radix x * (powerRZ radix (t - Nat.div2 t)%nat + 1) = (FtoRradix (Fmult x (Float (Zpower_nat radix (t - Nat.div2 t)%nat + 1) 0))))%R. intros K'; rewrite K'. unfold FtoRradix; apply Closestbbplus with 2 t; auto with zarith. unfold Fmult; simpl. assert (K:Fbounded b x);[elim Cx; auto|elim K; auto with zarith]. fold FtoRradix; rewrite <- K'; auto with real. unfold FtoRradix; rewrite Fmult_correct; auto. unfold FtoR; simpl; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; simpl; ring. assert (Closest (plusExp t b) radix (FtoR radix xx - FtoR radix p) q). rewrite X1; rewrite <- Fminus_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fminus; simpl; apply Zmin_Zle. assert (K:Fbounded b x);[elim Cx; auto|elim K; auto with zarith]. assert (K:Fbounded b p);[elim A1; auto|elim K; auto with zarith]. rewrite Fminus_correct; auto. assert (Closest (plusExp t b) radix (FtoR radix q + FtoR radix p) hx). rewrite <- Fplus_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fplus; simpl; apply Zmin_Zle. assert (K:Fbounded b q);[elim A2; auto|elim K; auto with zarith]. assert (K:Fbounded b p);[elim A1; auto|elim K; auto with zarith]. rewrite Fplus_correct; auto. assert (Closest (plusExp t b) radix (FtoR radix xx - FtoR radix hx) tx). rewrite X1; rewrite <- Fminus_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fminus; simpl; apply Zmin_Zle. assert (K:Fbounded b x);[elim Cx; auto|elim K; auto with zarith]. assert (K:Fbounded b hx);[elim A3; auto|elim K; auto with zarith]. rewrite Fminus_correct; auto. generalize VeltkampU; intros V. elim V with radix b s t y p' q' hy ty; auto. 2: unfold s; apply SLe; auto. 2: unfold s; apply SGe; auto. 2: left; auto. intros M1 T; elim T; intros M2 T'; elim T'; intros T1 T2; clear T T'. elim T1; intros hy' T1'; elim T1'; intros M3 T; elim T; intros M4 T'; clear T1 T1' T. lapply T'; auto; intros M5; clear T'. elim T2; intros ty' T1'; elim T1'; intros M6 T; elim T; intros M7 M8; clear T2 T1' T V. elim Veltkamp_tail with radix b s t x p q hx tx; auto. 2: unfold s; apply SLe; auto. 2: unfold s; apply SGe; auto. 2: elim Cx; auto. intros tx' T1'; elim T1'; intros N5 T; elim T; intros N7 T'; elim T'; intros N8 N9; clear T1' T T'. rewrite FcanonicFnormalizeEq in N9; auto with zarith;[idtac|right; auto]. assert (Fexp x <= Fexp hx)%Z. elim Cx; intros T1 T2; elim T2; intros T3 T4; rewrite T3. elim A3; intros G1 G2; elim G1; auto. apply DekkerN with (plusExp t b) t p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 t1 t2 t3; auto. rewrite <- M3. rewrite <- Fmult_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fmult; simpl; auto with zarith. rewrite Fmult_correct; auto with real; rewrite M3; auto. rewrite <- M6. rewrite <- Fmult_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fmult; simpl; auto with zarith. rewrite Fmult_correct; auto with real; rewrite M6; auto. rewrite <- M3; rewrite <- N5. rewrite <- Fmult_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fmult; simpl; auto with zarith. rewrite Fmult_correct; auto with real; rewrite M3; rewrite N5; auto. rewrite <- M6; rewrite <- N5. rewrite <- Fmult_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fmult; simpl; auto with zarith. rewrite Fmult_correct; auto with real; rewrite M6; rewrite N5; auto. rewrite X1. rewrite <- Fmult_correct; auto. apply Closestbbplus with 2 t; auto with zarith. rewrite Fmult_correct; auto with real. rewrite <- Fminus_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fminus; simpl; apply Zmin_Zle. assert (K:Fbounded b r);[elim D1; auto|elim K; auto with zarith]. assert (K:Fbounded b x1y1);[elim C1; auto|elim K; auto with zarith]. rewrite Fminus_correct; auto. rewrite <- Fminus_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fminus; simpl; apply Zmin_Zle. assert (K:Fbounded b t1);[elim D2; auto|elim K; auto with zarith]. assert (K:Fbounded b x1y2);[elim C2; auto|elim K; auto with zarith]. rewrite Fminus_correct; auto. rewrite <- Fminus_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fminus; simpl; apply Zmin_Zle. assert (K:Fbounded b t2);[elim D3; auto|elim K; auto with zarith]. assert (K:Fbounded b x2y1);[elim C3; auto|elim K; auto with zarith]. rewrite Fminus_correct; auto. rewrite <- Fminus_correct; auto. apply Closestbbplus with 2 t; auto with zarith. unfold Fminus; simpl; apply Zmin_Zle. assert (K:Fbounded b t3);[elim D4; auto|elim K; auto with zarith]. assert (K:Fbounded b x2y2);[elim C4; auto|elim K; auto with zarith]. rewrite Fminus_correct; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz