# Library Float.Fmin

Require Export Zenum.
Require Export FPred.

Section FMinMax.
Variable b : Fbound.
Variable precision : nat.

Coercion FtoRradix : float >-> R.

Hypothesis precisionNotZero : precision 0.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

Definition boundNat (n : nat) := Float 1%nat (digit radix n).

Theorem boundNatCorrect : n : nat, (n < boundNat n)%R.
intros n; unfold FtoRradix, FtoR, boundNat in |- *; simpl in |- ×.
rewrite Rmult_1_l.
rewrite <- Zpower_nat_Z_powerRZ; auto with real zarith.
rewrite INR_IZR_INZ; auto with real zarith.
apply Rle_lt_trans with (Zabs n); [rewrite (Zabs_eq (Z_of_nat n))|idtac];auto with real zarith.
Qed.

Theorem boundBoundNat : n : nat, Fbounded b (boundNat n).
intros n; repeat split; unfold boundNat in |- *; simpl in |- *;
auto with zarith.
auto with zarith.
apply Zle_trans with 0%Z;[case (dExp b)|idtac]; auto with zarith.
Qed.

Definition boundR (r : R) := boundNat (Zabs_nat (up (Rabs r))).

Theorem boundRCorrect1 : r : R, (r < boundR r)%R.
intros r; case (Rle_or_lt r 0); intros H'.
apply Rle_lt_trans with (1 := H').
unfold boundR, boundNat, FtoRradix, FtoR in |- *; simpl in |- *;
auto with real.
rewrite Rmult_1_l; auto with real zarith.
apply Rlt_trans with (2 := boundNatCorrect (Zabs_nat (up (Rabs r)))).
replace (Rabs r) with r; auto with real.
apply Rlt_le_trans with (r2 := IZR (up r)); auto with real zarith.
case (archimed r); auto.
rewrite INR_IZR_INZ; auto with real zarith.
unfold Rabs in |- *; case (Rcase_abs r); auto with real.
intros H'0; Contradict H'0; auto with real.
Qed.

Theorem boundRrOpp : r : R, boundR r = boundR (- r).
intros R; unfold boundR in |- ×.
rewrite Rabs_Ropp; auto.
Qed.

Theorem boundRCorrect2 : r : R, (Fopp (boundR r) < r)%R.
intros r; case (Rle_or_lt r 0); intros H'.
rewrite boundRrOpp.
pattern r at 2 in |- *; rewrite <- (Ropp_involutive r).
unfold FtoRradix in |- *; rewrite Fopp_correct.
apply Ropp_lt_contravar; apply boundRCorrect1; auto.
apply Rle_lt_trans with 0%R; auto.
replace 0%R with (-0)%R; auto with real.
unfold FtoRradix in |- *; rewrite Fopp_correct.
apply Ropp_le_contravar.
unfold boundR, boundNat, FtoRradix, FtoR in |- *; simpl in |- *;
auto with real zarith.
rewrite Rmult_1_l; apply Rlt_le; auto with real zarith arith.
Qed.

Definition mBFloat (p : R) :=
map (fun p : Z × ZFloat (fst p) (snd p))
(mProd Z Z (Z × Z)
(mZlist (- pPred (vNum b)) (pPred (vNum b)))
(mZlist (- dExp b) (Fexp (boundR p)))).

(r : R) (q : float),
¬ is_Fzero q
(Fopp (boundR r) < q)%R
(q < boundR r)%R Fbounded b q In q (mBFloat r).
intros r q.
case (Zle_or_lt (Fexp (boundR r)) (Fexp q)); intros H'.
intros H'0 H'1 H'2 H'3; case H'0.
rewrite <-
FshiftCorrect with (n := Zabs_nat (Fexp q - Fexp (boundR r))) (x := q);
auto with arith.
unfold is_Fzero in |- ×.
cut ( p : Z, (- 1%nat < p)%Z (p < 1%nat)%Z p = 0%Z);
[ intros tmp; apply tmp | idtac ].
replace (- 1%nat)%Z with (Fnum (Fopp (boundR r))).
rewrite FshiftCorrect; auto.
unfold Fshift in |- *; simpl in |- ×.
rewrite (fun x yinj_abs (x - y)); auto with zarith.
simpl in |- *; auto.
replace (Z_of_nat 1) with (Fnum (boundR r)).
rewrite FshiftCorrect; auto.
unfold Fshift in |- *; simpl in |- ×.
rewrite inj_abs; auto with zarith.
generalize H'; simpl in |- *; auto with zarith.
simpl in |- *; auto.
intros p0; case p0; simpl in |- *; auto with zarith.
intros H'0 H'1 H'2 H'3; unfold mBFloat in |- ×.
replace q with
((fun p : Z × ZFloat (fst p) (snd p)) (Fnum q, Fexp q)).
apply in_map with (f := fun p : Z × ZFloat (fst p) (snd p));
auto.
apply mProd_correct; auto.
apply mZlist_correct; auto with float.
apply Zle_Zabs_inv1; auto with float.
unfold pPred in |- *; apply Zle_Zpred; auto with float.
apply Zle_Zabs_inv2; auto with float.
unfold pPred in |- *; apply Zle_Zpred; auto with float.
apply mZlist_correct; auto with float.
auto with zarith.
case q; simpl in |- *; auto with zarith.
Qed.

Theorem mBFadic_correct2 : r : R, In (boundR r) (mBFloat r).
intros r; unfold mBFloat in |- ×.
replace (boundR r) with
((fun p : Z × ZFloat (fst p) (snd p))
(Fnum (boundR r), Fexp (boundR r))).
apply in_map with (f := fun p : Z × ZFloat (fst p) (snd p));
auto.
apply mProd_correct; auto.
apply mZlist_correct; auto.
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
apply Zle_trans with (- (0))%Z; auto with zarith.
apply Zle_Zopp; unfold pPred in |- *; apply Zle_Zpred; simpl in |- ×.
apply Zlt_trans with 1%Z; auto with zarith.
apply vNumbMoreThanOne with (3 := pGivesBound); auto.
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
unfold pPred in |- *; apply Zle_Zpred; simpl in |- ×.
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
apply vNumbMoreThanOne with (3 := pGivesBound); auto.
apply mZlist_correct; auto.
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
apply Zle_trans with 0%Z; auto with zarith arith.
case (dExp b); auto with zarith.
case (boundR r); simpl in |- *; auto with zarith.
case (boundR r); simpl in |- *; auto with zarith.
Qed.

Theorem mBFadic_correct3 : r : R, In (Fopp (boundR r)) (mBFloat r).
intros r; unfold mBFloat in |- ×.
replace (Fopp (boundR r)) with
((fun p : Z × ZFloat (fst p) (snd p))
(Fnum (Fopp (boundR r)), Fexp (Fopp (boundR r)))).
apply in_map with (f := fun p : Z × ZFloat (fst p) (snd p));
auto.
apply mProd_correct; auto.
apply mZlist_correct; auto.
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
replace (-1)%Z with (- Z_of_nat 1)%Z; auto with zarith.
apply Zle_Zopp.
unfold pPred in |- *; apply Zle_Zpred; simpl in |- ×.
apply (vNumbMoreThanOne radix) with (precision := precision);
auto with zarith.
unfold pPred in |- *; apply Zle_Zpred; simpl in |- ×.
red in |- *; simpl in |- *; auto.
apply mZlist_correct; auto.
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
apply Zle_trans with 0%Z; auto with zarith.
case (dExp b); auto with zarith.
case (boundR r); simpl in |- *; auto with zarith.
case (boundR r); simpl in |- *; auto with zarith.
Qed.

r : R, In (Float 0%nat (- dExp b)) (mBFloat r).
intros p; unfold mBFloat in |- ×.
replace (Float 0%nat (- dExp b)) with
((fun p : Z × ZFloat (fst p) (snd p))
(Fnum (Float 0%nat (- dExp b)), Fexp (Float 0%nat (- dExp b)))).
apply in_map with (f := fun p : Z × ZFloat (fst p) (snd p));
auto.
apply mProd_correct; auto.
apply mZlist_correct; auto.
simpl in |- *; auto with zarith.
replace 0%Z with (- (0))%Z; [ idtac | simpl in |- *; auto ].
apply Zle_Zopp; unfold pPred in |- *; apply Zle_Zpred.
red in |- *; simpl in |- *; auto with zarith.
simpl in |- *; auto with zarith.
unfold pPred in |- *; apply Zle_Zpred.
red in |- *; simpl in |- *; auto with zarith.
apply mZlist_correct; auto.
simpl in |- *; auto with zarith.
unfold boundR, boundNat in |- *; simpl in |- *; auto with zarith.
apply Zle_trans with 0%Z; auto with zarith.
case (dExp b); auto with zarith.
simpl in |- *; auto with zarith.
Qed.

(p : float) (r : R), In p (mBFloat r) Fbounded b p.
intros p r H'; red in |- *; repeat (split; auto).
apply Zpred_Zle_Zabs_intro.
apply mZlist_correct_rev1 with (q := Zpred (Zpos (vNum b)));
auto with real.
apply
mProd_correct_rev1
with
(l2 := mZlist (- dExp b) (Fexp (boundR r)))
(C := (Z × Z)%type)
(b := Fexp p); auto.
apply
in_map_inv with (f := fun p : Z × ZFloat (fst p) (snd p));
auto.
intros a1 b1; case a1; case b1; simpl in |- ×.
intros z z0 z1 z2 H'0; inversion H'0; auto.
generalize H'; case p; auto.
apply mZlist_correct_rev2 with (p := (- Zpred (Zpos (vNum b)))%Z);
auto.
apply
mProd_correct_rev1
with
(l2 := mZlist (- dExp b) (Fexp (boundR r)))
(C := (Z × Z)%type)
(b := Fexp p); auto.
apply
in_map_inv with (f := fun p : Z × ZFloat (fst p) (snd p));
auto.
intros a1 b1; case a1; case b1; simpl in |- ×.
intros z z0 z1 z2 H'0; inversion H'0; auto.
generalize H'; case p; auto.
apply mZlist_correct_rev1 with (q := Fexp (boundR r)); auto.
apply
mProd_correct_rev2
with
(l1 := mZlist (- pPred (vNum b)) (pPred (vNum b)))
(C := (Z × Z)%type)
(a := Fnum p); auto.
apply
in_map_inv with (f := fun p : Z × ZFloat (fst p) (snd p));
auto.
intros a1 b1; case a1; case b1; simpl in |- ×.
intros z z0 z1 z2 H'0; inversion H'0; auto.
generalize H'; case p; auto.
Qed.

Definition ProjectorP (P : R float Prop) :=
p q : float, Fbounded b p P p q p = q :>R.

Definition MonotoneP (P : R float Prop) :=
(p q : R) (p' q' : float),
(p < q)%R P p p' P q q' (p' q')%R.

Definition isMin (r : R) (min : float) :=
Fbounded b min
(min r)%R
( f : float, Fbounded b f (f r)%R (f min)%R).

Theorem isMin_inv1 : (p : float) (r : R), isMin r p (p r)%R.
intros p r H; case H; intros H1 H2; case H2; auto.
Qed.

Theorem ProjectMin : ProjectorP isMin.
red in |- ×.
intros p q H' H'0; apply Rle_antisym.
elim H'0; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2;
auto with real.
apply isMin_inv1 with (1 := H'0); auto.
Qed.

Theorem MonotoneMin : MonotoneP isMin.
red in |- ×.
intros p q p' q' H' H'0 H'1.
elim H'1; intros H'2 H'3; elim H'3; intros H'4 H'5; apply H'5; clear H'3 H'1;
auto.
case H'0; auto.
apply Rle_trans with p; auto.
apply isMin_inv1 with (1 := H'0); auto.
apply Rlt_le; auto.
Qed.

Definition isMax (r : R) (max : float) :=
Fbounded b max
(r max)%R
( f : float, Fbounded b f (r f)%R (max f)%R).

Theorem isMax_inv1 : (p : float) (r : R), isMax r p (r p)%R.
intros p r H; case H; intros H1 H2; case H2; auto.
Qed.

Theorem ProjectMax : ProjectorP isMax.
red in |- ×.
intros p q H' H'0; apply Rle_antisym.
apply isMax_inv1 with (1 := H'0); auto.
elim H'0; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2;
auto with real.
Qed.

Theorem MonotoneMax : MonotoneP isMax.
red in |- ×.
intros p q p' q' H' H'0 H'1.
elim H'0; intros H'2 H'3; elim H'3; intros H'4 H'5; apply H'5; clear H'3 H'0.
case H'1; auto.
apply Rle_trans with q; auto.
apply Rlt_le; auto.
apply isMax_inv1 with (1 := H'1); auto.
Qed.

Theorem MinEq :
(p q : float) (r : R), isMin r p isMin r q p = q :>R.
intros p q r H' H'0; apply Rle_antisym.
elim H'0; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2 H'0;
auto.
case H'; auto.
apply isMin_inv1 with (1 := H'); auto.
elim H'; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2 H';
auto.
case H'0; auto.
apply isMin_inv1 with (1 := H'0); auto.
Qed.

Theorem MaxEq :
(p q : float) (r : R), isMax r p isMax r q p = q :>R.
intros p q r H' H'0; apply Rle_antisym.
elim H'; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2 H';
auto.
case H'0; auto.
apply isMax_inv1 with (1 := H'0); auto.
elim H'0; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2 H'0;
auto.
case H'; auto.
apply isMax_inv1 with (1 := H'); auto.
Qed.

Theorem MinOppMax :
(p : float) (r : R), isMin r p isMax (- r) (Fopp p).
intros p r H'; split.
apply oppBounded; case H'; auto.
split.
unfold FtoRradix in |- *; rewrite Fopp_correct.
apply Ropp_le_contravar; apply isMin_inv1 with (1 := H'); auto.
intros f H'0 H'1.
rewrite <- (Fopp_Fopp f).
unfold FtoRradix in |- *; rewrite Fopp_correct; rewrite Fopp_correct.
apply Ropp_le_contravar.
elim H'.
intros H'2 H'3; elim H'3; intros H'4 H'5; apply H'5; clear H'3.
apply oppBounded; case H'; auto.
rewrite <- (Ropp_involutive r).
unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real.
Qed.

Theorem MaxOppMin :
(p : float) (r : R), isMax r p isMin (- r) (Fopp p).
intros p r H'; split.
apply oppBounded; case H'; auto.
split.
unfold FtoRradix in |- *; rewrite Fopp_correct.
apply Ropp_le_contravar; apply isMax_inv1 with (1 := H'); auto.
intros f H'0 H'1.
rewrite <- (Fopp_Fopp f).
unfold FtoRradix in |- *; repeat rewrite Fopp_correct.
apply Ropp_le_contravar.
elim H'.
intros H'2 H'3; elim H'3; intros H'4 H'5; apply H'5; clear H'3.
apply oppBounded; auto.
rewrite <- (Ropp_involutive r).
unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real.
Qed.

Theorem MinMax :
(p : float) (r : R),
isMin r p r p :>R isMax r (FNSucc b radix precision p).
intros p r H' H'0.
split.
apply FNSuccCanonic; auto.
inversion H'; auto.
split.
case (Rle_or_lt (FNSucc b radix precision p) r); intros H'2; auto.
absurd (FNSucc b radix precision p p)%R.
apply Rlt_not_le.
unfold FtoRradix in |- *; apply FNSuccLt; auto.
inversion H'; auto.
elim H0; intros H'1 H'3; apply H'3; auto.
apply Rlt_le; auto.
intros f H'2 H'3.
unfold FtoRradix in |- *; apply FNSuccProp; auto.
inversion H'; auto.
apply Rlt_le_trans with r; auto.
case (Rle_or_lt r p); auto.
apply Rle_antisym; auto; apply isMin_inv1 with (1 := H'); auto.
rewrite FnormalizeCorrect; auto.
unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
Qed.

Theorem MinExList :
(r : R) (L : list float),
( f : float, In f L (r < f)%R)
( min : float,
In min L
(min r)%R ( f : float, In f L (f r)%R (f min)%R)).
intros r L; elim L; simpl in |- *; auto.
left; intros f H'; elim H'.
intros a l H'.
elim H';
[ intros H'0; clear H'
| intros H'0; elim H'0; intros min E; elim E; intros H'1 H'2; elim H'2;
intros H'3 H'4; try exact H'4; clear H'2 E H'0 H' ].
case (Rle_or_lt a r); intros H'1.
right; a; repeat split; auto.
intros f H'; elim H';
[ intros H'2; rewrite <- H'2; clear H' | intros H'2; clear H' ];
auto with real.
intros H'; Contradict H'; auto with real.
apply Rlt_not_le; auto with real.
left; intros f H'; elim H';
[ intros H'2; rewrite <- H'2; clear H' | intros H'2; clear H' ];
auto.
case (Rle_or_lt a min); intros H'5.
right; min; repeat split; auto.
intros f H'; elim H';
[ intros H'0; rewrite <- H'0; clear H' | intros H'0; clear H' ];
auto.
case (Rle_or_lt a r); intros H'6.
right; a; repeat split; auto.
intros f H'; elim H';
[ intros H'0; rewrite <- H'0; clear H' | intros H'0; clear H' ];
auto with real.
intros H'; apply Rle_trans with (FtoRradix min); auto with real.
right; min; split; auto; split; auto.
intros f H'; elim H';
[ intros H'0; elim H'0; clear H' | intros H'0; clear H' ];
auto.
intros H'; Contradict H'6; auto with real.
apply Rle_not_lt; auto.
Qed.

Theorem MinEx : r : R, min : float, isMin r min.
intros r.
case (MinExList r (mBFloat r)).
intros H'0; absurd (Fopp (boundR r) r)%R; auto.
apply Rlt_not_le.
apply H'0.
apply Rlt_le.
apply boundRCorrect2; auto.
intros H'0; elim H'0; intros min E; elim E; intros H'1 H'2; elim H'2;
intros H'3 H'4; clear H'2 E H'0.
min; split; auto.
apply mBPadic_Fbounded with (r := r); auto.
split; auto.
intros f H'0 H'2.
case (Req_dec f 0); intros H'6.
apply H'4; auto.
rewrite H'6.
unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real.
rewrite H'6.
unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real.
case (Rle_or_lt f (Fopp (boundR r))); intros H'5.
apply Rle_trans with (FtoRradix (Fopp (boundR r))); auto.
apply H'4; auto.
apply Rlt_le.
apply boundRCorrect2; auto.
case (Rle_or_lt (boundR r) f); intros H'7.
apply Rlt_le_trans with (FtoRradix (boundR r)); auto.
apply boundRCorrect1; auto.
apply H'4; auto.
Qed.

Theorem MaxEx : r : R, max : float, isMax r max.
intros r; case (MinEx r).
intros x H'.
case (Req_dec x r); intros H'1.
x.
rewrite <- H'1.
red in |- *; split; [ case H' | split ]; auto with real.
apply MinMax; auto.
Qed.

(r : R) (p : float),
Fbounded b p
(p r)%R (r < FNSucc b radix precision p)%R isMin r p.
intros r p H' H'0 H'1.
split; auto.
split; auto.
intros f H'2 H'3.
case (Rle_or_lt f p); auto; intros H'5.
apply Rlt_not_le.
apply Rlt_le_trans with (1 := H'1); auto with real.
unfold FtoRradix in |- *; apply FNSuccProp; auto; try apply FnormalizeCanonic;
auto.
unfold FtoRradix in |- *; repeat rewrite FnormalizeCorrect; auto with real.
apply FnormalizeCanonic; auto.
unfold FtoRradix in |- *; rewrite FnormalizeCorrect; auto with real.
unfold FtoRradix in |- *; rewrite FnormalizeCorrect; auto with real.
Qed.

Theorem FminRep :
p q : float,
isMin p q m : Z, q = Float m (Fexp p) :>R.
intros p q H'.
2: unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
case (Zle_or_lt (Fexp (Fnormalize radix b precision q)) (Fexp p)); intros H'1.
(Fnum p).
unfold FtoRradix in |- *; apply FSuccZleEq with (3 := pGivesBound); auto.
replace (Float (Fnum p) (Fexp p)) with p; [ idtac | case p ]; auto.
[ idtac | rewrite FnormalizeCorrect ]; auto.
apply isMin_inv1 with (1 := H'); auto.
(FNSucc b radix precision q); [ idtac | case p ];
auto.
replace (Float (Fnum p) (Fexp p)) with p; [ idtac | case p ]; auto.
case (Req_dec p q); intros Eq0.
unfold FtoRradix in Eq0; rewrite Eq0.
apply FNSuccLt; auto.
case (MinMax q p); auto.
intros H'2 H'3; elim H'3; intros H'4 H'5; clear H'3.
case H'4; auto.
intros H'0; absurd (p q)%R; rewrite H'0; auto.
apply Rlt_not_le; auto.
unfold FtoRradix in |- *; apply FNSuccLt; auto.
inversion H'.
elim H0; intros H'3 H'6; apply H'6; clear H0; auto.
rewrite <- H'0; auto with real.

(Fnum
(Fshift radix (Zabs_nat (Fexp (Fnormalize radix b precision q) - Fexp p))
pattern (Fexp p) at 2 in |- *;
replace (Fexp p) with
(Fexp
(Zabs_nat (Fexp (Fnormalize radix b precision q) - Fexp p))
rewrite <-
FshiftCorrect
with
(n :=
Zabs_nat (Fexp (Fnormalize radix b precision q) - Fexp p))
(x := Fnormalize radix b precision q).
case
(Fshift radix (Zabs_nat (Fexp (Fnormalize radix b precision q) - Fexp p))
(Fnormalize radix b precision q)); auto.
auto with arith.
simpl in |- *; rewrite inj_abs; auto with zarith.
Qed.

(r : R) (p : float),
Fbounded b p
(r p)%R (FNPred b radix precision p < r)%R isMax r p.
intros r p H' H'0 H'1.
rewrite <- (Ropp_involutive r).
rewrite <- (Fopp_Fopp p).
apply MinOppMax.
apply MinBinade; auto with real float.
unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real.
rewrite <- (Fopp_Fopp (FNSucc b radix precision (Fopp p))).
rewrite <- FNPredFopFNSucc; auto.
unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real arith.
Qed.

Theorem MaxMin :
(p : float) (r : R),
isMax r p r p :>R isMin r (FNPred b radix precision p).
intros p r H' H'0.
rewrite <- (Fopp_Fopp (FNPred b radix precision p)).
rewrite <- (Ropp_involutive r).
apply MaxOppMin.
rewrite FNPredFopFNSucc; auto.
rewrite Fopp_Fopp; auto.
apply MinMax; auto.
apply MaxOppMin; auto.
rewrite <- (Ropp_involutive r); rewrite H'0; auto; unfold FtoRradix in |- *;
rewrite Fopp_correct; auto; apply Ropp_involutive.
Qed.

Theorem FmaxRep :
p q : float,
isMax p q m : Z, q = Float m (Fexp p) :>R.
intros p q H'; case (FminRep (Fopp p) (Fopp q)).
unfold FtoRradix in |- *; rewrite Fopp_correct.
apply MaxOppMin; auto.
intros x H'0.
(- x)%Z.