proposition: Theorem round_sign_any_correct : forall x m e l, inbetween_float beta m e (Rabs x) l -> (e = cexp beta fexp x \/ (l = loc_Exact /\ format x)) -> round beta fexp rnd x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m l)) e).
proof: Proof. Proof with auto with typeclass_instances. intros x m e l Hin [He|(Hl,Hf)]. rewrite He in Hin |- *. apply inbetween_float_round_sign with (2 := Hin). exact inbetween_int_valid. rewrite Hl in Hin. inversion_clear Hin. rewrite Hl. replace (choice (Rlt_bool x 0) m loc_Exact) with m. unfold Rabs in H. destruct (Rcase_abs x) as [Zx|Zx]. rewrite Rlt_bool_true with (1 := Zx). simpl. rewrite F2R_Zopp. rewrite <- H, Ropp_involutive. apply round_generic... rewrite Rlt_bool_false. simpl. rewrite <- H. now apply round_generic. now apply Rge_le. destruct (Rlt_bool_spec x 0) as [Zx|Zx]. apply Z.opp_inj. change (- m = cond_Zopp true (choice true m loc_Exact))%Z. rewrite <- (Zrnd_IZR rnd (-m)) at 1. assert (IZR (-m) < 0)%R. rewrite opp_IZR. apply Ropp_lt_gt_0_contravar. apply IZR_lt. apply gt_0_F2R with beta e. rewrite <- H. apply Rabs_pos_lt. now apply Rlt_not_eq. rewrite <- Rlt_bool_true with (1 := H0). apply inbetween_int_valid. constructor. rewrite Rabs_left with (1 := H0). rewrite opp_IZR. apply Ropp_involutive. change (m = cond_Zopp false (choice false m loc_Exact))%Z. rewrite <- (Zrnd_IZR rnd m) at 1. assert (0 <= IZR m)%R. apply IZR_le. apply ge_0_F2R with beta e. rewrite <- H. apply Rabs_pos. rewrite <- Rlt_bool_false with (1 := H0). apply inbetween_int_valid. constructor. now apply Rabs_pos_eq. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket