Library Float.Others.discriminant2
This proof file has been written by
Sylvie Boldo(1), following a proof
presented by Pr William Kahan (2),
and adapted to Coq proof checker with the help of
Guillaume Melquiond(1)
and Marc Daumas(1). This work
has been partially supported by the CNRS grant PICS 2533.
(1) LIP Computer science laboratory UMR 5668 CNRS - ENS de Lyon - INRIA Lyon, France
(2) University of California at Berkeley Berkeley, California
(1) LIP Computer science laboratory UMR 5668 CNRS - ENS de Lyon - INRIA Lyon, France
(2) University of California at Berkeley Berkeley, California
Require Export AllFloat.
Section Discriminant1.
Variable bo : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Theorem TwoMoreThanOne : (1 < radix)%Z.
unfold radix in |- *; red in |- *; simpl in |- *; auto.
Qed.
Hint Resolve TwoMoreThanOne.
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ TwoMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix precision.
Variables a b b' c p q d:float.
Let delta := (Rabs (d-(b*b'-a*c)))%R.
Hypothesis Fa : (Fbounded bo a).
Hypothesis Fb : (Fbounded bo b).
Hypothesis Fb': (Fbounded bo b').
Hypothesis Fc : (Fbounded bo c).
Hypothesis Fp : (Fbounded bo p).
Hypothesis Fq : (Fbounded bo q).
Hypothesis Fd : (Fbounded bo d).
There is no underflow
Hypothesis U1:(- dExp bo <= Fexp d - 1)%Z.
Hypothesis Nd:(Fnormal radix bo d).
Hypothesis Nq:(Fnormal radix bo q).
Hypothesis Np:(Fnormal radix bo p).
Hypothesis Square:(0 <=b*b')%R.
Hypothesis Roundp : (EvenClosest bo radix precision (b*b')%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).
Hypothesis Firstcase : (p+q <= 3*(Rabs (p-q)))%R.
Hypothesis Roundd : (EvenClosest bo radix precision (p-q)%R d).
Theorem delta_inf: (delta <= (/2)*(Fulp bo radix precision d)+
((/2)*(Fulp bo radix precision p)+(/2)*(Fulp bo radix precision q)))%R.
unfold delta; rewrite <- Rabs_Ropp.
replace (-(d - (b * b' - a * c)))%R with (((p-q)-d)+((b*b'-p)+-(a*c-q)))%R;[idtac|ring].
apply Rle_trans with ((Rabs ((p-q)-d))+(Rabs (b * b' - p + - (a * c - q))))%R;
[apply Rabs_triang|idtac].
apply Rplus_le_compat.
apply Rmult_le_reg_l with (S (S O)); auto with arith real.
apply Rle_trans with (Fulp bo radix precision d).
unfold FtoRradix; apply ClosestUlp;auto with zarith.
elim Roundd; auto.
right; simpl; field; auto with real.
apply Rle_trans with ((Rabs (b*b'-p))+(Rabs (-(a*c-q))))%R;
[apply Rabs_triang|idtac].
apply Rplus_le_compat.
apply Rmult_le_reg_l with (S (S O)); auto with arith real.
apply Rle_trans with (Fulp bo radix precision p).
unfold FtoRradix; apply ClosestUlp;auto with zarith.
elim Roundp; auto.
right; simpl; field; auto with real.
rewrite Rabs_Ropp; apply Rmult_le_reg_l with (S (S O)); auto with arith real.
apply Rle_trans with (Fulp bo radix precision q).
unfold FtoRradix; apply ClosestUlp;auto with zarith.
elim Roundq; auto.
right; simpl; field; auto with real.
Qed.
Theorem P_positive: (Rle 0 p)%R.
unfold FtoRradix; apply RleRoundedR0 with (b:=bo) (precision:=precision) (P:=(Closest bo radix)) (r:=(b*b')%R); auto.
apply ClosestRoundedModeP with precision; auto.
elim Roundp; auto.
Qed.
Theorem Fulp_le_twice_l: forall x y:float, (0 <= x)%R ->
(Fnormal radix bo x) -> (Fbounded bo y) -> (2*x<=y)%R ->
(2*(Fulp bo radix precision x) <= (Fulp bo radix precision y))%R.
intros.
assert (2*x=(Float (Fnum x) (Zsucc (Fexp x))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum x) (Zsucc (Fexp x)))).
right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto.
unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith.
simpl; ring.
elim H0; intros H4 H5; elim H4; intros.
left; split; auto.
split; simpl; auto with zarith.
apply LeFulpPos; auto with real.
elim H0; intros H4 H5; elim H4; intros;split; simpl; auto with zarith.
fold FtoRradix; rewrite <- H3; apply Rmult_le_pos; auto with real.
fold FtoRradix; rewrite <- H3; auto with real.
Qed.
Theorem Fulp_le_twice_r: forall x y:float, (0 <= x)%R ->
(Fnormal radix bo y) -> (Fbounded bo x) -> (x<=2*y)%R ->
((Fulp bo radix precision x) <= 2*(Fulp bo radix precision y))%R.
intros.
assert (2*y=(Float (Fnum y) (Zsucc (Fexp y))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum y) (Zsucc (Fexp y)))).
2:right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto.
2:unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith.
2:simpl; ring.
2:left; auto.
2:elim H0; intros H6 H5; elim H6; intros.
2:split; auto with zarith.
2:split; simpl; auto with zarith.
apply LeFulpPos; auto with real.
elim H0; intros H6 H5; elim H6; intros;split; simpl; auto with zarith.
fold FtoRradix; rewrite <- H3; auto with real.
Qed.
Theorem Half_Closest_Round: forall (x:float) (r:R),
(- dExp bo <= Zpred (Fexp x))%Z -> (Closest bo radix r x)
-> (Closest bo radix (r/2)%R (Float (Fnum x) (Zpred (Fexp x)))).
intros x r L H.
assert (x/2=(Float (Fnum x) (Zpred (Fexp x))))%R.
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; field.
elim H; intros H2 H3.
split; [split; simpl; auto with float zarith|idtac].
intros.
fold FtoRradix; rewrite <- H0.
replace (x/2-r/2)%R with (/2*(x-r))%R;[idtac|unfold Rdiv; ring].
rewrite Rabs_mult; rewrite Rabs_right; auto with real.
2: apply Rle_ge; auto with real.
replace (f-r/2)%R with (/2*((Float (Fnum f) (Zsucc (Fexp f)))-r))%R.
rewrite Rabs_mult; rewrite Rabs_right with (/2)%R.
2: apply Rle_ge; auto with real.
apply Rmult_le_compat_l; auto with real.
unfold FtoRradix; apply H3.
split; simpl; auto with zarith float.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; field; auto with real.
Qed.
Theorem Twice_EvenClosest_Round: forall (x:float) (r:R),
(-(dExp bo) <= (Fexp x)-1)%Z -> (Fnormal radix bo x)
-> (EvenClosest bo radix precision r x)
-> (EvenClosest bo radix precision (2*r)%R (Float (Fnum x) (Zsucc (Fexp x)))).
intros x r U Nx H.
assert (x*2=(Float (Fnum x) (Zsucc (Fexp x))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring.
elim H; intros H2 H3; elim H2; intros H'1 H'2; split.
split; [split; simpl; auto with float zarith|idtac].
intros.
fold FtoRradix; rewrite <- H0.
replace (x*2-2*r)%R with (2*(x-r))%R;[idtac|unfold Rdiv; ring].
rewrite Rabs_mult; rewrite Rabs_right; auto with real.
2: apply Rle_ge; auto with real.
case (Zle_lt_or_eq (-(dExp bo))%Z (Fexp f)); auto with zarith float; intros L.
replace (f-2*r)%R with (2*((Float (Fnum f) (Zpred (Fexp f)))-r))%R.
rewrite Rabs_mult; rewrite Rabs_right with (2)%R.
2: apply Rle_ge; auto with real.
apply Rmult_le_compat_l; auto with real.
unfold FtoRradix; apply H'2.
split; simpl; auto with zarith float.
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; field; auto with real.
replace (f-2*r)%R with (-((2*r)-f))%R;[rewrite Rabs_Ropp|ring].
apply Rle_trans with (2:=Rabs_triang_inv (2*r)%R f).
rewrite Rabs_mult; rewrite (Rabs_right 2%R); try apply Rle_ge;auto with real.
pattern r at 2 in |-*; replace r with (x-(x-r))%R;[idtac|ring].
apply Rle_trans with (2*(Rabs (x)-Rabs (x-r))-Rabs f)%R;[idtac|unfold Rminus; apply Rplus_le_compat_r; apply Rmult_le_compat_l; auto with real].
2: generalize (Rabs_triang_inv x (x-r)%R); unfold Rminus; auto with real.
apply Rplus_le_reg_l with (Rabs f -2*(Rabs (x-r)))%R.
apply Rle_trans with (Rabs f);[right;ring|idtac].
apply Rle_trans with (2*(Rabs x)-4*Rabs (x-r))%R;[idtac|right;ring].
apply Rle_trans with (((powerRZ radix precision)-1)*(powerRZ radix ((Fexp x)-1)))%R.
unfold FtoRradix; rewrite <- Fabs_correct; auto;unfold Fabs, FtoR; simpl.
apply Rmult_le_compat; auto with real zarith.
apply Rle_trans with (Zpred (Zpower_nat radix precision));[rewrite <- pGivesBound|idtac].
apply Rle_IZR;apply Zle_Zpred; auto with float.
unfold Zpred; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
rewrite <- L; apply Rle_powerRZ; auto with real zarith.
apply Rle_trans with (2*(powerRZ radix (Zpred precision))*(powerRZ radix (Fexp x))-2*(powerRZ radix (Fexp x)))%R.
apply Rle_trans with (((powerRZ radix (precision+1))-4)*(powerRZ radix (Fexp x-1)))%R;[apply Rmult_le_compat_r; auto with real zarith|idtac].
rewrite powerRZ_add; auto with real zarith; simpl.
apply Rplus_le_reg_l with (-(powerRZ 2 precision)+4)%R.
ring_simplify.
apply Rle_trans with (powerRZ 2 2)%R; auto with real zarith.
simpl; ring_simplify (2*(2*1))%R; auto with real zarith.
apply Rle_trans with (3+1)%R; auto with real; right; ring.
apply Rle_powerRZ; auto with arith zarith real.
replace (2*powerRZ radix (Fexp x))%R with (4*powerRZ radix (Fexp x -1))%R.
pattern 2%R at 3 in |-*; replace 2%R with (powerRZ radix 1%Z);[idtac|simpl; ring].
repeat rewrite <- powerRZ_add; auto with real zarith.
replace (1+Zpred precision+Fexp x)%Z with ((precision+1)+(Fexp x-1))%Z;[idtac|unfold Zpred; ring].
rewrite powerRZ_add with (n:=(precision+1)%Z);auto with real zarith; right;ring.
unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl; field.
unfold Rminus; apply Rplus_le_compat;[rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real|apply Ropp_le_contravar].
unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR, Fabs; simpl.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_reg_l with radix; auto with real zarith.
pattern (IZR radix) at 1 in |-*; replace (IZR radix) with (powerRZ radix 1%Z);[idtac|simpl; ring].
rewrite <- powerRZ_add; auto with real zarith; elim Nx; intros.
replace (1+Zpred precision)%Z with (Z_of_nat precision)%Z;[idtac|unfold Zpred; ring].
apply Rle_trans with (IZR (Zpos (vNum bo)));[rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith|idtac].
apply Rle_trans with (IZR (Zabs (radix * Fnum x))); auto with real zarith.
rewrite Zabs_Zmult; rewrite Zabs_eq; auto with real zarith.
rewrite mult_IZR; auto with real.
replace 4%R with (2*2%nat)%R; [rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real|simpl;ring].
replace (x+-r)%R with (-(r-x))%R;[rewrite Rabs_Ropp|ring].
apply Rle_trans with (Fulp bo radix precision x).
unfold FtoRradix; apply ClosestUlp; auto.
rewrite CanonicFulp; auto with real zarith.
right; unfold FtoR; simpl; ring.
left; auto.
case H3; intros V.
left; generalize V; unfold FNeven; rewrite FcanonicFnormalizeEq; auto with zarith.
rewrite FcanonicFnormalizeEq; auto with zarith.
elim Nx; intros; left; split; auto with zarith.
elim H1; intros; split; simpl; auto with zarith.
left; auto.
right; intros.
apply trans_eq with (2*(FtoR radix (Float (Fnum q0) (Zpred (Fexp q0)))))%R.
unfold FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; field; auto with real.
apply trans_eq with (2*(FtoR radix x))%R;[idtac|unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring].
apply Rmult_eq_compat_l; apply V.
replace r with ((2*r)/2)%R;[idtac|field; auto with real].
apply Half_Closest_Round; auto.
apply Zle_trans with (1:=U).
fold (Zpred (Fexp x)); cut (Fexp x <= Fexp q0)%Z; auto with zarith.
apply Zle_trans with (Fexp (Fnormalize radix bo precision q0)).
apply Fcanonic_Rle_Zle with radix bo precision; auto with zarith.
left; auto.
apply FnormalizeCanonic; auto with arith.
elim H1; auto.
generalize ClosestMonotone; unfold MonotoneP; intros.
repeat rewrite <- Fabs_correct; auto.
apply H4 with bo (Rabs r) (Rabs (2*r))%R.
rewrite Rabs_mult; rewrite (Rabs_right 2%R); try apply Rle_ge; auto with real.
apply Rle_lt_trans with (1*Rabs r)%R;[right;ring|apply Rmult_lt_compat_r; auto with real].
apply Rabs_pos_lt;unfold not;intros.
absurd (is_Fzero x).
apply FnormalNotZero with radix bo ; auto.
apply is_Fzero_rep2 with radix; auto.
cut (0 <= FtoR radix x)%R; intros.
cut (FtoR radix x <= 0)%R; intros; auto with real.
apply RleRoundedLessR0 with bo precision (Closest bo radix) r; auto with real.
apply ClosestRoundedModeP with precision; auto.
apply RleRoundedR0 with bo precision (Closest bo radix) r; auto with real.
apply ClosestRoundedModeP with precision; auto.
apply ClosestFabs with precision; auto.
apply ClosestFabs with precision; auto.
generalize ClosestCompatible; unfold CompatibleP; intros T.
apply T with (2*r)%R q0; auto with real float zarith.
apply sym_eq;apply FnormalizeCorrect; auto.
apply FnormalizeBounded; auto with zarith.
elim H1; auto.
apply FcanonicLeastExp with radix bo precision; auto with zarith float.
apply sym_eq; apply FnormalizeCorrect; auto.
elim H1; auto.
apply FnormalizeCanonic; auto with zarith;elim H1; auto.
Qed.
Theorem EvenClosestMonotone2: forall (p q : R) (p' q' : float),
(p <= q)%R -> (EvenClosest bo radix precision p p') ->
(EvenClosest bo radix precision q q') -> (p' <= q')%R.
intros.
case H; intros H2.
generalize EvenClosestMonotone; unfold MonotoneP.
intros W; unfold FtoRradix.
apply W with bo precision p0 q0; auto.
generalize EvenClosestUniqueP; unfold UniqueP.
intros W; unfold FtoRradix.
right; apply W with bo precision p0; auto with real.
rewrite H2; auto.
Qed.
Theorem Fulp_le_twice_r_round: forall (x y:float) (r:R), (0 <= x)%R ->
(Fbounded bo x) -> (Fnormal radix bo y) -> (- dExp bo <= Fexp y - 1)%Z
-> (x<=2*r)%R ->
(EvenClosest bo radix precision r y) ->
((Fulp bo radix precision x) <= 2*(Fulp bo radix precision y))%R.
intros x y r H H0 H1 U H2 H3.
assert (2*y=(Float (Fnum y) (Zsucc (Fexp y))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum y) (Zsucc (Fexp y)))).
2:right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto.
2:unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith.
2:simpl; ring.
2:left; auto.
2:elim H1; intros H6 H5; elim H6; intros.
2:split; simpl; auto with zarith.
2:split; simpl; auto with zarith.
apply LeFulpPos; auto with real.
elim H1; intros H6 H5; elim H6; intros;split; simpl; auto with zarith.
apply EvenClosestMonotone2 with x (2*r)%R; auto.
unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto.
apply EvenClosestRoundedModeP; auto.
apply Twice_EvenClosest_Round; auto.
Qed.
Theorem discri1: (delta <= 2*(Fulp bo radix precision d))%R.
apply Rle_trans with (1:=delta_inf).
case (Rle_or_lt q p); intros H1.
case (Rle_or_lt 0%R q); intros H2.
cut (2*(Fulp bo radix precision q)<=(Fulp bo radix precision p))%R; try intros H3.
cut ((Fulp bo radix precision p)<=2*(Fulp bo radix precision d))%R; try intros H4.
apply Rle_trans with ((/ 2 * Fulp bo radix precision d +
(/ 2 * (2*Fulp bo radix precision d) + / 2 * Fulp bo radix precision d)))%R.
apply Rplus_le_compat; auto with real.
apply Rplus_le_compat; auto with real.
apply Rmult_le_compat_l; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (1:=H3); auto with real.
right; field; auto with real.
apply Fulp_le_twice_r_round with (p-q)%R; auto.
apply P_positive.
apply Rplus_le_reg_l with (2*q-p)%R.
ring_simplify.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (p-3*q)%R.
ring_simplify.
apply Rle_trans with (1:=Firstcase); rewrite Rabs_right.
right; ring.
apply Rle_ge; apply Rplus_le_reg_l with q; ring_simplify; auto with real.
apply Fulp_le_twice_l; auto.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (p-3*q)%R.
ring_simplify.
apply Rle_trans with (1:=Firstcase); rewrite Rabs_right.
right; ring.
apply Rle_ge; apply Rplus_le_reg_l with q; ring_simplify; auto with real.
apply Rle_trans with ((/ 2 * Fulp bo radix precision d +
(/ 2 * (Fulp bo radix precision d) + / 2 * Fulp bo radix precision d)))%R.
apply Rplus_le_compat; auto with real.
apply Rplus_le_compat; auto with real.
apply Rmult_le_compat; auto with real.
unfold Fulp; auto with real zarith.
apply LeFulpPos; auto with real.
fold FtoRradix; apply P_positive.
fold FtoRradix; apply EvenClosestMonotone2 with p (p-q)%R; auto.
apply Rle_trans with (p-0)%R; unfold Rminus; auto with real; right;ring.
unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto.
apply EvenClosestRoundedModeP; auto.
apply Rmult_le_compat; auto with real.
unfold Fulp; auto with real zarith.
rewrite FulpFabs; auto.
apply LeFulpPos; auto with real.
split; auto with zarith float.
rewrite Fabs_correct; auto with real.
fold FtoRradix; apply EvenClosestMonotone2 with (-q)%R (p-q)%R; auto.
generalize P_positive; intros; auto with real.
apply Rle_trans with (0-q)%R; unfold Rminus; auto with real; right;ring.
replace (-q)%R with (FtoRradix (Fabs q)).
unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto.
apply EvenClosestRoundedModeP; auto.
split; auto with zarith float.
unfold FtoRradix;rewrite Fabs_correct; auto with real; rewrite Rabs_left; auto with real.
apply Rle_trans with ((3*/2)*(Fulp bo radix precision d))%R.
right; field; auto with real.
apply Rmult_le_compat_r;auto with zarith real.
unfold Fulp; auto with zarith real.
apply Rmult_le_reg_l with 2%R;auto with real.
apply Rle_trans with 3%R; auto with real.
right; field; auto with real.
replace 3%R with (IZR 3); auto with real zarith.
replace 4%R with (IZR 4); auto with real zarith.
simpl; ring.
simpl; ring.
cut (2*(Fulp bo radix precision p)<=(Fulp bo radix precision q))%R; try intros H3.
cut ((Fulp bo radix precision q)<=2*(Fulp bo radix precision d))%R; try intros H4.
apply Rle_trans with ((/ 2 * Fulp bo radix precision d +
(/ 2 * (Fulp bo radix precision d) + / 2 * (2*Fulp bo radix precision d))))%R.
apply Rplus_le_compat; auto with real.
apply Rplus_le_compat; auto with real.
apply Rmult_le_compat_l; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (1:=H3); auto with real.
right; field; auto with real.
assert (p-q <=0)%R.
apply Rplus_le_reg_l with q.
ring_simplify; auto with real.
rewrite FulpFabs with bo radix precision d; auto.
apply Fulp_le_twice_r_round with (Rabs (p-q))%R; auto.
apply Rle_trans with p; auto with real; apply P_positive.
apply FnormalFabs; auto.
rewrite Rabs_left; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (p-q)%R.
ring_simplify.
apply Rle_trans with (1:=Firstcase); rewrite Rabs_left1; auto.
right; ring.
generalize EvenClosestSymmetric; unfold SymmetricP; intros.
rewrite Rabsolu_left1; auto with real.
replace (Fabs d) with (Fopp d).
apply H0; auto.
unfold Fabs, Fopp; replace (Zabs (Fnum d)) with (-(Fnum d))%Z; auto.
rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto with zarith.
cut (Fnum d <= 0)%Z; auto with zarith.
apply R0LeFnum with radix; auto.
apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (p-q)%R; auto with real zarith.
apply EvenClosestRoundedModeP; auto.
apply Fulp_le_twice_l; auto.
apply P_positive.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (-3*p+q)%R.
ring_simplify.
apply Rle_trans with (1:=Firstcase); rewrite Rabs_left1; auto.
right; ring.
apply Rplus_le_reg_l with q.
ring_simplify; auto with real.
Qed.
End Discriminant1.
Section Discriminant2.
Variable bo : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ TwoMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix precision.
Variables a b b' c p q t dp dq s d:float.
Let delta := (Rabs (d-(b*b'-a*c)))%R.
Hypothesis Fa : (Fbounded bo a).
Hypothesis Fb : (Fbounded bo b).
Hypothesis Fb': (Fbounded bo b').
Hypothesis Fc : (Fbounded bo c).
Hypothesis Fp : (Fbounded bo p).
Hypothesis Fq : (Fbounded bo q).
Hypothesis Fd : (Fbounded bo d).
Hypothesis Ft : (Fbounded bo t).
Hypothesis Fs : (Fbounded bo s).
Hypothesis Fdp: (Fbounded bo dp).
Hypothesis Fdq: (Fbounded bo dq).
Hypothesis Cs:(Fcanonic radix bo s).
Hypothesis Nd:(Fnormal radix bo d).
Hypothesis Nq:(Fnormal radix bo q).
Hypothesis Np:(Fnormal radix bo p).
Hypothesis Square:(0 <=b*b')%R.
Hypothesis Roundp : (EvenClosest bo radix precision (b*b')%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).
Hypothesis Firstcase : (p+q <= 3*(Rabs (p-q)))%R.
Hypothesis Roundd : (EvenClosest bo radix precision (p-q)%R d).
Theorem delta_inf: (delta <= (/2)*(Fulp bo radix precision d)+
((/2)*(Fulp bo radix precision p)+(/2)*(Fulp bo radix precision q)))%R.
unfold delta; rewrite <- Rabs_Ropp.
replace (-(d - (b * b' - a * c)))%R with (((p-q)-d)+((b*b'-p)+-(a*c-q)))%R;[idtac|ring].
apply Rle_trans with ((Rabs ((p-q)-d))+(Rabs (b * b' - p + - (a * c - q))))%R;
[apply Rabs_triang|idtac].
apply Rplus_le_compat.
apply Rmult_le_reg_l with (S (S O)); auto with arith real.
apply Rle_trans with (Fulp bo radix precision d).
unfold FtoRradix; apply ClosestUlp;auto with zarith.
elim Roundd; auto.
right; simpl; field; auto with real.
apply Rle_trans with ((Rabs (b*b'-p))+(Rabs (-(a*c-q))))%R;
[apply Rabs_triang|idtac].
apply Rplus_le_compat.
apply Rmult_le_reg_l with (S (S O)); auto with arith real.
apply Rle_trans with (Fulp bo radix precision p).
unfold FtoRradix; apply ClosestUlp;auto with zarith.
elim Roundp; auto.
right; simpl; field; auto with real.
rewrite Rabs_Ropp; apply Rmult_le_reg_l with (S (S O)); auto with arith real.
apply Rle_trans with (Fulp bo radix precision q).
unfold FtoRradix; apply ClosestUlp;auto with zarith.
elim Roundq; auto.
right; simpl; field; auto with real.
Qed.
Theorem P_positive: (Rle 0 p)%R.
unfold FtoRradix; apply RleRoundedR0 with (b:=bo) (precision:=precision) (P:=(Closest bo radix)) (r:=(b*b')%R); auto.
apply ClosestRoundedModeP with precision; auto.
elim Roundp; auto.
Qed.
Theorem Fulp_le_twice_l: forall x y:float, (0 <= x)%R ->
(Fnormal radix bo x) -> (Fbounded bo y) -> (2*x<=y)%R ->
(2*(Fulp bo radix precision x) <= (Fulp bo radix precision y))%R.
intros.
assert (2*x=(Float (Fnum x) (Zsucc (Fexp x))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum x) (Zsucc (Fexp x)))).
right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto.
unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith.
simpl; ring.
elim H0; intros H4 H5; elim H4; intros.
left; split; auto.
split; simpl; auto with zarith.
apply LeFulpPos; auto with real.
elim H0; intros H4 H5; elim H4; intros;split; simpl; auto with zarith.
fold FtoRradix; rewrite <- H3; apply Rmult_le_pos; auto with real.
fold FtoRradix; rewrite <- H3; auto with real.
Qed.
Theorem Fulp_le_twice_r: forall x y:float, (0 <= x)%R ->
(Fnormal radix bo y) -> (Fbounded bo x) -> (x<=2*y)%R ->
((Fulp bo radix precision x) <= 2*(Fulp bo radix precision y))%R.
intros.
assert (2*y=(Float (Fnum y) (Zsucc (Fexp y))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum y) (Zsucc (Fexp y)))).
2:right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto.
2:unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith.
2:simpl; ring.
2:left; auto.
2:elim H0; intros H6 H5; elim H6; intros.
2:split; auto with zarith.
2:split; simpl; auto with zarith.
apply LeFulpPos; auto with real.
elim H0; intros H6 H5; elim H6; intros;split; simpl; auto with zarith.
fold FtoRradix; rewrite <- H3; auto with real.
Qed.
Theorem Half_Closest_Round: forall (x:float) (r:R),
(- dExp bo <= Zpred (Fexp x))%Z -> (Closest bo radix r x)
-> (Closest bo radix (r/2)%R (Float (Fnum x) (Zpred (Fexp x)))).
intros x r L H.
assert (x/2=(Float (Fnum x) (Zpred (Fexp x))))%R.
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; field.
elim H; intros H2 H3.
split; [split; simpl; auto with float zarith|idtac].
intros.
fold FtoRradix; rewrite <- H0.
replace (x/2-r/2)%R with (/2*(x-r))%R;[idtac|unfold Rdiv; ring].
rewrite Rabs_mult; rewrite Rabs_right; auto with real.
2: apply Rle_ge; auto with real.
replace (f-r/2)%R with (/2*((Float (Fnum f) (Zsucc (Fexp f)))-r))%R.
rewrite Rabs_mult; rewrite Rabs_right with (/2)%R.
2: apply Rle_ge; auto with real.
apply Rmult_le_compat_l; auto with real.
unfold FtoRradix; apply H3.
split; simpl; auto with zarith float.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; field; auto with real.
Qed.
Theorem Twice_EvenClosest_Round: forall (x:float) (r:R),
(-(dExp bo) <= (Fexp x)-1)%Z -> (Fnormal radix bo x)
-> (EvenClosest bo radix precision r x)
-> (EvenClosest bo radix precision (2*r)%R (Float (Fnum x) (Zsucc (Fexp x)))).
intros x r U Nx H.
assert (x*2=(Float (Fnum x) (Zsucc (Fexp x))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring.
elim H; intros H2 H3; elim H2; intros H'1 H'2; split.
split; [split; simpl; auto with float zarith|idtac].
intros.
fold FtoRradix; rewrite <- H0.
replace (x*2-2*r)%R with (2*(x-r))%R;[idtac|unfold Rdiv; ring].
rewrite Rabs_mult; rewrite Rabs_right; auto with real.
2: apply Rle_ge; auto with real.
case (Zle_lt_or_eq (-(dExp bo))%Z (Fexp f)); auto with zarith float; intros L.
replace (f-2*r)%R with (2*((Float (Fnum f) (Zpred (Fexp f)))-r))%R.
rewrite Rabs_mult; rewrite Rabs_right with (2)%R.
2: apply Rle_ge; auto with real.
apply Rmult_le_compat_l; auto with real.
unfold FtoRradix; apply H'2.
split; simpl; auto with zarith float.
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; field; auto with real.
replace (f-2*r)%R with (-((2*r)-f))%R;[rewrite Rabs_Ropp|ring].
apply Rle_trans with (2:=Rabs_triang_inv (2*r)%R f).
rewrite Rabs_mult; rewrite (Rabs_right 2%R); try apply Rle_ge;auto with real.
pattern r at 2 in |-*; replace r with (x-(x-r))%R;[idtac|ring].
apply Rle_trans with (2*(Rabs (x)-Rabs (x-r))-Rabs f)%R;[idtac|unfold Rminus; apply Rplus_le_compat_r; apply Rmult_le_compat_l; auto with real].
2: generalize (Rabs_triang_inv x (x-r)%R); unfold Rminus; auto with real.
apply Rplus_le_reg_l with (Rabs f -2*(Rabs (x-r)))%R.
apply Rle_trans with (Rabs f);[right;ring|idtac].
apply Rle_trans with (2*(Rabs x)-4*Rabs (x-r))%R;[idtac|right;ring].
apply Rle_trans with (((powerRZ radix precision)-1)*(powerRZ radix ((Fexp x)-1)))%R.
unfold FtoRradix; rewrite <- Fabs_correct; auto;unfold Fabs, FtoR; simpl.
apply Rmult_le_compat; auto with real zarith.
apply Rle_trans with (Zpred (Zpower_nat radix precision));[rewrite <- pGivesBound|idtac].
apply Rle_IZR;apply Zle_Zpred; auto with float.
unfold Zpred; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
rewrite <- L; apply Rle_powerRZ; auto with real zarith.
apply Rle_trans with (2*(powerRZ radix (Zpred precision))*(powerRZ radix (Fexp x))-2*(powerRZ radix (Fexp x)))%R.
apply Rle_trans with (((powerRZ radix (precision+1))-4)*(powerRZ radix (Fexp x-1)))%R;[apply Rmult_le_compat_r; auto with real zarith|idtac].
rewrite powerRZ_add; auto with real zarith; simpl.
apply Rplus_le_reg_l with (-(powerRZ 2 precision)+4)%R.
ring_simplify.
apply Rle_trans with (powerRZ 2 2)%R; auto with real zarith.
simpl; ring_simplify (2*(2*1))%R; auto with real zarith.
apply Rle_trans with (3+1)%R; auto with real; right; ring.
apply Rle_powerRZ; auto with arith zarith real.
replace (2*powerRZ radix (Fexp x))%R with (4*powerRZ radix (Fexp x -1))%R.
pattern 2%R at 3 in |-*; replace 2%R with (powerRZ radix 1%Z);[idtac|simpl; ring].
repeat rewrite <- powerRZ_add; auto with real zarith.
replace (1+Zpred precision+Fexp x)%Z with ((precision+1)+(Fexp x-1))%Z;[idtac|unfold Zpred; ring].
rewrite powerRZ_add with (n:=(precision+1)%Z);auto with real zarith; right;ring.
unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl; field.
unfold Rminus; apply Rplus_le_compat;[rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real|apply Ropp_le_contravar].
unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR, Fabs; simpl.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_reg_l with radix; auto with real zarith.
pattern (IZR radix) at 1 in |-*; replace (IZR radix) with (powerRZ radix 1%Z);[idtac|simpl; ring].
rewrite <- powerRZ_add; auto with real zarith; elim Nx; intros.
replace (1+Zpred precision)%Z with (Z_of_nat precision)%Z;[idtac|unfold Zpred; ring].
apply Rle_trans with (IZR (Zpos (vNum bo)));[rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith|idtac].
apply Rle_trans with (IZR (Zabs (radix * Fnum x))); auto with real zarith.
rewrite Zabs_Zmult; rewrite Zabs_eq; auto with real zarith.
rewrite mult_IZR; auto with real.
replace 4%R with (2*2%nat)%R; [rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real|simpl;ring].
replace (x+-r)%R with (-(r-x))%R;[rewrite Rabs_Ropp|ring].
apply Rle_trans with (Fulp bo radix precision x).
unfold FtoRradix; apply ClosestUlp; auto.
rewrite CanonicFulp; auto with real zarith.
right; unfold FtoR; simpl; ring.
left; auto.
case H3; intros V.
left; generalize V; unfold FNeven; rewrite FcanonicFnormalizeEq; auto with zarith.
rewrite FcanonicFnormalizeEq; auto with zarith.
elim Nx; intros; left; split; auto with zarith.
elim H1; intros; split; simpl; auto with zarith.
left; auto.
right; intros.
apply trans_eq with (2*(FtoR radix (Float (Fnum q0) (Zpred (Fexp q0)))))%R.
unfold FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; field; auto with real.
apply trans_eq with (2*(FtoR radix x))%R;[idtac|unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring].
apply Rmult_eq_compat_l; apply V.
replace r with ((2*r)/2)%R;[idtac|field; auto with real].
apply Half_Closest_Round; auto.
apply Zle_trans with (1:=U).
fold (Zpred (Fexp x)); cut (Fexp x <= Fexp q0)%Z; auto with zarith.
apply Zle_trans with (Fexp (Fnormalize radix bo precision q0)).
apply Fcanonic_Rle_Zle with radix bo precision; auto with zarith.
left; auto.
apply FnormalizeCanonic; auto with arith.
elim H1; auto.
generalize ClosestMonotone; unfold MonotoneP; intros.
repeat rewrite <- Fabs_correct; auto.
apply H4 with bo (Rabs r) (Rabs (2*r))%R.
rewrite Rabs_mult; rewrite (Rabs_right 2%R); try apply Rle_ge; auto with real.
apply Rle_lt_trans with (1*Rabs r)%R;[right;ring|apply Rmult_lt_compat_r; auto with real].
apply Rabs_pos_lt;unfold not;intros.
absurd (is_Fzero x).
apply FnormalNotZero with radix bo ; auto.
apply is_Fzero_rep2 with radix; auto.
cut (0 <= FtoR radix x)%R; intros.
cut (FtoR radix x <= 0)%R; intros; auto with real.
apply RleRoundedLessR0 with bo precision (Closest bo radix) r; auto with real.
apply ClosestRoundedModeP with precision; auto.
apply RleRoundedR0 with bo precision (Closest bo radix) r; auto with real.
apply ClosestRoundedModeP with precision; auto.
apply ClosestFabs with precision; auto.
apply ClosestFabs with precision; auto.
generalize ClosestCompatible; unfold CompatibleP; intros T.
apply T with (2*r)%R q0; auto with real float zarith.
apply sym_eq;apply FnormalizeCorrect; auto.
apply FnormalizeBounded; auto with zarith.
elim H1; auto.
apply FcanonicLeastExp with radix bo precision; auto with zarith float.
apply sym_eq; apply FnormalizeCorrect; auto.
elim H1; auto.
apply FnormalizeCanonic; auto with zarith;elim H1; auto.
Qed.
Theorem EvenClosestMonotone2: forall (p q : R) (p' q' : float),
(p <= q)%R -> (EvenClosest bo radix precision p p') ->
(EvenClosest bo radix precision q q') -> (p' <= q')%R.
intros.
case H; intros H2.
generalize EvenClosestMonotone; unfold MonotoneP.
intros W; unfold FtoRradix.
apply W with bo precision p0 q0; auto.
generalize EvenClosestUniqueP; unfold UniqueP.
intros W; unfold FtoRradix.
right; apply W with bo precision p0; auto with real.
rewrite H2; auto.
Qed.
Theorem Fulp_le_twice_r_round: forall (x y:float) (r:R), (0 <= x)%R ->
(Fbounded bo x) -> (Fnormal radix bo y) -> (- dExp bo <= Fexp y - 1)%Z
-> (x<=2*r)%R ->
(EvenClosest bo radix precision r y) ->
((Fulp bo radix precision x) <= 2*(Fulp bo radix precision y))%R.
intros x y r H H0 H1 U H2 H3.
assert (2*y=(Float (Fnum y) (Zsucc (Fexp y))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum y) (Zsucc (Fexp y)))).
2:right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto.
2:unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith.
2:simpl; ring.
2:left; auto.
2:elim H1; intros H6 H5; elim H6; intros.
2:split; simpl; auto with zarith.
2:split; simpl; auto with zarith.
apply LeFulpPos; auto with real.
elim H1; intros H6 H5; elim H6; intros;split; simpl; auto with zarith.
apply EvenClosestMonotone2 with x (2*r)%R; auto.
unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto.
apply EvenClosestRoundedModeP; auto.
apply Twice_EvenClosest_Round; auto.
Qed.
Theorem discri1: (delta <= 2*(Fulp bo radix precision d))%R.
apply Rle_trans with (1:=delta_inf).
case (Rle_or_lt q p); intros H1.
case (Rle_or_lt 0%R q); intros H2.
cut (2*(Fulp bo radix precision q)<=(Fulp bo radix precision p))%R; try intros H3.
cut ((Fulp bo radix precision p)<=2*(Fulp bo radix precision d))%R; try intros H4.
apply Rle_trans with ((/ 2 * Fulp bo radix precision d +
(/ 2 * (2*Fulp bo radix precision d) + / 2 * Fulp bo radix precision d)))%R.
apply Rplus_le_compat; auto with real.
apply Rplus_le_compat; auto with real.
apply Rmult_le_compat_l; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (1:=H3); auto with real.
right; field; auto with real.
apply Fulp_le_twice_r_round with (p-q)%R; auto.
apply P_positive.
apply Rplus_le_reg_l with (2*q-p)%R.
ring_simplify.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (p-3*q)%R.
ring_simplify.
apply Rle_trans with (1:=Firstcase); rewrite Rabs_right.
right; ring.
apply Rle_ge; apply Rplus_le_reg_l with q; ring_simplify; auto with real.
apply Fulp_le_twice_l; auto.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (p-3*q)%R.
ring_simplify.
apply Rle_trans with (1:=Firstcase); rewrite Rabs_right.
right; ring.
apply Rle_ge; apply Rplus_le_reg_l with q; ring_simplify; auto with real.
apply Rle_trans with ((/ 2 * Fulp bo radix precision d +
(/ 2 * (Fulp bo radix precision d) + / 2 * Fulp bo radix precision d)))%R.
apply Rplus_le_compat; auto with real.
apply Rplus_le_compat; auto with real.
apply Rmult_le_compat; auto with real.
unfold Fulp; auto with real zarith.
apply LeFulpPos; auto with real.
fold FtoRradix; apply P_positive.
fold FtoRradix; apply EvenClosestMonotone2 with p (p-q)%R; auto.
apply Rle_trans with (p-0)%R; unfold Rminus; auto with real; right;ring.
unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto.
apply EvenClosestRoundedModeP; auto.
apply Rmult_le_compat; auto with real.
unfold Fulp; auto with real zarith.
rewrite FulpFabs; auto.
apply LeFulpPos; auto with real.
split; auto with zarith float.
rewrite Fabs_correct; auto with real.
fold FtoRradix; apply EvenClosestMonotone2 with (-q)%R (p-q)%R; auto.
generalize P_positive; intros; auto with real.
apply Rle_trans with (0-q)%R; unfold Rminus; auto with real; right;ring.
replace (-q)%R with (FtoRradix (Fabs q)).
unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto.
apply EvenClosestRoundedModeP; auto.
split; auto with zarith float.
unfold FtoRradix;rewrite Fabs_correct; auto with real; rewrite Rabs_left; auto with real.
apply Rle_trans with ((3*/2)*(Fulp bo radix precision d))%R.
right; field; auto with real.
apply Rmult_le_compat_r;auto with zarith real.
unfold Fulp; auto with zarith real.
apply Rmult_le_reg_l with 2%R;auto with real.
apply Rle_trans with 3%R; auto with real.
right; field; auto with real.
replace 3%R with (IZR 3); auto with real zarith.
replace 4%R with (IZR 4); auto with real zarith.
simpl; ring.
simpl; ring.
cut (2*(Fulp bo radix precision p)<=(Fulp bo radix precision q))%R; try intros H3.
cut ((Fulp bo radix precision q)<=2*(Fulp bo radix precision d))%R; try intros H4.
apply Rle_trans with ((/ 2 * Fulp bo radix precision d +
(/ 2 * (Fulp bo radix precision d) + / 2 * (2*Fulp bo radix precision d))))%R.
apply Rplus_le_compat; auto with real.
apply Rplus_le_compat; auto with real.
apply Rmult_le_compat_l; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (1:=H3); auto with real.
right; field; auto with real.
assert (p-q <=0)%R.
apply Rplus_le_reg_l with q.
ring_simplify; auto with real.
rewrite FulpFabs with bo radix precision d; auto.
apply Fulp_le_twice_r_round with (Rabs (p-q))%R; auto.
apply Rle_trans with p; auto with real; apply P_positive.
apply FnormalFabs; auto.
rewrite Rabs_left; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (p-q)%R.
ring_simplify.
apply Rle_trans with (1:=Firstcase); rewrite Rabs_left1; auto.
right; ring.
generalize EvenClosestSymmetric; unfold SymmetricP; intros.
rewrite Rabsolu_left1; auto with real.
replace (Fabs d) with (Fopp d).
apply H0; auto.
unfold Fabs, Fopp; replace (Zabs (Fnum d)) with (-(Fnum d))%Z; auto.
rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto with zarith.
cut (Fnum d <= 0)%Z; auto with zarith.
apply R0LeFnum with radix; auto.
apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (p-q)%R; auto with real zarith.
apply EvenClosestRoundedModeP; auto.
apply Fulp_le_twice_l; auto.
apply P_positive.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (-3*p+q)%R.
ring_simplify.
apply Rle_trans with (1:=Firstcase); rewrite Rabs_left1; auto.
right; ring.
apply Rplus_le_reg_l with q.
ring_simplify; auto with real.
Qed.
End Discriminant1.
Section Discriminant2.
Variable bo : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ TwoMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix precision.
Variables a b b' c p q t dp dq s d:float.
Let delta := (Rabs (d-(b*b'-a*c)))%R.
Hypothesis Fa : (Fbounded bo a).
Hypothesis Fb : (Fbounded bo b).
Hypothesis Fb': (Fbounded bo b').
Hypothesis Fc : (Fbounded bo c).
Hypothesis Fp : (Fbounded bo p).
Hypothesis Fq : (Fbounded bo q).
Hypothesis Fd : (Fbounded bo d).
Hypothesis Ft : (Fbounded bo t).
Hypothesis Fs : (Fbounded bo s).
Hypothesis Fdp: (Fbounded bo dp).
Hypothesis Fdq: (Fbounded bo dq).
Hypothesis Cs:(Fcanonic radix bo s).
There is no underflow
Hypothesis U1: (- dExp bo <= (Fexp t)-1)%Z.
Hypothesis U2: (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (b*b'))%R.
Hypothesis U3: (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (a*c))%R.
Hypothesis Np:(Fnormal radix bo p).
Hypothesis Nq:(Fnormal radix bo q).
Hypothesis Nd:(Fnormal radix bo d).
Hypothesis Square:(0 <=b*b')%R.
Hypothesis Roundp : (EvenClosest bo radix precision (b*b')%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).
Hypothesis Secondcase : (3*(Rabs (p-q)) < p+q)%R.
Hypothesis Roundt : (EvenClosest bo radix precision (p-q)%R t).
Hypothesis dpEq : (FtoRradix dp=b*b'-p)%R.
Hypothesis dqEq : (FtoRradix dq=a*c-q)%R.
Hypothesis Rounds : (EvenClosest bo radix precision (dp-dq)%R s).
Hypothesis Roundd : (EvenClosest bo radix precision (t+s)%R d).
Hypothesis p_differ_q:~(p=q)%R.
Theorem Q_positive:(0 < q)%R.
case (Rle_or_lt q 0%R); auto; intros.
absurd (3*(Rabs (p-q)) < (Rabs (p-q)))%R.
apply Rle_not_lt; apply Rle_trans with (1*(Rabs (p-q)))%R; auto with real.
apply Rmult_le_compat_r; auto with real.
apply Rle_trans with (IZR 1); auto with real.
apply Rle_trans with (IZR 3); auto with real zarith.
simpl; auto with real zarith.
apply Rlt_le_trans with (1:=Secondcase).
apply Rle_trans with (2:=Rabs_triang_inv p q).
right; rewrite Rabs_right.
rewrite Rabs_left1; auto with real; ring.
apply Rle_ge; apply P_positive with bo precision b b'; auto.
Qed.
Theorem Q_le_two_P:(q <= 2*p)%R.
fold FtoRradix; apply Rmult_le_reg_l with 2%R; auto with real; simpl.
apply Rle_trans with (3*q-q)%R; [right; ring|idtac].
pattern (FtoRradix q) at 1; rewrite <- (Rabs_right q).
2: apply Rle_ge; generalize Q_positive; auto with real.
pattern (FtoRradix q) at 1; replace (FtoRradix q) with (-(p-q)+p)%R;[idtac|ring].
apply Rle_trans with (3*(Rabs (-(p-q))+(Rabs p))-q)%R.
unfold Rminus; apply Rplus_le_compat_r.
apply Rmult_le_compat_l; auto with real.
apply Rle_trans with 2%R; auto with real.
apply Rabs_triang.
rewrite Rabs_Ropp.
rewrite (Rabs_right p).
2:apply Rle_ge; apply P_positive with bo precision b b'; auto.
apply Rle_trans with (3 * (Rabs (p - q)) + (3*p - q))%R;[right;ring|idtac].
apply Rle_trans with (p+q+(3*p-q))%R; auto with real.
right;ring.
Qed.
Theorem P_le_two_Q:(p <= 2*q)%R.
fold FtoRradix; apply Rmult_le_reg_l with 2%R; auto with real; simpl.
apply Rle_trans with (3*p-p)%R; [right; ring|idtac].
pattern (FtoRradix p) at 1; rewrite <- (Rabs_right p).
2: apply Rle_ge; apply P_positive with bo precision b b'; auto with real.
pattern (FtoRradix p) at 1; replace (FtoRradix p) with ((p-q)+q)%R;[idtac|ring].
apply Rle_trans with (3*(Rabs (p-q)+(Rabs q))-p)%R.
unfold Rminus; apply Rplus_le_compat_r.
apply Rmult_le_compat_l; auto with real.
apply Rle_trans with 2%R; auto with real.
apply Rabs_triang.
rewrite (Rabs_right q).
2: apply Rle_ge; generalize Q_positive; auto with real.
apply Rle_trans with (3 * (Rabs (p - q)) + (3*q - p))%R;[right;ring|idtac].
apply Rle_trans with (p+q+(3*q-p))%R; auto with real.
right;ring.
Qed.
Theorem t_exact: (FtoRradix t=p-q)%R.
unfold FtoRradix; rewrite <- Fminus_correct; auto with zarith.
apply sym_eq; apply RoundedModeProjectorIdemEq with (b:=bo) (P:=(EvenClosest bo radix precision)) (precision:=precision); auto.
apply EvenClosestRoundedModeP; auto.
2: rewrite Fminus_correct; auto with zarith.
apply Sterbenz; auto.
fold FtoRradix; apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (FtoRradix q);[simpl; right; field; auto with real|idtac].
apply Q_le_two_P.
fold FtoRradix; simpl; apply P_le_two_Q.
Qed.
Theorem dp_dq_le:(Rabs (dp-dq) <= (3/2)*(Rmin
(Fulp bo radix precision p) (Fulp bo radix precision q)))%R.
unfold Rminus; apply Rle_trans with (1:=Rabs_triang dp (-dq)).
rewrite Rabs_Ropp;apply Rmult_le_reg_l with (S (S O))%R; auto with real.
apply Rle_trans with (S 1 * Rabs dp + S 1*Rabs dq)%R;[right;ring|idtac].
apply Rle_trans with ((Fulp bo radix precision p)+(Fulp bo radix precision q))%R.
apply Rplus_le_compat.
rewrite dpEq; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundp; auto.
rewrite dqEq; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundq; auto.
rewrite <- Rmult_assoc.
apply Rle_trans with (3*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q)))%R;[idtac|apply Rmult_le_compat_r].
2: unfold Rmin; case (Rle_dec (Fulp bo radix precision p) (Fulp bo radix precision q)); intros H1; unfold Fulp; auto with real zarith.
2: right; simpl; unfold Rdiv; field; auto with real.
unfold Rmin; case (Rle_dec (Fulp bo radix precision p) (Fulp bo radix precision q)); intros H1.
apply Rle_trans with (Fulp bo radix precision p+2*Fulp bo radix precision p)%R;[apply Rplus_le_compat_l|right;ring].
apply Fulp_le_twice_r; auto with real; fold radix FtoRradix.
generalize Q_positive; auto with real.
apply Q_le_two_P.
apply Rle_trans with (2*Fulp bo radix precision q+Fulp bo radix precision q)%R;[apply Rplus_le_compat_r|right;ring].
apply Fulp_le_twice_r; auto with real; fold radix FtoRradix.
apply P_positive with bo precision b b'; auto with real.
apply P_le_two_Q.
Qed.
Theorem EvenClosestFabs :
forall (f : float) (r : R), (Fcanonic radix bo f)
-> EvenClosest bo radix precision r f ->
EvenClosest bo radix precision (Rabs r) (Fabs f).
intros.
case (Rle_or_lt 0%R r); intros.
rewrite Rabs_right; auto with real.
unfold Fabs; rewrite Zabs_eq; auto with zarith.
apply LeR0Fnum with (radix := radix); auto with zarith.
apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) r; auto with float zarith.
rewrite Rabs_left; auto with real.
replace (Fabs f) with (Fopp f).
generalize EvenClosestSymmetric; unfold SymmetricP; auto.
unfold Fabs, Fopp; rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto.
assert (Fnum f <= 0)%Z; auto with zarith.
apply R0LeFnum with (radix:=radix); auto with zarith.
apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) r; auto with float zarith real.
Qed.
Theorem discri2: (3*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q))
<= (Rabs (p-q)))%R -> (delta <= 2*(Fulp bo radix precision d))%R.
intros H1; unfold delta.
apply Rle_trans with (1 * Fulp bo radix precision d)%R;[ring_simplify (1 * Fulp bo radix precision d)%R | unfold Fulp; auto with real zarith].
replace (d - (b * b' - a * c))%R with ((d-(t+s))+(t+s-b*b'+a*c))%R;[idtac|ring].
apply Rle_trans with (1:=Rabs_triang (d-(t+s))%R (t + s - b * b' + a * c)%R).
apply Rmult_le_reg_l with 2%R; auto with real.
rewrite Rmult_plus_distr_l.
apply Rle_trans with (Fulp bo radix precision d+Fulp bo radix precision d)%R;[idtac|right;ring].
apply Rplus_le_compat.
rewrite <- Rabs_Ropp; replace (- (d - (t + s)))%R with ((t+s)-d)%R;[idtac|ring].
replace 2%R with (INR 2); auto with real.
unfold FtoRradix; apply ClosestUlp; auto.
elim Roundd; auto.
rewrite t_exact.
replace (p - q + s - b * b' + a * c)%R with (-((dp-dq) - s))%R;[idtac|rewrite dpEq; rewrite dqEq; ring].
rewrite Rabs_Ropp; apply Rle_trans with (Fulp bo radix precision s).
unfold FtoRradix; apply ClosestUlp; auto.
elim Rounds; auto.
rewrite FulpFabs; auto; rewrite FulpFabs with (f:=d); auto.
apply LeFulpPos; auto with real zarith float.
rewrite Fabs_correct; auto with real.
apply EvenClosestMonotone2 with bo precision (Rabs (dp-dq)) (Rabs (t+s))%R; auto.
2: apply EvenClosestFabs; auto; left; auto.
2: apply EvenClosestFabs; auto; left; auto.
cut (Rabs (dp - dq) <= (Rabs (p-q))/2)%R.
intros H2; cut ((Rabs s) <= (Rabs t)/2)%R.
intros H3; apply Rle_trans with (1:=H2).
rewrite <- t_exact; apply Rle_trans with ((Rabs t)-(Rabs t)/2)%R.
right; unfold Rdiv; field; auto with real.
apply Rle_trans with ((Rabs t)-(Rabs s))%R; auto with real.
unfold Rminus; apply Rplus_le_compat_l; auto with real.
replace (t+s)%R with (t-(-s))%R; [idtac|ring].
apply Rle_trans with ((Rabs t)-(Rabs (-s)))%R;[idtac|apply Rabs_triang_inv].
rewrite Rabs_Ropp; auto with real.
assert (t/2=(Float (Fnum t) (Zpred (Fexp t))))%R.
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl ; field.
unfold Rdiv; rewrite <- (Rabs_right (/2)%R); auto with real.
2: apply Rle_ge; apply Rlt_le; auto with real.
rewrite <- Rabs_mult; fold (Rdiv t 2%R).
rewrite H; unfold FtoRradix; rewrite <- Fabs_correct; auto.
rewrite <- Fabs_correct; auto.
apply EvenClosestMonotone2 with bo precision (Rabs (dp-dq))%R (Rabs (p-q)/2)%R; auto.
apply EvenClosestFabs; auto; left; auto.
replace (Rabs (p - q) / 2)%R with (FtoRradix (Fabs (Float (Fnum t) (Zpred (Fexp t))))).
unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto.
apply EvenClosestRoundedModeP; auto.
split; simpl; auto with zarith float.
rewrite Zabs_eq; auto with zarith float.
unfold FtoRradix; rewrite Fabs_correct; auto; fold FtoRradix; rewrite <- H.
rewrite t_exact; unfold Rdiv; rewrite Rabs_mult; auto with real.
rewrite (Rabs_right (/2)%R); auto with real.
apply Rle_ge; apply Rlt_le; auto with real.
apply Rle_trans with (1:=dp_dq_le).
apply Rmult_le_reg_l with 2%R; auto with real; unfold Rdiv.
rewrite <- Rmult_assoc.
replace (2*(3*/2))%R with 3%R;[idtac|field; auto with real].
apply Rle_trans with (1:=H1).
right; field; auto with real.
Qed.
Theorem discri3: (exists f:float, (Fbounded bo f) /\ (FtoRradix f)=(dp-dq)%R)
-> (delta <= 2*(Fulp bo radix precision d))%R.
intros T; elim T; intros f T1; elim T1; intros H1 H2; clear T T1.
unfold delta.
replace (d - (b * b' - a * c))%R with (-((t+s)-d))%R.
apply Rmult_le_reg_l with (INR 2); auto with arith real.
apply Rle_trans with (Fulp bo radix precision d).
rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundd; auto.
simpl; apply Rle_trans with (1*(1*(Fulp bo radix precision d)))%R; unfold Fulp; auto with real zarith.
right; ring.
apply Rmult_le_compat; auto with real zarith.
ring_simplify (1 * powerRZ radix (Fexp (Fnormalize radix bo precision d)))%R; auto with real zarith.
replace (FtoRradix s) with (dp-dq)%R.
rewrite dpEq; rewrite dqEq; rewrite t_exact; ring.
rewrite <- H2.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with (b:=bo) (P:=(EvenClosest bo radix precision)) (precision:=precision); auto with real.
apply EvenClosestRoundedModeP; auto.
fold FtoRradix; rewrite H2; auto.
Qed.
Theorem errorBoundedMultClosest_Can:
forall f1 f2 g : float,
Fbounded bo f1 ->
Fbounded bo f2 ->
Closest bo radix (f1* f2) g ->
(powerRZ radix (-dExp bo+2*precision-1) <= Rabs (f1*f2))%R ->
Fcanonic radix bo g ->
(exists s : float,
Fbounded bo s /\
(FtoRradix s = f1*f2 - g)%R /\
Fexp s = (Fexp g - precision)%Z /\
(Rabs (Fnum s) <= powerRZ radix (Zpred precision))%R).
intros.
generalize errorBoundedMultClosest; intros T.
elim T with (b:=bo) (radix:=radix) (precision:=precision) (p:=f1) (q:=f2) (pq:=g); auto with zarith real; clear T; fold FtoRradix.
intros g' T1; elim T1; intros dg T2; elim T2; intros H5 T3; elim T3; intros H6 T4; elim T4; intros H7 T5; elim T5; intros H8 T6; elim T6; intros H9 H10; clear T1 T2 T3 T4 T5 T6.
exists dg; split; auto; split.
rewrite <- H8; auto with real.
split; [replace g with g'; auto with zarith|idtac].
apply FcanonicUnique with radix bo precision; auto with arith.
apply Rmult_le_reg_l with (powerRZ radix (Fexp dg)); auto with zarith real.
apply Rle_trans with (Rabs dg);[right; unfold FtoRradix, FtoR|idtac].
rewrite Rabs_mult;rewrite (Rabs_right (powerRZ radix (Fexp dg)));auto with real.
apply Rle_ge; auto with real zarith.
rewrite H9; rewrite <- powerRZ_add; auto with real zarith.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix precision g').
unfold FtoRradix; apply ClosestUlp; auto.
replace g' with g; auto.
apply FcanonicUnique with radix bo precision; auto with arith.
rewrite CanonicFulp; auto.
right; apply trans_eq with (powerRZ radix (Fexp g'));[unfold FtoR; simpl; ring|idtac].
apply trans_eq with ((powerRZ radix 1%Z)*(powerRZ radix (Fexp dg+Zpred precision)))%R;[rewrite <- powerRZ_add; auto with zarith real|simpl; ring].
rewrite H10; unfold Zpred; auto with zarith real.
ring_simplify (1 + (Fexp g' - precision + (precision + -1)))%Z; auto with real.
assert (- dExp bo + 2 * precision - 1 < 2*precision+Fexp f1+Fexp f2)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with (1:=H2).
rewrite Rabs_mult; unfold FtoRradix; repeat rewrite <- Fabs_correct; auto.
replace (2*precision)%Z with (precision+precision)%Z; auto with zarith.
unfold FtoR, Fabs; simpl.
repeat rewrite powerRZ_add; auto with real zarith.
repeat rewrite <- Rmult_assoc; apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (Zabs (Fnum f1)*Zabs (Fnum f2) * powerRZ 2 (Fexp f1))%R;
[right; ring| apply Rmult_lt_compat_r; auto with real zarith].
apply Rle_lt_trans with (Zabs (Fnum f1)* powerRZ 2 precision)%R.
apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (Zpos (vNum bo)); auto with real zarith float.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rlt_le_trans with (Zpos (vNum bo)); auto with real zarith float.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real.
rewrite FcanonicFnormalizeEq; auto with zarith.
assert (powerRZ radix (- dExp bo + 2 * precision - 1) <= Rabs g)%R.
cut (exists f:float, Fbounded bo f /\
(FtoRradix f=(powerRZ radix (- dExp bo + 2 * precision - 1)))%R).
intros T; elim T; intros f T'; elim T'; intros; clear T T'.
rewrite <- H5; unfold FtoRradix.
apply RoundAbsMonotonel with bo precision
(Closest bo radix) (f1*f2)%R; auto with zarith float real.
apply ClosestRoundedModeP with precision; auto with zarith.
fold FtoRradix; rewrite H5; auto.
exists (Float 1 (-dExp bo+2*precision-1)).
split;[split|idtac].
simpl; apply vNumbMoreThanOne with radix precision; auto with zarith.
apply Zle_trans with (- dExp bo + 2 * precision - 1)%Z; auto with zarith.
unfold FtoRradix, FtoR; simpl; ring.
assert (- dExp bo + 2 * precision - 1 < precision+Fexp g)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with zarith real.
apply Rle_lt_trans with (1:=H4).
unfold FtoRradix; rewrite <- Fabs_correct; auto.
rewrite powerRZ_add; auto with real zarith.
unfold FtoR, Fabs; simpl.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rlt_le_trans with (Zpos (vNum bo)).
elim H1; auto with real zarith float.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
Qed.
Theorem discri4: (Fexp p)=(Fexp q) -> (delta <= 2*(Fulp bo radix precision d))%R.
intros H1; apply discri3.
generalize errorBoundedMultClosest_Can; intros T.
elim T with (f1:=b) (f2:=b') (g:=p); auto with zarith real; clear T.
intros dp' T2; elim T2; intros H2 T3; elim T3; intros H3 T4; elim T4; intros H4 H5; clear T2 T3 T4.
2: elim Roundp; auto.
generalize errorBoundedMultClosest_Can; intros T.
elim T with (f1:=a) (f2:=c) (g:=q); auto with zarith real; clear T.
intros dq' T2; elim T2; intros H2' T3; elim T3; intros H3' T4; elim T4; intros H4' H5'; clear T2 T3 T4.
2: elim Roundq; auto.
2: left; auto.
2: left; auto.
assert ((Rabs (Fnum dp'-Fnum dq') < (powerRZ radix precision))%R \/
(((Rabs dp')= (powerRZ radix (Zpred (Fexp p))))%R /\ ((Rabs dq')= (powerRZ radix (Zpred (Fexp p))))%R)).
case H5; intros.
left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp') (-(Fnum dq'))%R).
rewrite Rabs_Ropp.
apply Rlt_le_trans with ((powerRZ radix (Zpred precision)) +(Rabs (Fnum dq')))%R; auto with real zarith.
apply Rle_trans with ((powerRZ radix (Zpred precision))+ (powerRZ radix (Zpred precision)))%R; auto with real zarith.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
case H5'; intros.
left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp') (-(Fnum dq'))%R); rewrite Rabs_Ropp.
apply Rle_lt_trans with ((powerRZ radix (Zpred precision)) +(Rabs (Fnum dq')))%R; auto with real zarith.
apply Rlt_le_trans with ((powerRZ radix (Zpred precision))+ (powerRZ radix (Zpred precision)))%R; auto with real zarith.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
right; unfold FtoRradix, FtoR;repeat rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (Fexp dp'))); try apply Rle_ge; auto with real zarith.
rewrite (Rabs_right (powerRZ radix (Fexp dq'))); try apply Rle_ge; auto with real zarith.
rewrite H; rewrite H0.
repeat rewrite <- powerRZ_add; auto with real zarith.
rewrite H4'; rewrite H4; unfold Zpred.
ring_simplify (precision + -1 + (Fexp p - precision))%Z; ring_simplify (precision + -1 + (Fexp q - precision))%Z;
ring_simplify (Fexp p+-1)%Z; rewrite <- H1; auto with zarith real.
case H; clear H; intros H.
exists (Float ((Fnum dp')-(Fnum dq'))%Z (Fexp dq')).
split; [split; auto with zarith|idtac].
simpl; apply Zlt_Rlt.
rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto.
rewrite <- Rabs_Zabs; unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; auto with real zarith.
simpl; auto with zarith float.
rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'.
unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; replace (Fexp dp') with (Fexp dq');[ring|idtac].
rewrite H4'; rewrite <- H1; auto with zarith.
rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'.
elim H; unfold Rabs; case (Rcase_abs dp'); case (Rcase_abs dq'); intros.
exists (Float 0%Z 0%Z); split;[split; auto with zarith|idtac].
simpl; case (dExp bo); auto with zarith.
apply trans_eq with (-(-dp')+-dq')%R;[rewrite H0; rewrite H6; unfold FtoRradix, FtoR;simpl|idtac];ring.
exists (Float (-2)%Z (Zpred (Fexp p))); split;[split; simpl; auto with zarith|idtac].
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 1); auto with zarith.
apply Zle_trans with (Fexp dp'); auto with zarith float.
apply trans_eq with (-(-dp')+-dq')%R;[rewrite H0; rewrite H6; unfold FtoRradix, FtoR; simpl|idtac];ring.
exists (Float 2%Z (Zpred (Fexp p))); split;[split;simpl;auto with zarith|idtac].
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 1); auto with zarith.
apply Zle_trans with (Fexp dp'); auto with zarith float.
unfold Rminus;rewrite H0; rewrite H6; unfold FtoRradix, FtoR;simpl; ring.
exists (Float 0%Z 0%Z); split;[split; auto with zarith|idtac].
simpl; case (dExp bo); auto with zarith.
rewrite H0; rewrite H6; unfold FtoRradix, FtoR; simpl;ring.
Qed.
End Discriminant2.
Section Discriminant3.
Variable bo : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ TwoMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix precision.
Variables a b b' c p q t dp dq s d:float.
Let delta := (Rabs (d-(b*b'-a*c)))%R.
Hypothesis Fa : (Fbounded bo a).
Hypothesis Fb : (Fbounded bo b).
Hypothesis Fb': (Fbounded bo b').
Hypothesis Fc : (Fbounded bo c).
Hypothesis Fp : (Fbounded bo p).
Hypothesis Fq : (Fbounded bo q).
Hypothesis Fd : (Fbounded bo d).
Hypothesis Ft : (Fbounded bo t).
Hypothesis Fs : (Fbounded bo s).
Hypothesis Fdp: (Fbounded bo dp).
Hypothesis Fdq: (Fbounded bo dq).
Hypothesis Cs:(Fcanonic radix bo s).
Hypothesis U2: (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (b*b'))%R.
Hypothesis U3: (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (a*c))%R.
Hypothesis Np:(Fnormal radix bo p).
Hypothesis Nq:(Fnormal radix bo q).
Hypothesis Nd:(Fnormal radix bo d).
Hypothesis Square:(0 <=b*b')%R.
Hypothesis Roundp : (EvenClosest bo radix precision (b*b')%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).
Hypothesis Secondcase : (3*(Rabs (p-q)) < p+q)%R.
Hypothesis Roundt : (EvenClosest bo radix precision (p-q)%R t).
Hypothesis dpEq : (FtoRradix dp=b*b'-p)%R.
Hypothesis dqEq : (FtoRradix dq=a*c-q)%R.
Hypothesis Rounds : (EvenClosest bo radix precision (dp-dq)%R s).
Hypothesis Roundd : (EvenClosest bo radix precision (t+s)%R d).
Hypothesis p_differ_q:~(p=q)%R.
Theorem Q_positive:(0 < q)%R.
case (Rle_or_lt q 0%R); auto; intros.
absurd (3*(Rabs (p-q)) < (Rabs (p-q)))%R.
apply Rle_not_lt; apply Rle_trans with (1*(Rabs (p-q)))%R; auto with real.
apply Rmult_le_compat_r; auto with real.
apply Rle_trans with (IZR 1); auto with real.
apply Rle_trans with (IZR 3); auto with real zarith.
simpl; auto with real zarith.
apply Rlt_le_trans with (1:=Secondcase).
apply Rle_trans with (2:=Rabs_triang_inv p q).
right; rewrite Rabs_right.
rewrite Rabs_left1; auto with real; ring.
apply Rle_ge; apply P_positive with bo precision b b'; auto.
Qed.
Theorem Q_le_two_P:(q <= 2*p)%R.
fold FtoRradix; apply Rmult_le_reg_l with 2%R; auto with real; simpl.
apply Rle_trans with (3*q-q)%R; [right; ring|idtac].
pattern (FtoRradix q) at 1; rewrite <- (Rabs_right q).
2: apply Rle_ge; generalize Q_positive; auto with real.
pattern (FtoRradix q) at 1; replace (FtoRradix q) with (-(p-q)+p)%R;[idtac|ring].
apply Rle_trans with (3*(Rabs (-(p-q))+(Rabs p))-q)%R.
unfold Rminus; apply Rplus_le_compat_r.
apply Rmult_le_compat_l; auto with real.
apply Rle_trans with 2%R; auto with real.
apply Rabs_triang.
rewrite Rabs_Ropp.
rewrite (Rabs_right p).
2:apply Rle_ge; apply P_positive with bo precision b b'; auto.
apply Rle_trans with (3 * (Rabs (p - q)) + (3*p - q))%R;[right;ring|idtac].
apply Rle_trans with (p+q+(3*p-q))%R; auto with real.
right;ring.
Qed.
Theorem P_le_two_Q:(p <= 2*q)%R.
fold FtoRradix; apply Rmult_le_reg_l with 2%R; auto with real; simpl.
apply Rle_trans with (3*p-p)%R; [right; ring|idtac].
pattern (FtoRradix p) at 1; rewrite <- (Rabs_right p).
2: apply Rle_ge; apply P_positive with bo precision b b'; auto with real.
pattern (FtoRradix p) at 1; replace (FtoRradix p) with ((p-q)+q)%R;[idtac|ring].
apply Rle_trans with (3*(Rabs (p-q)+(Rabs q))-p)%R.
unfold Rminus; apply Rplus_le_compat_r.
apply Rmult_le_compat_l; auto with real.
apply Rle_trans with 2%R; auto with real.
apply Rabs_triang.
rewrite (Rabs_right q).
2: apply Rle_ge; generalize Q_positive; auto with real.
apply Rle_trans with (3 * (Rabs (p - q)) + (3*q - p))%R;[right;ring|idtac].
apply Rle_trans with (p+q+(3*q-p))%R; auto with real.
right;ring.
Qed.
Theorem t_exact: (FtoRradix t=p-q)%R.
unfold FtoRradix; rewrite <- Fminus_correct; auto with zarith.
apply sym_eq; apply RoundedModeProjectorIdemEq with (b:=bo) (P:=(EvenClosest bo radix precision)) (precision:=precision); auto.
apply EvenClosestRoundedModeP; auto.
2: rewrite Fminus_correct; auto with zarith.
apply Sterbenz; auto.
fold FtoRradix; apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (FtoRradix q);[simpl; right; field; auto with real|idtac].
apply Q_le_two_P.
fold FtoRradix; simpl; apply P_le_two_Q.
Qed.
Theorem dp_dq_le:(Rabs (dp-dq) <= (3/2)*(Rmin
(Fulp bo radix precision p) (Fulp bo radix precision q)))%R.
unfold Rminus; apply Rle_trans with (1:=Rabs_triang dp (-dq)).
rewrite Rabs_Ropp;apply Rmult_le_reg_l with (S (S O))%R; auto with real.
apply Rle_trans with (S 1 * Rabs dp + S 1*Rabs dq)%R;[right;ring|idtac].
apply Rle_trans with ((Fulp bo radix precision p)+(Fulp bo radix precision q))%R.
apply Rplus_le_compat.
rewrite dpEq; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundp; auto.
rewrite dqEq; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundq; auto.
rewrite <- Rmult_assoc.
apply Rle_trans with (3*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q)))%R;[idtac|apply Rmult_le_compat_r].
2: unfold Rmin; case (Rle_dec (Fulp bo radix precision p) (Fulp bo radix precision q)); intros H1; unfold Fulp; auto with real zarith.
2: right; simpl; unfold Rdiv; field; auto with real.
unfold Rmin; case (Rle_dec (Fulp bo radix precision p) (Fulp bo radix precision q)); intros H1.
apply Rle_trans with (Fulp bo radix precision p+2*Fulp bo radix precision p)%R;[apply Rplus_le_compat_l|right;ring].
apply Fulp_le_twice_r; auto with real; fold radix FtoRradix.
generalize Q_positive; auto with real.
apply Q_le_two_P.
apply Rle_trans with (2*Fulp bo radix precision q+Fulp bo radix precision q)%R;[apply Rplus_le_compat_r|right;ring].
apply Fulp_le_twice_r; auto with real; fold radix FtoRradix.
apply P_positive with bo precision b b'; auto with real.
apply P_le_two_Q.
Qed.
Theorem EvenClosestFabs :
forall (f : float) (r : R), (Fcanonic radix bo f)
-> EvenClosest bo radix precision r f ->
EvenClosest bo radix precision (Rabs r) (Fabs f).
intros.
case (Rle_or_lt 0%R r); intros.
rewrite Rabs_right; auto with real.
unfold Fabs; rewrite Zabs_eq; auto with zarith.
apply LeR0Fnum with (radix := radix); auto with zarith.
apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) r; auto with float zarith.
rewrite Rabs_left; auto with real.
replace (Fabs f) with (Fopp f).
generalize EvenClosestSymmetric; unfold SymmetricP; auto.
unfold Fabs, Fopp; rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto.
assert (Fnum f <= 0)%Z; auto with zarith.
apply R0LeFnum with (radix:=radix); auto with zarith.
apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) r; auto with float zarith real.
Qed.
Theorem discri2: (3*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q))
<= (Rabs (p-q)))%R -> (delta <= 2*(Fulp bo radix precision d))%R.
intros H1; unfold delta.
apply Rle_trans with (1 * Fulp bo radix precision d)%R;[ring_simplify (1 * Fulp bo radix precision d)%R | unfold Fulp; auto with real zarith].
replace (d - (b * b' - a * c))%R with ((d-(t+s))+(t+s-b*b'+a*c))%R;[idtac|ring].
apply Rle_trans with (1:=Rabs_triang (d-(t+s))%R (t + s - b * b' + a * c)%R).
apply Rmult_le_reg_l with 2%R; auto with real.
rewrite Rmult_plus_distr_l.
apply Rle_trans with (Fulp bo radix precision d+Fulp bo radix precision d)%R;[idtac|right;ring].
apply Rplus_le_compat.
rewrite <- Rabs_Ropp; replace (- (d - (t + s)))%R with ((t+s)-d)%R;[idtac|ring].
replace 2%R with (INR 2); auto with real.
unfold FtoRradix; apply ClosestUlp; auto.
elim Roundd; auto.
rewrite t_exact.
replace (p - q + s - b * b' + a * c)%R with (-((dp-dq) - s))%R;[idtac|rewrite dpEq; rewrite dqEq; ring].
rewrite Rabs_Ropp; apply Rle_trans with (Fulp bo radix precision s).
unfold FtoRradix; apply ClosestUlp; auto.
elim Rounds; auto.
rewrite FulpFabs; auto; rewrite FulpFabs with (f:=d); auto.
apply LeFulpPos; auto with real zarith float.
rewrite Fabs_correct; auto with real.
apply EvenClosestMonotone2 with bo precision (Rabs (dp-dq)) (Rabs (t+s))%R; auto.
2: apply EvenClosestFabs; auto; left; auto.
2: apply EvenClosestFabs; auto; left; auto.
cut (Rabs (dp - dq) <= (Rabs (p-q))/2)%R.
intros H2; cut ((Rabs s) <= (Rabs t)/2)%R.
intros H3; apply Rle_trans with (1:=H2).
rewrite <- t_exact; apply Rle_trans with ((Rabs t)-(Rabs t)/2)%R.
right; unfold Rdiv; field; auto with real.
apply Rle_trans with ((Rabs t)-(Rabs s))%R; auto with real.
unfold Rminus; apply Rplus_le_compat_l; auto with real.
replace (t+s)%R with (t-(-s))%R; [idtac|ring].
apply Rle_trans with ((Rabs t)-(Rabs (-s)))%R;[idtac|apply Rabs_triang_inv].
rewrite Rabs_Ropp; auto with real.
assert (t/2=(Float (Fnum t) (Zpred (Fexp t))))%R.
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl ; field.
unfold Rdiv; rewrite <- (Rabs_right (/2)%R); auto with real.
2: apply Rle_ge; apply Rlt_le; auto with real.
rewrite <- Rabs_mult; fold (Rdiv t 2%R).
rewrite H; unfold FtoRradix; rewrite <- Fabs_correct; auto.
rewrite <- Fabs_correct; auto.
apply EvenClosestMonotone2 with bo precision (Rabs (dp-dq))%R (Rabs (p-q)/2)%R; auto.
apply EvenClosestFabs; auto; left; auto.
replace (Rabs (p - q) / 2)%R with (FtoRradix (Fabs (Float (Fnum t) (Zpred (Fexp t))))).
unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto.
apply EvenClosestRoundedModeP; auto.
split; simpl; auto with zarith float.
rewrite Zabs_eq; auto with zarith float.
unfold FtoRradix; rewrite Fabs_correct; auto; fold FtoRradix; rewrite <- H.
rewrite t_exact; unfold Rdiv; rewrite Rabs_mult; auto with real.
rewrite (Rabs_right (/2)%R); auto with real.
apply Rle_ge; apply Rlt_le; auto with real.
apply Rle_trans with (1:=dp_dq_le).
apply Rmult_le_reg_l with 2%R; auto with real; unfold Rdiv.
rewrite <- Rmult_assoc.
replace (2*(3*/2))%R with 3%R;[idtac|field; auto with real].
apply Rle_trans with (1:=H1).
right; field; auto with real.
Qed.
Theorem discri3: (exists f:float, (Fbounded bo f) /\ (FtoRradix f)=(dp-dq)%R)
-> (delta <= 2*(Fulp bo radix precision d))%R.
intros T; elim T; intros f T1; elim T1; intros H1 H2; clear T T1.
unfold delta.
replace (d - (b * b' - a * c))%R with (-((t+s)-d))%R.
apply Rmult_le_reg_l with (INR 2); auto with arith real.
apply Rle_trans with (Fulp bo radix precision d).
rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundd; auto.
simpl; apply Rle_trans with (1*(1*(Fulp bo radix precision d)))%R; unfold Fulp; auto with real zarith.
right; ring.
apply Rmult_le_compat; auto with real zarith.
ring_simplify (1 * powerRZ radix (Fexp (Fnormalize radix bo precision d)))%R; auto with real zarith.
replace (FtoRradix s) with (dp-dq)%R.
rewrite dpEq; rewrite dqEq; rewrite t_exact; ring.
rewrite <- H2.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with (b:=bo) (P:=(EvenClosest bo radix precision)) (precision:=precision); auto with real.
apply EvenClosestRoundedModeP; auto.
fold FtoRradix; rewrite H2; auto.
Qed.
Theorem errorBoundedMultClosest_Can:
forall f1 f2 g : float,
Fbounded bo f1 ->
Fbounded bo f2 ->
Closest bo radix (f1* f2) g ->
(powerRZ radix (-dExp bo+2*precision-1) <= Rabs (f1*f2))%R ->
Fcanonic radix bo g ->
(exists s : float,
Fbounded bo s /\
(FtoRradix s = f1*f2 - g)%R /\
Fexp s = (Fexp g - precision)%Z /\
(Rabs (Fnum s) <= powerRZ radix (Zpred precision))%R).
intros.
generalize errorBoundedMultClosest; intros T.
elim T with (b:=bo) (radix:=radix) (precision:=precision) (p:=f1) (q:=f2) (pq:=g); auto with zarith real; clear T; fold FtoRradix.
intros g' T1; elim T1; intros dg T2; elim T2; intros H5 T3; elim T3; intros H6 T4; elim T4; intros H7 T5; elim T5; intros H8 T6; elim T6; intros H9 H10; clear T1 T2 T3 T4 T5 T6.
exists dg; split; auto; split.
rewrite <- H8; auto with real.
split; [replace g with g'; auto with zarith|idtac].
apply FcanonicUnique with radix bo precision; auto with arith.
apply Rmult_le_reg_l with (powerRZ radix (Fexp dg)); auto with zarith real.
apply Rle_trans with (Rabs dg);[right; unfold FtoRradix, FtoR|idtac].
rewrite Rabs_mult;rewrite (Rabs_right (powerRZ radix (Fexp dg)));auto with real.
apply Rle_ge; auto with real zarith.
rewrite H9; rewrite <- powerRZ_add; auto with real zarith.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix precision g').
unfold FtoRradix; apply ClosestUlp; auto.
replace g' with g; auto.
apply FcanonicUnique with radix bo precision; auto with arith.
rewrite CanonicFulp; auto.
right; apply trans_eq with (powerRZ radix (Fexp g'));[unfold FtoR; simpl; ring|idtac].
apply trans_eq with ((powerRZ radix 1%Z)*(powerRZ radix (Fexp dg+Zpred precision)))%R;[rewrite <- powerRZ_add; auto with zarith real|simpl; ring].
rewrite H10; unfold Zpred; auto with zarith real.
ring_simplify (1 + (Fexp g' - precision + (precision + -1)))%Z; auto with real.
assert (- dExp bo + 2 * precision - 1 < 2*precision+Fexp f1+Fexp f2)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with (1:=H2).
rewrite Rabs_mult; unfold FtoRradix; repeat rewrite <- Fabs_correct; auto.
replace (2*precision)%Z with (precision+precision)%Z; auto with zarith.
unfold FtoR, Fabs; simpl.
repeat rewrite powerRZ_add; auto with real zarith.
repeat rewrite <- Rmult_assoc; apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (Zabs (Fnum f1)*Zabs (Fnum f2) * powerRZ 2 (Fexp f1))%R;
[right; ring| apply Rmult_lt_compat_r; auto with real zarith].
apply Rle_lt_trans with (Zabs (Fnum f1)* powerRZ 2 precision)%R.
apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (Zpos (vNum bo)); auto with real zarith float.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rlt_le_trans with (Zpos (vNum bo)); auto with real zarith float.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real.
rewrite FcanonicFnormalizeEq; auto with zarith.
assert (powerRZ radix (- dExp bo + 2 * precision - 1) <= Rabs g)%R.
cut (exists f:float, Fbounded bo f /\
(FtoRradix f=(powerRZ radix (- dExp bo + 2 * precision - 1)))%R).
intros T; elim T; intros f T'; elim T'; intros; clear T T'.
rewrite <- H5; unfold FtoRradix.
apply RoundAbsMonotonel with bo precision
(Closest bo radix) (f1*f2)%R; auto with zarith float real.
apply ClosestRoundedModeP with precision; auto with zarith.
fold FtoRradix; rewrite H5; auto.
exists (Float 1 (-dExp bo+2*precision-1)).
split;[split|idtac].
simpl; apply vNumbMoreThanOne with radix precision; auto with zarith.
apply Zle_trans with (- dExp bo + 2 * precision - 1)%Z; auto with zarith.
unfold FtoRradix, FtoR; simpl; ring.
assert (- dExp bo + 2 * precision - 1 < precision+Fexp g)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with zarith real.
apply Rle_lt_trans with (1:=H4).
unfold FtoRradix; rewrite <- Fabs_correct; auto.
rewrite powerRZ_add; auto with real zarith.
unfold FtoR, Fabs; simpl.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rlt_le_trans with (Zpos (vNum bo)).
elim H1; auto with real zarith float.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
Qed.
Theorem discri4: (Fexp p)=(Fexp q) -> (delta <= 2*(Fulp bo radix precision d))%R.
intros H1; apply discri3.
generalize errorBoundedMultClosest_Can; intros T.
elim T with (f1:=b) (f2:=b') (g:=p); auto with zarith real; clear T.
intros dp' T2; elim T2; intros H2 T3; elim T3; intros H3 T4; elim T4; intros H4 H5; clear T2 T3 T4.
2: elim Roundp; auto.
generalize errorBoundedMultClosest_Can; intros T.
elim T with (f1:=a) (f2:=c) (g:=q); auto with zarith real; clear T.
intros dq' T2; elim T2; intros H2' T3; elim T3; intros H3' T4; elim T4; intros H4' H5'; clear T2 T3 T4.
2: elim Roundq; auto.
2: left; auto.
2: left; auto.
assert ((Rabs (Fnum dp'-Fnum dq') < (powerRZ radix precision))%R \/
(((Rabs dp')= (powerRZ radix (Zpred (Fexp p))))%R /\ ((Rabs dq')= (powerRZ radix (Zpred (Fexp p))))%R)).
case H5; intros.
left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp') (-(Fnum dq'))%R).
rewrite Rabs_Ropp.
apply Rlt_le_trans with ((powerRZ radix (Zpred precision)) +(Rabs (Fnum dq')))%R; auto with real zarith.
apply Rle_trans with ((powerRZ radix (Zpred precision))+ (powerRZ radix (Zpred precision)))%R; auto with real zarith.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
case H5'; intros.
left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp') (-(Fnum dq'))%R); rewrite Rabs_Ropp.
apply Rle_lt_trans with ((powerRZ radix (Zpred precision)) +(Rabs (Fnum dq')))%R; auto with real zarith.
apply Rlt_le_trans with ((powerRZ radix (Zpred precision))+ (powerRZ radix (Zpred precision)))%R; auto with real zarith.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
right; unfold FtoRradix, FtoR;repeat rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (Fexp dp'))); try apply Rle_ge; auto with real zarith.
rewrite (Rabs_right (powerRZ radix (Fexp dq'))); try apply Rle_ge; auto with real zarith.
rewrite H; rewrite H0.
repeat rewrite <- powerRZ_add; auto with real zarith.
rewrite H4'; rewrite H4; unfold Zpred.
ring_simplify (precision + -1 + (Fexp p - precision))%Z; ring_simplify (precision + -1 + (Fexp q - precision))%Z;
ring_simplify (Fexp p+-1)%Z; rewrite <- H1; auto with zarith real.
case H; clear H; intros H.
exists (Float ((Fnum dp')-(Fnum dq'))%Z (Fexp dq')).
split; [split; auto with zarith|idtac].
simpl; apply Zlt_Rlt.
rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto.
rewrite <- Rabs_Zabs; unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; auto with real zarith.
simpl; auto with zarith float.
rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'.
unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; replace (Fexp dp') with (Fexp dq');[ring|idtac].
rewrite H4'; rewrite <- H1; auto with zarith.
rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'.
elim H; unfold Rabs; case (Rcase_abs dp'); case (Rcase_abs dq'); intros.
exists (Float 0%Z 0%Z); split;[split; auto with zarith|idtac].
simpl; case (dExp bo); auto with zarith.
apply trans_eq with (-(-dp')+-dq')%R;[rewrite H0; rewrite H6; unfold FtoRradix, FtoR;simpl|idtac];ring.
exists (Float (-2)%Z (Zpred (Fexp p))); split;[split; simpl; auto with zarith|idtac].
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 1); auto with zarith.
apply Zle_trans with (Fexp dp'); auto with zarith float.
apply trans_eq with (-(-dp')+-dq')%R;[rewrite H0; rewrite H6; unfold FtoRradix, FtoR; simpl|idtac];ring.
exists (Float 2%Z (Zpred (Fexp p))); split;[split;simpl;auto with zarith|idtac].
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 1); auto with zarith.
apply Zle_trans with (Fexp dp'); auto with zarith float.
unfold Rminus;rewrite H0; rewrite H6; unfold FtoRradix, FtoR;simpl; ring.
exists (Float 0%Z 0%Z); split;[split; auto with zarith|idtac].
simpl; case (dExp bo); auto with zarith.
rewrite H0; rewrite H6; unfold FtoRradix, FtoR; simpl;ring.
Qed.
End Discriminant2.
Section Discriminant3.
Variable bo : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ TwoMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix precision.
Variables a b b' c p q t dp dq s d:float.
Let delta := (Rabs (d-(b*b'-a*c)))%R.
Hypothesis Fa : (Fbounded bo a).
Hypothesis Fb : (Fbounded bo b).
Hypothesis Fb': (Fbounded bo b').
Hypothesis Fc : (Fbounded bo c).
Hypothesis Fp : (Fbounded bo p).
Hypothesis Fq : (Fbounded bo q).
Hypothesis Fd : (Fbounded bo d).
Hypothesis Ft : (Fbounded bo t).
Hypothesis Fs : (Fbounded bo s).
Hypothesis Fdp: (Fbounded bo dp).
Hypothesis Fdq: (Fbounded bo dq).
Hypothesis Cs:(Fcanonic radix bo s).
There is no underflow
Hypothesis U1: (- dExp bo <= (Fexp d)-1)%Z.
Hypothesis U2: (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (b*b'))%R.
Hypothesis U3: (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (a*c))%R.
Hypothesis Np:(Fnormal radix bo p).
Hypothesis Nq:(Fnormal radix bo q).
Hypothesis Nd:(Fnormal radix bo d).
Hypothesis Square:(0 <=b*b')%R.
Hypothesis Roundp : (EvenClosest bo radix precision (b*b')%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).
Hypothesis p_pos:(0 <= p)%R.
Hypothesis q_pos:(0 <= q)%R.
Hypothesis Secondcase : (3*(Rabs (p-q)) < p+q)%R.
Hypothesis Roundt : (EvenClosest bo radix precision (p-q)%R t).
Hypothesis dpEq : (FtoRradix dp=b*b'-p)%R.
Hypothesis dqEq : (FtoRradix dq=a*c-q)%R.
Hypothesis Rounds : (EvenClosest bo radix precision (dp-dq)%R s).
Hypothesis Roundd : (EvenClosest bo radix precision (t+s)%R d).
Hypothesis p_differ_q:~(p=q)%R.
Variable e:Z.
Hypothesis p_eqF : p=(Float (Zpower_nat radix (pred precision)) (Zsucc e)).
Hypothesis p_eqR : (FtoRradix p)=(powerRZ radix (precision+e)%Z).
Hypothesis q_eqExp : (Fexp q)=e.
Theorem discri5: (0 < dp*dq)%R -> (delta <= 2*(Fulp bo radix precision d))%R.
intros.
unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto.
assert (forall f1 f2 g : float,
Fbounded bo f1 ->
Fbounded bo f2 ->
Closest bo 2 (FtoR 2 f1 * FtoR 2 f2) g ->
(powerRZ (Zpos 2) (- dExp bo + 2 * precision - 1) <=
Rabs (FtoR 2 f1 * FtoR 2 f2))%R ->
Fcanonic 2 bo g ->
exists s : float,
Fbounded bo s /\
FtoR 2 s = (FtoR 2 f1 * FtoR 2 f2 - FtoR 2 g)%R /\
Fexp s = (Fexp g - precision)%Z /\
(Rabs (Fnum s) <= powerRZ (Zpos 2) (Zpred precision))%R).
apply errorBoundedMultClosest_Can; auto.
fold radix in H0; fold FtoRradix in H0.
elim H0 with (f1:=b) (f2:=b') (g:=p); auto with zarith real.
intros dp' T2; elim T2; intros H2 T3; elim T3; intros H3 T4; elim T4; intros H4 H5; clear T2 T3 T4.
2: elim Roundp; auto.
elim H0 with (f1:=a) (f2:=c) (g:=q); auto with zarith real; clear H0.
intros dq' T2; elim T2; intros H2' T3; elim T3; intros H3' T4; elim T4; intros H4' H5'; clear T2 T3 T4.
2: elim Roundq; auto.
2: left; auto.
2: left; auto.
fold radix; fold FtoRradix; rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'.
exists (Fminus radix dp' dq'); split.
2: unfold FtoRradix; rewrite Fminus_correct; auto with real.
unfold Fminus, Fopp, Fplus; simpl.
repeat rewrite H4'; repeat rewrite q_eqExp; repeat rewrite H4.
replace (Fexp p) with (Zsucc e); [idtac|rewrite p_eqF; auto].
rewrite Zmin_le2; auto with zarith.
split; auto with zarith.
simpl; unfold Zsucc.
ring_simplify (e + 1 - precision - (e - precision))%Z; ring_simplify (e - precision - (e - precision))%Z.
simpl.
unfold nat_of_P, Zpower_nat; simpl.
replace ( - Fnum dq' * 1)%Z with (- Fnum dq')%Z; [idtac|ring].
apply Zlt_Rlt.
rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto.
rewrite <- Rabs_Zabs; rewrite plus_IZR;rewrite mult_IZR;rewrite Ropp_Ropp_IZR.
assert (forall (x y z:R), (0 < x*y)%R -> (Rabs x <= z)%R ->
(Rabs y <= z)%R -> (Rabs (2*x-y) < 2*z)%R).
intros.
unfold Rabs; case (Rcase_abs (2*x-y)%R); case (Rle_or_lt 0%R x); intros.
case H7; intros;ring_simplify (- (2 * x - y))%R.
assert (-x <0)%R; auto with real.
apply Rlt_le_trans with (-2*0+y)%R; auto with real.
apply Rplus_lt_compat_r; repeat rewrite Ropp_mult_distr_l_reverse; auto with real.
ring_simplify (-2*0+y)%R; apply Rle_trans with z; auto with real.
apply Rle_trans with (2:=H6); apply RRle_abs.
apply Rle_trans with (1*z)%R; auto with real.
apply Rmult_le_compat_r; auto with real.
apply Rle_trans with (2:=H1); auto with real.
Contradict H0; rewrite <- H8; auto with real.
ring_simplify (0*y)%R; auto with real.
ring_simplify (- (2 * x - y))%R.
apply Rlt_le_trans with (-2*x+0)%R;[apply Rplus_lt_compat_l|idtac].
apply Rmult_lt_reg_l with (-x)%R; auto with real.
apply Rle_lt_trans with (-(x*y))%R; auto with real.
apply Rlt_le_trans with (-0)%R; auto with real; right;ring.
apply Rle_trans with (2*(-x))%R;[right;ring|apply Rmult_le_compat_l; auto with real].
apply Rle_trans with (2:=H1); rewrite <- Rabs_Ropp; apply RRle_abs.
apply Rlt_le_trans with (2*x-0)%R;[unfold Rminus; apply Rplus_lt_compat_l|idtac].
apply Ropp_lt_contravar; apply Rmult_lt_reg_l with x; auto with real.
case H7; auto with real.
intros H8; Contradict H0; rewrite <- H8; ring_simplify (0*y)%R; auto with real.
ring_simplify (x*0)%R; auto with real.
apply Rle_trans with (2*x)%R;[right;ring|apply Rmult_le_compat_l; auto with real].
apply Rle_trans with (2:=H1); apply RRle_abs.
apply Rlt_le_trans with (2*0-y)%R; [unfold Rminus; apply Rplus_lt_compat_r; apply Rmult_lt_compat_l; auto with real|idtac].
apply Rle_trans with (-y)%R;[right;ring|apply Rle_trans with z].
apply Rle_trans with (2:=H6); rewrite <- Rabs_Ropp; apply RRle_abs.
apply Rle_trans with (1*z)%R;[right;ring|apply Rmult_le_compat_r; auto with real].
apply Rle_trans with (2:=H1); auto with real.
replace (Fnum dp' * Zpos 2+-Fnum dq')%R with (2*(Fnum dp')-Fnum dq')%R; auto with real zarith.
apply Rlt_le_trans with (2*powerRZ radix (Zpred precision))%R.
apply H0; auto.
apply Rmult_lt_reg_l with (powerRZ radix (Fexp dq')); auto with real zarith.
apply Rmult_lt_reg_l with (powerRZ radix (Fexp dp')); auto with real zarith.
apply Rle_lt_trans with 0%R;[right;ring|apply Rlt_le_trans with (1:=H)].
rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'.
unfold FtoRradix, FtoR; right; ring.
right; unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith.
simpl; field; apply Rmult_integral_contrapositive; split; auto with real.
simpl; ring.
simpl;rewrite <-q_eqExp; rewrite <- H4'; auto with zarith float.
Qed.
Theorem discri6: (0< dp)%R -> (dq < 0)%R
-> (delta <= 2*(Fulp bo radix precision d))%R.
intros;unfold delta.
replace (d - (b * b' - a * c))%R with (-((t+s)-d)+-((dp-dq)-s))%R.
2: rewrite dpEq; rewrite dqEq; unfold FtoRradix, radix; rewrite t_exact with bo precision b b' p q t; auto; ring.
apply Rle_trans with (1:=Rabs_triang (-(t+s-d))%R (-(dp-dq-s))%R).
apply Rmult_le_reg_l with (INR 2); auto with real zarith;rewrite Rmult_plus_distr_l.
apply Rle_trans with ((Fulp bo radix precision d)+(Fulp bo radix precision s))%R;[apply Rplus_le_compat|idtac].
rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundd; auto.
rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto.
elim Rounds; auto.
apply Rle_trans with ((Fulp bo radix precision d+ 3* Fulp bo radix precision d))%R;[apply Rplus_le_compat_l|simpl;right;ring].
apply Rle_trans with (2*Fulp bo radix precision d)%R;[idtac|unfold Fulp; auto with real zarith].
rewrite FulpFabs; auto; rewrite FulpFabs with bo radix precision d; auto.
assert (2*(Fabs d)=(Float (Fnum (Fabs d)) (Zsucc (Fexp (Fabs d)))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum (Fabs d)) (Zsucc (Fexp (Fabs d))))).
2:assert (Fnormal radix bo (Fabs d));[apply FnormalFabs; auto|idtac].
2:right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto.
2:unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith.
2:simpl; ring.
2:left; auto.
2:elim H2; intros H6 H5; elim H6; intros.
2:split; simpl; auto with zarith.
2:split; simpl; auto with zarith.
apply LeFulpPos; auto with real float.
assert (Fnormal radix bo (Fabs d));[apply FnormalFabs; auto|idtac].
elim H2; intros H6 H5; elim H6; intros;split; simpl; auto with zarith.
rewrite Fabs_correct; auto with real zarith.
apply EvenClosestMonotone2 with bo precision (Rabs (dp-dq))%R (2*Rabs (t+s))%R; auto.
2: apply EvenClosestFabs; auto; left; auto.
2: apply Twice_EvenClosest_Round; auto.
2: apply FnormalFabs; auto.
2: apply EvenClosestFabs; auto; left; auto.
unfold Rminus; apply Rle_trans with (1:=Rabs_triang dp (-dq)%R).
apply Rmult_le_reg_l with (INR 2); auto with real zarith; rewrite Rmult_plus_distr_l.
apply Rle_trans with (Fulp bo radix precision p+Fulp bo radix precision q)%R;[apply Rplus_le_compat|idtac].
rewrite dpEq; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundp; auto.
rewrite Rabs_Ropp; rewrite dqEq; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundq; auto.
rewrite CanonicFulp; auto with float;[idtac|left; auto].
rewrite CanonicFulp; auto with float;[idtac|left; auto].
apply Rle_trans with (3*(powerRZ radix e))%R;[right|idtac].
unfold FtoRradix, FtoR; simpl; rewrite q_eqExp; rewrite p_eqF; simpl.
unfold Zsucc; rewrite powerRZ_add; auto with real zarith; simpl;ring.
assert ((powerRZ radix e <= t))%R.
unfold FtoRradix, radix; rewrite t_exact with bo precision b b' p q t; auto.
fold radix; fold FtoRradix; rewrite p_eqR.
apply Rle_trans with (powerRZ radix (precision + e) - ((powerRZ radix precision - 1) * powerRZ radix e))%R; auto with real.
rewrite powerRZ_add; auto with real zarith; right;ring.
unfold Rminus; apply Rplus_le_compat_l; auto with real.
apply Ropp_le_contravar.
unfold FtoRradix, FtoR; rewrite q_eqExp; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (1:=(RRle_abs (Fnum q))).
assert (Zabs (Fnum q) < Zpower_nat radix precision)%Z; auto with real zarith float.
rewrite <- pGivesBound; auto with zarith float.
rewrite Rabs_Zabs; apply Rle_trans with (Zpred (Zpower_nat radix precision)); auto with real zarith.
unfold Zpred; rewrite plus_IZR.
rewrite Zpower_nat_Z_powerRZ; right; simpl; ring.
assert (0<=s)%R.
unfold FtoRradix; apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) (dp-dq)%R; auto with real.
apply EvenClosestRoundedModeP; auto.
apply Rle_trans with (0-0)%R; unfold Rminus; auto with real.
apply Rplus_le_compat; auto with real.
rewrite Rabs_right; auto with real.
2: apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.
2: apply Rplus_le_compat; auto with real zarith.
2: apply Rle_trans with (2:=H2); auto with real zarith.
apply Rle_trans with (4*powerRZ radix e)%R;[apply Rmult_le_compat_r; auto with real zarith|idtac].
replace 3%R with (INR 3);[idtac|simpl; ring].
replace 4%R with (INR 4);[auto with real zarith|simpl;ring].
apply Rle_trans with (4*(t+s))%R;[apply Rmult_le_compat_l; auto with real|simpl; right; ring].
replace 4%R with (INR 4);[auto with real zarith|simpl;ring].
apply Rle_trans with (powerRZ radix e+0)%R;[idtac|apply Rplus_le_compat];auto with real.
Qed.
Theorem discri7: (dp < 0)%R -> (0 < dq)%R
-> (delta <= 2*(Fulp bo radix precision d))%R.
intros L1 L2.
unfold delta, FtoRradix; apply discri3 with p q t dp dq s; auto.
assert (H0:forall f1 f2 g : float,
Fbounded bo f1 ->
Fbounded bo f2 ->
Closest bo 2 (FtoR 2 f1 * FtoR 2 f2) g ->
(powerRZ (Zpos 2) (- dExp bo + 2 * precision - 1) <=
Rabs (FtoR 2 f1 * FtoR 2 f2))%R ->
Fcanonic 2 bo g ->
exists s : float,
Fbounded bo s /\
FtoR 2 s = (FtoR 2 f1 * FtoR 2 f2 - FtoR 2 g)%R /\
Fexp s = (Fexp g - precision)%Z /\
(Rabs (Fnum s) <= powerRZ (Zpos 2) (Zpred precision))%R).
apply errorBoundedMultClosest_Can; auto.
fold radix in H0; fold FtoRradix in H0.
elim H0 with (f1:=b) (f2:=b') (g:=p); auto with zarith real.
intros dp' T2; elim T2; intros H2 T3; elim T3; intros H3 T4; elim T4; intros H4
H5; clear T2 T3 T4.
2: elim Roundp; auto.
elim H0 with (f1:=a) (f2:=c) (g:=q); auto with zarith real; clear H0.
intros dq' T2; elim T2; intros H2' T3; elim T3; intros H3' T4; elim T4; intros H4' H5'; clear T2 T3 T4.
2: elim Roundq; auto.
2: left; auto.
2: left; auto.
cut (exists dp'':float, (Fexp dp''=Fexp dq' /\ (FtoRradix dp''=dp')%R /\
(Rabs (Fnum dp'') <= powerRZ radix (Zpred precision))%R)).
intros T; elim T; intros dp'' T1; elim T1; intros H4'' T2; elim T2;
intros H5'' H6''; clear T T1 T2.
assert ((Rabs (Fnum dp''-Fnum dq') < (powerRZ radix precision))%R \/
(((Rabs dp'')= (powerRZ radix (Zpred (Fexp q))))%R /\ ((Rabs dq')=
(powerRZ radix (Zpred (Fexp q))))%R)).
case H6''; intros.
left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp'')
(-(Fnum dq'))%R).
rewrite Rabs_Ropp.
apply Rlt_le_trans with ((powerRZ radix (Zpred precision)) +(Rabs (Fnum
dq')))%R; auto with real zarith.
apply Rle_trans with ((powerRZ radix (Zpred precision))+ (powerRZ radix
(Zpred precision)))%R; auto with real zarith.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
case H5'; intros.
left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp'') (-(Fnum
dq'))%R); rewrite Rabs_Ropp.
apply Rle_lt_trans with ((powerRZ radix (Zpred precision)) +(Rabs (Fnum dq')))%R
; auto with real zarith.
apply Rlt_le_trans with ((powerRZ radix (Zpred precision))+ (powerRZ radix (Zpred precision)))%R; auto with real zarith.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
right; unfold FtoRradix, FtoR;repeat rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (Fexp dp''))); try apply Rle_ge; auto with real zarith.
rewrite (Rabs_right (powerRZ radix (Fexp dq'))); try apply Rle_ge; auto with real zarith.
rewrite H; rewrite H0.
repeat rewrite <- powerRZ_add; auto with real zarith.
rewrite H4''; rewrite H4'; unfold Zpred.
ring_simplify (precision + -1 + (Fexp q - precision))%Z; ring_simplify (precision + -1 + (Fexp q -
precision))%Z; ring_simplify (Fexp q+-1)%Z; auto with zarith real.
case H; intros V; clear H.
exists (Float (Fnum dp''-Fnum dq') (Fexp dq')).
split;[split; auto with zarith|idtac].
simpl; apply Zlt_Rlt.
rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto.
rewrite <- Rabs_Zabs; unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; auto with real zarith.
simpl; auto with zarith float.
fold radix; fold FtoRradix; rewrite dpEq; rewrite dqEq.
rewrite <- H3'; rewrite <- H3;rewrite <- H5''.
unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR.
rewrite H4''; ring.
exists (Float (-1)%Z (Fexp q)).
split;[split; simpl; auto with zarith|idtac].
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 0); auto with zarith.
elim Roundq; auto with zarith float.
fold radix; fold FtoRradix; elim V; intros.
replace (FtoRradix dp) with (-(-dp))%R;[idtac|ring].
rewrite <- (Rabs_left dp); auto with real.
rewrite <- (Rabs_right dq); auto with real.
2: apply Rle_ge; auto with real.
rewrite dpEq; rewrite <- H3; rewrite <- H5''; rewrite H.
rewrite dqEq; rewrite <- H3'; rewrite H0.
unfold FtoRradix, FtoR, Zpred; simpl.
repeat rewrite powerRZ_add; auto with real zarith; simpl; field.
assert (FtoRradix dp'=(Float (2*Fnum dp') (Zpred (Fexp dp'))))%R.
unfold FtoRradix, FtoR, Zpred.
apply trans_eq with ((2 * Fnum dp')%Z*(powerRZ radix (Fexp dp'+-1)))%R;[auto|idtac].
rewrite mult_IZR;rewrite powerRZ_add; auto with real zarith; simpl; field.
simpl; auto with real.
exists (Float (2*Fnum dp') (Zpred (Fexp dp'))); split.
simpl; rewrite H4'; rewrite H4.
rewrite q_eqExp; rewrite p_eqF; unfold Zpred, Zsucc;simpl; auto with zarith.
split; auto with real.
apply Rmult_le_reg_l with (powerRZ radix (Zpred (Fexp dp'))); auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
rewrite <- (Rabs_right (powerRZ radix (Zpred (Fexp dp'))));auto with real.
2: apply Rle_ge; auto with real zarith.
rewrite <- Rabs_mult.
replace (powerRZ radix (Zpred (Fexp dp')) *
Fnum (Float (2 * Fnum dp') (Zpred (Fexp dp'))))%R with (FtoRradix dp'); auto with real.
2: rewrite H; unfold FtoRradix, FtoR; simpl; auto with real.
rewrite H3; rewrite <- dpEq.
rewrite H4; unfold Zpred;ring_simplify (Fexp p - precision + -1 + (precision + -1))%Z.
rewrite Rabs_left; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (FtoRradix dp).
ring_simplify (dp+2*(-dp))%R.
rewrite <- Rabs_left; auto with real.
assert (Fbounded bo (Float (Zpred (Zpower_nat radix precision)) e)).
split; auto with zarith.
simpl; rewrite pGivesBound; auto with zarith.
rewrite Zabs_eq; auto with zarith.
simpl; rewrite <- q_eqExp; elim Roundq; auto with zarith float.
rewrite <- Rabs_Ropp.
replace (-dp)%R with (p-b*b')%R; [idtac|rewrite dpEq;ring].
elim Roundp; intros K1 K2; elim K1; intros K3 K4.
apply Rle_trans with (Rabs ((Float (Zpred (Zpower_nat radix precision)) e)-b*b')).
unfold FtoRradix; apply K4; auto.
clear K1 K2 K3 K4; rewrite Rabs_left1.
rewrite dpEq; rewrite p_eqR.
apply Rle_trans with (b*b'-(powerRZ radix precision -1)*(powerRZ radix e))%R.
unfold FtoRradix, FtoR, Zpred, radix; simpl.
rewrite plus_IZR; simpl; right; ring_simplify.
rewrite Zpower_nat_Z_powerRZ; auto with real zarith; simpl; ring.
unfold Rminus; rewrite Rplus_assoc; apply Rplus_le_compat_l.
replace (Fexp p) with (Zsucc e);[unfold Zsucc|rewrite p_eqF; simpl; auto with zarith].
ring_simplify (e+1-2)%Z; unfold Zminus.
repeat rewrite powerRZ_add; auto with real zarith; simpl; right; field.
apply Rplus_le_reg_l with (p-(Float (Zpred (Zpower_nat radix precision)) e))%R.
apply Rle_trans with (-(b*b'-p))%R;[right;ring|idtac].
rewrite <- dpEq; rewrite <- Rabs_left; auto with real.
rewrite dpEq; apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix precision p).
unfold FtoRradix; apply ClosestUlp; auto.
elim Roundp; auto.
rewrite CanonicFulp; auto;[idtac|left; auto].
replace (Fexp p) with (Zsucc e);[unfold Zsucc|rewrite p_eqF; simpl; auto with zarith].
rewrite p_eqR; unfold FtoRradix, FtoR, Zpred; simpl.
rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
repeat rewrite powerRZ_add; auto with real zarith; simpl; right; field.
Qed.
Theorem discri8: (delta <= 2*(Fulp bo radix precision d))%R.
case (Rle_or_lt 0%R dp); intros H;[case H; clear H; intros H|idtac].
case (Rle_or_lt 0%R dq); intros H';[case H'; clear H'; intros H'|idtac].
apply discri5; auto with real.
apply Rle_lt_trans with (dp*0)%R;[right;ring|auto with real].
unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto.
exists dp; split; auto.
fold radix; fold FtoRradix; rewrite <- H'; ring.
apply discri6; auto.
unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto.
exists (Fopp dq); split; auto with float zarith.
rewrite Fopp_correct; fold radix; fold FtoRradix; rewrite <- H; ring.
case (Rle_or_lt 0%R dq); intros H';[case H'; clear H'; intros H'|idtac].
apply discri7; auto.
unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto.
exists dp; split; auto.
fold radix; fold FtoRradix; rewrite <- H'; ring.
apply discri5; auto.
apply Rle_lt_trans with (-dp*0)%R;[right;ring|idtac].
apply Rlt_le_trans with ((-dp)*(-dq))%R;[auto with real|right;ring].
Qed.
End Discriminant3.
Section Discriminant4.
Variable bo : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ TwoMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix precision.
Variables a b c p q t dp dq s d:float.
Let delta := (Rabs (d-(b*b-a*c)))%R.
Hypothesis Fa : (Fbounded bo a).
Hypothesis Fb : (Fbounded bo b).
Hypothesis Fc : (Fbounded bo c).
Hypothesis Fp : (Fbounded bo p).
Hypothesis Fq : (Fbounded bo q).
Hypothesis Fd : (Fbounded bo d).
Hypothesis Ft : (Fbounded bo t).
Hypothesis Fs : (3*(Rabs (p-q)) < p+q)%R -> (Fbounded bo s).
Hypothesis Fdp: (3*(Rabs (p-q)) < p+q)%R -> (Fbounded bo dp).
Hypothesis Fdq: (3*(Rabs (p-q)) < p+q)%R -> (Fbounded bo dq).
Hypothesis Cs:(3*(Rabs (p-q)) < p+q)%R -> (Fcanonic radix bo s).
Hypothesis U2: (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (b*b'))%R.
Hypothesis U3: (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (a*c))%R.
Hypothesis Np:(Fnormal radix bo p).
Hypothesis Nq:(Fnormal radix bo q).
Hypothesis Nd:(Fnormal radix bo d).
Hypothesis Square:(0 <=b*b')%R.
Hypothesis Roundp : (EvenClosest bo radix precision (b*b')%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).
Hypothesis p_pos:(0 <= p)%R.
Hypothesis q_pos:(0 <= q)%R.
Hypothesis Secondcase : (3*(Rabs (p-q)) < p+q)%R.
Hypothesis Roundt : (EvenClosest bo radix precision (p-q)%R t).
Hypothesis dpEq : (FtoRradix dp=b*b'-p)%R.
Hypothesis dqEq : (FtoRradix dq=a*c-q)%R.
Hypothesis Rounds : (EvenClosest bo radix precision (dp-dq)%R s).
Hypothesis Roundd : (EvenClosest bo radix precision (t+s)%R d).
Hypothesis p_differ_q:~(p=q)%R.
Variable e:Z.
Hypothesis p_eqF : p=(Float (Zpower_nat radix (pred precision)) (Zsucc e)).
Hypothesis p_eqR : (FtoRradix p)=(powerRZ radix (precision+e)%Z).
Hypothesis q_eqExp : (Fexp q)=e.
Theorem discri5: (0 < dp*dq)%R -> (delta <= 2*(Fulp bo radix precision d))%R.
intros.
unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto.
assert (forall f1 f2 g : float,
Fbounded bo f1 ->
Fbounded bo f2 ->
Closest bo 2 (FtoR 2 f1 * FtoR 2 f2) g ->
(powerRZ (Zpos 2) (- dExp bo + 2 * precision - 1) <=
Rabs (FtoR 2 f1 * FtoR 2 f2))%R ->
Fcanonic 2 bo g ->
exists s : float,
Fbounded bo s /\
FtoR 2 s = (FtoR 2 f1 * FtoR 2 f2 - FtoR 2 g)%R /\
Fexp s = (Fexp g - precision)%Z /\
(Rabs (Fnum s) <= powerRZ (Zpos 2) (Zpred precision))%R).
apply errorBoundedMultClosest_Can; auto.
fold radix in H0; fold FtoRradix in H0.
elim H0 with (f1:=b) (f2:=b') (g:=p); auto with zarith real.
intros dp' T2; elim T2; intros H2 T3; elim T3; intros H3 T4; elim T4; intros H4 H5; clear T2 T3 T4.
2: elim Roundp; auto.
elim H0 with (f1:=a) (f2:=c) (g:=q); auto with zarith real; clear H0.
intros dq' T2; elim T2; intros H2' T3; elim T3; intros H3' T4; elim T4; intros H4' H5'; clear T2 T3 T4.
2: elim Roundq; auto.
2: left; auto.
2: left; auto.
fold radix; fold FtoRradix; rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'.
exists (Fminus radix dp' dq'); split.
2: unfold FtoRradix; rewrite Fminus_correct; auto with real.
unfold Fminus, Fopp, Fplus; simpl.
repeat rewrite H4'; repeat rewrite q_eqExp; repeat rewrite H4.
replace (Fexp p) with (Zsucc e); [idtac|rewrite p_eqF; auto].
rewrite Zmin_le2; auto with zarith.
split; auto with zarith.
simpl; unfold Zsucc.
ring_simplify (e + 1 - precision - (e - precision))%Z; ring_simplify (e - precision - (e - precision))%Z.
simpl.
unfold nat_of_P, Zpower_nat; simpl.
replace ( - Fnum dq' * 1)%Z with (- Fnum dq')%Z; [idtac|ring].
apply Zlt_Rlt.
rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto.
rewrite <- Rabs_Zabs; rewrite plus_IZR;rewrite mult_IZR;rewrite Ropp_Ropp_IZR.
assert (forall (x y z:R), (0 < x*y)%R -> (Rabs x <= z)%R ->
(Rabs y <= z)%R -> (Rabs (2*x-y) < 2*z)%R).
intros.
unfold Rabs; case (Rcase_abs (2*x-y)%R); case (Rle_or_lt 0%R x); intros.
case H7; intros;ring_simplify (- (2 * x - y))%R.
assert (-x <0)%R; auto with real.
apply Rlt_le_trans with (-2*0+y)%R; auto with real.
apply Rplus_lt_compat_r; repeat rewrite Ropp_mult_distr_l_reverse; auto with real.
ring_simplify (-2*0+y)%R; apply Rle_trans with z; auto with real.
apply Rle_trans with (2:=H6); apply RRle_abs.
apply Rle_trans with (1*z)%R; auto with real.
apply Rmult_le_compat_r; auto with real.
apply Rle_trans with (2:=H1); auto with real.
Contradict H0; rewrite <- H8; auto with real.
ring_simplify (0*y)%R; auto with real.
ring_simplify (- (2 * x - y))%R.
apply Rlt_le_trans with (-2*x+0)%R;[apply Rplus_lt_compat_l|idtac].
apply Rmult_lt_reg_l with (-x)%R; auto with real.
apply Rle_lt_trans with (-(x*y))%R; auto with real.
apply Rlt_le_trans with (-0)%R; auto with real; right;ring.
apply Rle_trans with (2*(-x))%R;[right;ring|apply Rmult_le_compat_l; auto with real].
apply Rle_trans with (2:=H1); rewrite <- Rabs_Ropp; apply RRle_abs.
apply Rlt_le_trans with (2*x-0)%R;[unfold Rminus; apply Rplus_lt_compat_l|idtac].
apply Ropp_lt_contravar; apply Rmult_lt_reg_l with x; auto with real.
case H7; auto with real.
intros H8; Contradict H0; rewrite <- H8; ring_simplify (0*y)%R; auto with real.
ring_simplify (x*0)%R; auto with real.
apply Rle_trans with (2*x)%R;[right;ring|apply Rmult_le_compat_l; auto with real].
apply Rle_trans with (2:=H1); apply RRle_abs.
apply Rlt_le_trans with (2*0-y)%R; [unfold Rminus; apply Rplus_lt_compat_r; apply Rmult_lt_compat_l; auto with real|idtac].
apply Rle_trans with (-y)%R;[right;ring|apply Rle_trans with z].
apply Rle_trans with (2:=H6); rewrite <- Rabs_Ropp; apply RRle_abs.
apply Rle_trans with (1*z)%R;[right;ring|apply Rmult_le_compat_r; auto with real].
apply Rle_trans with (2:=H1); auto with real.
replace (Fnum dp' * Zpos 2+-Fnum dq')%R with (2*(Fnum dp')-Fnum dq')%R; auto with real zarith.
apply Rlt_le_trans with (2*powerRZ radix (Zpred precision))%R.
apply H0; auto.
apply Rmult_lt_reg_l with (powerRZ radix (Fexp dq')); auto with real zarith.
apply Rmult_lt_reg_l with (powerRZ radix (Fexp dp')); auto with real zarith.
apply Rle_lt_trans with 0%R;[right;ring|apply Rlt_le_trans with (1:=H)].
rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'.
unfold FtoRradix, FtoR; right; ring.
right; unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith.
simpl; field; apply Rmult_integral_contrapositive; split; auto with real.
simpl; ring.
simpl;rewrite <-q_eqExp; rewrite <- H4'; auto with zarith float.
Qed.
Theorem discri6: (0< dp)%R -> (dq < 0)%R
-> (delta <= 2*(Fulp bo radix precision d))%R.
intros;unfold delta.
replace (d - (b * b' - a * c))%R with (-((t+s)-d)+-((dp-dq)-s))%R.
2: rewrite dpEq; rewrite dqEq; unfold FtoRradix, radix; rewrite t_exact with bo precision b b' p q t; auto; ring.
apply Rle_trans with (1:=Rabs_triang (-(t+s-d))%R (-(dp-dq-s))%R).
apply Rmult_le_reg_l with (INR 2); auto with real zarith;rewrite Rmult_plus_distr_l.
apply Rle_trans with ((Fulp bo radix precision d)+(Fulp bo radix precision s))%R;[apply Rplus_le_compat|idtac].
rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundd; auto.
rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto.
elim Rounds; auto.
apply Rle_trans with ((Fulp bo radix precision d+ 3* Fulp bo radix precision d))%R;[apply Rplus_le_compat_l|simpl;right;ring].
apply Rle_trans with (2*Fulp bo radix precision d)%R;[idtac|unfold Fulp; auto with real zarith].
rewrite FulpFabs; auto; rewrite FulpFabs with bo radix precision d; auto.
assert (2*(Fabs d)=(Float (Fnum (Fabs d)) (Zsucc (Fexp (Fabs d)))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum (Fabs d)) (Zsucc (Fexp (Fabs d))))).
2:assert (Fnormal radix bo (Fabs d));[apply FnormalFabs; auto|idtac].
2:right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto.
2:unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith.
2:simpl; ring.
2:left; auto.
2:elim H2; intros H6 H5; elim H6; intros.
2:split; simpl; auto with zarith.
2:split; simpl; auto with zarith.
apply LeFulpPos; auto with real float.
assert (Fnormal radix bo (Fabs d));[apply FnormalFabs; auto|idtac].
elim H2; intros H6 H5; elim H6; intros;split; simpl; auto with zarith.
rewrite Fabs_correct; auto with real zarith.
apply EvenClosestMonotone2 with bo precision (Rabs (dp-dq))%R (2*Rabs (t+s))%R; auto.
2: apply EvenClosestFabs; auto; left; auto.
2: apply Twice_EvenClosest_Round; auto.
2: apply FnormalFabs; auto.
2: apply EvenClosestFabs; auto; left; auto.
unfold Rminus; apply Rle_trans with (1:=Rabs_triang dp (-dq)%R).
apply Rmult_le_reg_l with (INR 2); auto with real zarith; rewrite Rmult_plus_distr_l.
apply Rle_trans with (Fulp bo radix precision p+Fulp bo radix precision q)%R;[apply Rplus_le_compat|idtac].
rewrite dpEq; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundp; auto.
rewrite Rabs_Ropp; rewrite dqEq; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundq; auto.
rewrite CanonicFulp; auto with float;[idtac|left; auto].
rewrite CanonicFulp; auto with float;[idtac|left; auto].
apply Rle_trans with (3*(powerRZ radix e))%R;[right|idtac].
unfold FtoRradix, FtoR; simpl; rewrite q_eqExp; rewrite p_eqF; simpl.
unfold Zsucc; rewrite powerRZ_add; auto with real zarith; simpl;ring.
assert ((powerRZ radix e <= t))%R.
unfold FtoRradix, radix; rewrite t_exact with bo precision b b' p q t; auto.
fold radix; fold FtoRradix; rewrite p_eqR.
apply Rle_trans with (powerRZ radix (precision + e) - ((powerRZ radix precision - 1) * powerRZ radix e))%R; auto with real.
rewrite powerRZ_add; auto with real zarith; right;ring.
unfold Rminus; apply Rplus_le_compat_l; auto with real.
apply Ropp_le_contravar.
unfold FtoRradix, FtoR; rewrite q_eqExp; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (1:=(RRle_abs (Fnum q))).
assert (Zabs (Fnum q) < Zpower_nat radix precision)%Z; auto with real zarith float.
rewrite <- pGivesBound; auto with zarith float.
rewrite Rabs_Zabs; apply Rle_trans with (Zpred (Zpower_nat radix precision)); auto with real zarith.
unfold Zpred; rewrite plus_IZR.
rewrite Zpower_nat_Z_powerRZ; right; simpl; ring.
assert (0<=s)%R.
unfold FtoRradix; apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) (dp-dq)%R; auto with real.
apply EvenClosestRoundedModeP; auto.
apply Rle_trans with (0-0)%R; unfold Rminus; auto with real.
apply Rplus_le_compat; auto with real.
rewrite Rabs_right; auto with real.
2: apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.
2: apply Rplus_le_compat; auto with real zarith.
2: apply Rle_trans with (2:=H2); auto with real zarith.
apply Rle_trans with (4*powerRZ radix e)%R;[apply Rmult_le_compat_r; auto with real zarith|idtac].
replace 3%R with (INR 3);[idtac|simpl; ring].
replace 4%R with (INR 4);[auto with real zarith|simpl;ring].
apply Rle_trans with (4*(t+s))%R;[apply Rmult_le_compat_l; auto with real|simpl; right; ring].
replace 4%R with (INR 4);[auto with real zarith|simpl;ring].
apply Rle_trans with (powerRZ radix e+0)%R;[idtac|apply Rplus_le_compat];auto with real.
Qed.
Theorem discri7: (dp < 0)%R -> (0 < dq)%R
-> (delta <= 2*(Fulp bo radix precision d))%R.
intros L1 L2.
unfold delta, FtoRradix; apply discri3 with p q t dp dq s; auto.
assert (H0:forall f1 f2 g : float,
Fbounded bo f1 ->
Fbounded bo f2 ->
Closest bo 2 (FtoR 2 f1 * FtoR 2 f2) g ->
(powerRZ (Zpos 2) (- dExp bo + 2 * precision - 1) <=
Rabs (FtoR 2 f1 * FtoR 2 f2))%R ->
Fcanonic 2 bo g ->
exists s : float,
Fbounded bo s /\
FtoR 2 s = (FtoR 2 f1 * FtoR 2 f2 - FtoR 2 g)%R /\
Fexp s = (Fexp g - precision)%Z /\
(Rabs (Fnum s) <= powerRZ (Zpos 2) (Zpred precision))%R).
apply errorBoundedMultClosest_Can; auto.
fold radix in H0; fold FtoRradix in H0.
elim H0 with (f1:=b) (f2:=b') (g:=p); auto with zarith real.
intros dp' T2; elim T2; intros H2 T3; elim T3; intros H3 T4; elim T4; intros H4
H5; clear T2 T3 T4.
2: elim Roundp; auto.
elim H0 with (f1:=a) (f2:=c) (g:=q); auto with zarith real; clear H0.
intros dq' T2; elim T2; intros H2' T3; elim T3; intros H3' T4; elim T4; intros H4' H5'; clear T2 T3 T4.
2: elim Roundq; auto.
2: left; auto.
2: left; auto.
cut (exists dp'':float, (Fexp dp''=Fexp dq' /\ (FtoRradix dp''=dp')%R /\
(Rabs (Fnum dp'') <= powerRZ radix (Zpred precision))%R)).
intros T; elim T; intros dp'' T1; elim T1; intros H4'' T2; elim T2;
intros H5'' H6''; clear T T1 T2.
assert ((Rabs (Fnum dp''-Fnum dq') < (powerRZ radix precision))%R \/
(((Rabs dp'')= (powerRZ radix (Zpred (Fexp q))))%R /\ ((Rabs dq')=
(powerRZ radix (Zpred (Fexp q))))%R)).
case H6''; intros.
left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp'')
(-(Fnum dq'))%R).
rewrite Rabs_Ropp.
apply Rlt_le_trans with ((powerRZ radix (Zpred precision)) +(Rabs (Fnum
dq')))%R; auto with real zarith.
apply Rle_trans with ((powerRZ radix (Zpred precision))+ (powerRZ radix
(Zpred precision)))%R; auto with real zarith.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
case H5'; intros.
left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp'') (-(Fnum
dq'))%R); rewrite Rabs_Ropp.
apply Rle_lt_trans with ((powerRZ radix (Zpred precision)) +(Rabs (Fnum dq')))%R
; auto with real zarith.
apply Rlt_le_trans with ((powerRZ radix (Zpred precision))+ (powerRZ radix (Zpred precision)))%R; auto with real zarith.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
right; unfold FtoRradix, FtoR;repeat rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (Fexp dp''))); try apply Rle_ge; auto with real zarith.
rewrite (Rabs_right (powerRZ radix (Fexp dq'))); try apply Rle_ge; auto with real zarith.
rewrite H; rewrite H0.
repeat rewrite <- powerRZ_add; auto with real zarith.
rewrite H4''; rewrite H4'; unfold Zpred.
ring_simplify (precision + -1 + (Fexp q - precision))%Z; ring_simplify (precision + -1 + (Fexp q -
precision))%Z; ring_simplify (Fexp q+-1)%Z; auto with zarith real.
case H; intros V; clear H.
exists (Float (Fnum dp''-Fnum dq') (Fexp dq')).
split;[split; auto with zarith|idtac].
simpl; apply Zlt_Rlt.
rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto.
rewrite <- Rabs_Zabs; unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; auto with real zarith.
simpl; auto with zarith float.
fold radix; fold FtoRradix; rewrite dpEq; rewrite dqEq.
rewrite <- H3'; rewrite <- H3;rewrite <- H5''.
unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR.
rewrite H4''; ring.
exists (Float (-1)%Z (Fexp q)).
split;[split; simpl; auto with zarith|idtac].
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 0); auto with zarith.
elim Roundq; auto with zarith float.
fold radix; fold FtoRradix; elim V; intros.
replace (FtoRradix dp) with (-(-dp))%R;[idtac|ring].
rewrite <- (Rabs_left dp); auto with real.
rewrite <- (Rabs_right dq); auto with real.
2: apply Rle_ge; auto with real.
rewrite dpEq; rewrite <- H3; rewrite <- H5''; rewrite H.
rewrite dqEq; rewrite <- H3'; rewrite H0.
unfold FtoRradix, FtoR, Zpred; simpl.
repeat rewrite powerRZ_add; auto with real zarith; simpl; field.
assert (FtoRradix dp'=(Float (2*Fnum dp') (Zpred (Fexp dp'))))%R.
unfold FtoRradix, FtoR, Zpred.
apply trans_eq with ((2 * Fnum dp')%Z*(powerRZ radix (Fexp dp'+-1)))%R;[auto|idtac].
rewrite mult_IZR;rewrite powerRZ_add; auto with real zarith; simpl; field.
simpl; auto with real.
exists (Float (2*Fnum dp') (Zpred (Fexp dp'))); split.
simpl; rewrite H4'; rewrite H4.
rewrite q_eqExp; rewrite p_eqF; unfold Zpred, Zsucc;simpl; auto with zarith.
split; auto with real.
apply Rmult_le_reg_l with (powerRZ radix (Zpred (Fexp dp'))); auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
rewrite <- (Rabs_right (powerRZ radix (Zpred (Fexp dp'))));auto with real.
2: apply Rle_ge; auto with real zarith.
rewrite <- Rabs_mult.
replace (powerRZ radix (Zpred (Fexp dp')) *
Fnum (Float (2 * Fnum dp') (Zpred (Fexp dp'))))%R with (FtoRradix dp'); auto with real.
2: rewrite H; unfold FtoRradix, FtoR; simpl; auto with real.
rewrite H3; rewrite <- dpEq.
rewrite H4; unfold Zpred;ring_simplify (Fexp p - precision + -1 + (precision + -1))%Z.
rewrite Rabs_left; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (FtoRradix dp).
ring_simplify (dp+2*(-dp))%R.
rewrite <- Rabs_left; auto with real.
assert (Fbounded bo (Float (Zpred (Zpower_nat radix precision)) e)).
split; auto with zarith.
simpl; rewrite pGivesBound; auto with zarith.
rewrite Zabs_eq; auto with zarith.
simpl; rewrite <- q_eqExp; elim Roundq; auto with zarith float.
rewrite <- Rabs_Ropp.
replace (-dp)%R with (p-b*b')%R; [idtac|rewrite dpEq;ring].
elim Roundp; intros K1 K2; elim K1; intros K3 K4.
apply Rle_trans with (Rabs ((Float (Zpred (Zpower_nat radix precision)) e)-b*b')).
unfold FtoRradix; apply K4; auto.
clear K1 K2 K3 K4; rewrite Rabs_left1.
rewrite dpEq; rewrite p_eqR.
apply Rle_trans with (b*b'-(powerRZ radix precision -1)*(powerRZ radix e))%R.
unfold FtoRradix, FtoR, Zpred, radix; simpl.
rewrite plus_IZR; simpl; right; ring_simplify.
rewrite Zpower_nat_Z_powerRZ; auto with real zarith; simpl; ring.
unfold Rminus; rewrite Rplus_assoc; apply Rplus_le_compat_l.
replace (Fexp p) with (Zsucc e);[unfold Zsucc|rewrite p_eqF; simpl; auto with zarith].
ring_simplify (e+1-2)%Z; unfold Zminus.
repeat rewrite powerRZ_add; auto with real zarith; simpl; right; field.
apply Rplus_le_reg_l with (p-(Float (Zpred (Zpower_nat radix precision)) e))%R.
apply Rle_trans with (-(b*b'-p))%R;[right;ring|idtac].
rewrite <- dpEq; rewrite <- Rabs_left; auto with real.
rewrite dpEq; apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix precision p).
unfold FtoRradix; apply ClosestUlp; auto.
elim Roundp; auto.
rewrite CanonicFulp; auto;[idtac|left; auto].
replace (Fexp p) with (Zsucc e);[unfold Zsucc|rewrite p_eqF; simpl; auto with zarith].
rewrite p_eqR; unfold FtoRradix, FtoR, Zpred; simpl.
rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
repeat rewrite powerRZ_add; auto with real zarith; simpl; right; field.
Qed.
Theorem discri8: (delta <= 2*(Fulp bo radix precision d))%R.
case (Rle_or_lt 0%R dp); intros H;[case H; clear H; intros H|idtac].
case (Rle_or_lt 0%R dq); intros H';[case H'; clear H'; intros H'|idtac].
apply discri5; auto with real.
apply Rle_lt_trans with (dp*0)%R;[right;ring|auto with real].
unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto.
exists dp; split; auto.
fold radix; fold FtoRradix; rewrite <- H'; ring.
apply discri6; auto.
unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto.
exists (Fopp dq); split; auto with float zarith.
rewrite Fopp_correct; fold radix; fold FtoRradix; rewrite <- H; ring.
case (Rle_or_lt 0%R dq); intros H';[case H'; clear H'; intros H'|idtac].
apply discri7; auto.
unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto.
exists dp; split; auto.
fold radix; fold FtoRradix; rewrite <- H'; ring.
apply discri5; auto.
apply Rle_lt_trans with (-dp*0)%R;[right;ring|idtac].
apply Rlt_le_trans with ((-dp)*(-dq))%R;[auto with real|right;ring].
Qed.
End Discriminant3.
Section Discriminant4.
Variable bo : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ TwoMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix precision.
Variables a b c p q t dp dq s d:float.
Let delta := (Rabs (d-(b*b-a*c)))%R.
Hypothesis Fa : (Fbounded bo a).
Hypothesis Fb : (Fbounded bo b).
Hypothesis Fc : (Fbounded bo c).
Hypothesis Fp : (Fbounded bo p).
Hypothesis Fq : (Fbounded bo q).
Hypothesis Fd : (Fbounded bo d).
Hypothesis Ft : (Fbounded bo t).
Hypothesis Fs : (3*(Rabs (p-q)) < p+q)%R -> (Fbounded bo s).
Hypothesis Fdp: (3*(Rabs (p-q)) < p+q)%R -> (Fbounded bo dp).
Hypothesis Fdq: (3*(Rabs (p-q)) < p+q)%R -> (Fbounded bo dq).
Hypothesis Cs:(3*(Rabs (p-q)) < p+q)%R -> (Fcanonic radix bo s).
There is no underflow
Hypothesis U0: (- dExp bo <= (Fexp d)-1)%Z.
Hypothesis U1: (- dExp bo <= (Fexp t)-1)%Z.
Hypothesis U2: (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (b*b))%R.
Hypothesis U3: (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (a*c))%R.
Hypothesis Np:(Fnormal radix bo p).
Hypothesis Nq:(Fnormal radix bo q).
Hypothesis Nd:(Fnormal radix bo d).
Hypothesis Roundp : (EvenClosest bo radix precision (b*b)%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).
Hypothesis Firstcase : (p+q <= 3*(Rabs (p-q)))%R ->
(EvenClosest bo radix precision (p-q)%R d).
Hypothesis SRoundt : (3*(Rabs (p-q)) < p+q)%R -> (EvenClosest bo radix precision (p-q)%R t).
Hypothesis SdpEq : (3*(Rabs (p-q)) < p+q)%R -> (FtoRradix dp=b*b-p)%R.
Hypothesis SdqEq : (3*(Rabs (p-q)) < p+q)%R -> (FtoRradix dq=a*c-q)%R.
Hypothesis SRounds : (3*(Rabs (p-q)) < p+q)%R -> (EvenClosest bo radix precision (dp-dq)%R s).
Hypothesis SRoundd : (3*(Rabs (p-q)) < p+q)%R -> (EvenClosest bo radix precision (t+s)%R d).
Theorem discri9: (delta <= 2*(Fulp bo radix precision d))%R.
assert (Square:(0<=b*b)%R).
apply Rle_trans with (Rsqr b); auto with real.
case (Rle_or_lt (p + q)%R (3 * Rabs (p - q))%R); intros.
unfold delta;apply discri1 with p q; auto.
case (Rle_or_lt (3*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q)))%R (Rabs (p-q))%R); intros.
unfold delta; apply discri2 with p q t dp dq s; auto.
case (Zle_or_lt (Fexp q) (Fexp p)); intros.
case (Zle_lt_or_eq (Fexp q) (Fexp p)); auto;intros.
assert (Fexp q = Zpred (Fexp p))%Z.
cut (Zle (Fexp q) (Zpred (Fexp p))); auto with zarith.
cut (Zle (Zpred (Fexp p)) (Fexp q)); auto with zarith.
clear H1;apply Zle_powerRZ with radix; auto with real zarith.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum p) (Zpred (Fexp p)))).
rewrite CanonicFulp; auto.
unfold FtoR; simpl; right; ring.
left; split; auto with zarith.
split; simpl; auto with zarith float.
apply Zle_trans with (Fexp q); auto with zarith float.
simpl; elim Np; auto with zarith.
apply Rle_trans with (Fulp bo radix precision q).
apply LeFulpPos; auto with real float zarith.
split; simpl; auto with zarith float.
apply Zle_trans with (Fexp q); auto with zarith float.
apply LeFnumZERO; simpl; auto with real zarith.
apply LeR0Fnum with radix; auto with real zarith.
apply P_positive with bo precision b b; auto.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (FtoRradix p).
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; right; field.
apply P_le_two_Q with bo precision b b; auto.
rewrite CanonicFulp; auto with zarith.
unfold FtoR; simpl; right; ring.
left; auto.
clear H1 H2; assert (FtoRradix p=powerRZ radix (precision+Zpred (Fexp p)))%R.
case (Zle_lt_or_eq (Zpower_nat radix (pred precision)) (Fnum p)).
elim Np; intros.
apply Zmult_le_reg_r with radix; auto with zarith.
apply Zlt_gt; auto with zarith.
apply Zle_trans with (Zpower_nat radix precision).
pattern radix at 2 in |-*; replace radix with (Zpower_nat radix 1).
rewrite <- Zpower_nat_is_exp; auto with zarith.
simpl; auto with zarith.
rewrite <- pGivesBound; apply Zle_trans with (1:=H2).
rewrite Zabs_eq; auto with zarith.
cut (0<=Fnum p)%Z; auto with zarith.
apply LeR0Fnum with radix; auto.
apply P_positive with bo precision b b; auto.
intros H1; Contradict H0.
apply Rle_not_lt.
rewrite CanonicFulp; auto; [idtac|left; auto].
rewrite CanonicFulp; auto; [idtac|left; auto].
replace (FtoR radix (Float (S 0) (Fexp p))) with (powerRZ radix (Fexp p));[idtac|unfold FtoR; simpl; ring].
replace (FtoR radix (Float (S 0) (Fexp q))) with (powerRZ radix (Fexp q));[idtac|unfold FtoR; simpl; ring].
rewrite H3; unfold Rmin.
case (Rle_dec (powerRZ radix (Fexp p)) (powerRZ radix (Zpred (Fexp p)))); auto with real zarith; intros J.
Contradict J; apply Rlt_not_le; auto with real zarith.
clear J; rewrite Rabs_right.
unfold FtoRradix, FtoR, Rminus.
apply Rle_trans with ((Zsucc (Zpower_nat radix (pred precision))*(powerRZ radix (Fexp p))+-((Zpred (Zpower_nat radix precision))*(powerRZ radix (Fexp q)))))%R.
unfold Zpred, Zsucc; rewrite plus_IZR; rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith.
rewrite H3; unfold Zpred; simpl; right;ring_simplify.
repeat rewrite powerRZ_add; auto with real zarith; simpl; field.
apply Rplus_le_compat;[apply Rmult_le_compat_r; auto with real zarith|idtac].
apply Ropp_le_contravar; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (1:=RRle_abs (Fnum q)).
rewrite Rabs_Zabs; rewrite <- pGivesBound;auto with zarith float.
elim Fq; intros; auto with zarith.
apply Rle_IZR;apply Zle_Zpred; auto.
apply Rle_ge; apply Rlt_le; apply Rplus_lt_reg_r with q.
ring_simplify.
unfold FtoRradix; apply FcanonicPosFexpRlt with bo precision; auto with zarith.
apply Rlt_le; apply Q_positive with bo precision b b p; auto.
apply P_positive with bo precision b b; auto.
left; auto.
left; auto.
rewrite H3; auto with zarith.
intros H1; unfold FtoRradix, FtoR; rewrite <- H1.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith.
replace (Zpred precision+Fexp p)%Z with (precision + Zpred (Fexp p))%Z;[auto with real|unfold Zpred; ring].
unfold delta; apply discri8 with p q t dp dq s (Zpred (Fexp p)); auto.
apply FcanonicUnique with radix bo precision; auto with zarith real.
left; auto.
left; split; [split;simpl|idtac]; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; auto with zarith.
apply Zle_trans with (Fexp p); auto with zarith float.
unfold Zsucc, Zpred; auto with zarith.
simpl (Fnum (Float (Zpower_nat 2 (pred precision)) (Zsucc (Zpred (Fexp p))))).
replace radix with (Zpower_nat radix 1);[idtac|simpl; auto with zarith].
rewrite <-Zpower_nat_is_exp; rewrite pGivesBound; auto with zarith.
rewrite Zabs_eq; auto with zarith.
fold FtoRradix; rewrite H1; unfold FtoRradix, FtoR, Zpred, Zsucc; simpl.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith; unfold Zpred.
replace (precision + -1 + (Fexp p + -1 + 1))%Z with (precision+(Fexp p+-1))%Z; auto with real; ring.
unfold delta;apply discri4 with p q t dp dq s; auto.
assert (Fexp p = Zpred (Fexp q))%Z.
cut (Zle (Fexp p) (Zpred (Fexp q))); auto with zarith.
cut (Zle (Zpred (Fexp q)) (Fexp p)); auto with zarith.
clear H1;apply Zle_powerRZ with radix; auto with real zarith.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum q) (Zpred (Fexp q)))).
rewrite CanonicFulp; auto.
unfold FtoR; simpl; right; ring.
left; split; auto with zarith.
split; simpl; auto with zarith float.
assert (exists s : float,
Fbounded bo s /\
FtoR 2 s = (FtoR 2 a * FtoR 2 c - FtoR 2 q)%R /\
Fexp s = (Fexp q - precision)%Z /\
(Rabs (Fnum s) <= powerRZ (Zpos 2) (Zpred precision))%R).
apply errorBoundedMultClosest_Can; auto.
elim Roundq; auto.
left; auto.
elim H1; intros s' T; elim T; intros T1 T2; elim T2; intros T3 T4; elim T4; intros.
apply Zle_trans with (Fexp q - precision)%Z; auto with zarith float.
rewrite <- H2; auto with zarith float.
simpl; elim Nq; auto with zarith.
apply Rle_trans with (Fulp bo radix precision p).
apply LeFulpPos; auto with real float zarith.
split; simpl; auto with zarith float.
assert (exists s : float,
Fbounded bo s /\
FtoR 2 s = (FtoR 2 a * FtoR 2 c - FtoR 2 q)%R /\
Fexp s = (Fexp q - precision)%Z /\
(Rabs (Fnum s) <= powerRZ (Zpos 2) (Zpred precision))%R).
apply errorBoundedMultClosest_Can; auto.
elim Roundq; auto.
left; auto.
elim H1; intros s' T; elim T; intros T1 T2; elim T2; intros T3 T4; elim T4; intros.
apply Zle_trans with (Fexp q - precision)%Z; auto with zarith float.
rewrite <- H2; auto with zarith float.
apply LeFnumZERO; simpl; auto with real zarith.
apply LeR0Fnum with radix; auto with real zarith.
apply Rlt_le; apply Q_positive with bo precision b b p; auto.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (FtoRradix q).
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; right; field.
apply Q_le_two_P with bo precision b b; auto.
rewrite CanonicFulp; auto with zarith.
unfold FtoR; simpl; right; ring.
left; auto.
clear H1; assert (FtoRradix q=powerRZ radix (precision+Zpred (Fexp q)))%R.
case (Zle_lt_or_eq (Zpower_nat radix (pred precision)) (Fnum q)).
elim Nq; intros.
apply Zmult_le_reg_r with radix; auto with zarith.
apply Zlt_gt; auto with zarith.
apply Zle_trans with (Zpower_nat radix precision).
pattern radix at 2 in |-*; replace radix with (Zpower_nat radix 1).
rewrite <- Zpower_nat_is_exp; auto with zarith.
simpl; auto with zarith.
rewrite <- pGivesBound; apply Zle_trans with (1:=H3).
rewrite Zabs_eq; auto with zarith.
cut (0<=Fnum q)%Z; auto with zarith.
apply LeR0Fnum with radix; auto.
apply Rlt_le; apply Q_positive with bo precision b b p; auto.
intros H1; Contradict H0.
apply Rle_not_lt.
rewrite CanonicFulp; auto; [idtac|left; auto].
rewrite CanonicFulp; auto; [idtac|left; auto].
replace (FtoR radix (Float (S 0) (Fexp p))) with (powerRZ radix (Fexp p));[idtac|unfold FtoR; simpl; ring].
replace (FtoR radix (Float (S 0) (Fexp q))) with (powerRZ radix (Fexp q));[idtac|unfold FtoR; simpl; ring].
rewrite H2; unfold Rmin.
case (Rle_dec (powerRZ radix (Zpred (Fexp q))) (powerRZ radix (Fexp q))); auto with real zarith; intros J.
clear J; rewrite Rabs_left1.
unfold FtoRradix, FtoR, Rminus.
apply Rle_trans with (- ((Zpred (Zpower_nat radix precision)) * powerRZ radix (Fexp p) + - ((Zsucc (Zpower_nat radix (pred precision))) * powerRZ radix (Fexp q))))%R.
unfold Zpred, Zsucc; rewrite plus_IZR; rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith.
rewrite H2; unfold Zpred; simpl; right.
repeat rewrite powerRZ_add; auto with real zarith; simpl; field.
apply Ropp_le_contravar.
apply Rplus_le_compat;[apply Rmult_le_compat_r; auto with real zarith|idtac].
2:apply Ropp_le_contravar; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (1:=RRle_abs (Fnum p)).
rewrite Rabs_Zabs; rewrite <- pGivesBound;auto with zarith float.
elim Fp; intros; auto with zarith.
apply Rle_IZR;apply Zle_Zpred; auto.
apply Rlt_le; apply Rplus_lt_reg_r with q.
ring_simplify.
unfold FtoRradix; apply FcanonicPosFexpRlt with bo precision; auto with zarith.
2:apply Rlt_le; apply Q_positive with bo precision b b p; auto.
apply P_positive with bo precision b b; auto.
left; auto.
left; auto.
rewrite H2; auto with zarith.
Contradict J; auto with real zarith.
intros H1; unfold FtoRradix, FtoR; rewrite <- H1.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith.
replace (Zpred precision+Fexp q)%Z with (precision + Zpred (Fexp q))%Z;[auto with real|unfold Zpred; ring].
unfold delta; rewrite <-Rabs_Ropp.
replace (- (d - (b * b - a * c)))%R with (Fopp d-(a*c-b*b))%R;[idtac|unfold FtoRradix; rewrite Fopp_correct; ring].
replace (Fulp bo radix precision d) with (Fulp bo radix precision (Fopp d)); auto with float zarith.
2: unfold Fulp; rewrite Fnormalize_Fopp; unfold Fopp; simpl; auto with real zarith.
apply discri8 with q p (Fopp t) dq dp (Fopp s) (Zpred (Fexp q)); auto with float zarith.
apply FnormalFop; auto.
fold radix; fold FtoRradix; case (Rle_or_lt 0%R (a*c)%R); auto.
intros H3; absurd (0 < q)%R.
apply Rle_not_lt; unfold FtoRradix; apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (a*c)%R; auto with real.
apply EvenClosestRoundedModeP; auto.
apply Q_positive with bo precision b b p; auto.
fold radix; fold FtoRradix; rewrite (Rplus_comm q p).
replace (q-p)%R with (-(p-q))%R; auto with real; rewrite Rabs_Ropp; auto.
fold radix; fold FtoRradix; replace (q-p)%R with (-(p-q))%R; auto with real.
generalize EvenClosestSymmetric; unfold SymmetricP;intros T; apply T; auto.
fold radix; fold FtoRradix; replace (dq-dp)%R with (-(dp-dq))%R;auto with real.
generalize EvenClosestSymmetric; unfold SymmetricP;intros T; apply T; auto.
fold radix; fold FtoRradix; replace (Fopp t+Fopp s)%R with (-(t+s))%R;[idtac|unfold FtoRradix; repeat rewrite Fopp_correct; ring].
generalize EvenClosestSymmetric; unfold SymmetricP;intros T; apply T; auto.
apply FcanonicUnique with radix bo precision; auto with zarith real.
left; auto.
left; split; [split;simpl|idtac]; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; auto with zarith.
apply Zle_trans with (Fexp q); auto with zarith float.
unfold Zsucc, Zpred; auto with zarith.
simpl (Fnum (Float (Zpower_nat 2 (pred precision)) (Zsucc (Zpred (Fexp q))))).
replace radix with (Zpower_nat radix 1);[idtac|simpl; auto with zarith].
rewrite <-Zpower_nat_is_exp; rewrite pGivesBound; auto with zarith.
rewrite Zabs_eq; auto with zarith.
fold FtoRradix; rewrite H1; unfold FtoRradix, FtoR, Zpred, Zsucc; simpl.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith; unfold Zpred.
replace (precision + -1 + (Fexp q + -1 + 1))%Z with (precision+(Fexp q+-1))%Z; auto with real; ring.
Qed.
End Discriminant4.
Hypothesis U1: (- dExp bo <= (Fexp t)-1)%Z.
Hypothesis U2: (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (b*b))%R.
Hypothesis U3: (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (a*c))%R.
Hypothesis Np:(Fnormal radix bo p).
Hypothesis Nq:(Fnormal radix bo q).
Hypothesis Nd:(Fnormal radix bo d).
Hypothesis Roundp : (EvenClosest bo radix precision (b*b)%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).
Hypothesis Firstcase : (p+q <= 3*(Rabs (p-q)))%R ->
(EvenClosest bo radix precision (p-q)%R d).
Hypothesis SRoundt : (3*(Rabs (p-q)) < p+q)%R -> (EvenClosest bo radix precision (p-q)%R t).
Hypothesis SdpEq : (3*(Rabs (p-q)) < p+q)%R -> (FtoRradix dp=b*b-p)%R.
Hypothesis SdqEq : (3*(Rabs (p-q)) < p+q)%R -> (FtoRradix dq=a*c-q)%R.
Hypothesis SRounds : (3*(Rabs (p-q)) < p+q)%R -> (EvenClosest bo radix precision (dp-dq)%R s).
Hypothesis SRoundd : (3*(Rabs (p-q)) < p+q)%R -> (EvenClosest bo radix precision (t+s)%R d).
Theorem discri9: (delta <= 2*(Fulp bo radix precision d))%R.
assert (Square:(0<=b*b)%R).
apply Rle_trans with (Rsqr b); auto with real.
case (Rle_or_lt (p + q)%R (3 * Rabs (p - q))%R); intros.
unfold delta;apply discri1 with p q; auto.
case (Rle_or_lt (3*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q)))%R (Rabs (p-q))%R); intros.
unfold delta; apply discri2 with p q t dp dq s; auto.
case (Zle_or_lt (Fexp q) (Fexp p)); intros.
case (Zle_lt_or_eq (Fexp q) (Fexp p)); auto;intros.
assert (Fexp q = Zpred (Fexp p))%Z.
cut (Zle (Fexp q) (Zpred (Fexp p))); auto with zarith.
cut (Zle (Zpred (Fexp p)) (Fexp q)); auto with zarith.
clear H1;apply Zle_powerRZ with radix; auto with real zarith.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum p) (Zpred (Fexp p)))).
rewrite CanonicFulp; auto.
unfold FtoR; simpl; right; ring.
left; split; auto with zarith.
split; simpl; auto with zarith float.
apply Zle_trans with (Fexp q); auto with zarith float.
simpl; elim Np; auto with zarith.
apply Rle_trans with (Fulp bo radix precision q).
apply LeFulpPos; auto with real float zarith.
split; simpl; auto with zarith float.
apply Zle_trans with (Fexp q); auto with zarith float.
apply LeFnumZERO; simpl; auto with real zarith.
apply LeR0Fnum with radix; auto with real zarith.
apply P_positive with bo precision b b; auto.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (FtoRradix p).
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; right; field.
apply P_le_two_Q with bo precision b b; auto.
rewrite CanonicFulp; auto with zarith.
unfold FtoR; simpl; right; ring.
left; auto.
clear H1 H2; assert (FtoRradix p=powerRZ radix (precision+Zpred (Fexp p)))%R.
case (Zle_lt_or_eq (Zpower_nat radix (pred precision)) (Fnum p)).
elim Np; intros.
apply Zmult_le_reg_r with radix; auto with zarith.
apply Zlt_gt; auto with zarith.
apply Zle_trans with (Zpower_nat radix precision).
pattern radix at 2 in |-*; replace radix with (Zpower_nat radix 1).
rewrite <- Zpower_nat_is_exp; auto with zarith.
simpl; auto with zarith.
rewrite <- pGivesBound; apply Zle_trans with (1:=H2).
rewrite Zabs_eq; auto with zarith.
cut (0<=Fnum p)%Z; auto with zarith.
apply LeR0Fnum with radix; auto.
apply P_positive with bo precision b b; auto.
intros H1; Contradict H0.
apply Rle_not_lt.
rewrite CanonicFulp; auto; [idtac|left; auto].
rewrite CanonicFulp; auto; [idtac|left; auto].
replace (FtoR radix (Float (S 0) (Fexp p))) with (powerRZ radix (Fexp p));[idtac|unfold FtoR; simpl; ring].
replace (FtoR radix (Float (S 0) (Fexp q))) with (powerRZ radix (Fexp q));[idtac|unfold FtoR; simpl; ring].
rewrite H3; unfold Rmin.
case (Rle_dec (powerRZ radix (Fexp p)) (powerRZ radix (Zpred (Fexp p)))); auto with real zarith; intros J.
Contradict J; apply Rlt_not_le; auto with real zarith.
clear J; rewrite Rabs_right.
unfold FtoRradix, FtoR, Rminus.
apply Rle_trans with ((Zsucc (Zpower_nat radix (pred precision))*(powerRZ radix (Fexp p))+-((Zpred (Zpower_nat radix precision))*(powerRZ radix (Fexp q)))))%R.
unfold Zpred, Zsucc; rewrite plus_IZR; rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith.
rewrite H3; unfold Zpred; simpl; right;ring_simplify.
repeat rewrite powerRZ_add; auto with real zarith; simpl; field.
apply Rplus_le_compat;[apply Rmult_le_compat_r; auto with real zarith|idtac].
apply Ropp_le_contravar; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (1:=RRle_abs (Fnum q)).
rewrite Rabs_Zabs; rewrite <- pGivesBound;auto with zarith float.
elim Fq; intros; auto with zarith.
apply Rle_IZR;apply Zle_Zpred; auto.
apply Rle_ge; apply Rlt_le; apply Rplus_lt_reg_r with q.
ring_simplify.
unfold FtoRradix; apply FcanonicPosFexpRlt with bo precision; auto with zarith.
apply Rlt_le; apply Q_positive with bo precision b b p; auto.
apply P_positive with bo precision b b; auto.
left; auto.
left; auto.
rewrite H3; auto with zarith.
intros H1; unfold FtoRradix, FtoR; rewrite <- H1.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith.
replace (Zpred precision+Fexp p)%Z with (precision + Zpred (Fexp p))%Z;[auto with real|unfold Zpred; ring].
unfold delta; apply discri8 with p q t dp dq s (Zpred (Fexp p)); auto.
apply FcanonicUnique with radix bo precision; auto with zarith real.
left; auto.
left; split; [split;simpl|idtac]; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; auto with zarith.
apply Zle_trans with (Fexp p); auto with zarith float.
unfold Zsucc, Zpred; auto with zarith.
simpl (Fnum (Float (Zpower_nat 2 (pred precision)) (Zsucc (Zpred (Fexp p))))).
replace radix with (Zpower_nat radix 1);[idtac|simpl; auto with zarith].
rewrite <-Zpower_nat_is_exp; rewrite pGivesBound; auto with zarith.
rewrite Zabs_eq; auto with zarith.
fold FtoRradix; rewrite H1; unfold FtoRradix, FtoR, Zpred, Zsucc; simpl.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith; unfold Zpred.
replace (precision + -1 + (Fexp p + -1 + 1))%Z with (precision+(Fexp p+-1))%Z; auto with real; ring.
unfold delta;apply discri4 with p q t dp dq s; auto.
assert (Fexp p = Zpred (Fexp q))%Z.
cut (Zle (Fexp p) (Zpred (Fexp q))); auto with zarith.
cut (Zle (Zpred (Fexp q)) (Fexp p)); auto with zarith.
clear H1;apply Zle_powerRZ with radix; auto with real zarith.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum q) (Zpred (Fexp q)))).
rewrite CanonicFulp; auto.
unfold FtoR; simpl; right; ring.
left; split; auto with zarith.
split; simpl; auto with zarith float.
assert (exists s : float,
Fbounded bo s /\
FtoR 2 s = (FtoR 2 a * FtoR 2 c - FtoR 2 q)%R /\
Fexp s = (Fexp q - precision)%Z /\
(Rabs (Fnum s) <= powerRZ (Zpos 2) (Zpred precision))%R).
apply errorBoundedMultClosest_Can; auto.
elim Roundq; auto.
left; auto.
elim H1; intros s' T; elim T; intros T1 T2; elim T2; intros T3 T4; elim T4; intros.
apply Zle_trans with (Fexp q - precision)%Z; auto with zarith float.
rewrite <- H2; auto with zarith float.
simpl; elim Nq; auto with zarith.
apply Rle_trans with (Fulp bo radix precision p).
apply LeFulpPos; auto with real float zarith.
split; simpl; auto with zarith float.
assert (exists s : float,
Fbounded bo s /\
FtoR 2 s = (FtoR 2 a * FtoR 2 c - FtoR 2 q)%R /\
Fexp s = (Fexp q - precision)%Z /\
(Rabs (Fnum s) <= powerRZ (Zpos 2) (Zpred precision))%R).
apply errorBoundedMultClosest_Can; auto.
elim Roundq; auto.
left; auto.
elim H1; intros s' T; elim T; intros T1 T2; elim T2; intros T3 T4; elim T4; intros.
apply Zle_trans with (Fexp q - precision)%Z; auto with zarith float.
rewrite <- H2; auto with zarith float.
apply LeFnumZERO; simpl; auto with real zarith.
apply LeR0Fnum with radix; auto with real zarith.
apply Rlt_le; apply Q_positive with bo precision b b p; auto.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (FtoRradix q).
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; right; field.
apply Q_le_two_P with bo precision b b; auto.
rewrite CanonicFulp; auto with zarith.
unfold FtoR; simpl; right; ring.
left; auto.
clear H1; assert (FtoRradix q=powerRZ radix (precision+Zpred (Fexp q)))%R.
case (Zle_lt_or_eq (Zpower_nat radix (pred precision)) (Fnum q)).
elim Nq; intros.
apply Zmult_le_reg_r with radix; auto with zarith.
apply Zlt_gt; auto with zarith.
apply Zle_trans with (Zpower_nat radix precision).
pattern radix at 2 in |-*; replace radix with (Zpower_nat radix 1).
rewrite <- Zpower_nat_is_exp; auto with zarith.
simpl; auto with zarith.
rewrite <- pGivesBound; apply Zle_trans with (1:=H3).
rewrite Zabs_eq; auto with zarith.
cut (0<=Fnum q)%Z; auto with zarith.
apply LeR0Fnum with radix; auto.
apply Rlt_le; apply Q_positive with bo precision b b p; auto.
intros H1; Contradict H0.
apply Rle_not_lt.
rewrite CanonicFulp; auto; [idtac|left; auto].
rewrite CanonicFulp; auto; [idtac|left; auto].
replace (FtoR radix (Float (S 0) (Fexp p))) with (powerRZ radix (Fexp p));[idtac|unfold FtoR; simpl; ring].
replace (FtoR radix (Float (S 0) (Fexp q))) with (powerRZ radix (Fexp q));[idtac|unfold FtoR; simpl; ring].
rewrite H2; unfold Rmin.
case (Rle_dec (powerRZ radix (Zpred (Fexp q))) (powerRZ radix (Fexp q))); auto with real zarith; intros J.
clear J; rewrite Rabs_left1.
unfold FtoRradix, FtoR, Rminus.
apply Rle_trans with (- ((Zpred (Zpower_nat radix precision)) * powerRZ radix (Fexp p) + - ((Zsucc (Zpower_nat radix (pred precision))) * powerRZ radix (Fexp q))))%R.
unfold Zpred, Zsucc; rewrite plus_IZR; rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith.
rewrite H2; unfold Zpred; simpl; right.
repeat rewrite powerRZ_add; auto with real zarith; simpl; field.
apply Ropp_le_contravar.
apply Rplus_le_compat;[apply Rmult_le_compat_r; auto with real zarith|idtac].
2:apply Ropp_le_contravar; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (1:=RRle_abs (Fnum p)).
rewrite Rabs_Zabs; rewrite <- pGivesBound;auto with zarith float.
elim Fp; intros; auto with zarith.
apply Rle_IZR;apply Zle_Zpred; auto.
apply Rlt_le; apply Rplus_lt_reg_r with q.
ring_simplify.
unfold FtoRradix; apply FcanonicPosFexpRlt with bo precision; auto with zarith.
2:apply Rlt_le; apply Q_positive with bo precision b b p; auto.
apply P_positive with bo precision b b; auto.
left; auto.
left; auto.
rewrite H2; auto with zarith.
Contradict J; auto with real zarith.
intros H1; unfold FtoRradix, FtoR; rewrite <- H1.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith.
replace (Zpred precision+Fexp q)%Z with (precision + Zpred (Fexp q))%Z;[auto with real|unfold Zpred; ring].
unfold delta; rewrite <-Rabs_Ropp.
replace (- (d - (b * b - a * c)))%R with (Fopp d-(a*c-b*b))%R;[idtac|unfold FtoRradix; rewrite Fopp_correct; ring].
replace (Fulp bo radix precision d) with (Fulp bo radix precision (Fopp d)); auto with float zarith.
2: unfold Fulp; rewrite Fnormalize_Fopp; unfold Fopp; simpl; auto with real zarith.
apply discri8 with q p (Fopp t) dq dp (Fopp s) (Zpred (Fexp q)); auto with float zarith.
apply FnormalFop; auto.
fold radix; fold FtoRradix; case (Rle_or_lt 0%R (a*c)%R); auto.
intros H3; absurd (0 < q)%R.
apply Rle_not_lt; unfold FtoRradix; apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (a*c)%R; auto with real.
apply EvenClosestRoundedModeP; auto.
apply Q_positive with bo precision b b p; auto.
fold radix; fold FtoRradix; rewrite (Rplus_comm q p).
replace (q-p)%R with (-(p-q))%R; auto with real; rewrite Rabs_Ropp; auto.
fold radix; fold FtoRradix; replace (q-p)%R with (-(p-q))%R; auto with real.
generalize EvenClosestSymmetric; unfold SymmetricP;intros T; apply T; auto.
fold radix; fold FtoRradix; replace (dq-dp)%R with (-(dp-dq))%R;auto with real.
generalize EvenClosestSymmetric; unfold SymmetricP;intros T; apply T; auto.
fold radix; fold FtoRradix; replace (Fopp t+Fopp s)%R with (-(t+s))%R;[idtac|unfold FtoRradix; repeat rewrite Fopp_correct; ring].
generalize EvenClosestSymmetric; unfold SymmetricP;intros T; apply T; auto.
apply FcanonicUnique with radix bo precision; auto with zarith real.
left; auto.
left; split; [split;simpl|idtac]; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; auto with zarith.
apply Zle_trans with (Fexp q); auto with zarith float.
unfold Zsucc, Zpred; auto with zarith.
simpl (Fnum (Float (Zpower_nat 2 (pred precision)) (Zsucc (Zpred (Fexp q))))).
replace radix with (Zpower_nat radix 1);[idtac|simpl; auto with zarith].
rewrite <-Zpower_nat_is_exp; rewrite pGivesBound; auto with zarith.
rewrite Zabs_eq; auto with zarith.
fold FtoRradix; rewrite H1; unfold FtoRradix, FtoR, Zpred, Zsucc; simpl.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith; unfold Zpred.
replace (precision + -1 + (Fexp q + -1 + 1))%Z with (precision+(Fexp q+-1))%Z; auto with real; ring.
Qed.
End Discriminant4.