MSB.v

Require Import Float.
Require Import Fcomp.
Require Import Fprop.
Require Import Fop.
Require Import Fnorm.
Section mf.
Variable radix:nat.
Hypothesis radixMoreThanOne:(lt (1) radix).

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.

Fixpoint maxDiv[v, p:nat]: nat :=
   Cases p of
       O => O
      | (S p') => Cases (dividesP v (exp radix p)) of
                      (left _) => p
                     | (right _) => (maxDiv v p')
                  end
   end.

Theorem maxDivLess: (v, p:nat)(le (maxDiv v p) p).

Theorem maxDivLt: (v, p:nat) ~ (Ndivides v (exp radix p)) ->(lt (maxDiv v p) p).

Theorem maxDivCorrect: (v, p:nat)(Ndivides v (exp radix (maxDiv v p))).

Theorem maxDivSimplAux:
  (v, p, q:nat) p=(maxDiv v (S (plus q p))) ->p=(maxDiv v (S p)).

Theorem maxDivSimpl:
  (v, p, q:nat) (lt p q) -> p=(maxDiv v q) ->p=(maxDiv v (S p)).

Theorem maxDivSimplInvAux:
  (v, p, q:nat) p=(maxDiv v (S p)) ->p=(maxDiv v (S (plus q p))).

Theorem maxDivSimplInv:
  (v, p, q:nat) (lt p q) -> p=(maxDiv v (S p)) ->p=(maxDiv v q).

Theorem maxDivUnique:
  (v, p:nat) p=(maxDiv v (S p)) ->
  (Ndivides v (exp radix p)) /\ ~ (Ndivides v (exp radix (S p))).

Theorem maxDivUniqueDigit:
  (v:nat) ~ v=O ->
  (Ndivides v (exp radix (maxDiv v (digit radix v)))) /\
  ~ (Ndivides v (exp radix (S (maxDiv v (digit radix v))))).

Theorem maxDivUniqueInverse:
  (v, p:nat) (Ndivides v (exp radix p)) -> ~ (Ndivides v (exp radix (S p))) ->
  p=(maxDiv v (S p)).

Theorem maxDivUniqueInverseDigit:
  (v, p:nat)
  ~ v=O -> (Ndivides v (exp radix p)) -> ~ (Ndivides v (exp radix (S p))) ->
  p=(maxDiv v (digit radix v)).

Theorem maxDivPlus:
  (v, n:nat) ~ v=O ->
  (maxDiv (mult v (exp radix n)) (plus (digit radix v) n))=
  (plus (maxDiv v (digit radix v)) n).

Definition LSB :=
   [x:float]
   (Zplus (inject_nat (maxDiv (absolu (Fnum x)) (Fdigit radix x))) (Fexp x)).

Theorem LSB_shift:
  (x:float) (n:nat) ~ (is_Fzero x) ->(LSB x)=(LSB (Fshift radix n x)).

Theorem LSB_comp:
  (x, y:float) (n:nat) ~ (is_Fzero x) -> <R> x==y ->(LSB x)=(LSB y).

Theorem LSB_opp: (x:float)(LSB x)=(LSB (Fopp x)).

Theorem LSB_abs: (x:float)(LSB x)=(LSB (Fabs x)).

Definition MSB :=
   [x:float](Zpred (Zplus (inject_nat (Fdigit radix x)) (Fexp x))).

Theorem MSB_shift:
  (x:float) (n:nat) ~ (is_Fzero x) ->(MSB x)=(MSB (Fshift radix n x)).

Theorem MSB_comp:
  (x, y:float) (n:nat) ~ (is_Fzero x) -> <R> x==y ->(MSB x)=(MSB y).

Theorem MSB_opp: (x:float)(MSB x)=(MSB (Fopp x)).

Theorem MSB_abs: (x:float)(MSB x)=(MSB (Fabs x)).

Theorem LSB_le_MSB: (x:float) ~ (is_Fzero x) ->(Zle (LSB x) (MSB x)).

Theorem Fexp_le_LSB: (x:float)(Zle (Fexp x) (LSB x)).

Theorem Ulp_Le_LSigB: (x:float)(Rle (Float (1) (Fexp x)) (Float (1) (LSB x))).

Theorem Fexp_le_MSB: (x:float) ~ (is_Fzero x) ->(Zle (Fexp x) (MSB x)).

Theorem MSB_le_abs:
  (x:float) ~ (is_Fzero x) ->(Rle (Float (1) (MSB x)) (Fabs x)).

Theorem abs_lt_MSB: (x:float)(Rlt (Fabs x) (Float (1) (Zs (MSB x)))).

Theorem LSB_le_abs:
  (x:float) ~ (is_Fzero x) ->(Rle (Float (1) (LSB x)) (Fabs x)).

Theorem MSB_monotoneAux:
  (x, y:float) (Rle (Fabs x) (Fabs y)) -> (Fexp x)=(Fexp y) ->
  (Zle (MSB x) (MSB y)).

Theorem MSB_monotone:
  (x, y:float) ~ (is_Fzero x) -> ~ (is_Fzero y) -> (Rle (Fabs x) (Fabs y)) ->
  (Zle (MSB x) (MSB y)).

Theorem MSB_le_multAux:
  (x, y:float) ~ (is_Fzero x) -> ~ (is_Fzero y) ->
  (Zle (Zplus (MSB x) (MSB y)) (MSB (Fmult x y))).

Theorem MSB_le_mult:
  (x, y:float) ~ (is_Fzero x) -> ~ (is_Fzero y) ->
  (Rle
     (Fmult (Float (1) (MSB x)) (Float (1) (MSB y)))
     (Float (1) (MSB (Fmult x y)))).

Theorem mult_le_MSBAux:
  (x, y:float) ~ (is_Fzero x) -> ~ (is_Fzero y) ->
  (Zle (MSB (Fmult x y)) (Zs (Zplus (MSB x) (MSB y)))).

Theorem mult_le_MSB:
  (x, y:float) ~ (is_Fzero x) -> ~ (is_Fzero y) ->
  (Rle
     (Float (1) (MSB (Fmult x y)))
     (Rmult radix (Fmult (Float (1) (MSB x)) (Float (1) (MSB y))))).

Theorem MSB_mix:
  (x, y:float) ~ (is_Fzero x) -> ~ (is_Fzero y) ->
  (Rlt
     (Rmult (Fabs x) (Float (1) (MSB y)))
     (Rmult radix (Rmult (Fabs y) (Float (1) (MSB x))))).

Theorem LSB_rep:
  (x, y:float) ~ (is_Fzero y) -> (Zle (LSB x) (LSB y)) ->
  (Ex [z:Z] <R> y==(Float z (Fexp x))).

Theorem LSB_rep_min: (p:float)(Ex [z:Z] <R> p==(Float z (LSB p))).
End mf.

30/05/01, 18:19