proposition: Theorem ImplyClosestStrict: (Rabs(z-f) < (powerRZ radix e)/2)%R -> (forall g: float, Closest b radix z g -> (FtoRradix f=g)%R ).
proof: Proof. intros. case (Req_dec (FtoRradix f) (FtoRradix g));auto with real; intros M. cut (Closest b radix z f);[intros|apply ImplyClosest; auto with real]. cut ((FtoRradix g=2*z-f)%R -> False);[intros Y|idtac]. cut (Rabs (g - z) <= Rabs (f - z))%R;[intros Q1|idtac]. 2:elim H0; intros T1 T2; apply T2; auto. cut (Rabs (f - z) <= Rabs (g - z))%R;[intros Q2|idtac]. 2:elim H1; intros T1 T2; apply T2; auto; elim H0; auto. cut (Rabs (f - z) = Rabs (g - z))%R;[intros Q3; clear Q1 Q2|auto with real]. generalize Q3; unfold Rabs; case (Rcase_abs (f - z)%R);case (Rcase_abs (g - z)%R); intros. apply Rplus_eq_reg_l with (-z)%R; rewrite Rplus_comm;fold (Rminus f z); rewrite Rplus_comm;fold (Rminus g z). rewrite <- Ropp_involutive;rewrite <- (Ropp_involutive (f-z)%R);apply Ropp_eq_compat; auto with real. lapply Y;[intros V; contradict V; auto|idtac]. apply Rplus_eq_reg_l with (-z)%R; apply trans_eq with (g-z)%R; [ring|rewrite <- Q0; ring]. lapply Y;[intros V; contradict V; auto|idtac]. apply Rplus_eq_reg_l with (-z)%R; apply trans_eq with (g-z)%R; [ring|idtac]. rewrite <- (Ropp_involutive (g-z)%R); rewrite <- Q0; ring. apply Rplus_eq_reg_l with (-z)%R; apply trans_eq with (f-z)%R;[ring|apply trans_eq with (1:=Q0);ring]. intros T; contradict H;apply Rle_not_lt. replace (z-f)%R with ((g-f)/2)%R;[idtac|rewrite T; field; auto with real]. unfold Rdiv; rewrite Rabs_mult. rewrite (Rabs_right (/2)%R); [idtac|apply Rle_ge;auto with real]. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (Rabs (g - f))%R;[idtac|right;field; auto with real]. unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b p g; auto. rewrite <- Fminus_correct; auto. rewrite <- Fabs_correct; auto. apply Rle_trans with (FtoR radix (Float (S 0) (Fexp (((Fminus radix (Fnormalize radix b p g) f)))))). unfold FtoR; simpl. apply Rle_trans with (powerRZ radix e);[right; field; auto with real|idtac]. apply Rle_trans with (powerRZ radix (Z.min (Fexp (Fnormalize radix b p g)) (Fexp f)))%R;[idtac|right;ring]. apply Rle_powerRZ; auto with zarith real. apply IZR_le; lia. apply Zmin_Zle. replace e with (Fexp (Float (nNormMin radix p) e)); auto. apply Fcanonic_Rle_Zle with radix b p; auto with real zarith. apply FcanonicNnormMin; auto with zarith. apply FnormalizeCanonic; auto with zarith; elim H0; auto. apply Rle_trans with (powerRZ radix (e + p - 1))%R;[right|fold FtoRradix]. unfold nNormMin, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ. rewrite <- powerRZ_add; auto with real zarith. rewrite Rabs_right. replace (pred p+e)%Z with (e+p-1)%Z; auto with real zarith. rewrite inj_pred; unfold Z.pred; auto with zarith arith. apply Rle_ge; apply powerRZ_le, IZR_lt; lia. apply IZR_neq; lia. cut (powerRZ radix (e + p - 1) <= g)%R;[intros Y|idtac]. unfold FtoRradix;rewrite FnormalizeCorrect; auto with zarith. fold FtoRradix; rewrite Rabs_right; auto. apply Rle_ge; apply Rle_trans with (2:=Y); auto with real zarith. apply powerRZ_le, IZR_lt; lia. cut ((powerRZ radix (e + p - 1)= (Float (nNormMin radix p) e)))%R. intros U; rewrite U. case zGe; intros T'. generalize ClosestMonotone; unfold MonotoneP; intros. unfold FtoRradix; apply H with b (Float (nNormMin radix p) e) z; auto with zarith real. rewrite <- U; auto. unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b). apply ClosestRoundedModeP with p; auto. cut (Fcanonic radix b (Float (nNormMin radix p) e));[intros G; elim G; intros G'; elim G'; auto|idtac]. apply FcanonicNnormMin; auto with zarith. right; unfold FtoRradix; apply ClosestIdem with b; auto. cut (Fcanonic radix b (Float (nNormMin radix p) e));[intros G; elim G; intros G'; elim G'; auto|idtac]. apply FcanonicNnormMin; auto with zarith. fold FtoRradix; rewrite <- U; rewrite T'; auto. unfold nNormMin, FtoRradix, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ. rewrite <- powerRZ_add; auto with real zarith. replace (pred p+e)%Z with (e+p-1)%Z; try easy. lia. apply IZR_neq; lia. replace e with (Fexp (Float (nNormMin radix p) e)); auto. apply Fcanonic_Rle_Zle with radix b p; auto with real zarith. apply FcanonicNnormMin; auto with zarith. apply Rle_trans with (powerRZ radix (e + p - 1))%R;[right|fold FtoRradix]. unfold nNormMin, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ. rewrite <- powerRZ_add; auto with real zarith. rewrite Rabs_right. replace (pred p+e)%Z with (e+p-1)%Z; auto with real zarith. rewrite inj_pred; unfold Z.pred; auto with zarith arith. apply Rle_ge; apply powerRZ_le, IZR_lt; lia. apply IZR_neq; lia. rewrite Rabs_right; auto. apply Rle_ge; apply Rle_trans with (2:=fGe); auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply RleFexpFabs; auto with zarith. rewrite Fminus_correct; auto; rewrite FnormalizeCorrect; auto. fold FtoRradix; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz