proposition: Theorem ExactSum_Near : forall p q f : float, Fbounded b p -> Fbounded b q -> Fbounded b f -> Closest b radix (p + q) f -> Fexp p = (- dExp b)%Z -> (Rabs (p + q - f) < powerRZ radix (- dExp b))%R -> (p + q)%R = f.
proof: Proof. intros p q f Hp Hq Hf H H12 H1. case errorBoundedPlus with (b := b) (radix := radix) (precision := precision) (p := p) (q := q) (pq := f); auto with zarith. intros x0 H'; elim H'; intros H2 H'1; elim H'1; intros H3 H4; clear H' H'1. apply Rplus_eq_reg_l with (- FtoRradix f)%R; ring_simplify (-f+f)%R. apply trans_eq with (FtoR radix p + FtoR radix q - FtoR radix f)%R; [ fold FtoRradix; ring | rewrite <- H2 ]. generalize H1; unfold FtoRradix in |- *; rewrite <- H2; intros H5. cut (forall r : R, Rabs r = 0%R -> r = 0%R); [ intros V; apply V | auto with real ]. rewrite <- Fabs_correct; auto with zarith. apply is_Fzero_rep1; unfold is_Fzero in |- *. cut (forall z : Z, (0 <= z)%Z -> (z < 1)%Z -> z = 0%Z); [ intros W; apply W | auto with zarith ]. unfold Fabs in |- *; simpl in |- *; apply Z.abs_nonneg. replace 1%Z with (Fnum (Float 1 (- dExp b))); [ idtac | simpl in |- *; auto ]. apply Rlt_Fexp_eq_Zlt with (radix := radix); auto with zarith real. rewrite Fabs_correct; auto with zarith; apply Rlt_le_trans with (1 := H5). right; unfold FtoR in |- *; simpl in |- *; ring. unfold Fabs in |- *; simpl in |- *. rewrite H4; rewrite H12; apply Z.min_l; auto with zarith. elim Hq; auto with zarith. intros m; case (Rle_or_lt 0 m); intros H'. rewrite Rabs_right; auto with real. rewrite Rabs_left1; auto with real; intros H'1. rewrite <- (Ropp_involutive m); rewrite H'1; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz