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)).

Theorem boundBoundNat: (n:nat)(Fbounded b (boundNat n)).

(* 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)).

Theorem boundRrOpp: (r:R)(boundR r)=(boundR (Ropp r)).

Theorem boundRCorrect2: (r:R)(Rlt (Fopp (boundR r)) r).

(* 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)).

Theorem mBFadic_correct2: (r:R)(In (boundR r) (mBFloat r)).

Theorem mBFadic_correct3: (r:R)(In (Fopp (boundR r)) (mBFloat r)).

Theorem mBFadic_correct4: (r:R)(In (Float O (Zopp (dExp b))) (mBFloat r)).

Theorem mBPadic_Fbounded: (p:float) (r:R) (In p (mBFloat r)) ->(Fbounded b p).

(* 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).
(* It is monotone *)

Theorem MonotoneMin: (MonotoneP isMin).

(* 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).
(* It is monotone *)

Theorem MonotoneMax: (MonotoneP isMax).
(* Minimun is defined upto equality *)

Theorem MinEq: (p, q:float) (r:R) (isMin r p) -> (isMin r q) -><R> p==q.
(* Maximum is defined upto equality *)

Theorem MaxEq: (p, q:float) (r:R) (isMax r p) -> (isMax r q) -><R> p==q.
(* Min and Max are related *)

Theorem MinOppMax: (p:float) (r:R) (isMin r p) ->(isMax (Ropp r) (Fopp p)).
(* Max and Min are related *)

Theorem MaxOppMin: (p:float) (r:R) (isMax r p) ->(isMin (Ropp r) (Fopp p)).
(* 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)).
(* 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)))).
(* A minimum always exists *)

Theorem MinEx: (r:R)(Ex [min:float] (isMin r min)).
(* A maximum always exists *)

Theorem MaxEx: (r:R)(Ex [max:float] (isMax r max)).
(* 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).
(* 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))).
(* 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).
(* 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)).
(* 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))).
End FMinMax.

30/05/01, 18:00