proposition: Theorem ClosestImplyEven_int: (Even radix)%Z -> (EvenClosest b radix p z f) -> (Fcanonic radix b f) -> (0 <= f)%R -> (z=(powerRZ radix (Fexp f))*(m+1/2))%R -> (exists n:Z, IZR n=m) -> (FNeven b radix p f).
proof: Proof. intros I; intros. elim H3; clear H3; intros n H4. cut (0 <= Fnum f)%Z; [intros|apply LeR0Fnum with radix; auto with real zarith]. case (Zle_lt_or_eq _ _ H3); intros Y1. case (Z.eq_dec (nNormMin radix p) (Fnum f)). intros H5; unfold FNeven; rewrite FcanonicFnormalizeEq; auto with zarith. unfold Feven; rewrite <- H5; unfold nNormMin. replace (pred p) with (S (pred (pred p))); auto with zarith. apply EvenExp; auto with zarith. intros; apply ClosestImplyEven; auto. exists (Float n (Fexp f)). split. rewrite H2; unfold FtoRradix, FtoR; simpl. rewrite H4; field; auto with real. cut (Fnum f -1 <= n)%Z;[intros I1|idtac]. cut (n <= Fnum f)%Z;[intros I2|idtac]. cut (0 <= n)%Z;[intros I3|idtac]. split;[idtac|simpl; auto]. case H0; intros. cut (nNormMin radix p < Fnum f)%Z;[intros K|idtac]. elim H5; intros; elim H6; intros. left; split;[split| idtac]; simpl; auto. apply Z.le_lt_trans with (2:=H8); repeat rewrite Z.abs_eq; auto with zarith. rewrite Z.abs_eq; auto with zarith. rewrite PosNormMin with radix b p; auto with zarith. cut (nNormMin radix p <= Fnum f)%Z; auto with zarith. elim H5; intros. rewrite Z.abs_eq in H7 by auto with zarith. apply Zmult_le_reg_r with radix; auto with zarith. rewrite Zmult_comm; rewrite <- PosNormMin with radix b p; lia. elim H5; intros T1 T2; elim T1; elim T2; clear T1 T2; intros. right; split; split; simpl; try lia. apply Z.le_lt_trans with (2:=H7); rewrite Z.abs_eq; auto with zarith. rewrite Z.abs_eq; auto with zarith. apply Z.le_trans with (2:=I1); apply Zplus_le_reg_l with 1%Z. ring_simplify; auto with zarith. apply le_IZR. rewrite H4; apply Rplus_le_reg_l with (1/2)%R. rewrite Rplus_comm; apply Rmult_le_reg_l with (powerRZ radix (Fexp f)); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. rewrite <- H2; apply Rplus_le_reg_l with (-f)%R. apply Rle_trans with (z-f)%R;[right;ring|idtac]. apply Rle_trans with (Rabs (z-f))%R;[apply RRle_abs|idtac]. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (powerRZ radix (Fexp f)). unfold FtoRradix; apply ClosestExp with b p; auto with zarith. elim H; auto. unfold FtoRradix, FtoR; simpl; right; field; auto with real. apply le_IZR. rewrite H4; apply Rplus_le_reg_l with (1/2)%R. rewrite (Rplus_comm (1/2)%R m); apply Rmult_le_reg_l with (powerRZ radix (Fexp f)); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. rewrite <- H2; apply Rplus_le_reg_l with (-z+(1/2)*(powerRZ radix (Fexp f)))%R. unfold Zminus; rewrite plus_IZR; simpl. apply Rle_trans with (-(z-f))%R;[right;unfold FtoRradix, FtoR; field; auto with real|idtac]. apply Rle_trans with (Rabs (-(z-f)))%R;[apply RRle_abs|idtac]. rewrite Rabs_Ropp; apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (powerRZ radix (Fexp f)). unfold FtoRradix; apply ClosestExp with b p; auto with zarith. elim H; auto. simpl; right; field; auto with real. unfold FNeven; rewrite FcanonicFnormalizeEq; auto with zarith. unfold Feven; rewrite <- Y1; unfold Even; exists 0%Z; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz