proposition: Theorem ClosestImplyEven: (EvenClosest b radix p z f) -> (exists g: float, (z=g+(powerRZ radix (Fexp g))/2)%R /\ (Fcanonic radix b g) /\ (0 <= Fnum g)%Z) -> (FNeven b radix p f).
proof: Proof. intros H T1; elim T1; intros g T2; elim T2; intros H0 T3; elim T3; intros H1 H2 ; clear T1 T2 T3. cut (Fbounded b g);[intros L|apply FcanonicBound with radix; auto with zarith]. cut (g <z)%R;[intros I1|idtac]. cut (z=FSucc b radix p g - powerRZ radix (Fexp g) / 2)%R;[intros H0'|idtac]. cut (z < FSucc b radix p g)%R;[intros I2|idtac]. cut (Closest b radix z g);[intros H4|idtac]. cut (Closest b radix z (FSucc b radix p g));[intros H5|idtac]. generalize EvenClosestMinOrMax; unfold MinOrMaxP; intros T. elim T with b radix p z f; auto; clear T; intros H6. elim H; intros H7 H8; case H8; auto; intros. absurd (FtoRradix f=FSucc b radix p g). cut (f < FSucc b radix p g)%R; auto with real. apply Rle_lt_trans with (2:=I2);elim H6; intros K1 K2; elim K2; auto with real. unfold FtoRradix; apply sym_eq; apply H3; auto. elim H; intros H7 H8; case H8; auto; intros. absurd (FtoRradix f=g). cut (g < f)%R; auto with real. apply Rlt_le_trans with (1:=I1);elim H6; intros K1 K2; elim K2; auto with real. unfold FtoRradix; apply sym_eq; apply H3; auto. apply ClosestSuccPred with p; auto with zarith. apply FBoundedSuc; auto with zarith. apply FSuccCanonic; auto with zarith. rewrite Rabs_left1. rewrite Rabs_left1. apply Ropp_le_contravar; unfold Rminus; apply Rplus_le_compat_l; apply Ropp_le_contravar. apply Rlt_le; apply FSuccLt; auto with zarith. apply Rplus_le_reg_l with (FtoR radix (FSucc b radix p (FSucc b radix p g))). ring_simplify. apply Rlt_le; apply Rlt_trans with (1:=I2). unfold FtoRradix; apply FSuccLt; auto with zarith. fold FtoRradix; apply Rle_trans with (z-z)%R; unfold Rminus;auto with real. rewrite FPredSuc; auto with zarith. fold FtoRradix; pattern z at 1 in |-*; rewrite H0'; rewrite H0. ring_simplify (FSucc b radix p g - powerRZ radix (Fexp g) / 2 - FSucc b radix p g)%R. ring_simplify (g + powerRZ radix (Fexp g) / 2 - g)%R. rewrite Rabs_Ropp; auto with real. apply ClosestSuccPred with p; auto with zarith. fold FtoRradix; pattern z at 1 in |-*; rewrite H0; rewrite H0'. ring_simplify (FSucc b radix p g - powerRZ radix (Fexp g) / 2 - FSucc b radix p g)%R; ring_simplify (g + powerRZ radix (Fexp g) / 2 - g)%R. rewrite Rabs_Ropp; auto with real. rewrite Rabs_right. rewrite Rabs_right. unfold Rminus; apply Rplus_le_compat_l; apply Ropp_le_contravar. apply Rlt_le; apply FPredLt; auto with zarith. apply Rle_ge; apply Rplus_le_reg_l with (FtoR radix (FPred b radix p g)). ring_simplify. apply Rlt_le; apply Rlt_trans with (2:=I1). unfold FtoRradix; apply FPredLt; auto with zarith. apply Rle_ge; fold FtoRradix; apply Rle_trans with (z-z)%R; unfold Rminus;auto with real. rewrite H0'; apply Rlt_le_trans with (FSucc b radix p g - 0)%R; auto with real. unfold Rminus; apply Rplus_lt_compat_l; apply Ropp_lt_contravar. unfold Rdiv; apply Rmult_lt_0_compat; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. rewrite H0. apply Rplus_eq_reg_l with (-g+ powerRZ radix (Fexp g) / 2)%R; ring_simplify. apply trans_eq with (powerRZ radix (Fexp g));[field; auto with real|idtac]. apply trans_eq with (FtoRradix (Float 1 (Fexp g)));[unfold FtoRradix, FtoR; simpl; ring|idtac]. unfold FtoRradix; rewrite <- FSuccDiff1 with b radix p g; auto with zarith. rewrite Fminus_correct; auto with real; ring. cut (- nNormMin radix p < Fnum g)%Z; auto with zarith. apply Z.lt_le_trans with 0%Z; auto with zarith; apply Zplus_lt_reg_l with (nNormMin radix p). ring_simplify. unfold nNormMin; auto with zarith. apply Zpower_nat_less; lia. rewrite H0; apply Rle_lt_trans with (g+0)%R; auto with real. apply Rplus_lt_compat_l; unfold Rdiv; apply Rmult_lt_0_compat; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz