proposition: Lemma LeExp3: (Fexp ph = Fexp uh+1)%Z -> (Fexp uh = Fexp z+1)%Z -> False.
proof: Proof. intros. absurd (powerRZ radix (p+Fexp z) <= Rabs z)%R. apply Rlt_not_le. unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; apply Rmult_lt_compat_r; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. elim Nz; intros A1 A2; elim A1; intros. apply Rlt_le_trans with (IZR (Zpos (vNum bo))); try apply IZR_lt; auto with zarith real. right; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real. apply Rle_trans with (FtoRradix (Float 1 (p+Fexp z))). right; unfold FtoRradix, FtoR; simpl; ring. unfold FtoRradix; apply RoundAbsMonotonel with bo p (Closest bo radix) (a*x+b)%R; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. elim Nz; intros A1 A2; elim A1; intros; split; simpl; auto with zarith. apply vNumbMoreThanOne with radix p; auto with zarith. apply Rle_trans with (powerRZ radix (p+Fexp z));[right; unfold FtoRradix, FtoR; simpl; ring|idtac]. replace (a*x+b)%R with (a*x-(-b))%R;[idtac|ring]. apply Rle_trans with (Rabs (a*x)-Rabs (-b))%R;[rewrite Rabs_Ropp|apply Rabs_triang_inv]. apply Rle_trans with ((powerRZ radix (p-1) -/(2*radix))*powerRZ radix (Fexp ph) -(powerRZ radix p-1)*powerRZ radix (Fexp b))%R. apply Rle_trans with ((powerRZ radix (p-1) -/(2*radix))*powerRZ radix (Fexp z+2) -(powerRZ radix p-1)*powerRZ radix (Fexp z))%R. apply Rle_trans with ((powerRZ radix (p + 1) - radix/ 2 ) * powerRZ radix (Fexp z) - (powerRZ radix p-1) * powerRZ radix (Fexp z))%R; [idtac|unfold Rminus; apply Rplus_le_compat_r]. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. apply Rle_trans with ((powerRZ radix (p + 1) - radix / 2-powerRZ radix p+1)* powerRZ radix (Fexp z))%R;[apply Rmult_le_compat_r; auto with real zarith|right; ring]. apply powerRZ_le, IZR_lt; lia. case (Zle_lt_or_eq 2 radix); auto with zarith; intros I. assert (3 <= radix)%Z; auto with zarith. assert (3 <= radix)%R; try apply IZR_le; auto with real zarith. apply Rplus_le_reg_l with (radix/2-1-powerRZ radix p)%R. ring_simplify. unfold Rminus; rewrite Rplus_comm. apply Rle_trans with (0+radix/2)%R; auto with real. apply Rle_trans with (0+radix*1)%R; unfold Rdiv; auto with real. apply Rplus_le_compat_l; apply Rmult_le_compat_l; try apply IZR_le; auto with real zarith. apply Rle_trans with (/1)%R; auto with real. apply Rle_trans with (powerRZ radix 1);[simpl; right; ring|idtac]. apply Rle_trans with (powerRZ radix p);auto with real zarith. apply Rle_powerRZ; try apply IZR_le; lia. apply Rle_trans with (- 2*powerRZ radix p + powerRZ radix p * (3))%R; [right; ring|auto with real]. rewrite powerRZ_add; auto with real zarith. apply Rplus_le_compat_l; apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. simpl; ring_simplify (radix*1)%R; auto with real. apply IZR_neq; lia. right; rewrite <- I; rewrite powerRZ_add; auto with real zarith; simpl. field; auto with real. unfold Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl. ring_simplify (radix*1)%R; right; field; auto with real. apply IZR_neq; lia. unfold Rminus; apply Rplus_le_compat. replace (Fexp ph) with (Fexp z+2)%Z; auto with real zarith. apply Ropp_le_contravar; apply Rmult_le_compat_l. assert (1 <= powerRZ radix p)%R; auto with real. apply Rle_trans with (powerRZ radix 0); auto with real zarith. apply Rle_powerRZ; try apply IZR_le; lia. apply Rplus_le_reg_l with 1%R. ring_simplify (1+0)%R; apply Rle_trans with (1:=H1); right; ring. apply Rle_powerRZ; try apply IZR_le; auto with real zarith. apply Z.le_trans with (Fexp uh -1)%Z; auto with zarith. case (Zle_or_lt (Fexp b) (Fexp uh-1)); auto with zarith; intros. absurd (FtoRradix ul=0); auto with real. elim errorBoundedPlus with bo radix p ph b uh; auto with zarith. 2: elim phDef; auto. fold FtoRradix; intros ul' T; elim T; intros H2 T'; elim T'; intros; clear T T'. rewrite ulDef; rewrite <- H2. absurd (Fexp uh < Fexp uh)%Z; auto with zarith. apply Z.le_lt_trans with (Fexp ul'); try lia. apply ClosestErrorExpStrict with bo radix p (ph+b)%R; auto with zarith. elim uhDef; auto. fold FtoRradix; rewrite H2; rewrite <- ulDef; auto with real. unfold Rminus; apply Rplus_le_compat. apply RleRoundedAbs; auto. assert (-dExp bo <= Fexp uh)%Z; auto with zarith. elim uhDef; intros I1 I2; elim I1; auto. apply Ropp_le_contravar; unfold FtoRradix; rewrite <- Fabs_correct; auto. unfold FtoR; simpl; apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. elim Fb; intros. apply Rle_trans with (Z.pred (Zpos (vNum bo))); try apply IZR_le; auto with real zarith. right; unfold Z.pred, Zminus; rewrite plus_IZR; rewrite pGivesBound; simpl. rewrite Zpower_nat_Z_powerRZ; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz