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))) .
Hints Resolve EvenO EvenSS Odd1 OddSS :arith.

Theorem OddSEven: (n:nat) (Odd n) ->(Even (S n)).
Intros n H'; Elim H'; Auto with arith.
Qed.

Theorem EvenSOdd: (n:nat) (Even n) ->(Odd (S n)).
Intros n H'; Elim H'; Auto with arith.
Qed.
Hints Resolve OddSEven EvenSOdd :arith.

Theorem OddSEvenInv: (n:nat) (Odd (S n)) ->(Even n).
Intros n H'; Elim H'; Auto with arith.
Inversion H'; Auto with arith.
Qed.

Theorem EvenSOddInv: (n:nat) (Even (S n)) ->(Odd n).
Intros n H'; Elim H'; Auto with arith.
Inversion H'; Auto with arith.
Qed.

Theorem OddEvenDec: (n:nat){(Odd n)}+{(Even n)}.
Intros n; Elim n; Auto with arith.
Intros n0 H'; Case H'; Auto with arith.
Qed.

Theorem OddNEven: (n:nat) (Odd n) ->~ (Even n).
Intros n H'; Elim H'; Auto with arith.
Red; Intros H'0; Inversion H'0.
Intros n0 H'0 H'1; Contradict H'1.
Apply OddSEvenInv.
Apply EvenSOddInv; Auto.
Qed.

Theorem EvenNOdd: (n:nat) (Even n) ->~ (Odd n).
Intros n H'; Elim H'; Auto with arith.
Red; Intros H'0; Inversion H'0.
Intros n0 H'0 H'1; Contradict H'1.
Apply EvenSOddInv.
Apply OddSEvenInv; Auto.
Qed.
Hints Resolve OddNEven EvenNOdd :arith.

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)).
Intros n; Elim n; Simpl; Auto with arith.
Intros m; Split; Auto.
Split.
Intuition.
Intros H'; Elim H'; Auto with arith.
Intros H'0; Elim H'0; Intros H'1 H'2; Inversion H'1.
Intuition.
Split.
Intuition.
Intros H'; Elim H'; Auto with arith.
Intuition.
Intros H'0; Elim H'0; Intros H'1 H'2; Inversion H'1.
Intros n0 H' m; Elim (H' m); Intros H'1 H'2; Elim H'1; Intros E1 E2; Elim H'2;
Intros E3 E4; Clear H'1 H'2.
Split; Split.
Intros H'0; Case E3.
Apply OddSEvenInv; Auto.
Intuition.
Intuition.
Intros H'0; Case H'0; Intros C0; Case C0; Intros C1 C2.
Apply EvenSOdd.
Apply E4; Left; Split; Auto with arith.
Apply OddSEvenInv; Auto.
Apply EvenSOdd.
Apply E4; Right; Split; Auto with arith.
Apply EvenSOddInv; Auto.
Intros H'0.
Case E1.
Apply EvenSOddInv; Auto.
Intuition.
Intuition.
Intros H'0; Case H'0; Intros C0; Case C0; Intros C1 C2.
Apply OddSEven.
Apply E2; Left; Split; Auto with arith.
Apply EvenSOddInv; Auto.
Apply OddSEven.
Apply E2; Right; Split; Auto with arith.
Apply OddSEvenInv; Auto.
Qed.

Theorem EvenPlus1: (n, m:nat) (Even n) -> (Even m) ->(Even (plus n m)).
Intros n m; Generalize (EvenPlusAux n m); Intuition.
Qed.

Theorem EvenPlus2: (n, m:nat) (Odd n) -> (Odd m) ->(Even (plus n m)).
Intros n m; Generalize (EvenPlusAux n m); Intuition.
Qed.

Theorem EvenPlusInv1: (n, m:nat) (Even (plus n m)) -> (Even n) ->(Even m).
Intros n m H; Case (EvenPlusAux n m).
Intros H' H'0; Elim H'0.
Intros H'1; Case H'1; Auto.
Intuition.
Intros H'2 H'3 H'4; Contradict H'4; Case H'2; Auto with arith.
Qed.

Theorem EvenPlusInv2: (n, m:nat) (Even (plus n m)) -> (Odd n) ->(Odd m).
Intros n m H; Case (EvenPlusAux n m).
Intros H' H'0; Elim H'0.
Intros H'1; Case H'1; Auto.
Intros H'2 H'3 H'4; Contradict H'4; Case H'2; Auto with arith.
Intuition.
Qed.
Hints Resolve EvenPlus1 EvenPlus2 :arith.

Theorem OddPlus1: (n, m:nat) (Odd n) -> (Even m) ->(Odd (plus n m)).
Intros n m; Generalize (EvenPlusAux n m); Intuition.
Qed.

Theorem OddPlus2: (n, m:nat) (Even n) -> (Odd m) ->(Odd (plus n m)).
Intros n m; Generalize (EvenPlusAux n m); Intuition.
Qed.

Theorem OddPlusInv1: (n, m:nat) (Odd (plus n m)) -> (Odd m) ->(Even n).
Intros n m H; Case (EvenPlusAux n m).
Intros H' H'0; Elim H'.
Intros H'1; Case H'1; Auto.
Intros H'2 H'3 H'4; Contradict H'4; Case H'2; Auto with arith.
Intuition.
Qed.

Theorem OddPlusInv2: (n, m:nat) (Odd (plus n m)) -> (Even m) ->(Odd n).
Intros n m H; Case (EvenPlusAux n m).
Intros H' H'0; Elim H'.
Intros H'1; Case H'1; Auto.
Intuition.
Intros H'2 H'3 H'4; Contradict H'4; Case H'2; Auto with arith.
Qed.
Hints Resolve OddPlus1 OddPlus2 :arith.

Theorem EvenMultAux:
  (n, m:nat)
  (iff (Odd (mult n m)) (Odd n) /\ (Odd m)) /\
  (iff (Even (mult n m)) (Even n) \/ (Even m)).
Intros n; Elim n; Simpl; Auto with arith.
Intros m; Split; Split; Auto with arith.
Intros H'; Inversion H'.
Intros H'; Elim H'; Auto.
Intros n0 H' m; Split; Split; Auto with arith.
Intros H'0.
Elim (EvenPlusAux m (mult n0 m)); Intros H'3 H'4; Case H'3; Intros H'1 H'2;
Case H'1; Auto.
Intros H'5; Elim H'5; Intros H'6 H'7; Auto with arith.
Split; Auto with arith.
Case (H' m).
Intros H'8 H'9; Case H'9.
Intros H'10; Case H'10; Auto with arith.
Intros H'11 H'12; Contradict H'11; Auto with arith.
Intros H'5; Elim H'5; Intros H'6 H'7; Contradict H'7.
Apply EvenNOdd.
Case (H' m).
Intros H'8 H'9; Case H'9; Intuition.
Intros H'0; Elim H'0; Intros H'1 H'2; Clear H'0.
Elim (EvenPlusAux m (mult n0 m)); Auto.
Intros H'0 H'3.
Elim H'0.
Intros H'4 H'5; Apply H'5; Auto.
Left; Split; Auto with arith.
Case (H' m).
Intros H'6 H'7; Elim H'7.
Intros H'8 H'9; Apply H'9.
Left.
Apply OddSEvenInv; Auto.
Intros H'0.
Elim (EvenPlusAux m (mult n0 m)); Intros H'3 H'4; Case H'4.
Intros H'1 H'2.
Elim H'1; Auto.
Intuition.
Intros H'5; Elim H'5; Intros H'6 H'7; Auto with arith.
Left.
Case (H' m).
Intros H'8; Elim H'8.
Intros H'9; Elim H'9; Auto with arith.
Intros H'0; Elim H'0; Intros H'1.
Case (OddEvenDec m).
Intros H'2.
Elim (EvenPlusAux m (mult n0 m)); Intros H'3 H'4; Case H'4.
Intros H'5 H'6; Apply H'6.
Right; Split; Auto with arith.
Case (H' m).
Intros H'7; Elim H'7.
Intros H'8 H'9 H'10.
Apply H'9.
Split; Auto with arith.
Apply EvenSOddInv; Auto.
Intros H'2.
Elim (EvenPlusAux m (mult n0 m)); Intros H'3 H'4; Case H'4.
Intros H'5 H'6; Apply H'6.
Left; Split; Auto with arith.
Case (H' m).
Intros H'7 H'8; Elim H'8; Auto.
Elim (EvenPlusAux m (mult n0 m)); Intros H'3 H'4; Case H'4.
Intros H'2 H'5; Apply H'5; Auto.
Left; Split; Auto with arith.
Case (H' m).
Intros H'7 H'8; Elim H'8; Auto.
Qed.

Theorem EvenMult1: (n, m:nat) (Even n) ->(Even (mult n m)).
Intros n m; Generalize (EvenMultAux n m); Intuition.
Qed.

Theorem EvenMult2: (n, m:nat) (Even m) ->(Even (mult n m)).
Intros n m; Generalize (EvenMultAux n m); Intuition.
Qed.
Hints Resolve EvenMult1 EvenMult2 :arith.

Theorem EvenMultInv: (n, m:nat) (Even (mult n m)) -> (Odd n) ->(Even m).
Intros n m H' H'0.
Case (EvenMultAux n m).
Intros H'1 H'2; Elim H'2.
Intros H'3; Elim H'3; Auto.
Intros H'4; Contradict H'4; Auto with arith.
Qed.

Theorem OddMult: (n, m:nat) (Odd n) -> (Odd m) ->(Odd (mult n m)).
Intros n m; Generalize (EvenMultAux n m); Intuition.
Qed.
Hints Resolve OddMult :arith.

Theorem OddMultInv: (n, m:nat) (Odd (mult n m)) ->(Odd n).
Intros n m H'.
Case (EvenMultAux n m).
Intros H'1 H'2; Elim H'1.
Intros H'3; Elim H'3; Auto.
Qed.

Theorem OddExp: (n, m:nat) (Odd n) ->(Odd (exp n m)).
Intros n m; Elim m; Simpl.
Intros H'; Apply Odd1.
Intros n0 H' H'0.
Apply OddMult; Auto.
Qed.

Theorem EvenExp: (n, m:nat) (Even n) ->(Even (exp n (S m))).
Intros n m; Simpl; Auto with arith.
Qed.
Hints Resolve OddExp EvenExp :arith.

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).
Intros p H'; Red; Rewrite H'; Simpl; Auto with arith.
Qed.

Theorem FevenOrFodd: (p:float)(Feven p) \/ (Fodd p).
Intros p; Case (OddEvenDec (absolu (Fnum p))); Auto.
Qed.

Theorem FevenSucProp:
  (p:float)
  ((Fodd p) ->(Feven (FSucc b radix precision p))) /\
  ((Feven p) ->(Fodd (FSucc b radix precision p))).
Intros p; Unfold FSucc Fodd Feven.
Case (Z_eq_dec (Fnum p) (vNum b)); Intros H'1.
Rewrite H'1; Simpl; Auto.
Repeat Rewrite absolu_INR.
Rewrite pGivesBound; Unfold nNormMin.
Case (OddEvenDec radix); Auto with arith.
Intros H'; Split; Intros H'0; Auto with arith.
Apply EvenMultInv with n := radix; Auto.
Replace (mult radix (exp radix (pred precision)))
     with (plus (1) (minus (exp radix precision) (1))); Auto with arith.
Rewrite <- le_plus_minus; Auto.
Inversion precisionGreaterThanOne; Simpl; Auto.
Replace (1) with (exp radix O); Auto with arith.
Intros H'; Split; Intros H'0; Auto with arith.
Replace (pred precision) with (S (pred (pred precision))); Auto with arith.
Inversion precisionGreaterThanOne; Simpl; Auto.
Inversion H; Simpl; Auto.
Apply OddMultInv with m := radix.
(Rewrite mult_sym;
  Replace (mult radix (exp radix (pred precision)))
       with (plus (1) (minus (exp radix precision) (1)))); Auto with arith.
Rewrite <- le_plus_minus; Auto.
Inversion precisionGreaterThanOne; Simpl; Auto.
Replace (1) with (exp radix O); Auto with arith.
Case (Z_eq_dec (Fnum p) (Zopp (nNormMin radix precision))); Intros H'2.
Case (Z_eq_dec (Fexp p) (Zopp (dExp b))); Intros H'3.
Simpl; Auto with arith.
Case (Zle_or_lt ZERO (Fnum p)); Intros Zle0.
Rewrite absolu_Zs; Auto with arith.
Rewrite <- (absolu_Zs_neg (Fnum p)); Auto with arith.
Split; Intros H'.
Apply OddSEvenInv; Auto.
Apply EvenSOddInv; Auto.
Rewrite H'2; Simpl; Auto.
Repeat Rewrite absolu_Zopp; Repeat Rewrite absolu_INR.
Rewrite pGivesBound; Unfold nNormMin.
Case (OddEvenDec radix); Auto with arith.
Intros H'; Split; Intros H'0.
Apply OddPlusInv1 with m := (1); Auto with arith.
Rewrite plus_sym; Rewrite <- le_plus_minus.
Replace precision with (S (pred precision)); Simpl; Auto with arith.
Inversion precisionGreaterThanOne; Auto.
Replace (1) with (exp radix O); Auto with arith.
Contradict H'0; Auto with arith.
Intros H'; Split; Intros H'0.
Contradict H'0; Replace (pred precision) with (S (pred (pred precision)));
Auto with arith.
Inversion precisionGreaterThanOne; Simpl; Auto.
Inversion H; Simpl; Auto.
Apply EvenPlusInv2 with n := (1); Auto with arith.
Rewrite <- le_plus_minus; Auto.
Replace precision with (S (pred precision)); Auto with arith.
Inversion precisionGreaterThanOne; Simpl; Auto.
Replace (1) with (exp radix O); Auto with arith.
Simpl; Auto with arith.
Case (Zle_or_lt ZERO (Fnum p)); Intros Zle0.
Rewrite absolu_Zs; Auto with arith.
Rewrite <- (absolu_Zs_neg (Fnum p)); Auto with arith.
Split; Intros H'.
Apply OddSEvenInv; Auto.
Apply EvenSOddInv; Auto.
Qed.

Theorem FoddSuc: (p:float) (Fodd p) ->(Feven (FSucc b radix precision p)).
Intros p H'; Case (FevenSucProp p); Auto.
Qed.

Theorem FevenSuc: (p:float) (Feven p) ->(Fodd (FSucc b radix precision p)).
Intros p H'; Case (FevenSucProp p); Auto.
Qed.

Theorem FevenFop: (p:float) (Feven p) ->(Feven (Fopp p)).
Intros p; Unfold Feven.
Case p; Simpl; Auto.
Intros Fnum1 Fexp1; Rewrite absolu_Zopp; Auto.
Qed.

Theorem FoddFop: (p:float) (Fodd p) ->(Fodd (Fopp p)).
Intros p; Unfold Fodd.
Case p; Simpl; Auto.
Intros Fnum1 Fexp1; Rewrite absolu_Zopp; Auto.
Qed.

Theorem FevenPred: (p:float) (Fodd p) ->(Feven (FPred b radix precision p)).
Intros p H'; Rewrite FPredFopFSucc; Auto with arith.
Apply FevenFop; Auto.
Apply FoddSuc; Auto.
Apply FoddFop; Auto with arith.
Qed.

Theorem FoddPred: (p:float) (Feven p) ->(Fodd (FPred b radix precision p)).
Intros p H'; Rewrite FPredFopFSucc; Auto with arith.
Apply FoddFop; Auto.
Apply FevenSuc; Auto.
Apply FevenFop; Auto.
Qed.

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).
Intros f1 f2 H' H'0 H'1 H'2; Red.
Rewrite FcanonicUnique with 3 := pGivesBound
                            p := (Fnormalize radix b precision f2)
                            q := (Fnormalize radix b precision f1);
Auto with float arith.
Repeat Rewrite FnormalizeCorrect; Auto.
Qed.

Theorem FNevenEq:
  (f1, f2:float)
  (Fbounded b f1) -> (Fbounded b f2) -> <R> f1==f2 -> (FNeven f1) ->(FNeven f2).
Intros f1 f2 H' H'0 H'1 H'2; Red.
Rewrite FcanonicUnique with 3 := pGivesBound
                            p := (Fnormalize radix b precision f2)
                            q := (Fnormalize radix b precision f1);
Auto with float arith.
Repeat Rewrite FnormalizeCorrect; Auto.
Qed.

Theorem FNevenFop: (p:float) (FNeven p) ->(FNeven (Fopp p)).
Intros p; Unfold FNeven.
Rewrite Fnormalize_Fopp; Auto.
Intros; Apply FevenFop; Auto.
Qed.

Theorem FNoddFop: (p:float) (FNodd p) ->(FNodd (Fopp p)).
Intros p; Unfold FNodd.
Rewrite Fnormalize_Fopp; Auto.
Intros; Apply FoddFop; Auto.
Qed.

Theorem FNoddSuc:
  (p:float) (Fbounded b p) -> (FNodd p) ->(FNeven (FNSucc b radix precision p)).
Unfold FNodd FNeven FNSucc.
Intros p H' H'0.
Rewrite FcanonicFormalizeEq; Auto with float arith.
Apply FoddSuc; Auto with float arith.
Qed.

Theorem FNevenSuc:
  (p:float) (Fbounded b p) -> (FNeven p) ->(FNodd (FNSucc b radix precision p)).
Unfold FNodd FNeven FNSucc.
Intros p H' H'0.
Rewrite FcanonicFormalizeEq; Auto with float arith.
Apply FevenSuc; Auto.
Qed.

Theorem FNevenPred:
  (p:float) (Fbounded b p) -> (FNodd p) ->(FNeven (FNPred b radix precision p)).
Unfold FNodd FNeven FNPred.
Intros p H' H'0.
Rewrite FcanonicFormalizeEq; Auto with float arith.
Apply FevenPred; Auto.
Qed.

Theorem FNoddPred:
  (p:float) (Fbounded b p) -> (FNeven p) ->(FNodd (FNPred b radix precision p)).
Unfold FNodd FNeven FNPred.
Intros p H' H'0.
Rewrite FcanonicFormalizeEq; Auto with float arith.
Apply FoddPred; Auto.
Qed.
End FOdd.
Hints Resolve
FevenO FoddSuc FevenSuc FevenFop FoddFop FevenPred FoddPred FNevenFop FNoddFop
FNoddSuc FNevenSuc FNevenPred FNoddPred :float.

14/12/100, 15:32