proposition: Theorem plusExpUpperBound : forall P, RoundedModeP b radix P -> forall p q pq : float, P (p + q)%R pq -> Fbounded b p -> Fbounded b q -> exists r : float, Fbounded b r /\ r = pq :>R /\ (Fexp r <= Z.succ (Zmax (Fexp p) (Fexp q)))%Z.
proof: Proof. intros P H' p q pq H'0 H'1 H'2. replace (Z.succ (Zmax (Fexp p) (Fexp q))) with (Fexp (Float (pPred (vNum b)) (Z.succ (Zmax (Fexp p) (Fexp q))))); [ idtac | simpl in |- *; auto ]. unfold FtoRradix in |- *; apply eqExpMax; auto. apply RoundedModeBounded with (radix := radix) (P := P) (r := (p + q)%R); auto with arith. unfold pPred in |- *; apply maxFbounded; auto. apply Z.le_trans with (Fexp p); try apply H'1. apply Z.le_trans with (Z.succ (Fexp p)); auto with zarith. apply Zsucc_le_compat, ZmaxLe1. replace (FtoR radix (Float (pPred (vNum b)) (Z.succ (Zmax (Fexp p) (Fexp q))))) with (radix * Float (pPred (vNum b)) (Zmax (Fexp p) (Fexp q)))%R. rewrite Fabs_correct; auto with zarith. unfold FtoRradix in |- *; apply RoundedModeMultAbs with (b := b) (precision := precision) (P := P) (r := (p + q)%R); auto. unfold pPred in |- *; apply maxFbounded; auto. apply Z.le_trans with (Fexp p); try apply H'1; apply ZmaxLe1. apply Rle_trans with (Rabs p + Rabs q)%R. apply Rabs_triang; auto. apply Rle_trans with (2 * FtoR radix (Float (pPred (vNum b)) (Zmax (Fexp p) (Fexp q))))%R; auto. cut (forall r : R, (2 * r)%R = (r + r)%R); [ intros tmp; rewrite tmp; clear tmp | intros; simpl in |- *; ring ]. apply Rplus_le_compat; auto. rewrite <- (Fabs_correct radix); auto with arith; apply maxMax1; auto; apply ZmaxLe1. rewrite <- (Fabs_correct radix); auto with arith; apply maxMax1; auto; apply ZmaxLe2. apply Rmult_le_compat; auto with real arith. apply LeFnumZERO; simpl in |- *; auto. unfold pPred in |- *; apply Zle_Zpred; auto with zarith. apply IZR_le; simpl in |- *; auto with zarith. cut (1 < radix)%Z; auto with zarith;intros. unfold FtoRradix, FtoR in |- *; simpl in |- *. rewrite powerRZ_Zs; auto with real zarith; try ring. apply IZR_neq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz