proposition: Lemma gaCorrect: exists v:float, (FtoRradix v=be1-r1+be2)%R /\ (Fbounded bo v).
proof: Proof. elim gatCorrect with bo radix p a x y r1 u1 u2 al1 al2 be1; auto. intros v T; elim T; intros H1 T'; elim T'; intros H2 H3; clear T T'. case (Req_dec al2 0); intros Z1. exists be2; split; auto. cut (FtoRradix be1=r1)%R. intros T; rewrite T; ring. apply P2 with (u1+al1)%R (a*x+y)%R; auto. apply trans_eq with (u1+al1+al2)%R;[rewrite Z1; ring|rewrite al2Def; rewrite u2Def; ring]. case (Req_dec u2 0); intros Z2. contradict Z1. rewrite al2Def; rewrite Z2. cut (FtoRradix y=al1);[intros I; rewrite I; ring|idtac]. apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. replace (FtoR radix y) with (y+u2)%R; auto with real. rewrite Z2; unfold FtoRradix; ring. elim Midpoint_aux with bo radix p be1 be2 al2 r1; auto with zarith. 3: fold FtoRradix; replace (be1+be2)%R with (u1+al1)%R; auto. 3: rewrite be2Def; ring. 3: fold FtoRradix; replace (be1+be2+al2)%R with (a*x+y)%R; auto. 3: rewrite al2Def; rewrite u2Def; rewrite be2Def; ring. 3: apply be2MuchSmaller; auto. fold FtoRradix; intros; exists be2; split; auto. rewrite H; ring. intros T'; elim T'; intros v' T; elim T; intros; clear T T'. elim BoundedL with bo radix p (be1 - r1 + be2)%R (Fplus radix v v') (Fexp be1 - 2)%Z; auto with zarith. intros v'' T; elim T; intros H4 T'; elim T'; intros; clear T T'. exists v''; split; auto. simpl; apply Zmin_Zle; auto. rewrite H3; apply Zmin_Zle; auto with zarith. generalize Expbe1; auto with zarith. auto with zarith. unfold FtoRradix; rewrite Fplus_correct; auto; rewrite H; rewrite H1; ring. replace (be1-r1+be2)%R with (((a*x+y)-r1)+-al2)%R. 2: rewrite al2Def; rewrite u2Def; rewrite be2Def; ring. apply Rle_lt_trans with (Rabs (a * x + y - r1) + Rabs(- al2))%R; [apply Rabs_triang|rewrite Rabs_Ropp]. apply Rle_lt_trans with ((powerRZ radix (Fexp be1+1))/2+(powerRZ radix (Fexp be1))/2)%R; [apply Rplus_le_compat|idtac]. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (Fulp bo radix p r1). unfold FtoRradix; apply ClosestUlp; auto with zarith. unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith;[idtac|left; auto]. apply Rle_trans with (powerRZ radix (Fexp be1 + 1)); [apply Rle_powerRZ; try apply IZR_le; auto with real zarith|right; simpl; field; auto with real]. apply Expr1. apply Rle_trans with (Rabs be2). assert (MSB radix al2 < LSB radix be2)%Z. apply be2MuchSmaller; auto. unfold FtoRradix; repeat rewrite <- Fabs_correct; auto. apply Rle_trans with (FtoR radix (Float (S 0) (Z.succ (MSB radix al2))))%R. apply Rlt_le; apply abs_lt_MSB; auto. apply Rle_trans with (FtoR radix (Float (S 0) (LSB radix be2))). unfold FtoR; simpl; apply Rmult_le_compat_l; auto with real. apply Rle_powerRZ; try apply IZR_le; auto with real zarith. apply LSB_le_abs; auto. contradict Be2NonZero; unfold FtoRradix; apply is_Fzero_rep1; auto. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (Fulp bo radix p be1). rewrite be2Def; unfold FtoRradix; apply ClosestUlp; auto with zarith. unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith;[idtac|left; auto]. right; simpl; field; auto with real. apply Rlt_le_trans with (powerRZ radix (Fexp be1 + 1)); [idtac|apply Rle_powerRZ; auto with real zarith]. apply Rlt_le_trans with (powerRZ radix (Fexp be1 + 1) / 2 + powerRZ radix (Fexp be1+1) / 2)%R; [apply Rplus_lt_compat_l|right; field; auto with real]. unfold Rdiv; apply Rmult_lt_compat_r; auto with real. apply Rlt_powerRZ; try apply IZR_lt; auto with real zarith. apply IZR_le; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz