ClosestProp.v
Require Export FroundProp.
Require Export Closest.
Section Fclosestp.
Variable b:Fbound.
Variable radix:nat.
Variable precision:nat.
Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne:(lt (S O) radix).
Hypothesis precisionGreaterThanOne:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).
Theorem
ClosestOpp:
(p:float) (r:R) (Closest b radix r p) ->(Closest b radix (Ropp r) (Fopp p)).
Intros p r H'; Split.
Apply oppBounded; Auto.
Intuition.
Intros f H'0.
Rewrite Fopp_correct.
Replace (Rminus (Ropp (FtoR radix p)) (Ropp r))
with (Ropp (Rminus (FtoR radix p) r)); [Idtac | Ring].
Replace (Rminus (FtoR radix f) (Ropp r))
with (Ropp (Rminus (Ropp (FtoR radix f)) r)); [Idtac | Ring].
Rewrite <- Fopp_correct.
Repeat Rewrite Rabsolu_Ropp.
Case H'; Auto with float.
Qed.
Theorem
ClosestFabs:
(p:float) (r:R) (Closest b radix r p) ->(Closest b radix (Rabsolu r) (Fabs p)).
Intros p r H'; Case (Rle_or_lt R0 r); Intros Rl0.
Rewrite Rabsolu_simpl1; Auto.
Replace (Fabs p) with p; Auto.
Unfold Fabs; Apply floatEq; Simpl; Auto.
Cut (Zle ZERO (Fnum p)).
Case (Fnum p); Simpl; Auto; Intros p H0; Contradict H0; Apply Zlt_not_le; Red;
Simpl; Auto with zarith.
Apply LeR0Fnum with radix := radix; Auto.
Apply RleRoundedR0
with b := b precision := precision P := (Closest b radix) r := r; Auto.
Apply ClosestRoundedModeP with precision := precision; Auto.
Rewrite Rabsolu_simpl2; Auto.
Replace (Fabs p) with (Fopp p).
Apply ClosestOpp; Auto.
Unfold Fabs; Apply floatEq; Simpl; Auto.
Cut (Zle (Fnum p) ZERO).
Case (Fnum p); Simpl; Auto; Intros p H0; Contradict H0; Apply Zlt_not_le; Red;
Simpl; Auto with zarith.
Apply R0LeFnum with radix := radix; Auto.
Apply RleRoundedLessR0
with b := b precision := precision P := (Closest b radix) r := r; Auto.
Apply ClosestRoundedModeP with precision := precision; Auto.
Apply Rlt_le; Auto.
Apply Rlt_le; Auto.
Qed.
Theorem
ClosestUlp:
(p, q:float) (Closest b radix p q) ->
(Rle (Rmult (2) (Rabsolu (Rminus p q))) (Fulp b radix precision q)).
Intros p q H'.
Case (Req_EM p q); Intros Eqpq.
Rewrite Eqpq.
Replace (Rabsolu (Rminus q q)) with R0;
[AutoRewrite [Rsimpl] |
Replace (Rminus q q) with R0; Try Ring; Rewrite Rabsolu_simpl1;
Auto with real].
Unfold Fulp; Apply Rlt_le; Auto with real arith.
Replace (Rmult (2) (Rabsolu (Rminus p q)))
with (Rplus (Rabsolu (Rminus p q)) (Rabsolu (Rminus p q)));
[Idtac | Simpl; AutoRewrite [Rsimpl]; Ring].
Case ClosestMinOrMax with 1 := H'; Intros H'1.
Apply Rle_trans
with (Rplus
(Rabsolu (Rminus p q))
(Rabsolu (Rminus (FNSucc b radix precision q) p))).
Apply Rle_compatibility.
Rewrite <- (Rabsolu_Ropp (Rminus p q)).
Rewrite Rminus_Ropp.
Elim H'; Auto.
Intros H'0 H'2; Apply H'2; Auto.
Apply FcanonicBound with radix := radix precision := precision;
Auto with float arith.
Repeat Rewrite Rminus_Rabsolu.
Replace (Rplus (Rminus p q) (Rminus (FNSucc b radix precision q) p))
with (Rminus (FNSucc b radix precision q) q); [Idtac | Ring].
Unfold FtoRradix; Apply FulpSuc; Auto.
Intuition.
Case MinMax with 3 := pGivesBound r := (FtoRradix p) p := q; Auto with arith.
Intros H'0 H'2; Elim H'2; Intros H'3 H'4; Apply H'3; Clear H'2; Auto.
Intuition.
Apply Rle_trans
with (Rplus
(Rabsolu (Rminus p q))
(Rabsolu (Rminus p (FNPred b radix precision q)))).
Apply Rle_compatibility.
Rewrite <- (Rabsolu_Ropp (Rminus p q));
Rewrite <- (Rabsolu_Ropp (Rminus p (FNPred b radix precision q))).
Repeat Rewrite Rminus_Ropp.
Elim H'; Auto.
Intros H'0 H'2; Apply H'2; Auto.
Apply FcanonicBound with radix := radix precision := precision;
Auto with float arith.
Rewrite <- (Rabsolu_Ropp (Rminus p q)); Rewrite Rminus_Ropp.
Repeat Rewrite Rminus_Rabsolu.
Replace (Rplus (Rminus q p) (Rminus p (FNPred b radix precision q)))
with (Rminus q (FNPred b radix precision q)); [Idtac | Ring].
Unfold FtoRradix; Apply FulpPred; Auto.
Intuition.
Case MaxMin with 3 := pGivesBound r := (FtoRradix p) p := q; Auto with arith.
Intros H'0 H'2; Elim H'2; Intros H'3 H'4; Apply H'3; Clear H'2; Auto.
Intuition.
Qed.
Theorem
ClosestIdem:
(p, q:float) (Fbounded b p) -> (Closest b radix p q) -><R> p==q.
Intros p q H' H'0.
Apply r_Rplus_plus with r := (Ropp p).
Replace (Rplus (Ropp p) p) with R0; [Idtac | Ring].
Replace (Rplus (Ropp p) q) with (Rminus q p); [Idtac | Ring].
Apply sym_eqT.
Apply RabsoluR0Inv; Auto.
Replace R0 with (Rabsolu R0); [Idtac | AutoRewrite [Rsimpl]]; Auto.
Replace R0 with (Rminus p p); [Idtac | Ring].
Case H'0; Auto.
Qed.
Theorem
ClosestM1:
(r1, r2:R)
(min, max, p, q:float)
(isMin b radix r1 min) ->
(isMax b radix r1 max) ->
(Rlt (Rplus min max) (Rmult (2) r2)) ->
(Closest b radix r1 p) -> (Closest b radix r2 q) ->(Rle p q).
Intros r1 r2 min max p q H' H'0 H'1 H'2 H'3.
Case (Rle_or_lt r2 max); Intros H'4.
2:Apply (ClosestMonotone b radix) with p := r1 q := r2; Auto.
2:Apply Rle_lt_trans with (FtoRradix max); Auto.
2:Intuition.
Case H'4; Clear H'4; Intros H'4.
2:Replace (FtoRradix q) with (FtoRradix max).
2:Case ClosestMinOrMax with 1 := H'2; Intros H'5.
2:Replace (FtoRradix p) with (FtoRradix min).
2:Apply Rle_trans with r1; Intuition.
2:Apply MinEq with 1 := H'; Auto.
2:Replace (FtoRradix p) with (FtoRradix max); Auto with real.
2:Apply MaxEq with 1 := H'0; Auto.
2:Apply ClosestIdem; Auto.
2:Intuition.
2:Rewrite <- H'4; Auto.
Cut (Rlt min r2).
2:Apply Rlt_mult_anticompatibility with z := (INR (2)); Auto with real.
2:Replace (Rmult (2) min) with (Rplus min min); [Idtac | Simpl; Ring].
2:Apply Rle_lt_trans with 2 := H'1.
2:Apply Rle_compatibility; Auto with real.
2:Apply Rle_trans with r1; Intuition.
Intros H'5.
Replace (FtoRradix q) with (FtoRradix max).
Case ClosestMinOrMax with 1 := H'2; Intros H'6.
Replace (FtoRradix p) with (FtoRradix min).
Apply Rle_trans with r1; Intuition.
Apply MinEq with 1 := H'; Auto.
Replace (FtoRradix p) with (FtoRradix max); Auto with real.
Apply MaxEq with 1 := H'0; Auto.
Apply sym_eqT.
Apply (ClosestMaxEq b radix) with r := r2 min := min; Auto.
Apply isMinComp with 2 := H'0; Auto.
Apply isMaxComp with 1 := H'; Auto.
Qed.
End Fclosestp.
Hints Resolve ClosestOpp ClosestFabs ClosestUlp :float.
14/12/100, 16:37