Fmin.v

(****************************************************************************                                                                                         IEEE754  :  Fmin                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Import PolyList.
Require Import Float.
Require Import Fnorm.
Require Import Fop.
Require Import Fcomp.
Require Import FSucc.
Require Import FPred.
Require Import Zenum.

Inductive Option[A:Set]: Set :=
     Some: (x:A)(Option A)
    | None: (Option A) .
Section FMinMax.
Variable b:Fbound.
Variable radix:nat.
Variable precision:nat.

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne:(lt (S O) radix).
Hypothesis precisionNotZero:~ precision=O.
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).

(* a function that returns a boundd greater than a given nat *)

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

Theorem boundNatCorrect: (n:nat)(Rlt n (boundNat n)).
Intros n; Unfold FtoRradix FtoR boundNat; Simpl.
Rewrite Rmult_ne_r.
Rewrite powerRZ_is_exp; Auto with real arith.
Qed.

Theorem boundBoundNat: (n:nat)(Fbounded b (boundNat n)).
Intros n; Repeat Split; Unfold boundNat; Simpl; Auto with zarith.
Replace (POS xH) with (inject_nat (1)); [Apply inj_le | Simpl; Auto].
Apply le_trans with m := (minus radix (1)); Auto with zarith.
Rewrite pGivesBound.
Apply minus_le; Auto with arith.
Pattern 1 radix; Replace radix with (exp radix (1)); Auto with arith zarith.
Simpl; Auto with zarith.
Qed.

(* A function that returns a bounded greater than a given r *)

Definition boundR := [r:R](boundNat (absolu (up (Rabsolu r)))).

Theorem boundRCorrect1: (r:R)(Rlt r (boundR r)).
Intros r; Case (Rle_or_lt r R0); Intros H'.
Apply Rle_lt_trans with 1 := H'.
Unfold boundR boundNat FtoRradix FtoR; Simpl; Auto with real.
Rewrite Rmult_ne_r; Auto with real arith.
Apply Rlt_trans with 2 := (boundNatCorrect (absolu (up (Rabsolu r)))).
Replace (Rabsolu r) with r; Auto with real.
Apply Rlt_le_trans with r2 := (IZR (up r)); Auto with real zarith.
Generalize (archimed r); Intuition.
Rewrite INR_IZR_INZ; Auto with real zarith.
Unfold Rabsolu; Case (case_Rabsolu r); Auto with real.
Intros H'0; Contradict H'0; Auto with real.
Qed.

Theorem boundRrOpp: (r:R)(boundR r)=(boundR (Ropp r)).
Intros R; Unfold boundR.
Rewrite Rabsolu_Ropp; Auto.
Qed.

Theorem boundRCorrect2: (r:R)(Rlt (Fopp (boundR r)) r).
Intros r; Case (Rle_or_lt r R0); Intros H'.
Rewrite boundRrOpp.
Pattern 2 r; Rewrite <- (Ropp_Ropp r).
Unfold FtoRradix; Rewrite Fopp_correct.
Apply Rlt_Ropp; Apply boundRCorrect1; Auto.
Apply Rle_lt_trans with R0; Auto.
Replace R0 with (Ropp R0); Auto with real.
Unfold FtoRradix; Rewrite Fopp_correct.
Apply Rle_Ropp.
Unfold boundR boundNat FtoRradix FtoR; Simpl; Auto with real zarith.
AutoRewrite [Rsimpl]; Apply Rlt_le; Auto with real zarith arith.
Qed.

(* A function that returns a list containing all the bounded smaller than a given real *)

Definition mBFloat :=
   [p:R]
   (map
      [p:Z * Z](Float (Fst p) (Snd p))
      (mProd
         Z Z Z * Z (mZlist (Zopp (vNum b)) (vNum b))
         (mZlist (Zopp (dExp b)) (Fexp (boundR p))))).

Theorem mBFadic_correct1:
  (r:R)
  (q:float)
  ~ (is_Fzero q) ->
  (Rlt (Fopp (boundR r)) q) -> (Rlt q (boundR 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.
Apply is_Fzero_rep2 with radix := radix; Auto.
Rewrite <- FshiftCorrect with n := (absolu (Zminus (Fexp q) (Fexp (boundR r))))
                              x := q; Auto with arith.
Apply is_Fzero_rep1 with radix := radix.
Unfold is_Fzero.
Cut (p:Z) (Zlt (Zopp (1)) p) -> (Zlt p (1)) ->p=ZERO;
[Intros tmp; Apply tmp | Idtac].
Replace (Zopp (1)) with (Fnum (Fopp (boundR r))).
Apply Rlt_Fexp_eq_Zlt with radix := radix; Auto with zarith.
Rewrite FshiftCorrect; Auto.
Unfold Fshift; Simpl.
Rewrite inj_abs; Auto with zarith.
Generalize H'; Simpl; Auto with zarith.
Simpl; Auto.
Replace (inject_nat (1)) with (Fnum (boundR r)).
Apply Rlt_Fexp_eq_Zlt with radix := radix; Auto with zarith.
Rewrite FshiftCorrect; Auto.
Unfold Fshift; Simpl.
Rewrite inj_abs; Auto with zarith.
Generalize H'; Simpl; Auto with zarith.
Simpl; Auto.
Intros p0; Case p0; Simpl; Auto with zarith.
Intros H'0 H'1 H'2 H'3; Unfold mBFloat.
Replace q with ([p:Z * Z](Float (Fst p) (Snd p)) ((Fnum q), (Fexp q))).
Apply in_map with f := [p:Z * Z](Float (Fst p) (Snd p)); Auto.
Apply mProd_correct; Auto.
Apply mZlist_correct; Auto.
Intuition.
Intuition.
Apply mZlist_correct; Auto.
Intuition.
Auto with zarith.
Case q; Simpl; Auto with zarith.
Qed.

Theorem mBFadic_correct2: (r:R)(In (boundR r) (mBFloat r)).
Intros r; Unfold mBFloat.
Replace (boundR r)
     with ([p:Z * Z](Float (Fst p) (Snd p))
             ((Fnum (boundR r)), (Fexp (boundR r)))).
Apply in_map with f := [p:Z * Z](Float (Fst p) (Snd p)); Auto.
Apply mProd_correct; Auto.
Apply mZlist_correct; Auto.
Unfold boundR boundNat; Simpl; Auto with zarith.
Unfold boundR boundNat; Simpl; Auto with zarith.
Replace (POS xH) with (inject_nat (1)); Auto with zarith.
Apply inj_le.
Cut (lt O (vNum b)); Auto with arith.
Apply lt_vNum with 3 := pGivesBound; Auto.
Apply mZlist_correct; Auto.
Unfold boundR boundNat; Simpl; Auto with zarith.
Case (boundR r); Simpl; Auto with zarith.
Case (boundR r); Simpl; Auto with zarith.
Qed.

Theorem mBFadic_correct3: (r:R)(In (Fopp (boundR r)) (mBFloat r)).
Intros r; Unfold mBFloat.
Replace (Fopp (boundR r))
     with ([p:Z * Z](Float (Fst p) (Snd p))
             ((Fnum (Fopp (boundR r))), (Fexp (Fopp (boundR r))))).
Apply in_map with f := [p:Z * Z](Float (Fst p) (Snd p)); Auto.
Apply mProd_correct; Auto.
Apply mZlist_correct; Auto.
Unfold boundR boundNat; Simpl; Auto with zarith.
Replace (NEG xH) with (Zopp (inject_nat (1))); Auto with zarith.
Apply Zle_Zopp.
Apply inj_le.
Cut (lt O (vNum b)); Auto with arith.
Apply lt_vNum with 3 := pGivesBound; Auto.
Unfold boundR boundNat; Simpl; Auto with zarith.
Apply mZlist_correct; Auto.
Unfold boundR boundNat; Simpl; Auto with zarith.
Case (boundR r); Simpl; Auto with zarith.
Case (boundR r); Simpl; Auto with zarith.
Qed.

Theorem mBFadic_correct4: (r:R)(In (Float O (Zopp (dExp b))) (mBFloat r)).
Intros p; Unfold mBFloat.
Replace (Float O (Zopp (dExp b)))
     with ([p:Z * Z](Float (Fst p) (Snd p))
             ((Fnum (Float O (Zopp (dExp b)))),
              (Fexp (Float O (Zopp (dExp b)))))).
Apply in_map with f := [p:Z * Z](Float (Fst p) (Snd p)); Auto.
Apply mProd_correct; Auto.
Apply mZlist_correct; Auto.
Simpl; Auto with zarith.
Simpl; Auto with zarith.
Apply mZlist_correct; Auto.
Simpl; Auto with zarith.
Unfold boundR boundNat; Simpl; Auto with zarith.
Simpl; Auto with zarith.
Qed.

Theorem mBPadic_Fbounded: (p:float) (r:R) (In p (mBFloat r)) ->(Fbounded b p).
Intros p r H'; Red; Repeat Split.
Apply mZlist_correct_rev1 with q := (inject_nat (vNum b)); Auto.
Apply mProd_correct_rev1
     with l2 := (mZlist (Zopp (dExp b)) (Fexp (boundR r))) C := Z * Z
          b := (Fexp p); Auto.
Apply in_map_inv with f := [p:Z * Z](Float (Fst p) (Snd p)); Auto.
Intros a1 b1; Case a1; Case b1; Simpl.
Intros z z0 z1 z2 H'0; Inversion H'0; Auto.
Generalize H'; Case p; Auto.
Apply mZlist_correct_rev2 with p := (Zopp (vNum b)); Auto with real.
Apply mProd_correct_rev1
     with l2 := (mZlist (Zopp (dExp b)) (Fexp (boundR r))) C := Z * Z
          b := (Fexp p); Auto.
Apply in_map_inv with f := [p:Z * Z](Float (Fst p) (Snd p)); Auto.
Intros a1 b1; Case a1; Case b1; Simpl.
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 (Zopp (vNum b)) (vNum b)) C := Z * Z a := (Fnum p); Auto.
Apply in_map_inv with f := [p:Z * Z](Float (Fst p) (Snd p)); Auto.
Intros a1 b1; Case a1; Case b1; Simpl.
Intros z z0 z1 z2 H'0; Inversion H'0; Auto.
Generalize H'; Case p; Auto.
Qed.

(* Some general properties of rounded predicate :    -Projector A bounded is rounded to something equal to itself   - Monotone : the rounded predicate is monotone *)

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

Definition MonotoneP :=
   [P:R -> float ->Prop]
   (p, q:R) (p', q':float) (Rlt p q) -> (P p p') -> (P q q') ->(Rle p' q').

(* What it is to be a minimum*)

Definition isMin :=
   [r:R] [min:float]
   (Fbounded b min) /\
   ((Rle min r) /\ ((f:float) (Fbounded b f) -> (Rle f r) ->(Rle f min))).
(* Min is a projector *)

Theorem ProjectMin: (ProjectorP isMin).
Red.
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.
Intuition.
Qed.
(* It is monotone *)

Theorem MonotoneMin: (MonotoneP isMin).
Red.
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.
Intuition.
Apply Rle_trans with p; Auto.
Intuition.
Apply Rlt_le; Auto.
Qed.

(* What it is to be a maximum *)

Definition isMax :=
   [r:R] [max:float]
   (Fbounded b max) /\
   ((Rle r max) /\ ((f:float) (Fbounded b f) -> (Rle r f) ->(Rle max f))).
(* It is a projector *)

Theorem ProjectMax: (ProjectorP isMax).
Red.
Intros p q H' H'0; Apply Rle_antisym.
Intuition.
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.
(* It is monotone *)

Theorem MonotoneMax: (MonotoneP isMax).
Red.
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.
Intuition.
Apply Rle_trans with q; Auto.
Apply Rlt_le; Auto.
Intuition.
Qed.
(* Minimun is defined upto equality *)

Theorem MinEq: (p, q:float) (r:R) (isMin r p) -> (isMin r q) -><R> p==q.
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; Intuition.
Elim H'; Intros H'1 H'2; Elim H'2; Intros H'3 H'4; Apply H'4; Clear H'2 H';
Auto; Intuition.
Qed.
(* Maximum is defined upto equality *)

Theorem MaxEq: (p, q:float) (r:R) (isMax r p) -> (isMax r q) -><R> p==q.
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; Intuition.
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; Intuition.
Qed.
(* Min and Max are related *)

Theorem MinOppMax: (p:float) (r:R) (isMin r p) ->(isMax (Ropp r) (Fopp p)).
Intros p r H'; Split.
Apply oppBounded; Intuition.
Split.
Unfold FtoRradix; Rewrite Fopp_correct.
Apply Rle_Ropp; Intuition.
Intros f H'0 H'1.
Rewrite <- (Fopp_Fopp f).
Unfold FtoRradix; Rewrite Fopp_correct; Rewrite Fopp_correct.
Apply Rle_Ropp.
Elim H'.
Intros H'2 H'3; Elim H'3; Intros H'4 H'5; Apply H'5; Clear H'3.
Apply oppBounded; Intuition.
Rewrite <- (Ropp_Ropp r).
Unfold FtoRradix; Rewrite Fopp_correct; Auto with real.
Qed.
(* Max and Min are related *)

Theorem MaxOppMin: (p:float) (r:R) (isMax r p) ->(isMin (Ropp r) (Fopp p)).
Intros p r H'; Split.
Apply oppBounded; Intuition.
Split.
Unfold FtoRradix; Rewrite Fopp_correct.
Apply Rle_Ropp; Intuition.
Intros f H'0 H'1.
Rewrite <- (Fopp_Fopp f).
Unfold FtoRradix; Repeat Rewrite Fopp_correct.
Apply Rle_Ropp.
Rewrite <- (Fopp_correct radix f).
Elim H'.
Intros H'2 H'3; Elim H'3; Intros H'4 H'5; Apply H'5; Clear H'3.
Apply oppBounded; Intuition.
Rewrite <- (Ropp_Ropp r).
Unfold FtoRradix; Rewrite Fopp_correct; Auto with real.
Qed.
(* If I have a strict min I can get a max using FNSucc *)

Theorem MinMax:
  (p:float) (r:R) (isMin r p) -> ~ <R> r==p ->
  (isMax r (FNSucc b radix precision p)).
Intros p r H' H'0.
Split.
Apply FcanonicBound with radix := radix precision := precision; Auto with float.
Apply FNSuccCanonic; Auto.
Inversion H'; Auto.
Split.
Case (Rle_or_lt (FNSucc b radix precision p) r); Intros H'2; Auto.
Absurd (Rle (FNSucc b radix precision p) p).
Apply Rle_not.
Unfold FtoRradix; Apply FNSuccLt; Auto.
Inversion H'; Auto.
Elim H0; Intros H'1 H'3; Apply H'3; Auto.
Apply FcanonicBound with radix := radix precision := precision; Auto with float.
Apply Rlt_le; Auto.
Intros f H'2 H'3.
Replace (FtoRradix f) with (FtoRradix (Fnormalize radix b precision f)).
Unfold FtoRradix; Apply FNSuccProp; Auto.
Inversion H'; Auto.
Apply FcanonicBound with radix := radix precision := precision; Auto with float.
Apply Rlt_le_trans with r; Auto.
Case (Rle_or_lt r p); Auto.
Intros H'4; Contradict H'0.
Apply Rle_antisym; Auto; Intuition.
Rewrite FnormalizeCorrect; Auto.
Unfold FtoRradix; Apply FnormalizeCorrect; Auto.
Qed.
(* Find a minimun in a given list if it exists *)

Theorem MinExList:
  (r:R) (L:(list float))
  ((f:float) (In f L) ->(Rlt r f)) \/
  (Ex [min:float]
  (In min L) /\ ((Rle min r) /\ ((f:float) (In f L) -> (Rle f r) ->(Rle f min)))).
Intros r L; Elim L; Simpl; 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; Exists 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.
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; Exists 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; Exists 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.
Apply Rlt_le; Auto.
Right; Exists 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 Rlt_not; Auto.
Qed.
(* A minimum always exists *)

Theorem MinEx: (r:R)(Ex [min:float] (isMin r min)).
Intros r.
Case (MinExList r (mBFloat r)).
Intros H'0; Absurd (Rle (Fopp (boundR r)) r); Auto.
Apply Rle_not.
Apply H'0.
Apply mBFadic_correct3; Auto.
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.
Exists min; Split; Auto.
Apply mBPadic_Fbounded with r := r; Auto.
Split; Auto.
Intros f H'0 H'2.
Case (Req_EM f R0); Intros H'6.
Replace (FtoRradix f) with (FtoRradix (Float O (Zopp (dExp b)))).
Apply H'4; Auto.
Apply mBFadic_correct4; Auto.
Replace (FtoRradix (Float O (Zopp (dExp b)))) with (FtoRradix f); Auto.
Rewrite H'6.
Unfold FtoRradix FtoR; Simpl; Auto with real.
Rewrite H'6.
Unfold FtoRradix FtoR; Simpl; 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 mBFadic_correct3; Auto.
Apply Rlt_le.
Apply boundRCorrect2; Auto.
Case (Rle_or_lt (boundR r) f); Intros H'7.
Contradict H'2; Apply Rle_not.
Apply Rlt_le_trans with (FtoRradix (boundR r)); Auto.
Apply boundRCorrect1; Auto.
Apply H'4; Auto.
Apply mBFadic_correct1; Auto.
Contradict H'6; Unfold FtoRradix; Apply is_Fzero_rep1; Auto.
Qed.
(* A maximum always exists *)

Theorem MaxEx: (r:R)(Ex [max:float] (isMax r max)).
Intros r; Case (MinEx r).
Intros x H'.
Case (Req_EM x r); Intros H'1.
Exists x.
Rewrite <- H'1.
Generalize ProjectMin; Intuition.
Exists (FNSucc b radix precision x).
Apply MinMax; Auto.
Qed.
(* If we are between a bound and its successor, it is our minimum *)

Theorem MinBinade:
  (r:R)
  (p:float)
  (Fbounded b p) -> (Rle p r) -> (Rlt r (FNSucc b radix precision p)) ->
  (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.
Contradict H'3.
Apply Rle_not.
Apply Rlt_le_trans with 1 := H'1; Auto with real.
Replace (FtoRradix f) with (FtoRradix (Fnormalize radix b precision f)).
(Unfold FtoRradix; Apply FNSuccProp); Auto; Try Apply FnormalizeCanonic; Auto.
(Unfold FtoRradix; Repeat Rewrite FnormalizeCorrect); Auto with real.
Apply FcanonicBound with radix := radix precision := precision; Auto.
Apply FnormalizeCanonic; Auto.
(Unfold FtoRradix; Rewrite FnormalizeCorrect); Auto with real.
(Unfold FtoRradix; Rewrite FnormalizeCorrect); Auto with real.
Qed.
(* A min of a float is always represnetable with the same exposant *)

Theorem FminRep:
  (p, q:float) (isMin p q) ->(Ex [m:Z] <R> q==(Float m (Fexp p))).
Intros p q H'.
Replace (FtoRradix q) with (FtoRradix (Fnormalize radix b precision q)).
2:Unfold FtoRradix; Apply FnormalizeCorrect; Auto.
Case (Zle_or_lt (Fexp (Fnormalize radix b precision q)) (Fexp p)); Intros H'1.
Exists (Fnum p).
Unfold FtoRradix; Apply FSuccZleEq with 3 := pGivesBound; Auto.
Replace (Float (Fnum p) (Fexp p)) with p; [Idtac | Case p]; Auto.
Replace (FtoR radix (Fnormalize radix b precision q)) with (FtoR radix q);
[Idtac | Rewrite FnormalizeCorrect]; Auto.
Intuition.
Replace (FSucc b radix precision (Fnormalize radix b precision q))
     with (FNSucc b radix precision q); [Idtac | Case p]; Auto.
Replace (Float (Fnum p) (Fexp p)) with p; [Idtac | Case p]; Auto.
Case (Req_EM 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 (Rle p q); Rewrite H'0; Auto.
Apply Rle_not; Auto.
Unfold FtoRradix; Apply FNSuccLt; Auto.
Inversion H'.
Elim H0; Intros H'3 H'6; Apply H'6; Clear H0; Auto.
Rewrite <- H'0; Auto with real.
Exists (Fnum
          (Fshift
             radix
             (absolu (Zminus (Fexp (Fnormalize radix b precision q)) (Fexp p)))
             (Fnormalize radix b precision q))).
Pattern 2 (Fexp p);
Replace (Fexp p)
      with (Fexp
              (Fshift
                 radix
                 (absolu
                    (Zminus (Fexp (Fnormalize radix b precision q)) (Fexp p)))
                 (Fnormalize radix b precision q))).
Unfold FtoRradix;
Rewrite <- FshiftCorrect with n :=
                               (absolu
                                  (Zminus
                                     (Fexp (Fnormalize radix b precision q))
                                     (Fexp p)))
                               x := (Fnormalize radix b precision q).
Case (Fshift
        radix (absolu (Zminus (Fexp (Fnormalize radix b precision q)) (Fexp p)))
        (Fnormalize radix b precision q)); Auto.
Auto with arith.
Simpl; Rewrite inj_abs; Auto with zarith.
Qed.
(* Same for max *)

Theorem MaxBinade:
  (r:R)
  (p:float)
  (Fbounded b p) -> (Rle r p) -> (Rlt (FNPred b radix precision p) r) ->
  (isMax r p).
Intros r p H' H'0 H'1.
Rewrite <- (Ropp_Ropp r).
Rewrite <- (Fopp_Fopp p).
Apply MinOppMax.
Apply MinBinade; Auto with real float.
Unfold FtoRradix; Rewrite Fopp_correct; Auto with real.
Rewrite <- (Fopp_Fopp (FNSucc b radix precision (Fopp p))).
Rewrite <- FNPredFopFNSucc; Auto.
Unfold FtoRradix; Rewrite Fopp_correct; Auto with real arith.
Qed.
(* Taking the pred of a max we get a min *)

Theorem MaxMin:
  (p:float) (r:R) (isMax r p) -> ~ <R> r==p ->
  (isMin r (FNPred b radix precision p)).
Intros p r H' H'0.
Rewrite <- (Fopp_Fopp (FNPred b radix precision p)).
Rewrite <- (Ropp_Ropp r).
Apply MaxOppMin.
Rewrite FNPredFopFNSucc; Auto.
Rewrite Fopp_Fopp; Auto.
Apply MinMax; Auto.
Apply MaxOppMin; Auto.
Contradict H'0.
Rewrite <- (Ropp_Ropp r); Rewrite H'0; Auto; Unfold FtoRradix;
Rewrite Fopp_correct; Auto; Apply Ropp_Ropp.
Qed.
(* The max of a float can be represented with the same exposant *)

Theorem FmaxRep:
  (p, q:float) (isMax p q) ->(Ex [m:Z] <R> q==(Float m (Fexp p))).
Intros p q H'; Case (FminRep (Fopp p) (Fopp q)).
Unfold FtoRradix; Rewrite Fopp_correct.
Apply MaxOppMin; Auto.
Intros x H'0.
Exists (Zopp x).
Rewrite <- (Ropp_Ropp (FtoRradix q)).
Unfold FtoRradix; Rewrite <- Fopp_correct.
Unfold FtoRradix in H'0; Rewrite H'0.
Unfold FtoR; Simpl; Auto with real.
AutoRewrite [Rsimpl]; Auto.
Qed.
End FMinMax.
Hints Resolve
ProjectMax MonotoneMax MinOppMax MaxOppMin MinMax MinBinade MaxBinade MaxMin
                                                                             :float.

14/12/100, 15:17