proposition: Lemma Midpoint_aux_aux: (FtoRradix x1= f) \/ (exists v:float, (FtoRradix v=x2)%R /\ (Fexp x1 -2 <= Fexp v)%Z).
proof: Proof. case (Z.eq_dec (Fnum x1) (nNormMin radix p)); intros H1. case (Rle_or_lt 0 x2); intros G. assert (Rabs x2 <= powerRZ radix (Fexp x1)/2)%R. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (powerRZ radix (Fexp x1));[idtac|right; simpl; field; auto with real]. replace (FtoRradix x2) with ((x1+x2) -x1)%R;[idtac|ring]. apply Rle_trans with (Fulp bo radix p x1). unfold FtoRradix; apply ClosestUlp; auto with zarith. unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto. case H; clear H; intros H. assert (Rabs (x2 + y) < powerRZ radix (Fexp x1) / 2)%R. apply Rle_lt_trans with (Rabs x2+Rabs y)%R;[apply Rabs_triang|idtac]. apply Rplus_lt_reg_l with (-Rabs y)%R. ring_simplify (- Rabs y + (Rabs x2 + Rabs y))%R. elim Evenradix; intros n Hn. assert (powerRZ radix (Fexp x1) / 2 = Float n (Fexp x1 -1))%R. unfold FtoRradix, FtoR; simpl; unfold Zminus; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl. repeat (rewrite Hn;rewrite mult_IZR); simpl; field; auto with real zarith. apply IZR_neq; auto with zarith. apply Rle_lt_trans with (Rabs (Float n (Fexp x1 - 1)) - powerRZ radix (LSB radix x2))%R. apply LSB_Pred; auto. rewrite (Rabs_right (Float n (Fexp x1 - 1))); auto with real. rewrite <- H0; auto. apply Rle_ge; unfold FtoRradix; apply LeFnumZERO; simpl; auto with real zarith. apply Z.le_trans with (MSB radix x2). apply LSB_le_MSB; auto with zarith. contradict x2NonZero. unfold FtoRradix; apply is_Fzero_rep1; auto. apply Z.le_trans with (Fexp x1-1)%Z. 2: apply Z.le_trans with (Fexp ((Float n (Fexp x1 - 1)))); auto with zarith. 2: apply Fexp_le_LSB. assert (MSB radix x2 < Fexp x1)%Z; auto with zarith. apply Zlt_powerRZ with radix; auto with real. apply IZR_le; lia. apply Rle_lt_trans with (FtoR radix (Float (S 0) (MSB radix x2))); [right; unfold FtoR; simpl; ring|idtac]. apply Rle_lt_trans with (FtoR radix (Fabs x2)). apply MSB_le_abs; auto. contradict x2NonZero. unfold FtoRradix; apply is_Fzero_rep1; auto. rewrite Fabs_correct; auto; fold FtoRradix. apply Rlt_le_trans with (1:=H). unfold Rdiv; apply Rle_trans with ( (powerRZ radix (Fexp x1)*1))%R; auto with real zarith. apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (/1)%R; auto with real. rewrite (Rabs_right (Float n (Fexp x1 - 1))); auto with real. 2: apply Rle_ge; unfold FtoRradix; apply LeFnumZERO; simpl; auto with real zarith. rewrite <- H0; unfold Rminus; rewrite Rplus_comm. apply Rplus_lt_compat_r; apply Ropp_lt_contravar. unfold FtoRradix; rewrite <- Fabs_correct; auto. apply Rlt_le_trans with (FtoR radix (Float (S 0) (Z.succ (MSB radix y))))%R. apply abs_lt_MSB; auto. unfold FtoR; simpl; ring_simplify (1 * powerRZ radix (Z.succ (MSB radix y)))%R. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. assert (powerRZ radix (Fexp x1 + p - 1) <= x1)%R. apply Rle_trans with (((nNormMin radix p))*(powerRZ radix (Fexp x1)))%R. unfold nNormMin; rewrite Zpower_nat_Z_powerRZ. replace (Fexp x1 + p - 1)%Z with (Fexp x1 + pred p)%Z. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; right;ring. rewrite inj_pred; unfold Z.pred; auto with zarith. unfold FtoRradix, FtoR; apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply IZR_le; auto with zarith. left; unfold FtoRradix. apply ImplyClosestStrict with bo p (x1+x2+y)%R (Fexp x1); auto with zarith. elim x1Def; auto. left; auto. replace (x1+x2+y)%R with (x1+(x2+y))%R;[idtac|ring]. apply Rle_trans with ((powerRZ radix (Fexp x1 + p - 1) + 0))%R;[right; ring|idtac]. apply Rplus_le_compat; auto. apply Rplus_le_reg_l with (-y)%R. ring_simplify. apply Rle_trans with (Rabs (-y));[apply RRle_abs|rewrite Rabs_Ropp]. rewrite <- (Rabs_right x2); auto with real. case (Req_dec y 0); intros. rewrite H3; rewrite Rabs_R0; auto with real. apply Rabs_pos. case (Rle_or_lt (Rabs y) (Rabs x2)); auto. intros I; absurd (MSB radix y < LSB radix x2)%Z; auto. apply Zle_not_lt. apply Z.le_trans with (MSB radix x2). apply LSB_le_MSB; auto with zarith. contradict x2NonZero. unfold FtoRradix; apply is_Fzero_rep1; auto. apply MSB_monotone; auto with zarith real. contradict x2NonZero. unfold FtoRradix; apply is_Fzero_rep1; auto. contradict H3. unfold FtoRradix; apply is_Fzero_rep1; auto. repeat rewrite Fabs_correct; auto with real zarith. fold FtoRradix; replace (x1+x2+y-x1)%R with (x2+y)%R; auto with real; ring. right; elim Evenradix; intros n Hn. exists (Float n (Fexp x1-1)); split;[idtac|simpl; auto with zarith]. apply trans_eq with (Rabs x2);[rewrite H|idtac]. unfold FtoRradix, FtoR; simpl; unfold Zminus; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. simpl; ring_simplify (radix*1)%R; rewrite Hn; rewrite mult_IZR; simpl; field; auto with real zarith. apply IZR_neq; auto with zarith. rewrite Rabs_right; auto with real. assert (Rabs x2 <= powerRZ radix (Fexp x1-1)/2)%R. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (powerRZ radix (Fexp x1-1));[idtac|right; simpl; field; auto with real]. assert (FPred bo radix p x1 - (x1 + x2) = -(powerRZ radix (Fexp x1-1)-Rabs x2))%R. apply trans_eq with (-(Fminus radix x1 (FPred bo radix p x1) - Rabs x2))%R. rewrite (Rabs_left x2); auto with real. unfold FtoRradix; rewrite Fminus_correct; auto with zarith; ring. unfold FtoRradix; rewrite FPredDiff3; auto with zarith. unfold FtoR, Z.pred,Zminus; simpl;ring. apply Rplus_le_reg_l with (-(Rabs x2))%R. ring_simplify (- Rabs x2 + 2 * Rabs x2)%R. apply Rle_trans with (Rabs ((FPred bo radix p x1)-(x1+x2)))%R. pattern (FtoRradix x2) at 1; replace (FtoRradix x2) with (-(x1-(x1+x2)))%R;[rewrite Rabs_Ropp|ring]. elim x1Def; intros Y1 Y2; unfold FtoRradix; apply Y2; auto. apply FBoundedPred; auto with zarith. rewrite H; rewrite Rabs_Ropp. rewrite Rabs_right. right; ring. apply Rle_ge; apply Rplus_le_reg_l with (Rabs x2). ring_simplify. case (Rle_or_lt (Rabs x2) (powerRZ radix (Fexp x1 - 1))); auto; intros. absurd (Rabs x2 <= Rabs (FPred bo radix p x1 - (x1 + x2)))%R. rewrite H; rewrite Rabs_Ropp; apply Rlt_not_le. rewrite Rabs_left; auto with real. apply Rplus_lt_reg_r with (-Rabs x2+powerRZ radix (Fexp x1-1))%R. ring_simplify; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. pattern (FtoRradix x2) at 1; replace (FtoRradix x2) with (-(x1-(x1+x2)))%R;[rewrite Rabs_Ropp|ring]. elim x1Def; intros Y1 Y2; unfold FtoRradix; apply Y2; auto. apply FBoundedPred; auto with zarith. case H; clear H; intros H. assert (Rabs (x2 + y) < powerRZ radix (Fexp x1-1) / 2)%R. apply Rle_lt_trans with (Rabs x2+Rabs y)%R;[apply Rabs_triang|idtac]. apply Rplus_lt_reg_l with (-Rabs y)%R. ring_simplify (- Rabs y + (Rabs x2 + Rabs y))%R. elim Evenradix; intros n Hn. assert (powerRZ radix (Fexp x1-1) / 2 = Float n (Fexp x1 -2))%R. unfold FtoRradix, FtoR; simpl; unfold Zminus; repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl. repeat (rewrite Hn; rewrite mult_IZR);simpl; field; auto with real zarith. apply IZR_neq; auto with zarith. apply Rle_lt_trans with (Rabs (Float n (Fexp x1 - 2)) - powerRZ radix (LSB radix x2))%R. apply LSB_Pred; auto. rewrite (Rabs_right (Float n (Fexp x1 - 2))); auto with real. rewrite <- H0; auto. apply Rle_ge; unfold FtoRradix; apply LeFnumZERO; simpl; auto with real zarith. apply Z.le_trans with (MSB radix x2). apply LSB_le_MSB; auto with zarith. contradict x2NonZero. unfold FtoRradix; apply is_Fzero_rep1; auto. apply Z.le_trans with (Fexp x1-2)%Z. 2: apply Z.le_trans with (Fexp ((Float n (Fexp x1 - 2)))); auto with zarith. 2: apply Fexp_le_LSB. assert (MSB radix x2 < Fexp x1-1)%Z; auto with zarith. apply Zlt_powerRZ with radix; auto with real. apply IZR_le; lia. apply Rle_lt_trans with (FtoR radix (Float (S 0) (MSB radix x2))); [right; unfold FtoR; simpl; ring|idtac]. apply Rle_lt_trans with (FtoR radix (Fabs x2)). apply MSB_le_abs; auto. contradict x2NonZero. unfold FtoRradix; apply is_Fzero_rep1; auto. rewrite Fabs_correct; auto; fold FtoRradix. apply Rlt_le_trans with (1:=H). unfold Rdiv; apply Rle_trans with ( (powerRZ radix (Fexp x1-1)*1))%R; auto with real zarith. apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (/1)%R; auto with real. rewrite (Rabs_right (Float n (Fexp x1 - 2))); auto with real. 2: apply Rle_ge; unfold FtoRradix; apply LeFnumZERO; simpl; auto with real zarith. rewrite <- H0; unfold Rminus; rewrite Rplus_comm. apply Rplus_lt_compat_r; apply Ropp_lt_contravar. unfold FtoRradix; rewrite <- Fabs_correct; auto. apply Rlt_le_trans with (FtoR radix (Float (S 0) (Z.succ (MSB radix y))))%R. apply abs_lt_MSB; auto. unfold FtoR; simpl; ring_simplify (1 * powerRZ radix (Z.succ (MSB radix y)))%R. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. assert (powerRZ radix (Fexp x1 + p - 1) = x1)%R. unfold FtoRradix, FtoR; replace (Fexp x1+p-1)%Z with (Fexp x1+pred p)%Z. rewrite powerRZ_add; auto with real zarith. rewrite H1; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. apply IZR_neq; lia. rewrite inj_pred; auto with zarith; unfold Z.pred; ring. left; unfold FtoRradix. apply ImplyClosestStrict with bo p (x1+x2+y)%R (Fexp x1-1)%Z; auto with zarith. elim x1Def; auto. left; auto. replace (x1+x2+y)%R with (x1+(x2+y))%R;[idtac|ring]. apply Rle_trans with ((powerRZ radix (Fexp x1 + p - 1) + -((powerRZ radix (Fexp x1-1))/2)))%R. apply Rplus_le_reg_l with ((powerRZ radix (Fexp x1-1))/2)%R. ring_simplify. apply Rle_trans with (powerRZ radix (Fexp x1 - 1 + p - 1)+powerRZ radix (Fexp x1 - 1))%R. rewrite Rplus_comm; apply Rplus_le_compat_l. apply Rle_trans with (powerRZ radix (Fexp x1 - 1) *1)%R; [unfold Rdiv; apply Rmult_le_compat_l; auto with real zarith|right; ring]. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (/1)%R; auto with real. apply Rle_trans with (powerRZ radix ((Fexp x1 - 1 + p - 1)+1)). apply powerRZSumRle; auto with zarith. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. apply Rplus_le_compat; auto with real. apply Rle_trans with (-(-(x2+y)))%R;[apply Ropp_le_contravar|right; ring]. apply Rle_trans with (Rabs (-(x2+y)));[apply RRle_abs|rewrite Rabs_Ropp; auto with real]. fold FtoRradix; rewrite <- H2; apply Rle_powerRZ; auto with zarith real. apply IZR_le; lia. fold FtoRradix; replace (x1+x2+y-x1)%R with (x2+y)%R; auto with real; ring. right; elim Evenradix; intros n Hn. exists (Float (-n) (Fexp x1-2)); split;[idtac|simpl; auto with zarith]. apply trans_eq with (-(Rabs x2))%R;[rewrite H|idtac]. unfold FtoRradix, FtoR; simpl; unfold Zminus; rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith;rewrite Ropp_Ropp_IZR. simpl; ring_simplify (radix*1)%R; rewrite Hn; rewrite mult_IZR; simpl; field; auto with real. apply IZR_neq; auto with zarith. apply IZR_neq; auto with zarith. rewrite Rabs_left; auto with real. assert (Rabs x2 <= powerRZ radix (Fexp x1)/2)%R. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (powerRZ radix (Fexp x1));[idtac|right; simpl; field; auto with real]. replace (FtoRradix x2) with ((x1+x2) -x1)%R;[idtac|ring]. apply Rle_trans with (Fulp bo radix p x1). unfold FtoRradix; apply ClosestUlp; auto with zarith. unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto. case H; clear H; intros H. assert (Rabs (x2 + y) < powerRZ radix (Fexp x1) / 2)%R. apply Rle_lt_trans with (Rabs x2+Rabs y)%R;[apply Rabs_triang|idtac]. apply Rplus_lt_reg_l with (-Rabs y)%R. ring_simplify (- Rabs y + (Rabs x2 + Rabs y))%R. elim Evenradix; intros n Hn. assert (powerRZ radix (Fexp x1) / 2 = Float n (Fexp x1 -1))%R. unfold FtoRradix, FtoR; simpl; unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl. repeat (rewrite Hn; rewrite mult_IZR); simpl; field; auto with real zarith. apply IZR_neq; auto with zarith. apply IZR_neq; auto with zarith. apply Rle_lt_trans with (Rabs (Float n (Fexp x1 - 1)) - powerRZ radix (LSB radix x2))%R. apply LSB_Pred; auto. rewrite (Rabs_right (Float n (Fexp x1 - 1))); auto with real. rewrite <- H0; auto. apply Rle_ge; unfold FtoRradix; apply LeFnumZERO; simpl; auto with real zarith. apply Z.le_trans with (MSB radix x2). apply LSB_le_MSB; auto with zarith. contradict x2NonZero. unfold FtoRradix; apply is_Fzero_rep1; auto. apply Z.le_trans with (Fexp x1-1)%Z. 2: apply Z.le_trans with (Fexp ((Float n (Fexp x1 - 1)))); auto with zarith. 2: apply Fexp_le_LSB. assert (MSB radix x2 < Fexp x1)%Z; auto with zarith. apply Zlt_powerRZ with radix; auto with real. apply IZR_le; lia. apply Rle_lt_trans with (FtoR radix (Float (S 0) (MSB radix x2))); [right; unfold FtoR; simpl; ring|idtac]. apply Rle_lt_trans with (FtoR radix (Fabs x2)). apply MSB_le_abs; auto. contradict x2NonZero. unfold FtoRradix; apply is_Fzero_rep1; auto. rewrite Fabs_correct; auto; fold FtoRradix. apply Rlt_le_trans with (1:=H). unfold Rdiv; apply Rle_trans with ( (powerRZ radix (Fexp x1)*1))%R; auto with real zarith. apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (/1)%R; auto with real. rewrite (Rabs_right (Float n (Fexp x1 - 1))); auto with real. 2: apply Rle_ge; unfold FtoRradix; apply LeFnumZERO; simpl; auto with real zarith. rewrite <- H0; unfold Rminus; rewrite Rplus_comm. apply Rplus_lt_compat_r; apply Ropp_lt_contravar. unfold FtoRradix; rewrite <- Fabs_correct; auto. apply Rlt_le_trans with (FtoR radix (Float (S 0) (Z.succ (MSB radix y))))%R. apply abs_lt_MSB; auto. unfold FtoR; simpl; ring_simplify (1 * powerRZ radix (Z.succ (MSB radix y)))%R. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. assert (powerRZ radix (Fexp x1 + p - 1) +powerRZ radix (Fexp x1) <= x1)%R. apply Rle_trans with (((nNormMin radix p)+1)*(powerRZ radix (Fexp x1)))%R. unfold nNormMin; rewrite Zpower_nat_Z_powerRZ. replace (Fexp x1 + p - 1)%Z with (Fexp x1 + pred p)%Z. rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; right;ring. rewrite inj_pred; unfold Z.pred; auto with zarith. unfold FtoRradix, FtoR; apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. replace 1%R with (IZR 1); auto with zarith; rewrite <- plus_IZR. assert (nNormMin radix p + 1 <= Fnum x1)%Z; auto with real zarith. assert (nNormMin radix p <= Fnum x1)%Z; auto with real zarith. elim Nx1; intros. apply Zmult_le_reg_r with radix; auto with zarith. rewrite Zmult_comm; rewrite <- PosNormMin with radix bo p; auto with zarith. apply Z.le_trans with (1:=H3). rewrite Z.abs_eq; auto with zarith. apply Z.mul_nonneg_nonneg; auto with zarith. apply LeR0Fnum with radix; auto with real zarith. apply IZR_le; auto. left; unfold FtoRradix. apply ImplyClosestStrict with bo p (x1+x2+y)%R (Fexp x1); auto with zarith. elim x1Def; auto. left; auto. replace (x1+x2+y)%R with (x1+(x2+y))%R;[idtac|ring]. apply Rle_trans with ((powerRZ radix (Fexp x1 + p - 1) + powerRZ radix (Fexp x1)) +-powerRZ radix (Fexp x1))%R;[right; ring|idtac]. apply Rplus_le_compat; auto. rewrite <- (Ropp_involutive (x2+y)); apply Ropp_le_contravar. apply Rle_trans with (Rabs (-(x2+y))); [apply RRle_abs|rewrite Rabs_Ropp]. apply Rle_trans with (powerRZ radix (Fexp x1) / 2)%R; auto with real. apply Rle_trans with (powerRZ radix (Fexp x1) *1)%R; auto with real. unfold Rdiv; apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (/1)%R; auto with real. fold FtoRradix; apply Rle_trans with (2:=H2); auto with real zarith. apply Rle_trans with (powerRZ radix (Fexp x1 + p - 1)+0)%R; auto with real zarith. apply Rplus_le_compat_l. apply powerRZ_le, IZR_lt; lia. fold FtoRradix; replace (x1+x2+y-x1)%R with (x2+y)%R; auto with real; ring. right; elim Evenradix; intros n Hn. case (Rle_or_lt 0%R x2); intros. exists (Float n (Fexp x1-1)); split;[idtac|simpl; auto with zarith]. apply trans_eq with (Rabs x2);[rewrite H|idtac]. unfold FtoRradix, FtoR; simpl; unfold Zminus; rewrite powerRZ_add; auto with real zarith. simpl; ring_simplify (radix*1)%R; rewrite Hn; rewrite mult_IZR; simpl; field; auto with real zarith. apply IZR_neq; auto with zarith. apply IZR_neq; auto with zarith. rewrite Rabs_right; auto with real. exists (Float (-n) (Fexp x1-1)); split;[idtac|simpl; auto with zarith]. apply trans_eq with (-(Rabs x2))%R;[rewrite H|idtac]. unfold FtoRradix, FtoR; simpl; unfold Zminus; rewrite powerRZ_add; auto with real zarith. rewrite Ropp_Ropp_IZR; simpl; ring_simplify (radix*1)%R; rewrite Hn; rewrite mult_IZR; simpl; field; auto with real zarith. apply IZR_neq; auto with zarith. apply IZR_neq; auto with zarith. rewrite Rabs_left; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz