Fodd.v

(****************************************************************************                                                                                         IEEE754  :  Fodd                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Import ZArith.
Require Import PolyList.
Require Import Float.
Require Import Fnorm.
Require Import Fop.
Require Import Fcomp.
Require Import FSucc.
Require Import FPred.
Require Import Fmin.
Section FOdd.
Variable b:Fbound.
Variable radix:nat.
Variable precision:nat.

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne:(lt (S O) radix).
Hypothesis precisionGreaterThanOne:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).
(* We define the parity predicates*)

Inductive Even: nat ->Prop :=
     EvenO: (Even O)
    | EvenSS: (n:nat) (Even n) ->(Even (S (S n))) .

Inductive Odd: nat ->Prop :=
     Odd1: (Odd (S O))
    | OddSS: (n:nat) (Odd n) ->(Odd (S (S n))) .

Theorem OddSEven: (n:nat) (Odd n) ->(Even (S n)).

Theorem EvenSOdd: (n:nat) (Even n) ->(Odd (S n)).

Theorem OddSEvenInv: (n:nat) (Odd (S n)) ->(Even n).

Theorem EvenSOddInv: (n:nat) (Even (S n)) ->(Odd n).

Theorem OddEvenDec: (n:nat){(Odd n)}+{(Even n)}.

Theorem OddNEven: (n:nat) (Odd n) ->~ (Even n).

Theorem EvenNOdd: (n:nat) (Even n) ->~ (Odd n).

Theorem EvenPlusAux:
  (n, m:nat)
  (iff (Odd (plus n m)) (Odd n) /\ (Even m) \/ (Even n) /\ (Odd m)) /\
  (iff (Even (plus n m)) (Even n) /\ (Even m) \/ (Odd n) /\ (Odd m)).

Theorem EvenPlus1: (n, m:nat) (Even n) -> (Even m) ->(Even (plus n m)).

Theorem EvenPlus2: (n, m:nat) (Odd n) -> (Odd m) ->(Even (plus n m)).

Theorem EvenPlusInv1: (n, m:nat) (Even (plus n m)) -> (Even n) ->(Even m).

Theorem EvenPlusInv2: (n, m:nat) (Even (plus n m)) -> (Odd n) ->(Odd m).

Theorem OddPlus1: (n, m:nat) (Odd n) -> (Even m) ->(Odd (plus n m)).

Theorem OddPlus2: (n, m:nat) (Even n) -> (Odd m) ->(Odd (plus n m)).

Theorem OddPlusInv1: (n, m:nat) (Odd (plus n m)) -> (Odd m) ->(Even n).

Theorem OddPlusInv2: (n, m:nat) (Odd (plus n m)) -> (Even m) ->(Odd n).

Theorem EvenMultAux:
  (n, m:nat)
  (iff (Odd (mult n m)) (Odd n) /\ (Odd m)) /\
  (iff (Even (mult n m)) (Even n) \/ (Even m)).

Theorem EvenMult1: (n, m:nat) (Even n) ->(Even (mult n m)).

Theorem EvenMult2: (n, m:nat) (Even m) ->(Even (mult n m)).

Theorem EvenMultInv: (n, m:nat) (Even (mult n m)) -> (Odd n) ->(Even m).

Theorem OddMult: (n, m:nat) (Odd n) -> (Odd m) ->(Odd (mult n m)).

Theorem OddMultInv: (n, m:nat) (Odd (mult n m)) ->(Odd n).

Theorem OddExp: (n, m:nat) (Odd n) ->(Odd (exp n m)).

Theorem EvenExp: (n, m:nat) (Even n) ->(Even (exp n (S m))).

Definition Feven := [p:float](Even (absolu (Fnum p))).

Definition Fodd := [p:float](Odd (absolu (Fnum p))).

Theorem FevenO: (p:float) (is_Fzero p) ->(Feven p).

Theorem FevenOrFodd: (p:float)(Feven p) \/ (Fodd p).

Theorem FevenSucProp:
  (p:float)
  ((Fodd p) ->(Feven (FSucc b radix precision p))) /\
  ((Feven p) ->(Fodd (FSucc b radix precision p))).

Theorem FoddSuc: (p:float) (Fodd p) ->(Feven (FSucc b radix precision p)).

Theorem FevenSuc: (p:float) (Feven p) ->(Fodd (FSucc b radix precision p)).

Theorem FevenFop: (p:float) (Feven p) ->(Feven (Fopp p)).

Theorem FoddFop: (p:float) (Fodd p) ->(Fodd (Fopp p)).

Theorem FevenPred: (p:float) (Fodd p) ->(Feven (FPred b radix precision p)).

Theorem FoddPred: (p:float) (Feven p) ->(Fodd (FPred b radix precision p)).

Definition FNodd := [p:float](Fodd (Fnormalize radix b precision p)).

Definition FNeven := [p:float](Feven (Fnormalize radix b precision p)).

Theorem FNoddEq:
  (f1, f2:float)
  (Fbounded b f1) -> (Fbounded b f2) -> <R> f1==f2 -> (FNodd f1) ->(FNodd f2).

Theorem FNevenEq:
  (f1, f2:float)
  (Fbounded b f1) -> (Fbounded b f2) -> <R> f1==f2 -> (FNeven f1) ->(FNeven f2).

Theorem FNevenFop: (p:float) (FNeven p) ->(FNeven (Fopp p)).

Theorem FNoddFop: (p:float) (FNodd p) ->(FNodd (Fopp p)).

Theorem FNoddSuc:
  (p:float) (Fbounded b p) -> (FNodd p) ->(FNeven (FNSucc b radix precision p)).

Theorem FNevenSuc:
  (p:float) (Fbounded b p) -> (FNeven p) ->(FNodd (FNSucc b radix precision p)).

Theorem FNevenPred:
  (p:float) (Fbounded b p) -> (FNodd p) ->(FNeven (FNPred b radix precision p)).

Theorem FNoddPred:
  (p:float) (Fbounded b p) -> (FNeven p) ->(FNodd (FNPred b radix precision p)).

Theorem FNevenOrFNodd: (p:float)(FNeven p) \/ (FNodd p).

Theorem FnOddNEven: (n:float) (FNodd n) ->~ (FNeven n).

Theorem EvenD: (n:nat) (Even n) ->(Ex [m:nat] n=(mult (2) m)).

Theorem FEvenD:
  (p:float) (Fbounded b p) -> (Feven p) ->
  (Ex [q:float] (Fbounded b q) /\ <R> p==(Rmult (2) q)).

Theorem FNEvenD:
  (p:float) (Fbounded b p) -> (FNeven p) ->
  (Ex [q:float] (Fbounded b q) /\ <R> p==(Rmult (2) q)).
End FOdd.

30/05/01, 18:07