proposition: Lemma round_N_odd_pos : round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) = round beta fexp (Znearest choice) x.
proof: Proof. Proof with auto with typeclass_instances. set (o:=round beta fexpe Zrnd_odd x). case (generic_format_EM beta fexp x); intros Hx. replace o with x; trivial. unfold o; apply sym_eq, round_generic... now apply generic_format_fexpe_fexp. assert (K1:(F2R d <= o)%R). apply round_ge_generic... apply generic_format_fexpe_fexp, Hd. apply Hd. assert (K2:(o <= F2R u)%R). apply round_le_generic... apply generic_format_fexpe_fexp, Hu. apply Hu. assert (P:(x <> m -> o=m -> (forall P:Prop, P))). intros Y1 Y2. assert (H:(Rnd_odd_pt beta fexpe x o)). apply round_odd_pt... destruct H as (_,H); destruct H. absurd (x=m)%R; try trivial. now rewrite <- Y2, H. destruct H as (_,(k,(Hk1,(Hk2,Hk3)))). destruct Zm as (k',(Hk'1,(Hk'2,Hk'3))). absurd (true=false). discriminate. rewrite <- Hk3, <- Hk'3. apply f_equal, f_equal. apply canonical_unique with fexpe... now rewrite Hk'1, <- Y2. assert (generic_format beta fexp o -> (forall P:Prop, P)). intros Y. assert (H:(Rnd_odd_pt beta fexpe x o)). apply round_odd_pt... destruct H as (_,H); destruct H. absurd (generic_format beta fexp x); trivial. now rewrite <- H. destruct H as (_,(k,(Hk1,(Hk2,Hk3)))). destruct (exists_even_fexp_lt fexpe o) as (k',(Hk'1,(Hk'2,Hk'3))). eexists; split. apply sym_eq, Y. simpl; unfold cexp. apply Z.le_lt_trans with (1:=fexpe_fexp _). lia. absurd (true=false). discriminate. rewrite <- Hk3, <- Hk'3. apply f_equal, f_equal. apply canonical_unique with fexpe... now rewrite Hk'1, <- Hk1. case K1; clear K1; intros K1. 2: apply H; rewrite <- K1; apply Hd. case K2; clear K2; intros K2. 2: apply H; rewrite K2; apply Hu. case (Rle_or_lt x m); intros Y;[destruct Y|idtac]. apply trans_eq with (F2R d). apply round_N_eq_DN_pt with (F2R u)... apply DN_odd_d_aux; split; try left; assumption. apply UP_odd_d_aux; split; try left; assumption. assert (o <= (F2R d + F2R u) / 2)%R. apply round_le_generic... apply Fm. now left. destruct H1; trivial. apply P. now apply Rlt_not_eq. trivial. apply sym_eq, round_N_eq_DN_pt with (F2R u)... replace o with x. reflexivity. apply sym_eq, round_generic... rewrite H0; apply Fm. apply trans_eq with (F2R u). apply round_N_eq_UP_pt with (F2R d)... apply DN_odd_d_aux; split; try left; assumption. apply UP_odd_d_aux; split; try left; assumption. assert ((F2R d + F2R u) / 2 <= o)%R. apply round_ge_generic... apply Fm. now left. destruct H0; trivial. apply P. now apply Rgt_not_eq. rewrite <- H0; trivial. apply sym_eq, round_N_eq_UP_pt with (F2R d)... Qed.
imports: Coq(ZArith Reals Psatz) Core Operations