proposition: Theorem FSucPred : forall x : float, Fcanonic radix b x -> FSucc b radix precision (FPred 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 Z.lt_neq; auto. rewrite <- (Z.opp_involutive (pPred (vNum b))); apply Zlt_Zopp. apply Z.lt_le_trans with (- 0)%Z. apply Zlt_Zopp; unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *. apply (vNumbMoreThanOne radix) with (precision := precision); auto. simpl in |- *; apply Zlt_le_weak; apply nNormPos; auto with zarith arith. 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. intros H' H'0 H'1 H'2; rewrite <- H'2; apply floatEq; simpl in |- *; auto; unfold Z.succ, Z.pred in |- *; ring. 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.pred (Fnum x)) (pPred (vNum b))); case (Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b))); simpl in |- *. intros H' H'0 H'1 H'2; absurd (nNormMin radix precision <= pPred (vNum b))%Z. rewrite <- H'; rewrite H'1; auto with zarith. apply Zle_Zpred, ZltNormMinVnum; easy. generalize (Z_eq_bool_correct (Z.pred (Fnum x)) (- nNormMin radix precision)); case (Z_eq_bool (Z.pred (Fnum x)) (- nNormMin radix precision)); simpl in |- *. intros H' H'0 H'1 H'2 H'3; absurd (Z.pred (nNormMin radix precision) = (- nNormMin radix precision)%Z); auto with zarith. intros H' H'0 H'1 H'2 H'3; apply floatEq; simpl in |- *; auto; unfold Z.pred, Z.succ in |- *; ring. 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; apply floatEq; simpl in |- *; auto; unfold Z.pred, Z.succ in |- *; ring. intros H'; case H'; auto. generalize (Z_eq_bool_correct (Z.pred (Fnum x)) (pPred (vNum b))); case (Z_eq_bool (Z.pred (Fnum x)) (pPred (vNum b))); simpl in |- *. intros H'; absurd (Fnum x <= pPred (vNum b))%Z; auto with zarith. apply Zle_Zabs_inv2; unfold pPred in |- *; apply Zle_Zpred, Fb0. generalize (Z_eq_bool_correct (Z.pred (Fnum x)) (- nNormMin radix precision)); case (Z_eq_bool (Z.pred (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; apply floatEq; simpl in |- *; auto; unfold Z.succ, Z.pred in |- *; ring. intros H' H'0 H'1 H'2 H'3; case H; intros C0. absurd (nNormMin radix precision <= Z.abs (Fnum x))%Z. replace (Fnum x) with (Z.succ (Z.pred (Fnum x))); [ idtac | unfold Z.succ, Z.pred in |- *; ring ]. rewrite H'0. rewrite <- Zopp_Zpred_Zs; rewrite Zabs_Zopp. rewrite Z.abs_eq; auto with zarith. apply Zle_Zpred; simpl in |- *; apply nNormPos; auto with zarith. apply pNormal_absolu_min with (b := b); auto. contradict H'; apply FsubnormalFexp with (1 := C0). 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