proposition: Lemma Veltkamp_pos: forall x p q hx:float, Fnormal radix b x -> Fcanonic radix b p -> Fcanonic radix b q -> (0 < x)%R -> (Closest b radix (x*((powerRZ radix s)+1))%R p) -> (Closest b radix (x-p)%R q) -> (Closest b radix (q+p)%R hx) -> (Rabs (x-hx) <= (powerRZ radix (s+Fexp x)) /2)%R /\ (exists hx':float, (FtoRradix hx'=hx) /\ (Closest b' radix x hx') /\ (s+Fexp x <= Fexp hx')%Z).
proof: Proof. intros x p q hx Nx Cp Cq; intros. unfold FtoRradix, b'; apply Veltkamp_aux with p q; auto. elim Nx; auto. case Cp; auto; intros T. absurd (p < (firstNormalPos radix b t))%R. apply Rle_not_lt; generalize ClosestMonotone; unfold MonotoneP; intros H3. unfold FtoRradix; apply H3 with b (firstNormalPos radix b t) (x * (powerRZ radix s + 1))%R; auto. apply Rle_lt_trans with x. unfold FtoRradix; apply FnormalLtFirstNormalPos; auto with zarith real. apply Rle_lt_trans with (x*1)%R; auto with real. apply Rmult_lt_compat_l; auto with real zarith. apply Rle_lt_trans with (0+1)%R; auto with real zarith. apply Rplus_lt_compat_r. apply powerRZ_lt; try apply IZR_lt; auto with zarith. unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b). apply ClosestRoundedModeP with t; auto with zarith. generalize firstNormalPosNormal; intros H4. elim H4 with radix b t; auto with zarith. unfold FtoRradix; apply FsubnormalLtFirstNormalPos; auto with zarith. apply pPos with b s t x; auto. rewrite <- Fopp_Fopp; apply FnormalFop. cut (Fcanonic radix b (Fopp q));[intros T'|apply FcanonicFopp; auto]. case T'; auto; intros T. absurd (Fopp q < (firstNormalPos radix b t))%R. apply Rle_not_lt; generalize ClosestMonotone; unfold MonotoneP; intros H3. unfold FtoRradix; apply H3 with b (firstNormalPos radix b t) (-(x-p))%R; auto. apply Rle_lt_trans with x. unfold FtoRradix; apply FnormalLtFirstNormalPos; auto with zarith real. apply Rplus_lt_reg_r with (FtoRradix x). apply Rle_lt_trans with ((IZR 2)*x)%R;[right; simpl; ring| idtac]. apply Rle_lt_trans with (radix*x)%R;auto with real zarith. apply Rmult_le_compat_r; try apply IZR_le; auto with real zarith. apply Rlt_le_trans with (radix*(radix*x))%R. apply Rle_lt_trans with (1*(radix*x))%R; auto with real zarith. apply Rmult_lt_compat_r; auto with real zarith. apply Rmult_lt_0_compat; auto with real zarith. apply IZR_lt; lia. apply IZR_lt; lia. apply Rle_trans with (FtoRradix p);[idtac|right; ring]. apply Rle_trans with (FtoRradix (Float (Fnum x) (Fexp x+2))). unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add; simpl. right; ring. apply IZR_neq; lia. unfold FtoRradix; apply H3 with b (Float (Fnum x) (Fexp x + 2)) (x * (powerRZ radix s + 1))%R; auto. apply Rle_lt_trans with (x * (powerRZ radix 2))%R. unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add. auto with real. apply IZR_neq; lia. apply Rmult_lt_compat_l; auto with real zarith. apply Rle_lt_trans with (powerRZ radix s+0)%R; auto with real zarith. apply Rle_trans with (powerRZ radix s)%R; auto with real zarith. apply Rle_powerRZ; try apply IZR_le; auto with zarith real. unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b). apply ClosestRoundedModeP with t; auto with zarith. elim Nx; intros T1 T2; elim T1; intros. split; simpl; auto with zarith. unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b). apply ClosestRoundedModeP with t; auto with zarith. generalize firstNormalPosNormal; intros H4. elim H4 with radix b t; auto with zarith. apply ClosestOpp; auto. unfold FtoRradix; apply FsubnormalLtFirstNormalPos; auto with zarith. rewrite Fopp_correct; cut (q <= 0)%R; auto with real. unfold FtoRradix; apply qNeg with b s t p x; auto. elim Nx; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz