proposition: Lemma VeltkampEvenS: forall x p q hx:float, Fsubnormal radix b x -> (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p) -> (EvenClosest b radix t (x-p)%R q) -> (EvenClosest b radix t (q+p)%R hx) -> (exists hx':float, (FtoRradix hx'=hx) /\ (EvenClosest b' radix (t-s) x hx')).
proof: Proof. intros x p q hx Sx pDef qDef hxDef. case (Req_dec 0%R x); intros Y. exists (Fzero (-(dExp b'))). split. cut (FtoR radix p=(Fzero (-(dExp b))))%R; [intros I1|idtac]. cut (FtoR radix q=(Fzero (-(dExp b))))%R; [intros I2|idtac]. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (EvenClosest b radix t); auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. unfold b'; simpl; apply FboundedFzero. replace (FtoR radix (Fzero (- dExp b'))) with (q+p)%R; auto. unfold FtoRradix; rewrite I1; rewrite I2; unfold FtoRradix. repeat rewrite FzeroisZero; ring. apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (EvenClosest b radix t); auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. apply FboundedFzero. replace (FtoR radix (Fzero (- dExp b))) with (x -p)%R; auto. rewrite <- Y; unfold FtoRradix; rewrite I1; unfold FtoRradix. repeat rewrite FzeroisZero; ring. apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (EvenClosest b radix t); auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. apply FboundedFzero. replace (FtoR radix (Fzero (- dExp b))) with (x * (powerRZ radix s + 1))%R; auto. rewrite <- Y; rewrite FzeroisZero; ring. rewrite <- Y; rewrite <- FzeroisZero with radix b'. apply RoundedModeProjectorIdem with (P:=(EvenClosest b' radix (t-s))) (b:=b'). apply EvenClosestRoundedModeP; auto with zarith. unfold b'; apply p'GivesBound; auto. apply FboundedFzero. lapply (bimplybplusNorm x);[intros T|elim Sx; auto]. lapply T; clear T; [intros T; elim T; intros x' T'; elim T'; intros x'Eq Nx'; clear T T'|auto with real]. generalize VeltkampEvenN; intros. elim H with radix (plusExp b) s t x' p q hx; auto with zarith; clear H. intros f H; elim H; intros; clear H. cut (EvenClosest (plusExp b') radix (t-s) x f);[clear H1; intros H1|idtac]. case (Zle_or_lt (-(dExp b)) (Fexp f)); intros H2. cut (Fbounded b' f);[intros H3|idtac]. exists f; split;auto with real. apply EvenClosestbplusb; auto with zarith. unfold b'; apply p'GivesBound; auto. unfold b'; simpl; elim Sx; intros J1 J2; elim J1; auto. split; [idtac|unfold b'; simpl; auto]. elim H1; intros J1 J2; elim J1; intros J3 J4; elim J3; auto with zarith. generalize RoundedModeRep; intros T. elim T with (plusExp b') radix (t-s) (Closest (plusExp b') radix) x f; auto with zarith. clear T;intros m H3. cut (Fbounded b' (Float m (Fexp x)));[intros H4|idtac]. exists (Float m (Fexp x)); split. unfold FtoRradix; rewrite <- H3; rewrite H0; auto with real. apply EvenClosestbplusb; auto with zarith. unfold b'; apply p'GivesBound; auto. unfold b'; simpl; elim Sx; intros J1 J2; elim J1; auto. generalize EvenClosestCompatible; unfold CompatibleP; intros C. apply C with x f; auto with real zarith; clear C. rewrite <- p'GivesBound with radix b s t; auto; unfold plusExp, b'; simpl; auto. elim H4; intros; split; try easy; auto with zarith. cut (forall (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z). intros T; simpl; rewrite <- T. apply Z.le_trans with (2 := H5). apply Z.le_trans with (-(dExp b') + Zneg (P_of_succ_nat (pred (pred t))))%Z. apply Zeq_le; ring_simplify; easy. lia. intros;unfold Nplus. case x0; auto with zarith. unfold b'; simpl; auto with zarith. split. apply Z.le_lt_trans with (Z.abs (Fnum f)). apply Z.le_trans with ((Z.abs m)*1)%Z; auto with zarith. simpl; auto with zarith. apply Z.le_trans with ((Z.abs m)*(Zpower_nat radix (Z.abs_nat (Fexp x-Fexp f))))%Z. apply Zmult_le_compat_l; auto with zarith. apply Zpower_NR1; lia. replace (Fnum f) with (m*Zpower_nat radix (Z.abs_nat (Fexp x - Fexp f)))%Z. rewrite Zabs_Zmult; rewrite (Z.abs_eq (Zpower_nat radix (Z.abs_nat (Fexp x - Fexp f)))); auto with zarith. apply Zpower_NR0; lia. apply eq_IZR; rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ. apply Rmult_eq_reg_l with (powerRZ radix (Fexp f)); auto with real zarith. apply trans_eq with (FtoR radix f);[rewrite H3|unfold FtoR; ring]. unfold FtoR; simpl. apply trans_eq with (m*(powerRZ radix (Fexp f)*powerRZ radix (Z.abs_nat (Fexp x - Fexp f))))%R;[ring|idtac]. rewrite <- powerRZ_add. replace (Fexp f + Z.abs_nat (Fexp x - Fexp f))%Z with (Fexp x);[ring|idtac]. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. elim Sx; intros J1 J2; elim J1; intros; auto with zarith. apply IZR_neq; lia. apply Rgt_not_eq, powerRZ_lt, IZR_lt; lia. elim H1; intros J1 J2; elim J1; intros J3 J4; elim J3; unfold plusExp; simpl; auto with zarith. elim Sx; intros J1 J2; elim J1; intros ; unfold b'; simpl; auto. rewrite <- p'GivesBound with radix b s t; unfold plusExp, b'; simpl; auto with zarith. apply ClosestRoundedModeP with (t-s); auto with zarith. rewrite <- p'GivesBound with radix b s t; unfold plusExp, b'; simpl; auto with zarith. elim H1; auto. rewrite <- x'Eq; unfold FtoRradix;auto with zarith. replace (FtoR radix x' * (powerRZ radix s + 1))%R with (FtoRradix (Fplus radix x (Float (Fnum x) (s+Fexp x)%Z))). apply EvenClosestbbplus; auto with zarith. unfold Fplus; simpl;apply Zmin_Zle. elim Sx; intros J1 J2; elim J1; auto. elim Sx; intros J1 J2; elim J1; auto with zarith. replace (FtoRradix (Fplus radix x (Float (Fnum x) (s + Fexp x)))) with (x * (powerRZ radix s + 1))%R; auto with real. unfold FtoRradix; rewrite Fplus_correct; auto. unfold FtoR; simpl; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; ring. fold FtoRradix; rewrite x'Eq; unfold FtoRradix; rewrite Fplus_correct; auto. unfold FtoR; simpl; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; ring. unfold FtoRradix in x'Eq; rewrite x'Eq; rewrite <- Fminus_correct; auto. apply EvenClosestbbplus; auto with zarith. unfold Fplus; simpl;apply Zmin_Zle. elim Sx; intros J1 J2; elim J1; auto. elim pDef; intros J1 J2; elim J1; intros J3 J4; elim J3; auto with zarith. replace (FtoRradix (Fminus radix x p)) with (x -p)%R; auto with real. unfold FtoRradix; rewrite Fminus_correct; auto with real. rewrite <- Fplus_correct; auto. apply EvenClosestbbplus; auto with zarith. unfold Fplus; simpl;apply Zmin_Zle. elim qDef; intros J1 J2; elim J1; intros J3 J4; elim J3; auto. elim pDef; intros J1 J2; elim J1; intros J3 J4; elim J3; auto with zarith. replace (FtoRradix (Fplus radix q p)) with (q +p)%R; auto with real. unfold FtoRradix; rewrite Fplus_correct; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz