proposition: Theorem plusExactExp : forall p q pq : float, Fbounded b p -> Fbounded b q -> Closest b radix (p + q) pq -> ex (fun r : float => ex (fun s : float => Fbounded b r /\ Fbounded b s /\ s = pq :>R /\ r = (p + q - s)%R :>R /\ Fexp r = Z.min (Fexp p) (Fexp q) :>Z /\ (Fexp r <= Fexp s)%Z /\ (Fexp s <= Z.succ (Zmax (Fexp p) (Fexp q)))%Z)).
proof: Proof. intros p q pq H H0 H1. case (plusExpBound b radix precision) with (P := Closest b radix) (5 := H1); auto with zarith. apply (ClosestRoundedModeP b radix precision); auto with zarith. intros r (H2, (H3, (H4, H5))); fold FtoRradix in H3. case (Req_dec (p + q - pq) 0); intros Hr. cut (Fbounded b (Fzero (Z.min (Fexp p) (Fexp q)))); [ intros Fbs | idtac ]. exists (Fzero (Z.min (Fexp p) (Fexp q))); exists r; repeat (split; auto). rewrite (FzeroisReallyZero radix); rewrite <- Hr; rewrite <- H3; auto. case (Zmin_or (Fexp p) (Fexp q)); intros Hz; rewrite Hz; apply FboundedZeroSameExp; auto. case (errorBoundedPlus p q pq); auto. intros error (H6, (H7, H8)). exists error; exists r; repeat (split; auto). rewrite H3; auto. rewrite H8; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz