proposition: Theorem errorBoundedPlusLe : forall p q pq : float, Fbounded b p -> Fbounded b q -> (Fexp p <= Fexp q)%Z -> Closest b radix (p + q) pq -> exists error : float, error = Rabs (p + q - pq) :>R /\ Fbounded b error /\ Fexp error = Z.min (Fexp p) (Fexp q).
proof: Proof. intros p q pq H' H'0 H'1 H'2. cut (ex (fun m : Z => pq = Float m (Fexp (Fplus radix p q)) :>R)). 2: unfold FtoRradix in |- *; apply RoundedModeRep with (b := b) (precision := precision) (P := Closest b radix); auto. 2: apply ClosestRoundedModeP with (precision := precision); auto. 2: rewrite (Fplus_correct radix); auto with arith. intros H'3; elim H'3; intros m E; clear H'3. exists (Fabs (Fminus radix q (Fminus radix (Float m (Fexp (Fplus radix p q))) p))). cut (forall A B : Prop, A -> (A -> B) -> A /\ B); [ intros tmp; apply tmp; clear tmp | auto ]. unfold FtoRradix in |- *; rewrite Fabs_correct; auto with arith. cut (forall p q : R, p = q -> Rabs p = Rabs q); [ intros tmp; apply tmp; clear tmp | intros p' q' H; rewrite H; auto ]. unfold FtoRradix in |- *; repeat rewrite Fminus_correct; auto with arith. unfold FtoRradix in E; rewrite E; auto. ring. intros H'4. cut (Rabs (pq - (p + q)) <= Rabs (q - (p + q)))%R. 2: elim H'2; auto. replace (q - (p + q))%R with (- FtoRradix p)%R. 2: ring. rewrite Rabs_Ropp. unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with arith. rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr. unfold FtoRradix in H'4; rewrite <- H'4. simpl in |- *. rewrite Z.min_l; auto. generalize H'1 H'; case p; case q; unfold Fabs, Fminus, Fopp, Fplus in |- *; simpl in |- *; clear H'1 H'. intros Fnum1 Fexp1 Fnum2 Fexp2 H'5 H'6. repeat rewrite Zmin_n_n; auto. repeat rewrite (Z.min_r _ _ H'5); auto with zarith. replace (Z.abs_nat (Fexp2 - Fexp2)) with 0. rewrite Zpower_nat_O. rewrite 3!Zmult_1_r. unfold FtoRradix, FtoR in |- *; simpl in |- *. intros H'. repeat split; simpl in |- *. rewrite (fun x => Z.abs_eq (Z.abs x)); auto with zarith. apply Z.le_lt_trans with (Z.abs Fnum2); auto. apply le_IZR. apply (Rle_monotony_contra_exp radix) with (z := Fexp2); auto. case H'6; auto. case H'6; auto. replace (Fexp2 - Fexp2)%Z with 0%Z; simpl in |- *; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz