proposition: Theorem FPredSuc : forall x : float, Fcanonic radix b x -> FPred (FSucc b radix precision x) = x.
proof: Proof. intros x H; unfold FPred, FSucc in |- *. cut (Fbounded b x); [ intros Fb0 | apply FcanonicBound with (1 := H) ]. generalize (Z_eq_bool_correct (Fnum x) (pPred (vNum b))); case (Z_eq_bool (Fnum x) (pPred (vNum b))); simpl in |- *. generalize (Z_eq_bool_correct (nNormMin radix precision) (- pPred (vNum b))); case (Z_eq_bool (nNormMin radix precision) (- pPred (vNum b))); simpl in |- *. intros H'; contradict H'; apply sym_not_equal; apply Z.lt_neq; auto. apply Z.lt_le_trans with (- 0)%Z. apply Zlt_Zopp; unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *; apply vNumbMoreThanOne with (3 := pGivesBound); auto. simpl in |- *; apply Zlt_le_weak; apply nNormPos; auto. generalize (Z_eq_bool_correct (nNormMin radix precision) (nNormMin radix precision)); case (Z_eq_bool (nNormMin radix precision) (nNormMin radix precision)); simpl in |- *. generalize (Z_eq_bool_correct (Z.succ (Fexp x)) (- dExp b)); case (Z_eq_bool (Z.succ (Fexp x)) (- dExp b)); simpl in |- *. intros H' H'0 H'1 H'2; absurd (- dExp b <= Fexp x)%Z; try apply Fb0. rewrite <- H'; auto with zarith. replace (Z.pred (Z.succ (Fexp x))) with (Fexp x); [ idtac | unfold Z.succ, Z.pred in |- *; ring ]; auto. intros H' H'0 H'1 H'2; rewrite <- H'2; auto. apply floatEq; auto. intros H'; case H'; auto. generalize (Z_eq_bool_correct (Fnum x) (- nNormMin radix precision)); case (Z_eq_bool (Fnum x) (- nNormMin radix precision)); simpl in |- *. generalize (Z_eq_bool_correct (Fexp x) (- dExp b)); case (Z_eq_bool (Fexp x) (- dExp b)); simpl in |- *. generalize (Z_eq_bool_correct (Z.succ (Fnum x)) (- pPred (vNum b))); case (Z_eq_bool (Z.succ (Fnum x)) (- pPred (vNum b))); simpl in |- *. intros H0 H1 H2; absurd (Z.succ (Fnum x) <= Fnum x)%Z; auto with zarith. rewrite H0; rewrite H2; (apply Zle_Zopp; auto with zarith). unfold pPred in |- *; apply Zle_Zpred; apply ZltNormMinVnum; auto with zarith. generalize (Z_eq_bool_correct (Z.succ (Fnum x)) (nNormMin radix precision)); case (Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision)); simpl in |- *. intros H' H'0 H'1 H'2; contradict H'2. rewrite <- H'; auto with zarith. replace (Z.pred (Z.succ (Fnum x))) with (Fnum x); [ idtac | unfold Z.succ, Z.pred in |- *; ring ]; auto. intros H' H'0 H'1 H'2 H'3; apply floatEq; auto. generalize (Z_eq_bool_correct (- pPred (vNum b)) (- pPred (vNum b))); case (Z_eq_bool (- pPred (vNum b)) (- pPred (vNum b))); auto. intros H' H'0 H'1 H'2; rewrite <- H'1. replace (Z.succ (Z.pred (Fexp x))) with (Fexp x); [ idtac | unfold Z.succ, Z.pred in |- *; ring ]; auto. apply floatEq; auto. intros H'; case H'; auto. generalize (Z_eq_bool_correct (Z.succ (Fnum x)) (- pPred (vNum b))); case (Z_eq_bool (Z.succ (Fnum x)) (- pPred (vNum b))); simpl in |- *. intros H'; absurd (- pPred (vNum b) <= Fnum x)%Z; auto with zarith. apply Zle_Zabs_inv1; try apply Fb0. unfold pPred in |- *; apply Zle_Zpred; try apply Fb0. generalize (Z_eq_bool_correct (Z.succ (Fnum x)) (nNormMin radix precision)); case (Z_eq_bool (Z.succ (Fnum x)) (nNormMin radix precision)); simpl in |- *. generalize (Z_eq_bool_correct (Fexp x) (- dExp b)); case (Z_eq_bool (Fexp x) (- dExp b)); simpl in |- *. intros H' H'0 H'1 H'2 H'3. replace (Z.pred (Z.succ (Fnum x))) with (Fnum x); [ idtac | unfold Z.succ, Z.pred in |- *; ring ]; auto. apply floatEq; auto. intros H' H'0 H'1 H'2 H'3; case H. intros H'4; absurd (nNormMin radix precision <= Z.abs (Fnum x))%Z. replace (Fnum x) with (Z.pred (Z.succ (Fnum x))); [ idtac | unfold Z.succ, Z.pred in |- *; ring ]; auto. rewrite H'0. apply Zlt_not_le; rewrite Z.abs_eq; auto with zarith. apply Zle_Zpred; apply nNormPos; auto with zarith. apply pNormal_absolu_min with (b := b); auto. intros H'4; contradict H'; apply FsubnormalFexp with (1 := H'4). intros H' H'0 H'1 H'2; apply floatEq; simpl in |- *; auto. unfold Z.pred, Z.succ in |- *; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz