proposition: Theorem plusExact1 : forall p q r : float, Fbounded b p -> Fbounded b q -> Closest b radix (p + q) r -> (Fexp r <= Z.min (Fexp p) (Fexp q))%Z -> r = (p + q)%R :>R.
proof: Proof. intros p q r H' H'0 H'1 H'2. cut (2 * Rabs (FtoR radix (Fplus radix p q) - FtoR radix r) <= Float 1 (Fexp r))%R; [ rewrite Fplus_correct; auto with zarith; intros Rl1 | idtac ]. case errorBoundedPlus with (p := p) (q := q) (pq := r); auto. intros x H'3; elim H'3; intros H'4 H'5; elim H'5; intros H'6 H'7; clear H'5 H'3. unfold FtoRradix in H'4; rewrite <- H'4 in Rl1. 2: apply Rle_trans with (Fulp b radix precision r); auto. 2: apply (ClosestUlp b radix precision); auto. 2: rewrite Fplus_correct; auto with zarith. 2: unfold FtoRradix in |- *; apply FulpLe; auto. 2: apply RoundedModeBounded with (radix := radix) (P := Closest b radix) (r := (p + q)%R); auto. 2: apply ClosestRoundedModeP with (precision := precision); auto. cut (x = 0%R :>R); [ unfold FtoRradix in |- *; intros Eq1 | idtac ]. replace (FtoR radix r) with (FtoR radix r + 0)%R; [ idtac | ring ]. rewrite <- Eq1. rewrite H'4; ring. apply (is_Fzero_rep1 radix). case (Z_zerop (Fnum x)); simpl in |- *; auto. intros H'3; contradict Rl1. apply Rgt_not_le. red in |- *; apply Rle_lt_trans with (Rabs (FtoR radix x)). unfold FtoRradix, FtoR in |- *; simpl in |- *; auto. rewrite Rabs_mult. apply Rmult_le_compat; auto with real arith. apply powerRZ_le, IZR_lt; lia. rewrite Rabs_Zabs. apply IZR_le. assert (0 < Z.abs (Fnum x))%Z; [idtac|auto with zarith]. now apply <- Z.abs_pos. rewrite Rabs_right; auto with real arith. apply Rle_powerRZ; auto with real arith. apply IZR_le; auto with zarith. auto with zarith. apply Rle_ge, powerRZ_le, IZR_lt; lia. cut (forall r : R, (2 * r)%R = (r + r)%R); [ intros tmp; rewrite tmp; clear tmp | intros f; simpl in |- *; ring ]. pattern (Rabs (FtoR radix x)) at 1 in |- *; replace (Rabs (FtoR radix x)) with (Rabs (FtoR radix x) + 0)%R; [ idtac | ring ]. apply Rplus_lt_compat_l; auto. case (Rabs_pos (FtoR radix x)); auto. rewrite <- Fabs_correct; auto with arith. intros H'5; contradict H'3. cut (Fnum (Fabs x) = 0%Z). unfold Fabs in |- *; simpl in |- *; case (Fnum x); simpl in |- *; auto; intros; discriminate. change (is_Fzero (Fabs x)) in |- *. apply (is_Fzero_rep2 radix); auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz