proposition: Theorem FevenSucProp : forall p : float, (Fodd p -> Feven (FSucc b radix precision p)) /\ (Feven p -> Fodd (FSucc b radix precision p)).
proof: Proof. 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. now apply OddSEven. now apply OddExp. intros H'; split; intros H'0; auto with zarith. replace (pred precision) with (S (pred (pred precision))); auto with zarith. now apply EvenExp. 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 ]. apply OddPlus2. now apply EvenExp. apply OddOpp, Odd1. 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 |- *; split. apply OddSEven. apply EvenSOdd. 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. apply OddExp; easy. contradict H'0; replace precision with (S (pred precision)); [ auto with zarith | inversion precisionGreaterThanOne; auto ]. now apply OddNEven, OddOpp, OddExp. 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 ]. now apply EvenNOdd, EvenOpp, EvenExp. replace precision with (S (pred precision)); [ auto with zarith | inversion precisionGreaterThanOne; auto ]. apply OddOpp; apply EvenSOddInv; rewrite <- Zsucc_pred; auto with zarith. apply EvenExp; easy. simpl in |- *; split. apply OddSEven. apply EvenSOdd. Qed.
imports: Reals ZArith List PeanoNat Psatz