proposition: Theorem FSuccZleEq : forall p q : float, (p <= q)%R -> (q < FSucc p)%R -> (Fexp p <= Fexp q)%Z -> p = q :>R.
proof: Proof. intros p q H'. generalize (Z_eq_bool_correct (Fnum p) (pPred (vNum b))); case (Z_eq_bool (Fnum p) (pPred (vNum b))); intros H'0. rewrite FSuccSimpl1; simpl in |- *; auto with arith. intros H'1 H'2. replace p with (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q). unfold FtoRradix in |- *; rewrite FshiftCorrect; auto with real. cut (Fexp (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q) = Fexp p); [ intros Eq0 | idtac ]. apply floatEq; auto. apply sym_equal; apply Zeq_Zs; auto. apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith. rewrite FshiftCorrect; auto. replace (Z.succ (Fnum p)) with (Fnum (Fshift radix 1 (FSucc p))); auto. apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with arith. repeat rewrite FshiftCorrect; auto. rewrite FSuccSimpl1; simpl in |- *; auto with arith. unfold Fshift in |- *; simpl in |- *. rewrite FSuccSimpl1; simpl in |- *; auto with arith. rewrite inj_abs; auto with zarith. unfold Fshift in |- *; simpl in |- *. rewrite FSuccSimpl1; simpl in |- *; auto with arith. rewrite Z.mul_1_r. rewrite H'0. unfold pPred in |- *; rewrite <- Zsucc_pred. rewrite (PosNormMin radix) with (precision := precision); auto with zarith; apply Zmult_comm. unfold Fshift in |- *; simpl in |- *. rewrite inj_abs; auto with zarith. generalize (Z_eq_bool_correct (Fnum p) (- nNormMin radix precision)); case (Z_eq_bool (Fnum p) (- nNormMin radix precision)); intros H'1. generalize (Z_eq_bool_correct (Fexp p) (- dExp b)); case (Z_eq_bool (Fexp p) (- dExp b)); intros H'2. pattern p at 1 in |- *; replace p with (Float (Fnum p) (Fexp p)). rewrite H'1; rewrite H'2. rewrite FSuccSimpl3; auto with arith. intros H'3 H'4. replace p with (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q). unfold FtoRradix in |- *; rewrite FshiftCorrect; auto with real. cut (Fexp (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q) = Fexp p); [ intros Eq0 | idtac ]. apply floatEq; auto. apply sym_equal; apply Zeq_Zs; auto. apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith. rewrite FshiftCorrect; auto. replace (Z.succ (Fnum p)) with (Fnum (FSucc p)); auto. pattern p at 2 in |- *; replace p with (Float (Fnum p) (Fexp p)). rewrite H'1; rewrite H'2. rewrite FSuccSimpl3; auto with arith. rewrite <- H'2. apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with arith. rewrite FshiftCorrect; auto. rewrite H'2; auto. case p; simpl in |- *; auto. pattern p at 1 in |- *; replace p with (Float (Fnum p) (Fexp p)). rewrite H'1; rewrite H'2. rewrite FSuccSimpl3; auto with arith. case p; simpl in |- *; auto. unfold Fshift in |- *; simpl in |- *. rewrite inj_abs; auto with zarith. case p; simpl in |- *; auto. rewrite FSuccSimpl2; auto with arith. intros H'3 H'4. unfold FtoRradix in |- *; rewrite <- FshiftCorrect with (n := 1) (x := p); auto. replace (Fshift radix 1 p) with (Fshift radix (S (Z.abs_nat (Fexp q - Fexp p))) q). repeat rewrite FshiftCorrect; auto with real. cut (Fexp (Fshift radix (S (Z.abs_nat (Fexp q - Fexp p))) q) = Fexp (Fshift radix 1 p)); [ intros Eq0 | idtac ]. apply floatEq; auto. apply sym_equal; apply Zeq_Zs; auto. apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith. repeat rewrite FshiftCorrect; auto. replace (Z.succ (Fnum (Fshift radix 1 p))) with (Fnum (FSucc p)); auto. apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with arith. repeat rewrite FshiftCorrect; auto. rewrite FSuccSimpl2; auto with arith. rewrite FSuccSimpl2; auto with arith. rewrite FSuccSimpl2; auto with arith. unfold Fshift in |- *; simpl in |- *. rewrite Z.mul_1_r; auto. rewrite H'1; unfold pPred in |- *; rewrite (PosNormMin radix) with (precision := precision); lia. unfold Fshift in |- *; simpl in |- *. replace (Zpos (P_of_succ_nat (Z.abs_nat (Fexp q - Fexp p)))) with (Z.succ (Fexp q - Fexp p)). unfold Z.succ, Z.pred in |- *; ring. rewrite <- (inj_abs (Fexp q - Fexp p)); lia. rewrite FSuccSimpl4; auto. intros H'2 H'3. replace p with (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q). unfold FtoRradix in |- *; rewrite FshiftCorrect; auto with real. cut (Fexp (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q) = Fexp p); [ intros Eq0 | idtac ]. apply floatEq; auto. apply sym_equal; apply Zeq_Zs; auto. apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith. rewrite FshiftCorrect; auto. replace (Z.succ (Fnum p)) with (Fnum (FSucc p)); auto. rewrite FSuccSimpl4; auto. apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with arith. repeat rewrite FshiftCorrect; auto. rewrite FSuccSimpl4; auto. unfold Fshift in |- *; simpl in |- *. rewrite inj_abs; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz