Library Float.Fodd

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.

Definition Even (z : Z) : Prop := z1 : _, z = (2 × z1)%Z.

Definition Odd (z : Z) : Prop := z1 : _, z = (2 × z1 + 1)%Z.

Theorem OddSEven : n : Z, Odd n Even (Z.succ n).
intros n H'; case H'; intros m H'1; (Z.succ m).
rewrite H'1; unfold Z.succ in |- *; ring.
Qed.

Theorem EvenSOdd : n : Z, Even n Odd (Z.succ n).
intros n H'; case H'; intros m H'1; m.
rewrite H'1; unfold Z.succ in |- *; ring.
Qed.
Hint Resolve OddSEven EvenSOdd: zarith.

Theorem OddSEvenInv : n : Z, Odd (Z.succ n) Even n.
intros n H'; case H'; intros m H'1; m.
apply Z.succ_inj; rewrite H'1; (unfold Z.succ in |- *; ring).
Qed.

Theorem EvenSOddInv : n : Z, Even (Z.succ n) Odd n.
intros n H'; case H'; intros m H'1; (Z.pred m).
apply Z.succ_inj; rewrite H'1; (unfold Z.succ, Z.pred in |- *; ring).
Qed.

Theorem EvenO : Even 0.
0%Z; simpl in |- *; auto.
Qed.
Hint Resolve EvenO: zarith.

Theorem Odd1 : Odd 1.
0%Z; simpl in |- *; auto.
Qed.
Hint Resolve Odd1: zarith.

Theorem OddOpp : z : Z, Odd z Odd (- z).
intros z H; case H; intros z1 H1; (- Z.succ z1)%Z; rewrite H1.
unfold Z.succ in |- *; ring.
Qed.

Theorem EvenOpp : z : Z, Even z Even (- z).
intros z H; case H; intros z1 H1; (- z1)%Z; rewrite H1; ring.
Qed.
Hint Resolve OddOpp EvenOpp: zarith.

Theorem OddEvenDec : n : Z, {Odd n} + {Even n}.
intros z; case z; simpl in |- *; auto with zarith.
intros p; case p; simpl in |- *; auto with zarith.
intros p1; left; (Zpos p1); rewrite Zplus_comm;
 simpl in |- *; auto.
intros p1; right; (Zpos p1); simpl in |- *; auto.
change
  ( p : positive,
   {Odd (- Zpos p)} + {Even (- Zpos p)})
 in |- ×.
intros p; case p; auto with zarith.
intros p1; left; apply OddOpp; (Zpos p1);
 rewrite Zplus_comm; simpl in |- *; auto.
intros p1; right; apply EvenOpp; (Zpos p1); simpl in |- *; auto.
Qed.

Theorem OddNEven : n : Z, Odd n ¬ Even n.
intros n H1; red in |- *; intros H2; case H1; case H2; intros z1 Hz1 z2 Hz2.
absurd (n = n); auto.
pattern n at 1 in |- *; rewrite Hz1; rewrite Hz2;
 repeat rewrite (fun xZplus_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 : n : Z, Even n ¬ Odd n.
intros n H1; red in |- *; intros H2; case H1; case H2; intros z1 Hz1 z2 Hz2.
absurd (n = n); auto.
pattern n at 1 in |- *; rewrite Hz1; rewrite Hz2;
 repeat rewrite (fun xZplus_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 : n m : Z, Even n Even m Even (n + m).
intros n m H H0; case H; case H0; intros z1 Hz1 z2 Hz2.
(z2 + z1)%Z; try rewrite Hz1; try rewrite Hz2; ring.
Qed.

Theorem EvenPlus2 : n m : Z, Odd n Odd m Even (n + m).
intros n m H H0; case H; case H0; intros z1 Hz1 z2 Hz2.
(z2 + z1 + 1)%Z; try rewrite Hz1; try rewrite Hz2; ring.
Qed.

Theorem OddPlus1 : n m : Z, Odd n Even m Odd (n + m).
intros n m H H0; case H; case H0; intros z1 Hz1 z2 Hz2.
(z2 + z1)%Z; try rewrite Hz1; try rewrite Hz2; ring.
Qed.

Theorem OddPlus2 : n m : Z, Even n Odd m Odd (n + m).
intros n m H H0; case H; case H0; intros z1 Hz1 z2 Hz2.
(z2 + z1)%Z; try rewrite Hz1; try rewrite Hz2; ring.
Qed.
Hint Resolve EvenPlus1 EvenPlus2 OddPlus1 OddPlus2: zarith.

Theorem EvenPlusInv1 :
  n m : Z, Even (n + m) Even n Even m.
intros n m H H0; replace m with (n + m + - n)%Z; auto with zarith.
Qed.

Theorem EvenPlusInv2 : n m : Z, Even (n + m) Odd n Odd m.
intros n m H H0; replace m with (n + m + - n)%Z; auto with zarith.
Qed.

Theorem OddPlusInv1 : n m : Z, Odd (n + m) Odd m Even n.
intros n m H H0; replace n with (n + m + - m)%Z; auto with zarith.
Qed.

Theorem OddPlusInv2 : n m : Z, Odd (n + m) Even m Odd n.
intros n m H H0; replace n with (n + m + - m)%Z; auto with zarith.
Qed.

Theorem EvenMult1 : n m : Z, Even n Even (n × m).
intros n m H; case H; intros z1 Hz1; (z1 × m)%Z; rewrite Hz1; ring.
Qed.

Theorem EvenMult2 : n m : Z, Even m Even (n × m).
intros n m H; case H; intros z1 Hz1; (z1 × n)%Z; rewrite Hz1; ring.
Qed.
Hint Resolve EvenMult1 EvenMult2: zarith.

Theorem OddMult : n m : Z, Odd n Odd m Odd (n × m).
intros n m H1 H2; case H1; case H2; intros z1 Hz1 z2 Hz2;
  (2 × z1 × z2 + z1 + z2)%Z; rewrite Hz1; rewrite Hz2;
 ring.
Qed.
Hint Resolve OddMult: zarith.

Theorem EvenMultInv : n m : Z, Even (n × m) Odd n Even m.
intros n m H H0; case (OddEvenDec m); auto; intros Z1.
Contradict H; auto with zarith.
Qed.

Theorem OddMultInv : n m : Z, Odd (n × m) Odd n.
intros n m H; case (OddEvenDec n); auto; intros Z1.
Contradict H; auto with zarith.
Qed.

Theorem EvenExp :
  (n : Z) (m : nat), Even n Even (Zpower_nat n (S m)).
intros n m; elim m.
rewrite Zpower_nat_1; simpl in |- *; auto with zarith.
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 |- *;
 auto with zarith.
Qed.

Theorem OddExp :
  (n : Z) (m : nat), Odd n Odd (Zpower_nat n m).
intros n m; elim m; simpl in |- ×. auto with zarith.
intros n0 H H0; replace (S n0) with (1 + n0); auto with arith.
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 : p : float, is_Fzero p Feven p.
intros p H'; red in |- *; rewrite H'; simpl in |- *; auto with zarith.
Qed.

Theorem FevenOrFodd : p : float, Feven p Fodd p.
intros p; case (OddEvenDec (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 in |- ×.
generalize (Z_eq_bool_correct (Fnum p) (pPred (vNum b)));
 case (Z_eq_bool (Fnum p) (pPred (vNum b))); intros H'1.
rewrite H'1; simpl in |- *; auto.
unfold pPred in |- *; rewrite pGivesBound; unfold nNormMin in |- ×.
case (OddEvenDec radix); auto with zarith.
intros H'; split; intros H'0; auto with zarith.
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 ].
rewrite (Zsucc_pred (Zpower_nat radix precision)); auto with zarith.
intros H'; split; intros H'0; auto with zarith.
replace (pred precision) with (S (pred (pred precision))); auto with zarith.
Contradict H'0; apply OddNEven.
replace (Z.pred (Zpower_nat radix precision)) with
 (Zpower_nat radix precision + - (1))%Z;
 [ idtac | unfold Z.pred 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.
simpl in |- *; auto with zarith.
simpl in |- *; auto with zarith.
rewrite H'2; unfold pPred, nNormMin in |- *; rewrite pGivesBound.
case (OddEvenDec radix); auto with zarith.
intros H'; split; intros H'0; auto with zarith.
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 ].
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 ].
apply OddOpp; apply EvenSOddInv; rewrite <- Zsucc_pred; auto with zarith.
simpl in |- *; auto with zarith.
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, Fopp in |- *; simpl in |- *; auto with zarith.
Qed.

Theorem FoddFop : p : float, Fodd p Fodd (Fopp p).
intros p; unfold Fodd, Fopp in |- *; simpl in |- *; auto with zarith.
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 f1 = f2 :>R FNodd f1 FNodd 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.
repeat rewrite FnormalizeCorrect; auto.
Qed.

Theorem FNevenEq :
  f1 f2 : float,
 Fbounded b f1 Fbounded b f2 f1 = f2 :>R 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.
repeat rewrite FnormalizeCorrect; auto.
Qed.

Theorem FNevenFop : p : float, FNeven p FNeven (Fopp p).
intros p; unfold FNeven in |- ×.
rewrite Fnormalize_Fopp; auto with arith.
intros; apply FevenFop; auto.
Qed.

Theorem FNoddFop : p : float, FNodd p FNodd (Fopp p).
intros p; unfold FNodd in |- ×.
rewrite Fnormalize_Fopp; auto with arith.
intros; apply FoddFop; auto.
Qed.

Theorem FNoddSuc :
  p : float,
 Fbounded b p FNodd p FNeven (FNSucc b radix precision p).
unfold FNodd, FNeven, FNSucc in |- ×.
intros p H' H'0.
rewrite FcanonicFnormalizeEq; 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 in |- ×.
intros p H' H'0.
rewrite FcanonicFnormalizeEq; 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 in |- ×.
intros p H' H'0.
rewrite FcanonicFnormalizeEq; 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 in |- ×.
intros p H' H'0.
rewrite FcanonicFnormalizeEq; auto with float arith.
apply FoddPred; auto.
Qed.

Theorem FNevenOrFNodd : p : float, FNeven p FNodd p.
intros p; unfold FNeven, FNodd in |- *; apply FevenOrFodd.
Qed.

Theorem FnOddNEven : n : float, FNodd n ¬ FNeven n.
intros n H'; unfold FNeven, Feven in |- *; apply OddNEven; auto.
Qed.

Theorem FEvenD :
  p : float,
 Fbounded b p
 Feven p q : float, Fbounded b q p = (2%nat × q)%R :>R.
intros p H H0; case H0.
intros z Hz; (Float z (Fexp p)); split; auto.
repeat split; simpl in |- *; auto with float.
apply Z.le_lt_trans with (Z.abs (Fnum p)); auto with float zarith.
rewrite Hz; rewrite Zabs_Zmult;
 replace (Z.abs 2 × Z.abs z)%Z with (Z.abs z + Z.abs z)%Z;
 auto with zarith arith.
pattern (Z.abs z) at 1 in |- *; replace (Z.abs z) with (0 + Z.abs z)%Z;
 auto with zarith.
rewrite (Z.abs_eq 2); auto with zarith.
unfold FtoRradix, FtoR in |- *; simpl in |- ×.
rewrite Hz; rewrite Rmult_IZR; simpl in |- *; ring.
Qed.

Theorem FNEvenD :
  p : float,
 Fbounded b p
 FNeven p 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.
intros x H'1; elim H'1; intros H'2 H'3; clear H'1; x; split; auto.
apply sym_eq.
rewrite <- H'3; auto.
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.