proposition: Lemma VeltkampEvenN_aux: forall x p q hx:float, Fnormal radix b x -> Fcanonic radix b p -> Fcanonic radix b q -> (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 Nx Cp Cq; intros. case (Rle_or_lt 0%R x); intros H2. case H2; clear H2; intros H2. apply VeltkampEven_pos with p q; auto. 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 <- H2; 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 <- H2; rewrite FzeroisZero; ring. rewrite <- H2; 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. elim VeltkampEven_pos with (Fopp x) (Fopp p) (Fopp q) (Fopp hx). intros v T; elim T; intros; clear T. exists (Fopp v); split. unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix; rewrite H3. unfold FtoRradix; rewrite Fopp_correct; ring. replace (FtoRradix x) with (-(Fopp x))%R. apply EvenClosestSymmetric; auto with zarith. unfold FtoRradix; rewrite Fopp_correct; ring. apply FnormalFop; auto. apply FcanonicFopp; auto. apply FcanonicFopp; auto. unfold FtoRradix; rewrite Fopp_correct; auto with real. replace (Fopp x * (powerRZ radix s + 1))%R with (-(x * (powerRZ radix s + 1)))%R. apply EvenClosestSymmetric; auto with zarith. unfold FtoRradix; rewrite Fopp_correct; ring. replace (Fopp x - Fopp p)%R with (-(x-p))%R;[apply EvenClosestSymmetric; auto with zarith|idtac]. unfold FtoRradix; repeat rewrite Fopp_correct; ring. replace (Fopp q + Fopp p)%R with (-(q+p))%R;[apply EvenClosestSymmetric; auto with zarith|idtac]. unfold FtoRradix; repeat rewrite Fopp_correct; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz