(****************************************************************************
                                                                             
          IEEE754  :  Fodd                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  ******************************************************************************)
Require Export Fmin.
Section FOdd.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.
 
Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.

Hypothesis radixMoreThanOne : (1 < radix)%Z.
 
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
(* We define the parity predicates*)
 
Definition Even (z : Z) : Prop := exists z1 : _, z = (2 * z1)%Z.
 
Definition Odd (z : Z) : Prop := exists z1 : _, z = (2 * z1 + 1)%Z.
 
Theorem OddSEven : forall n : Z, Odd n -> Even (Zsucc n).
(* Goal: forall (n : Z) (_ : Odd n), Even (Z.succ n) *)
intros n H'; case H'; intros m H'1; exists (Zsucc m).
(* Goal: @eq Z (Z.succ n) (Z.add (Z.mul (Zpos (xO xH)) m) (Zpos xH)) *)
rewrite H'1; unfold Zsucc in |- *; ring.
Qed.
 
Theorem EvenSOdd : forall n : Z, Even n -> Odd (Zsucc n).
(* Goal: forall (n : Z) (_ : Odd (Z.succ n)), Even n *)
intros n H'; case H'; intros m H'1; exists m.
(* Goal: @eq Z (Z.succ n) (Z.add (Z.mul (Zpos (xO xH)) m) (Zpos xH)) *)
rewrite H'1; unfold Zsucc in |- *; ring.
Qed.
Hint Resolve OddSEven EvenSOdd: zarith.
 
Theorem OddSEvenInv : forall n : Z, Odd (Zsucc n) -> Even n.
(* Goal: forall (n : Z) (_ : Odd (Z.succ n)), Even n *)
intros n H'; case H'; intros m H'1; exists m.
(* Goal: @eq Z n (Z.mul (Zpos (xO xH)) m) *)
apply Zsucc_inj; rewrite H'1; (unfold Zsucc in |- *; ring).
Qed.
 
Theorem EvenSOddInv : forall n : Z, Even (Zsucc n) -> Odd n.
(* Goal: forall (n : Z) (_ : Even (Z.succ n)), Odd n *)
intros n H'; case H'; intros m H'1; exists (Zpred m).
(* Goal: @eq Z n (Z.add (Z.mul (Zpos (xO xH)) (Z.pred m)) (Zpos xH)) *)
apply Zsucc_inj; rewrite H'1; (unfold Zsucc, Zpred in |- *; ring).
Qed.
 
Theorem EvenO : Even 0.
(* Goal: Odd (Zpos xH) *)
exists 0%Z; simpl in |- *; auto.
Qed.
Hint Resolve EvenO: zarith.
 
Theorem Odd1 : Odd 1.
(* Goal: Odd (Zpos xH) *)
exists 0%Z; simpl in |- *; auto.
Qed.
Hint Resolve Odd1: zarith.
 
Theorem OddOpp : forall z : Z, Odd z -> Odd (- z).
(* Goal: forall (z : Z) (_ : Odd z), Odd (Z.opp z) *)
intros z H; case H; intros z1 H1; exists (- Zsucc z1)%Z; rewrite H1.
(* Goal: @eq Z (Z.opp (Z.add (Z.mul (Zpos (xO xH)) z1) (Zpos xH))) (Z.add (Z.mul (Zpos (xO xH)) (Z.opp (Z.succ z1))) (Zpos xH)) *)
unfold Zsucc in |- *; ring.
Qed.
 
Theorem EvenOpp : forall z : Z, Even z -> Even (- z).
(* Goal: forall (z : Z) (_ : Even z), Even (Z.opp z) *)
intros z H; case H; intros z1 H1; exists (- z1)%Z; rewrite H1; ring.
Qed.
Hint Resolve OddOpp EvenOpp: zarith.
 
Theorem OddEvenDec : forall n : Z, {Odd n} + {Even n}.
(* Goal: forall n : Z, sumbool (Odd n) (Even n) *)
intros z; case z; simpl in |- *; auto with zarith.
(* Goal: forall p : positive, sumbool (Odd (Zpos p)) (Even (Zpos p)) *)
(* Goal: forall p : positive, sumbool (Odd (Zneg p)) (Even (Zneg p)) *)
intros p; case p; simpl in |- *; auto with zarith.
intros p1; left; exists (Zpos p1); rewrite Zplus_comm;
 simpl in |- *; auto.
(* Goal: forall p : positive, sumbool (Odd (Zpos (xO p))) (Even (Zpos (xO p))) *)
(* Goal: forall p : positive, sumbool (Odd (Zneg p)) (Even (Zneg p)) *)
intros p1; right; exists (Zpos p1); simpl in |- *; auto.
change
  (forall p : positive,
   {Odd (- Zpos p)} + {Even (- Zpos p)}) 
 in |- *.
(* Goal: forall p : positive, sumbool (Odd (Z.opp (Zpos p))) (Even (Z.opp (Zpos p))) *)
intros p; case p; auto with zarith.
intros p1; left; apply OddOpp; exists (Zpos p1);
 rewrite Zplus_comm; simpl in |- *; auto.
(* Goal: forall p : positive, sumbool (Odd (Z.opp (Zpos (xO p)))) (Even (Z.opp (Zpos (xO p)))) *)
intros p1; right; apply EvenOpp; exists (Zpos p1); simpl in |- *; auto.
Qed.
 
Theorem OddNEven : forall n : Z, Odd n -> ~ Even n.
(* Goal: forall (n : Z) (_ : Even n), not (Odd n) *)
intros n H1; red in |- *; intros H2; case H1; case H2; intros z1 Hz1 z2 Hz2.
(* Goal: False *)
absurd (n = n); auto.
pattern n at 1 in |- *; rewrite Hz1; rewrite Hz2;
 repeat rewrite (fun x => Zplus_comm x 1).
case z1; case z2; simpl in |- *;
 try (intros; red in |- *; intros; discriminate).
intros p p0; case p; simpl in |- *;
 try (intros; red in |- *; intros; discriminate).
Qed.
 
Theorem EvenNOdd : forall n : Z, Even n -> ~ Odd n.
(* Goal: forall (n : Z) (_ : Even n), not (Odd n) *)
intros n H1; red in |- *; intros H2; case H1; case H2; intros z1 Hz1 z2 Hz2.
(* Goal: False *)
absurd (n = n); auto.
pattern n at 1 in |- *; rewrite Hz1; rewrite Hz2;
 repeat rewrite (fun x => Zplus_comm x 1).
case z1; case z2; simpl in |- *;
 try (intros; red in |- *; intros; discriminate).
intros p p0; case p0; simpl in |- *;
 try (intros; red in |- *; intros; discriminate).
Qed.
Hint Resolve OddNEven EvenNOdd: zarith.
 
Theorem EvenPlus1 : forall n m : Z, Even n -> Even m -> Even (n + m).
(* Goal: forall (n m : Z) (_ : Even n) (_ : Odd m), Odd (Z.add n m) *)
intros n m H H0; case H; case H0; intros z1 Hz1 z2 Hz2.
(* Goal: Odd (Z.add n m) *)
exists (z2 + z1)%Z; try rewrite Hz1; try rewrite Hz2; ring.
Qed.
 
Theorem EvenPlus2 : forall n m : Z, Odd n -> Odd m -> Even (n + m).
(* Goal: forall (n m : Z) (_ : Even n) (_ : Odd m), Odd (Z.add n m) *)
intros n m H H0; case H; case H0; intros z1 Hz1 z2 Hz2.
(* Goal: Even (Z.add n m) *)
exists (z2 + z1 + 1)%Z; try rewrite Hz1; try rewrite Hz2; ring.
Qed.
 
Theorem OddPlus1 : forall n m : Z, Odd n -> Even m -> Odd (n + m).
(* Goal: forall (n m : Z) (_ : Even n) (_ : Odd m), Odd (Z.add n m) *)
intros n m H H0; case H; case H0; intros z1 Hz1 z2 Hz2.
(* Goal: Odd (Z.add n m) *)
exists (z2 + z1)%Z; try rewrite Hz1; try rewrite Hz2; ring.
Qed.
 
Theorem OddPlus2 : forall n m : Z, Even n -> Odd m -> Odd (n + m).
(* Goal: forall (n m : Z) (_ : Even n) (_ : Odd m), Odd (Z.add n m) *)
intros n m H H0; case H; case H0; intros z1 Hz1 z2 Hz2.
(* Goal: Odd (Z.add n m) *)
exists (z2 + z1)%Z; try rewrite Hz1; try rewrite Hz2; ring.
Qed.
Hint Resolve EvenPlus1 EvenPlus2 OddPlus1 OddPlus2: zarith.
 
Theorem EvenPlusInv1 :
 forall n m : Z, Even (n + m) -> Even n -> Even m.
(* Goal: forall (n m : Z) (_ : Even (Z.add n m)) (_ : Odd n), Odd m *)
intros n m H H0; replace m with (n + m + - n)%Z; auto with zarith.
Qed.
 
Theorem EvenPlusInv2 : forall n m : Z, Even (n + m) -> Odd n -> Odd m.
(* Goal: forall (n m : Z) (_ : Even (Z.add n m)) (_ : Odd n), Odd m *)
intros n m H H0; replace m with (n + m + - n)%Z; auto with zarith.
Qed.
 
Theorem OddPlusInv1 : forall n m : Z, Odd (n + m) -> Odd m -> Even n.
(* Goal: forall (n m : Z) (_ : Odd (Z.add n m)) (_ : Even m), Odd n *)
intros n m H H0; replace n with (n + m + - m)%Z; auto with zarith.
Qed.
 
Theorem OddPlusInv2 : forall n m : Z, Odd (n + m) -> Even m -> Odd n.
(* Goal: forall (n m : Z) (_ : Odd (Z.add n m)) (_ : Even m), Odd n *)
intros n m H H0; replace n with (n + m + - m)%Z; auto with zarith.
Qed.
 
Theorem EvenMult1 : forall n m : Z, Even n -> Even (n * m).
(* Goal: forall (n m : Z) (_ : Even n), Even (Z.mul n m) *)
intros n m H; case H; intros z1 Hz1; exists (z1 * m)%Z; rewrite Hz1; ring.
Qed.
 
Theorem EvenMult2 : forall n m : Z, Even m -> Even (n * m).
(* Goal: forall (n m : Z) (_ : Even m), Even (Z.mul n m) *)
intros n m H; case H; intros z1 Hz1; exists (z1 * n)%Z; rewrite Hz1; ring.
Qed.
Hint Resolve EvenMult1 EvenMult2: zarith.
 
Theorem OddMult : forall n m : Z, Odd n -> Odd m -> Odd (n * m).
intros n m H1 H2; case H1; case H2; intros z1 Hz1 z2 Hz2;
 exists (2 * z1 * z2 + z1 + z2)%Z; rewrite Hz1; rewrite Hz2; 
 ring.
Qed.
Hint Resolve OddMult: zarith.
 
Theorem EvenMultInv : forall n m : Z, Even (n * m) -> Odd n -> Even m.
(* Goal: forall (n m : Z) (_ : Even (Z.mul n m)) (_ : Odd n), Even m *)
intros n m H H0; case (OddEvenDec m); auto; intros Z1.
(* Goal: Odd n *)
Contradict H; auto with zarith.
Qed.
 
Theorem OddMultInv : forall n m : Z, Odd (n * m) -> Odd n.
(* Goal: forall (n m : Z) (_ : Odd (Z.mul n m)), Odd n *)
intros n m H; case (OddEvenDec n); auto; intros Z1.
(* Goal: Odd n *)
Contradict H; auto with zarith.
Qed.
 
Theorem EvenExp :
 forall (n : Z) (m : nat), Even n -> Even (Zpower_nat n (S m)).
(* Goal: forall (n : Z) (m : nat) (_ : Even n), Even (Zpower_nat n (S m)) *)
intros n m; elim m.
(* Goal: forall _ : Even n, Even (Zpower_nat n (S O)) *)
(* Goal: forall (n0 : nat) (_ : forall _ : Even n, Even (Zpower_nat n (S n0))) (_ : Even n), Even (Zpower_nat n (S (S n0))) *)
rewrite Zpower_nat_1; simpl in |- *; auto with zarith.
(* Goal: forall (n0 : nat) (_ : forall _ : Even n, Even (Zpower_nat n (S n0))) (_ : Even n), Even (Zpower_nat n (S (S n0))) *)
intros n0 H H0; replace (S (S n0)) with (1 + S n0); auto with arith.
rewrite Zpower_nat_is_exp; rewrite Zpower_nat_1; simpl in |- *;
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
 auto with zarith.
Qed.
 
Theorem OddExp :
 forall (n : Z) (m : nat), Odd n -> Odd (Zpower_nat n m).
(* Goal: forall (n : Z) (m : nat) (_ : Odd n), Odd (Zpower_nat n m) *)
intros n m; elim m; simpl in |- *. auto with zarith.
(* Goal: forall (n0 : nat) (_ : forall _ : Odd n, Odd (Zpower_nat n n0)) (_ : Odd n), Odd (Z.mul n (Zpower_nat n n0)) *)
intros n0 H H0; replace (S n0) with (1 + n0); auto with arith.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
auto with zarith.
Qed.
Hint Resolve OddExp EvenExp: zarith.
 
Definition Feven (p : float) := Even (Fnum p).
 
Definition Fodd (p : float) := Odd (Fnum p).
 
Theorem FevenO : forall p : float, is_Fzero p -> Feven p.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
intros p H'; red in |- *; rewrite H'; simpl in |- *; auto with zarith.
Qed.
 
Theorem FevenOrFodd : forall p : float, Feven p \/ Fodd p.
(* Goal: forall p : float, or (Feven p) (Fodd p) *)
intros p; case (OddEvenDec (Fnum p)); auto.
Qed.
 
Theorem FevenSucProp :
 forall p : float,
 (Fodd p -> Feven (FSucc b radix precision p)) /\
 (Feven p -> Fodd (FSucc b radix precision p)).
(* Goal: forall p : float, and (forall _ : Fodd p, Feven (FSucc b radix precision p)) (forall _ : Feven p, Fodd (FSucc b radix precision p)) *)
intros p; unfold FSucc, Fodd, Feven in |- *.
generalize (Z_eq_bool_correct (Fnum p) (pPred (vNum b)));
 case (Z_eq_bool (Fnum p) (pPred (vNum b))); intros H'1.
(* Goal: and (forall _ : Odd (Fnum p), Even (Fnum (Float (nNormMin radix precision) (Z.succ (Fexp p))))) (forall _ : Even (Fnum p), Odd (Fnum (Float (nNormMin radix precision) (Z.succ (Fexp p))))) *)
(* Goal: and (forall _ : Odd (Fnum p), Even (Fnum (if Z_eq_bool (Fnum p) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp p) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum p)) (Fexp p) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp p)) else Float (Z.succ (Fnum p)) (Fexp p)))) (forall _ : Even (Fnum p), Odd (Fnum (if Z_eq_bool (Fnum p) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp p) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum p)) (Fexp p) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp p)) else Float (Z.succ (Fnum p)) (Fexp p)))) *)
rewrite H'1; simpl in |- *; auto.
(* Goal: and (forall _ : Odd (pPred (vNum b)), Even (nNormMin radix precision)) (forall _ : Even (pPred (vNum b)), Odd (nNormMin radix precision)) *)
(* Goal: and (forall _ : Odd (Fnum p), Even (Fnum (if Z_eq_bool (Fnum p) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp p) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum p)) (Fexp p) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp p)) else Float (Z.succ (Fnum p)) (Fexp p)))) (forall _ : Even (Fnum p), Odd (Fnum (if Z_eq_bool (Fnum p) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp p) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum p)) (Fexp p) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp p)) else Float (Z.succ (Fnum p)) (Fexp p)))) *)
unfold pPred in |- *; rewrite pGivesBound; unfold nNormMin in |- *.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
case (OddEvenDec radix); auto with zarith.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
intros H'; split; intros H'0; auto with zarith.
(* Goal: Even (Zpower_nat radix (Init.Nat.pred precision)) *)
(* Goal: forall _ : Even radix, and (forall _ : Odd (Z.pred (Zpower_nat radix precision)), Even (Zpower_nat radix (Init.Nat.pred precision))) (forall _ : Even (Z.pred (Zpower_nat radix precision)), Odd (Zpower_nat radix (Init.Nat.pred precision))) *)
(* Goal: and (forall _ : Odd (Fnum p), Even (Fnum (if Z_eq_bool (Fnum p) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp p) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum p)) (Fexp p) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp p)) else Float (Z.succ (Fnum p)) (Fexp p)))) (forall _ : Even (Fnum p), Odd (Fnum (if Z_eq_bool (Fnum p) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp p) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum p)) (Fexp p) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp p)) else Float (Z.succ (Fnum p)) (Fexp p)))) *)
apply EvenMultInv with (n := radix); auto.
pattern radix at 1 in |- *; rewrite <- Zpower_nat_1;
 rewrite <- Zpower_nat_is_exp.
replace (1 + pred precision) with precision;
 [ idtac | inversion precisionGreaterThanOne; auto ].
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
rewrite (Zsucc_pred (Zpower_nat radix precision)); auto with zarith.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
intros H'; split; intros H'0; auto with zarith.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
replace (pred precision) with (S (pred (pred precision))); auto with zarith.
(* Goal: Odd (Zpower_nat radix (Init.Nat.pred precision)) *)
(* Goal: and (forall _ : Odd (Fnum p), Even (Fnum (if Z_eq_bool (Fnum p) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp p) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum p)) (Fexp p) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp p)) else Float (Z.succ (Fnum p)) (Fexp p)))) (forall _ : Even (Fnum p), Odd (Fnum (if Z_eq_bool (Fnum p) (Z.opp (nNormMin radix precision)) then if Z_eq_bool (Fexp p) (Z.opp (Z.of_N (dExp b))) then Float (Z.succ (Fnum p)) (Fexp p) else Float (Z.opp (pPred (vNum b))) (Z.pred (Fexp p)) else Float (Z.succ (Fnum p)) (Fexp p)))) *)
Contradict H'0; apply OddNEven.
replace (Zpred (Zpower_nat radix precision)) with
 (Zpower_nat radix precision + - (1))%Z;
 [ idtac | unfold Zpred in |- *; simpl in |- *; auto ].
replace precision with (S (pred precision));
 [ auto with zarith | inversion precisionGreaterThanOne; auto ].
generalize (Z_eq_bool_correct (Fnum p) (- nNormMin radix precision));
 case (Z_eq_bool (Fnum p) (- nNormMin radix precision)); 
 intros H'2.
generalize (Z_eq_bool_correct (Fexp p) (- dExp b));
 case (Z_eq_bool (Fexp p) (- dExp b)); intros H'3.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
simpl in |- *; auto with zarith.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
simpl in |- *; auto with zarith.
(* Goal: and (forall _ : Odd (Fnum p), Even (Z.opp (pPred (vNum b)))) (forall _ : Even (Fnum p), Odd (Z.opp (pPred (vNum b)))) *)
(* Goal: and (forall _ : Odd (Fnum p), Even (Fnum (Float (Z.succ (Fnum p)) (Fexp p)))) (forall _ : Even (Fnum p), Odd (Fnum (Float (Z.succ (Fnum p)) (Fexp p)))) *)
rewrite H'2; unfold pPred, nNormMin in |- *; rewrite pGivesBound.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
case (OddEvenDec radix); auto with zarith.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
intros H'; split; intros H'0; auto with zarith.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
apply EvenOpp; apply OddSEvenInv; rewrite <- Zsucc_pred; auto with zarith.
Contradict H'0; replace precision with (S (pred precision));
 [ auto with zarith | inversion precisionGreaterThanOne; auto ].
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
intros H'; split; intros H'0; auto with zarith.
Contradict H'0; replace (pred precision) with (S (pred (pred precision)));
 [ auto with zarith | auto with zarith ].
replace precision with (S (pred precision));
 [ auto with zarith | inversion precisionGreaterThanOne; auto ].
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
apply OddOpp; apply EvenSOddInv; rewrite <- Zsucc_pred; auto with zarith.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
simpl in |- *; auto with zarith.
Qed.
 
Theorem FoddSuc :
 forall p : float, Fodd p -> Feven (FSucc b radix precision p).
(* Goal: forall (p : float) (_ : Feven p), Fodd (FSucc b radix precision p) *)
intros p H'; case (FevenSucProp p); auto.
Qed.
 
Theorem FevenSuc :
 forall p : float, Feven p -> Fodd (FSucc b radix precision p).
(* Goal: forall (p : float) (_ : Feven p), Fodd (FSucc b radix precision p) *)
intros p H'; case (FevenSucProp p); auto.
Qed.
 
Theorem FevenFop : forall p : float, Feven p -> Feven (Fopp p).
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
intros p; unfold Feven, Fopp in |- *; simpl in |- *; auto with zarith.
Qed.
 
Theorem FoddFop : forall p : float, Fodd p -> Fodd (Fopp p).
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
intros p; unfold Fodd, Fopp in |- *; simpl in |- *; auto with zarith.
Qed.
 
Theorem FevenPred :
 forall p : float, Fodd p -> Feven (FPred b radix precision p).
(* Goal: forall (p : float) (_ : Feven p), Fodd (FPred b radix precision p) *)
intros p H'; rewrite FPredFopFSucc; auto with arith.
(* Goal: Feven (Fopp p) *)
apply FevenFop; auto.
(* Goal: Feven (FSucc b radix precision (Fopp p)) *)
apply FoddSuc; auto.
(* Goal: Fodd (Fopp p) *)
apply FoddFop; auto with arith.
Qed.
 
Theorem FoddPred :
 forall p : float, Feven p -> Fodd (FPred b radix precision p).
(* Goal: forall (p : float) (_ : Feven p), Fodd (FPred b radix precision p) *)
intros p H'; rewrite FPredFopFSucc; auto with arith.
(* Goal: Fodd (Fopp (FSucc b radix precision (Fopp p))) *)
apply FoddFop; auto.
(* Goal: Fodd (FSucc b radix precision (Fnormalize radix b precision p)) *)
apply FevenSuc; auto.
(* Goal: Feven (Fopp p) *)
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 :
 forall f1 f2 : float,
 Fbounded b f1 -> Fbounded b f2 -> f1 = f2 :>R -> FNodd f1 -> FNodd f2.
(* Goal: forall (f1 f2 : float) (_ : Fbounded b f1) (_ : Fbounded b f2) (_ : @eq R (FtoRradix f1) (FtoRradix f2)) (_ : FNeven f1), FNeven f2 *)
intros f1 f2 H' H'0 H'1 H'2; red in |- *.
rewrite
 FcanonicUnique
                with
                (3 := pGivesBound)
               (p := Fnormalize radix b precision f2)
               (q := Fnormalize radix b precision f1); 
 auto with float arith.
(* Goal: @eq R (FtoR radix (Fnormalize radix b precision f2)) (FtoR radix (Fnormalize radix b precision f1)) *)
repeat rewrite FnormalizeCorrect; auto.
Qed.
 
Theorem FNevenEq :
 forall f1 f2 : float,
 Fbounded b f1 -> Fbounded b f2 -> f1 = f2 :>R -> FNeven f1 -> FNeven f2.
(* Goal: forall (f1 f2 : float) (_ : Fbounded b f1) (_ : Fbounded b f2) (_ : @eq R (FtoRradix f1) (FtoRradix f2)) (_ : FNeven f1), FNeven f2 *)
intros f1 f2 H' H'0 H'1 H'2; red in |- *.
rewrite
 FcanonicUnique
                with
                (3 := pGivesBound)
               (p := Fnormalize radix b precision f2)
               (q := Fnormalize radix b precision f1); 
 auto with float arith.
(* Goal: @eq R (FtoR radix (Fnormalize radix b precision f2)) (FtoR radix (Fnormalize radix b precision f1)) *)
repeat rewrite FnormalizeCorrect; auto.
Qed.
 
Theorem FNevenFop : forall p : float, FNeven p -> FNeven (Fopp p).
(* Goal: forall (p : float) (_ : FNeven p), FNeven (Fopp p) *)
intros p; unfold FNeven in |- *.
(* Goal: forall _ : Fodd (Fnormalize radix b precision p), Fodd (Fnormalize radix b precision (Fopp p)) *)
rewrite Fnormalize_Fopp; auto with arith.
(* Goal: Feven (Fopp p) *)
intros; apply FevenFop; auto.
Qed.
 
Theorem FNoddFop : forall p : float, FNodd p -> FNodd (Fopp p).
(* Goal: forall (p : float) (_ : FNodd p), FNodd (Fopp p) *)
intros p; unfold FNodd in |- *.
(* Goal: forall _ : Fodd (Fnormalize radix b precision p), Fodd (Fnormalize radix b precision (Fopp p)) *)
rewrite Fnormalize_Fopp; auto with arith.
(* Goal: Fodd (Fopp (FSucc b radix precision (Fopp p))) *)
intros; apply FoddFop; auto.
Qed.
 
Theorem FNoddSuc :
 forall p : float,
 Fbounded b p -> FNodd p -> FNeven (FNSucc b radix precision p).
(* Goal: forall (p : float) (_ : Fbounded b p) (_ : FNeven p), FNodd (FNSucc b radix precision p) *)
unfold FNodd, FNeven, FNSucc in |- *.
(* Goal: forall (p : float) (_ : Fbounded b p) (_ : Feven (Fnormalize radix b precision p)), Fodd (Fnormalize radix b precision (FPred b radix precision (Fnormalize radix b precision p))) *)
intros p H' H'0.
(* Goal: Fodd (Fnormalize radix b precision (FPred b radix precision (Fnormalize radix b precision p))) *)
rewrite FcanonicFnormalizeEq; auto with float arith.
(* Goal: Feven (FSucc b radix precision (Fnormalize radix b precision p)) *)
apply FoddSuc; auto with float arith.
Qed.
 
Theorem FNevenSuc :
 forall p : float,
 Fbounded b p -> FNeven p -> FNodd (FNSucc b radix precision p).
(* Goal: forall (p : float) (_ : Fbounded b p) (_ : FNeven p), FNodd (FNSucc b radix precision p) *)
unfold FNodd, FNeven, FNSucc in |- *.
(* Goal: forall (p : float) (_ : Fbounded b p) (_ : Feven (Fnormalize radix b precision p)), Fodd (Fnormalize radix b precision (FPred b radix precision (Fnormalize radix b precision p))) *)
intros p H' H'0.
(* Goal: Fodd (Fnormalize radix b precision (FPred b radix precision (Fnormalize radix b precision p))) *)
rewrite FcanonicFnormalizeEq; auto with float arith.
(* Goal: Fodd (FSucc b radix precision (Fnormalize radix b precision p)) *)
apply FevenSuc; auto.
Qed.
 
Theorem FNevenPred :
 forall p : float,
 Fbounded b p -> FNodd p -> FNeven (FNPred b radix precision p).
(* Goal: forall (p : float) (_ : Fbounded b p) (_ : FNeven p), FNodd (FNPred b radix precision p) *)
unfold FNodd, FNeven, FNPred in |- *.
(* Goal: forall (p : float) (_ : Fbounded b p) (_ : Feven (Fnormalize radix b precision p)), Fodd (Fnormalize radix b precision (FPred b radix precision (Fnormalize radix b precision p))) *)
intros p H' H'0.
(* Goal: Fodd (Fnormalize radix b precision (FPred b radix precision (Fnormalize radix b precision p))) *)
rewrite FcanonicFnormalizeEq; auto with float arith.
(* Goal: Feven (FPred b radix precision (Fnormalize radix b precision p)) *)
apply FevenPred; auto.
Qed.
 
Theorem FNoddPred :
 forall p : float,
 Fbounded b p -> FNeven p -> FNodd (FNPred b radix precision p).
(* Goal: forall (p : float) (_ : Fbounded b p) (_ : FNeven p), FNodd (FNPred b radix precision p) *)
unfold FNodd, FNeven, FNPred in |- *.
(* Goal: forall (p : float) (_ : Fbounded b p) (_ : Feven (Fnormalize radix b precision p)), Fodd (Fnormalize radix b precision (FPred b radix precision (Fnormalize radix b precision p))) *)
intros p H' H'0.
(* Goal: Fodd (Fnormalize radix b precision (FPred b radix precision (Fnormalize radix b precision p))) *)
rewrite FcanonicFnormalizeEq; auto with float arith.
(* Goal: Fodd (FPred b radix precision (Fnormalize radix b precision p)) *)
apply FoddPred; auto.
Qed.
 
Theorem FNevenOrFNodd : forall p : float, FNeven p \/ FNodd p.
(* Goal: forall p : float, or (FNeven p) (FNodd p) *)
intros p; unfold FNeven, FNodd in |- *; apply FevenOrFodd.
Qed.
 
Theorem FnOddNEven : forall n : float, FNodd n -> ~ FNeven n.
(* Goal: forall (n : float) (_ : FNodd n), not (FNeven n) *)
intros n H'; unfold FNeven, Feven in |- *; apply OddNEven; auto.
Qed.
 
Theorem FEvenD :
 forall p : float,
 Fbounded b p ->
 Feven p -> exists q : float, Fbounded b q /\ p = (2%nat * q)%R :>R.
(* Goal: forall (p : float) (_ : Fbounded b p) (_ : Feven p), @ex float (fun q : float => and (Fbounded b q) (@eq R (FtoRradix p) (Rmult (INR (S (S O))) (FtoRradix q)))) *)
intros p H H0; case H0.
(* Goal: forall (x : Z) (_ : @eq Z (Fnum p) (Z.mul (Zpos (xO xH)) x)), @ex float (fun q : float => and (Fbounded b q) (@eq R (FtoRradix p) (Rmult (INR (S (S O))) (FtoRradix q)))) *)
intros z Hz; exists (Float z (Fexp p)); split; auto.
(* Goal: Fbounded b (Float z (Fexp p)) *)
(* Goal: @eq R (FtoRradix p) (Rmult (INR (S (S O))) (FtoRradix (Float z (Fexp p)))) *)
repeat split; simpl in |- *; auto with float.
(* Goal: Z.lt (Z.abs z) (Zpos (vNum b)) *)
(* Goal: @eq R (FtoRradix p) (Rmult (INR (S (S O))) (FtoRradix (Float z (Fexp p)))) *)
apply Zle_lt_trans with (Zabs (Fnum p)); auto with float zarith.
rewrite Hz; rewrite Zabs_Zmult;
 replace (Zabs 2 * Zabs z)%Z with (Zabs z + Zabs z)%Z; 
 auto with zarith arith.
pattern (Zabs z) at 1 in |- *; replace (Zabs z) with (0 + Zabs z)%Z;
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
 auto with zarith.
(* Goal: Odd (Z.mul n (Zpower_nat n n0)) *)
rewrite (Zabs_eq 2); auto with zarith.
(* Goal: @eq R (FtoRradix p) (Rmult (INR (S (S O))) (FtoRradix (Float z (Fexp p)))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (Rplus (IZR (Zpos xH)) (IZR (Zpos xH))) (Rmult (IZR z) (powerRZ (IZR radix) (Fexp p)))) *)
rewrite Hz; rewrite Rmult_IZR; simpl in |- *; ring.
Qed.
 
Theorem FNEvenD :
 forall p : float,
 Fbounded b p ->
 FNeven p -> exists q : float, Fbounded b q /\ p = (2%nat * q)%R :>R.
intros p H' H'0; case (FEvenD (Fnormalize radix b precision p));
 auto with float zarith arith.
(* Goal: forall (x : float) (_ : and (Fbounded b x) (@eq R (FtoRradix (Fnormalize radix b precision p)) (Rmult (INR (S (S O))) (FtoRradix x)))), @ex float (fun q : float => and (Fbounded b q) (@eq R (FtoRradix p) (Rmult (INR (S (S O))) (FtoRradix q)))) *)
intros x H'1; elim H'1; intros H'2 H'3; clear H'1; exists x; split; auto.
(* Goal: @eq R (FtoRradix p) (Rmult (INR (S (S O))) (FtoRradix x)) *)
apply sym_eq.
(* Goal: @eq R (Rmult (INR (S (S O))) (FtoRradix x)) (FtoRradix p) *)
rewrite <- H'3; auto.
(* Goal: @eq R (FtoRradix (Fnormalize radix b precision p)) (FtoRradix p) *)
unfold FtoRradix in |- *; apply FnormalizeCorrect; auto.
Qed.
End FOdd.
Hint Resolve FevenO FoddSuc FevenSuc FevenFop FoddFop FevenPred FoddPred
  FNevenFop FNoddFop FNoddSuc FNevenSuc FNevenPred FNoddPred: float.
