Library Float.FnElem.MinOrMax
Require Export AllFloat.
Section MinOrMax_def.
Variable radix : Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variable b : Fbound.
Variable precision : nat.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Definition MinOrMax (z : R) (f : float) :=
isMin b radix z f \/ isMax b radix z f.
Theorem MinOrMax_Rlt :
forall (z : R) (p : float),
1 < precision ->
Zpos (vNum b) = Zpower_nat radix precision ->
MinOrMax z p -> (Rabs (z - p) < Fulp b radix precision p)%R.
intros z p H'1 H'2 H; case H; intros H1.
unfold FtoRradix in |- *; apply RoundedModeUlp with (P := isMin b radix);
auto with zarith.
apply MinRoundedModeP with precision; auto with zarith.
unfold FtoRradix in |- *; apply RoundedModeUlp with (P := isMax b radix);
auto with zarith.
apply MaxRoundedModeP with precision; auto with zarith.
Qed.
Theorem MinOrMax_Fopp :
forall (x : R) (f : float), MinOrMax (- x) (Fopp f) -> MinOrMax x f.
unfold MinOrMax in |- *; intros x f H.
rewrite <- (Ropp_involutive x); rewrite <- (Fopp_Fopp f).
case H; intros H1.
right; apply MinOppMax; auto.
left; apply MaxOppMin; auto.
Qed.
Theorem MinOrMax1 :
forall (z : R) (p : float),
Fbounded b p ->
Fcanonic radix b p ->
(0 < p)%R ->
(Rabs (z - p) < Fulp b radix precision (FPred b radix precision p))%R ->
MinOrMax z p.
intros z p Hp Hcan Hblop.
case (Rcase_abs (z - p)); intros H1;
[ rewrite Rabs_left | rewrite Rabs_right ]; auto;
intros H.
right; unfold isMax in |- *.
split; auto; split.
fold FtoRradix in |- *; apply Rplus_le_reg_l with (- p)%R.
ring_simplify (- p + p)%R; rewrite Rplus_comm; auto with real.
intros f Hf H2.
replace (FtoR radix f) with (FtoR radix (Fnormalize radix b precision f));
[ idtac | apply FnormalizeCorrect; auto with zarith arith ].
replace p with (FSucc b radix precision (FPred b radix precision p));
[ idtac | apply FSucPred; auto with zarith arith ].
apply FSuccProp; auto with zarith arith.
apply FPredCanonic; auto with arith zarith.
apply FnormalizeCanonic; auto with arith zarith.
apply Rlt_le_trans with z.
2: rewrite FnormalizeCorrect; auto with arith zarith.
apply
Rle_lt_trans with (p - Fulp b radix precision (FPred b radix precision p))%R.
2: apply Ropp_lt_cancel.
2: apply Rplus_lt_reg_r with (FtoRradix p).
2: ring_simplify.
2: apply Rle_lt_trans with (2 := H); right; ring.
replace (FtoRradix p) with
(FPred b radix precision p +
Fulp b radix precision (FPred b radix precision p))%R;
[ right; fold FtoRradix; ring
| unfold FtoRradix in |- *; apply FpredUlpPos; auto with zarith arith ].
left; unfold isMin in |- *.
split; auto; split.
fold FtoRradix in |- *; apply Rplus_le_reg_l with (- p)%R.
ring_simplify (- p + p)%R; rewrite Rplus_comm; auto with real.
intros f Hf H2.
replace (FtoR radix f) with (FtoR radix (Fnormalize radix b precision f));
[ idtac | apply FnormalizeCorrect; auto with zarith arith ].
replace p with (FPred b radix precision (FSucc b radix precision p));
[ idtac | apply FPredSuc; auto with zarith arith ].
apply FPredProp; auto with zarith arith.
apply FnormalizeCanonic; auto with arith zarith.
apply FSuccCanonic; auto with arith zarith.
apply Rle_lt_trans with z.
rewrite FnormalizeCorrect; auto with arith zarith.
apply
Rlt_le_trans with (p + Fulp b radix precision (FPred b radix precision p))%R.
apply Rplus_lt_reg_r with (- FtoRradix p)%R.
ring_simplify.
apply Rle_lt_trans with (2 := H); right; ring.
apply Rle_trans with (FtoRradix p + Fulp b radix precision p)%R;
[ apply Rplus_le_compat_l | idtac ].
apply LeFulpPos; auto with arith zarith.
apply FBoundedPred; auto with arith zarith.
unfold FtoRradix in |- *; apply R0RltRlePred; auto with arith zarith.
apply Rlt_le; unfold FtoRradix in |- *; apply FPredLt; auto with arith zarith.
pattern p at -3 in |- *;
replace p with (FPred b radix precision (FSucc b radix precision p));
[ idtac | apply FPredSuc; auto with zarith arith ].
unfold FtoRradix in |- *;
rewrite FpredUlpPos with (x := FSucc b radix precision p);
auto with zarith arith real.
apply FSuccCanonic; auto with zarith arith.
apply Rlt_trans with (FtoRradix p); auto with float real.
unfold FtoRradix in |- *; apply FSuccLt; auto with zarith float real.
Qed.
Theorem MinOrMax2 :
forall (z : R) (p : float),
Fbounded b p ->
Fcanonic radix b p ->
(0 < p)%R ->
(Rabs (z - p) < Fulp b radix precision p)%R -> (p <= z)%R -> MinOrMax z p.
intros z p Hp1 Hp2 H H1 H2.
unfold MinOrMax in |- *; left; unfold isMin in |- *.
split; auto; split; auto.
intros f Hf H3.
replace (FtoR radix f) with (FtoR radix (Fnormalize radix b precision f));
[ idtac | apply FnormalizeCorrect; auto with zarith arith ].
replace p with (FPred b radix precision (FSucc b radix precision p));
[ idtac | apply FPredSuc; auto with zarith arith ].
apply FPredProp; auto with zarith arith.
apply FnormalizeCanonic; auto with arith zarith.
apply FSuccCanonic; auto with arith zarith.
apply Rle_lt_trans with z.
rewrite FnormalizeCorrect; auto with arith zarith.
apply Rlt_le_trans with (FtoRradix p + Fulp b radix precision p)%R.
apply Rplus_lt_reg_r with (- FtoRradix p)%R.
ring_simplify.
apply Rle_lt_trans with (2 := H1); right.
rewrite Rabs_right; try ring.
apply Rle_ge; apply Rplus_le_reg_l with (FtoRradix p); auto with real.
ring_simplify; auto with real.
pattern p at -3 in |- *;
replace p with (FPred b radix precision (FSucc b radix precision p));
[ idtac | apply FPredSuc; auto with zarith arith ].
unfold FtoRradix in |- *;
rewrite FpredUlpPos with (x := FSucc b radix precision p);
auto with zarith arith real.
apply FSuccCanonic; auto with zarith arith.
apply Rlt_trans with (FtoRradix p); auto with float real.
unfold FtoRradix in |- *; apply FSuccLt; auto with zarith float real.
Qed.
Theorem MinOrMax3_aux :
forall (z : R) (p : float),
Fbounded b p ->
Fcanonic radix b p ->
0%R = p ->
(z <= 0)%R ->
(- z < Fulp b radix precision (FPred b radix precision p))%R -> MinOrMax z p.
intros z p Hp Hcan Hzero H.
right; unfold isMax in |- *.
fold FtoRradix in |- *; rewrite <- Hzero.
split; auto; split; auto with real.
intros f Hf H2.
unfold FtoRradix in |- *;
replace (FtoR radix f) with (FtoR radix (Fnormalize radix b precision f));
[ idtac | apply FnormalizeCorrect; auto with zarith arith ].
cut (Fcanonic radix b (Fzero (- dExp b))); [ intros H3 | idtac ].
2: right; repeat (split; simpl in |- *; auto with zarith).
2: ring_simplify (radix * 0)%Z; rewrite Zabs_eq; auto with zarith.
cut (p = Fzero (- dExp b)); [ intros H4 | idtac ].
2: apply
FcanonicUnique with (radix := radix) (precision := precision) (b := b);
auto with zarith.
2: fold FtoRradix in |- *; rewrite <- Hzero; auto with float real.
2: unfold FtoRradix in |- *; apply sym_eq; apply FzeroisZero.
cut (0 < pPred (vNum b))%Z;
[ intros V | apply pPredMoreThanOne with radix precision; auto with zarith ].
cut (1 < Zpos (vNum b))%Z;
[ intros V'
| apply vNumbMoreThanOne with radix precision; auto with zarith ].
replace 0%R with
(FtoR radix
(FSucc b radix precision (FPred b radix precision (Fzero (- dExp b))))).
apply FSuccProp; auto with zarith arith.
apply FPredCanonic; auto with arith zarith.
apply FnormalizeCanonic; auto with arith zarith.
apply Rlt_le_trans with z.
2: rewrite FnormalizeCorrect; auto with arith zarith.
apply Ropp_lt_cancel; apply Rlt_le_trans with (1 := H0).
rewrite H4; right.
rewrite FPredSimpl4; simpl in |- *; auto with zarith.
2: unfold nNormMin in |- *; auto with zarith.
unfold Fulp in |- *.
replace (Fnormalize radix b precision (Float (-1) (- dExp b))) with
(Float (-1) (- dExp b));
[ unfold FtoRradix, FtoR in |- *; simpl in |- *; ring | idtac ].
apply FcanonicUnique with (radix := radix) (precision := precision) (b := b);
auto with zarith.
right; repeat (split; simpl in |- *; auto with zarith).
rewrite pGivesBound.
rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto with zarith.
replace (- (radix * -1))%Z with (Zpower_nat radix 1); auto with arith zarith.
unfold Zpower_nat in |- *; simpl in |- *; ring.
apply FnormalizeCanonic; auto with zarith.
repeat (split; simpl in |- *; auto with zarith).
apply sym_eq; apply FnormalizeCorrect; auto with zarith.
rewrite FPredSimpl4; simpl in |- *; auto with zarith.
rewrite FSuccSimpl4; simpl in |- *; auto with zarith.
simpl in |- *; unfold FtoR in |- *; simpl in |- *; ring.
unfold nNormMin in |- *.
replace (-1)%Z with (- Zpower_nat radix (pred 1))%Z; auto with zarith arith.
unfold nNormMin in |- *; auto with zarith arith.
Qed.
Theorem MinOrMax3 :
forall (z : R) (p : float),
Fbounded b p ->
Fcanonic radix b p ->
0%R = p ->
(Rabs (z - p) < Fulp b radix precision (FPred b radix precision p))%R ->
MinOrMax z p.
intros z p Hp Hcan Hzero.
replace (z - FtoRradix p)%R with z; [ idtac | rewrite <- Hzero; ring ].
case (Rcase_abs z); intros H1; [ rewrite Rabs_left | rewrite Rabs_right ];
auto; intros H.
apply MinOrMax3_aux; auto with real.
apply MinOrMax_Fopp.
apply MinOrMax3_aux; auto with real float.
unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real.
rewrite Ropp_involutive.
replace (Fopp p) with p; auto.
apply floatEq; auto; simpl in |- *.
cut (is_Fzero p);
[ unfold is_Fzero in |- *; intros H2; repeat rewrite H2
| apply is_Fzero_rep2 with radix ]; auto with zarith real float.
Qed.
End MinOrMax_def.
Section MinOrMax_def.
Variable radix : Z.
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variable b : Fbound.
Variable precision : nat.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Definition MinOrMax (z : R) (f : float) :=
isMin b radix z f \/ isMax b radix z f.
Theorem MinOrMax_Rlt :
forall (z : R) (p : float),
1 < precision ->
Zpos (vNum b) = Zpower_nat radix precision ->
MinOrMax z p -> (Rabs (z - p) < Fulp b radix precision p)%R.
intros z p H'1 H'2 H; case H; intros H1.
unfold FtoRradix in |- *; apply RoundedModeUlp with (P := isMin b radix);
auto with zarith.
apply MinRoundedModeP with precision; auto with zarith.
unfold FtoRradix in |- *; apply RoundedModeUlp with (P := isMax b radix);
auto with zarith.
apply MaxRoundedModeP with precision; auto with zarith.
Qed.
Theorem MinOrMax_Fopp :
forall (x : R) (f : float), MinOrMax (- x) (Fopp f) -> MinOrMax x f.
unfold MinOrMax in |- *; intros x f H.
rewrite <- (Ropp_involutive x); rewrite <- (Fopp_Fopp f).
case H; intros H1.
right; apply MinOppMax; auto.
left; apply MaxOppMin; auto.
Qed.
Theorem MinOrMax1 :
forall (z : R) (p : float),
Fbounded b p ->
Fcanonic radix b p ->
(0 < p)%R ->
(Rabs (z - p) < Fulp b radix precision (FPred b radix precision p))%R ->
MinOrMax z p.
intros z p Hp Hcan Hblop.
case (Rcase_abs (z - p)); intros H1;
[ rewrite Rabs_left | rewrite Rabs_right ]; auto;
intros H.
right; unfold isMax in |- *.
split; auto; split.
fold FtoRradix in |- *; apply Rplus_le_reg_l with (- p)%R.
ring_simplify (- p + p)%R; rewrite Rplus_comm; auto with real.
intros f Hf H2.
replace (FtoR radix f) with (FtoR radix (Fnormalize radix b precision f));
[ idtac | apply FnormalizeCorrect; auto with zarith arith ].
replace p with (FSucc b radix precision (FPred b radix precision p));
[ idtac | apply FSucPred; auto with zarith arith ].
apply FSuccProp; auto with zarith arith.
apply FPredCanonic; auto with arith zarith.
apply FnormalizeCanonic; auto with arith zarith.
apply Rlt_le_trans with z.
2: rewrite FnormalizeCorrect; auto with arith zarith.
apply
Rle_lt_trans with (p - Fulp b radix precision (FPred b radix precision p))%R.
2: apply Ropp_lt_cancel.
2: apply Rplus_lt_reg_r with (FtoRradix p).
2: ring_simplify.
2: apply Rle_lt_trans with (2 := H); right; ring.
replace (FtoRradix p) with
(FPred b radix precision p +
Fulp b radix precision (FPred b radix precision p))%R;
[ right; fold FtoRradix; ring
| unfold FtoRradix in |- *; apply FpredUlpPos; auto with zarith arith ].
left; unfold isMin in |- *.
split; auto; split.
fold FtoRradix in |- *; apply Rplus_le_reg_l with (- p)%R.
ring_simplify (- p + p)%R; rewrite Rplus_comm; auto with real.
intros f Hf H2.
replace (FtoR radix f) with (FtoR radix (Fnormalize radix b precision f));
[ idtac | apply FnormalizeCorrect; auto with zarith arith ].
replace p with (FPred b radix precision (FSucc b radix precision p));
[ idtac | apply FPredSuc; auto with zarith arith ].
apply FPredProp; auto with zarith arith.
apply FnormalizeCanonic; auto with arith zarith.
apply FSuccCanonic; auto with arith zarith.
apply Rle_lt_trans with z.
rewrite FnormalizeCorrect; auto with arith zarith.
apply
Rlt_le_trans with (p + Fulp b radix precision (FPred b radix precision p))%R.
apply Rplus_lt_reg_r with (- FtoRradix p)%R.
ring_simplify.
apply Rle_lt_trans with (2 := H); right; ring.
apply Rle_trans with (FtoRradix p + Fulp b radix precision p)%R;
[ apply Rplus_le_compat_l | idtac ].
apply LeFulpPos; auto with arith zarith.
apply FBoundedPred; auto with arith zarith.
unfold FtoRradix in |- *; apply R0RltRlePred; auto with arith zarith.
apply Rlt_le; unfold FtoRradix in |- *; apply FPredLt; auto with arith zarith.
pattern p at -3 in |- *;
replace p with (FPred b radix precision (FSucc b radix precision p));
[ idtac | apply FPredSuc; auto with zarith arith ].
unfold FtoRradix in |- *;
rewrite FpredUlpPos with (x := FSucc b radix precision p);
auto with zarith arith real.
apply FSuccCanonic; auto with zarith arith.
apply Rlt_trans with (FtoRradix p); auto with float real.
unfold FtoRradix in |- *; apply FSuccLt; auto with zarith float real.
Qed.
Theorem MinOrMax2 :
forall (z : R) (p : float),
Fbounded b p ->
Fcanonic radix b p ->
(0 < p)%R ->
(Rabs (z - p) < Fulp b radix precision p)%R -> (p <= z)%R -> MinOrMax z p.
intros z p Hp1 Hp2 H H1 H2.
unfold MinOrMax in |- *; left; unfold isMin in |- *.
split; auto; split; auto.
intros f Hf H3.
replace (FtoR radix f) with (FtoR radix (Fnormalize radix b precision f));
[ idtac | apply FnormalizeCorrect; auto with zarith arith ].
replace p with (FPred b radix precision (FSucc b radix precision p));
[ idtac | apply FPredSuc; auto with zarith arith ].
apply FPredProp; auto with zarith arith.
apply FnormalizeCanonic; auto with arith zarith.
apply FSuccCanonic; auto with arith zarith.
apply Rle_lt_trans with z.
rewrite FnormalizeCorrect; auto with arith zarith.
apply Rlt_le_trans with (FtoRradix p + Fulp b radix precision p)%R.
apply Rplus_lt_reg_r with (- FtoRradix p)%R.
ring_simplify.
apply Rle_lt_trans with (2 := H1); right.
rewrite Rabs_right; try ring.
apply Rle_ge; apply Rplus_le_reg_l with (FtoRradix p); auto with real.
ring_simplify; auto with real.
pattern p at -3 in |- *;
replace p with (FPred b radix precision (FSucc b radix precision p));
[ idtac | apply FPredSuc; auto with zarith arith ].
unfold FtoRradix in |- *;
rewrite FpredUlpPos with (x := FSucc b radix precision p);
auto with zarith arith real.
apply FSuccCanonic; auto with zarith arith.
apply Rlt_trans with (FtoRradix p); auto with float real.
unfold FtoRradix in |- *; apply FSuccLt; auto with zarith float real.
Qed.
Theorem MinOrMax3_aux :
forall (z : R) (p : float),
Fbounded b p ->
Fcanonic radix b p ->
0%R = p ->
(z <= 0)%R ->
(- z < Fulp b radix precision (FPred b radix precision p))%R -> MinOrMax z p.
intros z p Hp Hcan Hzero H.
right; unfold isMax in |- *.
fold FtoRradix in |- *; rewrite <- Hzero.
split; auto; split; auto with real.
intros f Hf H2.
unfold FtoRradix in |- *;
replace (FtoR radix f) with (FtoR radix (Fnormalize radix b precision f));
[ idtac | apply FnormalizeCorrect; auto with zarith arith ].
cut (Fcanonic radix b (Fzero (- dExp b))); [ intros H3 | idtac ].
2: right; repeat (split; simpl in |- *; auto with zarith).
2: ring_simplify (radix * 0)%Z; rewrite Zabs_eq; auto with zarith.
cut (p = Fzero (- dExp b)); [ intros H4 | idtac ].
2: apply
FcanonicUnique with (radix := radix) (precision := precision) (b := b);
auto with zarith.
2: fold FtoRradix in |- *; rewrite <- Hzero; auto with float real.
2: unfold FtoRradix in |- *; apply sym_eq; apply FzeroisZero.
cut (0 < pPred (vNum b))%Z;
[ intros V | apply pPredMoreThanOne with radix precision; auto with zarith ].
cut (1 < Zpos (vNum b))%Z;
[ intros V'
| apply vNumbMoreThanOne with radix precision; auto with zarith ].
replace 0%R with
(FtoR radix
(FSucc b radix precision (FPred b radix precision (Fzero (- dExp b))))).
apply FSuccProp; auto with zarith arith.
apply FPredCanonic; auto with arith zarith.
apply FnormalizeCanonic; auto with arith zarith.
apply Rlt_le_trans with z.
2: rewrite FnormalizeCorrect; auto with arith zarith.
apply Ropp_lt_cancel; apply Rlt_le_trans with (1 := H0).
rewrite H4; right.
rewrite FPredSimpl4; simpl in |- *; auto with zarith.
2: unfold nNormMin in |- *; auto with zarith.
unfold Fulp in |- *.
replace (Fnormalize radix b precision (Float (-1) (- dExp b))) with
(Float (-1) (- dExp b));
[ unfold FtoRradix, FtoR in |- *; simpl in |- *; ring | idtac ].
apply FcanonicUnique with (radix := radix) (precision := precision) (b := b);
auto with zarith.
right; repeat (split; simpl in |- *; auto with zarith).
rewrite pGivesBound.
rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto with zarith.
replace (- (radix * -1))%Z with (Zpower_nat radix 1); auto with arith zarith.
unfold Zpower_nat in |- *; simpl in |- *; ring.
apply FnormalizeCanonic; auto with zarith.
repeat (split; simpl in |- *; auto with zarith).
apply sym_eq; apply FnormalizeCorrect; auto with zarith.
rewrite FPredSimpl4; simpl in |- *; auto with zarith.
rewrite FSuccSimpl4; simpl in |- *; auto with zarith.
simpl in |- *; unfold FtoR in |- *; simpl in |- *; ring.
unfold nNormMin in |- *.
replace (-1)%Z with (- Zpower_nat radix (pred 1))%Z; auto with zarith arith.
unfold nNormMin in |- *; auto with zarith arith.
Qed.
Theorem MinOrMax3 :
forall (z : R) (p : float),
Fbounded b p ->
Fcanonic radix b p ->
0%R = p ->
(Rabs (z - p) < Fulp b radix precision (FPred b radix precision p))%R ->
MinOrMax z p.
intros z p Hp Hcan Hzero.
replace (z - FtoRradix p)%R with z; [ idtac | rewrite <- Hzero; ring ].
case (Rcase_abs z); intros H1; [ rewrite Rabs_left | rewrite Rabs_right ];
auto; intros H.
apply MinOrMax3_aux; auto with real.
apply MinOrMax_Fopp.
apply MinOrMax3_aux; auto with real float.
unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real.
rewrite Ropp_involutive.
replace (Fopp p) with p; auto.
apply floatEq; auto; simpl in |- *.
cut (is_Fzero p);
[ unfold is_Fzero in |- *; intros H2; repeat rewrite H2
| apply is_Fzero_rep2 with radix ]; auto with zarith real float.
Qed.
End MinOrMax_def.