proposition: Lemma gatCorrect: exists v:float, (FtoRradix v=be1-r1)%R /\ (Fbounded bo v) /\ (Fexp v=Z.min (Fexp be1) (Fexp r1))%Z.
proof: Proof. unfold FtoRradix; apply Subexact with p u1 al1 al2; auto. apply Rle_trans with (Rabs u2). apply TwoSumProp with y al1; auto. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (Fulp bo radix p u1);[idtac|simpl; right; field; auto with real]. rewrite u2Def; unfold FtoRradix; apply ClosestUlp; auto with zarith. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (Fulp bo radix p al1);[idtac|simpl; right; field; auto with real]. fold FtoRradix; rewrite al2Def; unfold FtoRradix; apply ClosestUlp; auto with zarith. fold FtoRradix; replace (u1+al1+al2)%R with (a*x+y)%R; auto. rewrite al2Def; rewrite u2Def; ring. case (Rle_or_lt 0 (a*x+y))%R; intros I1. fold FtoRradix; split; intros I2. unfold FtoRradix; apply RleRoundedR0 with bo p (Closest bo radix) (u1+al1)%R; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply Rplus_le_reg_l with (-u1)%R. ring_simplify. unfold FtoRradix; rewrite <- Fopp_correct. apply RleBoundRoundl with bo p (Closest bo radix) (y + u2)%R; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply oppBounded; elim u1Def; auto. rewrite Fopp_correct; fold FtoRradix; apply Rplus_le_reg_l with (FtoRradix u1). ring_simplify (u1+-u1)%R; apply Rle_trans with (1:=I1). right; rewrite u2Def; ring. absurd (FtoRradix r1 =0)%R. assert (~ is_Fzero r1). apply FnormalNotZero with radix bo; auto. unfold is_Fzero in H. unfold FtoRradix, FtoR; apply prod_neq_R0; auto with real zarith. apply IZR_neq; auto. apply Rgt_not_eq; apply powerRZ_lt, IZR_lt; lia. assert (I3: (0<= r1)%R); auto with real. unfold FtoRradix; apply RleRoundedR0 with bo p (Closest bo radix) (a*x+y)%R; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. fold FtoRradix; split; intros I2. absurd (FtoRradix r1 =0)%R. assert (~ is_Fzero r1). apply FnormalNotZero with radix bo; auto. unfold is_Fzero in H. unfold FtoRradix, FtoR; apply prod_neq_R0; auto with real zarith. apply IZR_neq; auto. apply Rgt_not_eq; apply powerRZ_lt, IZR_lt; lia. assert (I3: (r1 <= 0)%R); auto with real. unfold FtoRradix; apply RleRoundedLessR0 with bo p (Closest bo radix) (a*x+y)%R; auto with zarith real. apply ClosestRoundedModeP with p; auto with zarith. unfold FtoRradix; apply RleRoundedLessR0 with bo p (Closest bo radix) (u1+al1)%R; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply Rplus_le_reg_l with (-u1)%R. ring_simplify. unfold FtoRradix; rewrite <- Fopp_correct. apply RleBoundRoundr with bo p (Closest bo radix) (y + u2)%R; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply oppBounded; elim u1Def; auto. rewrite Fopp_correct; fold FtoRradix; apply Rplus_le_reg_l with (FtoRradix u1). ring_simplify (u1+-u1)%R; apply Rle_trans with (a*x+y)%R; auto with real. right; rewrite u2Def; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz