Library Float.Expansions.ThreeSum2
Require Export AllFloat.
Section F2.
Variable b : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Coercion Local FtoRradix := FtoR radix.
Let TMTO : (1 < radix)%Z := TwoMoreThanOne.
Hint Resolve TMTO: zarith.
Hypothesis precisionNotZero : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Variables p q r u v w p' q' r' : float.
Hypothesis Fp : Fbounded b p.
Hypothesis Fq : Fbounded b q.
Hypothesis Fr : Fbounded b r.
Hypothesis Fu : Fbounded b u.
Hypothesis Fv : Fbounded b v.
Hypothesis Fw : Fbounded b w.
Hypothesis Fp' : Fbounded b p'.
Hypothesis Fq' : Fbounded b q'.
Hypothesis Fr' : Fbounded b r'.
Hypothesis epq : (Fexp q ≤ Fexp p)%Z.
Hypothesis eqr : (Fexp r ≤ Fexp q)%Z.
Hypothesis uDef : Closest b radix (q + r) u.
Hypothesis vDef : v = (q + r - u)%R :>R.
Hypothesis p'Def : Closest b radix (p + u) p'.
Hypothesis wDef : w = (p + u - p')%R :>R.
Hypothesis q'Def : Closest b radix (w + v) q'.
Hypothesis r'Def : r' = (w + v - q')%R :>R.
Theorem TwoSumNul :
∀ f g x : float,
Closest b radix (f + g) x →
x = 0%R :>R → Fbounded b f → Fbounded b g → (f + g - x)%R = 0%R.
intros f g x H H0 H1 H2.
replace (FtoRradix f + FtoRradix g - FtoRradix x)%R with
(FtoRradix f + FtoRradix g)%R; [ idtac | rewrite H0; ring ].
replace 0%R with (FtoRradix (Fzero (- dExp b)));
[ idtac | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
apply sym_eq; apply (plusExact1 b radix) with (precision := precision);
auto with arith.
cut (CompatibleP b radix (Closest b radix));
[ intros Cp | apply ClosestCompatible; auto ].
apply Cp with (r1 := (f + g)%R) (p := x); auto with real.
fold FtoRradix in |- *; rewrite H0; unfold FtoRradix, FtoR in |- *;
simpl in |- *; ring.
repeat split; simpl in |- *; auto with zarith.
simpl in |- *; apply Zmin_Zle; auto with float.
Qed.
Theorem bound3Sum :
r' ≠ 0%R :>R →
(Rabs (q' + r') < 3%nat × radix × / pPred (vNum b) × Rabs p')%R.
intros H'; case (Req_dec w 0); intros Hw.
Contradict H'.
rewrite r'Def; auto.
rewrite Hw; rewrite Rplus_0_l.
apply Rminus_diag_eq.
unfold FtoRradix in |- *; apply ClosestIdem with (b := b); auto.
replace (FtoR radix v) with (w + v)%R; auto.
rewrite Hw; rewrite Rplus_0_l; auto.
rewrite r'Def; rewrite Rplus_minus.
apply Rle_lt_trans with (1 := Rabs_triang w v).
apply
Rlt_le_trans
with
(3%nat × radix × / pPred (vNum b) × (/ radix × Rmax (Rabs p) (Rabs u)))%R.
replace (3%nat × radix × / pPred (vNum b))%R with
(radix × radix × / pPred (vNum b) + radix × / pPred (vNum b))%R;
[ idtac | simpl in |- *; ring ].
rewrite (fun x y : R ⇒ Rmult_comm x (/ radix × y));
rewrite Rmult_plus_distr_l;
repeat rewrite (fun y : R ⇒ Rmult_comm (/ radix × y)).
apply Rplus_lt_compat.
replace
(radix × radix × / pPred (vNum b) × (/ radix × Rmax (Rabs p) (Rabs u)))%R
with
(radix × / radix × (radix × / pPred (vNum b) × Rmax (Rabs p) (Rabs u)))%R;
[ rewrite Rinv_r; auto with real zarith; try rewrite Rmult_1_l | ring ].
rewrite wDef.
rewrite <- Ropp_minus_distr; rewrite Rabs_Ropp.
apply (plusErrorBound2 b precision); auto.
Contradict Hw.
rewrite wDef.
apply Rminus_diag_eq.
unfold FtoRradix in |- *; rewrite (is_Fzero_rep1 radix _ Hw); auto.
rewrite <- (FzeroisZero radix b).
apply sym_eq; apply (plusExact1 b radix precision); auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u)%R p');
auto.
rewrite FzeroisZero; apply is_Fzero_rep1; auto.
apply FboundedFzero; auto.
simpl in |- *; unfold Zmin in |- *; case (Fexp p ?= Fexp u)%Z;
auto with float.
apply Rlt_le_trans with (radix × / pPred (vNum b) × (/ radix × Rabs u))%R.
rewrite vDef.
rewrite <- Ropp_minus_distr; rewrite Rabs_Ropp.
replace (radix × / pPred (vNum b) × (/ radix × Rabs u))%R with
(Rabs u × / radix × (radix × / pPred (vNum b)))%R;
[ idtac | ring ].
unfold FtoRradix in |- *; apply (plusErrorBound1 b radix precision); auto.
Contradict Hw.
rewrite wDef.
unfold FtoRradix in |- *; rewrite (is_Fzero_rep1 radix _ Hw).
rewrite Rplus_0_r.
apply Rminus_diag_eq.
unfold FtoRradix in |- *; apply ClosestIdem with (b := b); auto.
replace (FtoR radix p) with (p + u)%R; auto.
unfold FtoRradix in |- *; rewrite (is_Fzero_rep1 radix _ Hw).
rewrite Rplus_0_r; auto.
apply Rmult_le_compat_l; auto with real.
replace 0%R with (radix × 0)%R; auto with real; apply Rmult_le_compat_l;
auto with real arith.
apply Rlt_le; apply Rinv_0_lt_compat; auto with real arith.
apply Rlt_IZRO.
apply (pPredMoreThanOne b radix precision); auto with arith.
apply Rmult_le_compat_l; auto with real arith.
apply RmaxLess2; auto.
apply Rmult_le_compat_l; auto with real arith.
replace 0%R with (3%nat × radix × 0)%R; auto with real;
apply Rmult_le_compat_l; auto with real arith.
replace (3%nat × radix)%R with (INR 6); [ idtac | simpl in |- *; ring ].
replace 0%R with (INR 0); auto with real arith.
apply Rlt_le; apply Rinv_0_lt_compat; auto with real arith.
apply Rlt_IZRO.
apply (pPredMoreThanOne b radix precision); auto with arith.
apply (plusClosestLowerBound b precision); auto with real.
Contradict Hw.
rewrite wDef.
unfold FtoRradix, radix in |- *; rewrite Hw; ring.
Qed.
Theorem exp3Sum :
∃ p'' : float,
(∃ q'' : float,
(∃ r'' : float,
(Fbounded b p'' ∧ Fbounded b q'' ∧ Fbounded b r'') ∧
(p'' = p' :>R ∧ q'' = q' :>R ∧ r'' = r' :>R) ∧
(Fexp r ≤ Fexp r'')%Z ∧
((Fexp r'' ≤ Fexp q'')%Z ∧ (Fexp q'' ≤ Fexp p'')%Z) ∧
Fexp r'' = Fexp r)).
cut (Fbounded b (Fzero (Fexp r))); [ intros Fbr | apply FboundedZeroSameExp ];
auto.
case (Req_dec v 0); intros Hv.
cut (Fzero (Fexp r) = r' :>R);
[ intros EqZr
| rewrite (FzeroisReallyZero radix); rewrite r'Def; rewrite Hv;
rewrite Rplus_0_r; apply sym_eq; apply Rminus_diag_eq;
unfold FtoRradix in |- *; apply (ClosestIdem b radix);
auto; apply (ClosestCompatible b radix (w + v)%R w q');
auto; rewrite Hv; ring ].
case (plusExpMin b radix precision) with (P := Closest b radix) (5 := uDef);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
intros u' (H'0, (H'2, H'3)).
case (Req_dec w 0); intros Hw.
case
(plusExpMin b radix precision)
with (P := Closest b radix) (p := p) (q := u') (pq := p');
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
auto.
rewrite H'2; auto.
intros p'' (H'1, (H'5, H'6)).
∃ p''; ∃ (Fzero (Fexp r)); ∃ (Fzero (Fexp r)); split;
[ idtac | split ]; (split; [ idtac | split ]); auto.
rewrite (FzeroisReallyZero radix); auto.
rewrite <- (FzeroisZero radix b).
unfold FtoRradix in |- *; apply (ClosestIdem b radix); auto.
apply FboundedFzero; auto.
apply (ClosestCompatible b radix (w + v)%R (Fzero (- dExp b)) q'); auto.
rewrite Hw; rewrite Hv; unfold FtoRradix in |- *;
rewrite (FzeroisZero radix b); ring.
simpl in |- *; auto with zarith.
split; simpl in |- *; auto with zarith.
simpl in |- ×.
apply Zle_trans with (2 := H'6).
apply Zmin_Zle; auto.
apply Zle_trans with (Fexp q); auto.
rewrite <- (Zmin_le2 (Fexp q) (Fexp r)); auto.
case (errorBoundedPlus b radix precision) with (p := p) (q := u') (pq := p');
auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
auto.
rewrite H'2; auto.
intros w' (H'1, (H'5, H'6)).
∃ p'; ∃ w'; ∃ (Fzero (Fexp r)); split; [ idtac | split ];
(split; [ idtac | split ]); auto.
unfold FtoRradix in |- *; apply (ClosestIdem b radix); auto.
apply (ClosestCompatible b radix (w + v)%R (FtoR radix w') q'); auto.
rewrite Hv; rewrite Rplus_0_r; auto.
rewrite wDef; unfold FtoRradix in |- *; rewrite <- H'2; auto.
simpl in |- *; auto with zarith.
split; simpl in |- *; auto with zarith.
simpl in |- *; rewrite H'6.
apply Zmin_Zle; auto.
apply Zle_trans with (Fexp q); auto.
apply Zle_trans with (2 := H'3); auto with zarith.
rewrite Zmin_le2; auto with zarith.
rewrite H'6.
apply Zlt_le_weak.
apply (plusExact1bis b radix precision); auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
auto.
rewrite H'2; auto.
Contradict Hw.
rewrite wDef; auto.
unfold FtoRradix in |- *; rewrite <- H'2.
rewrite <- Hw; ring; ring.
case (Req_dec w 0); intros Hw.
cut (Fzero (Fexp r) = r' :>R);
[ intros EqZr
| rewrite (FzeroisReallyZero radix); rewrite r'Def; rewrite Hw;
rewrite Rplus_0_l; apply sym_eq; apply Rminus_diag_eq;
unfold FtoRradix in |- *; apply (ClosestIdem b radix);
auto; apply (ClosestCompatible b radix (w + v)%R (FtoR radix v) q');
auto; rewrite Hw; unfold FtoRradix in |- *; ring ].
case (plusExpMin b radix precision) with (P := Closest b radix) (5 := uDef);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
intros u' (H'0, (H'2, H'3)).
case (errorBoundedPlus b radix precision) with (p := q) (q := r) (pq := u');
auto.
apply
(ClosestCompatible b radix (FtoR radix q + FtoR radix r)%R
(FtoR radix q + FtoR radix r)%R u); auto.
intros v' H'; elim H'; intros H'1 H'4; elim H'4; intros H'5 H'6; clear H'4 H'.
case
(plusExpMin b radix precision)
with (P := Closest b radix) (p := p) (q := u') (pq := p');
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
auto.
rewrite H'2; auto.
intros p'' (H'4, (H'8, H'9)).
∃ p''; ∃ v'; ∃ (Fzero (Fexp r)); split; [ idtac | split ];
(split; [ idtac | split ]); auto.
replace (FtoRradix v') with (FtoRradix v); [ idtac | rewrite vDef; auto ].
unfold FtoRradix in |- *; apply (ClosestIdem b radix); auto;
apply (ClosestCompatible b radix (w + v)%R (FtoR radix v) q');
auto; rewrite Hw; unfold FtoRradix in |- *; ring.
unfold FtoRradix in |- *; rewrite H'1; auto.
rewrite H'2; auto.
simpl in |- *; auto with zarith.
split; simpl in |- *; auto with zarith.
rewrite H'6; rewrite Zmin_le2; auto with zarith.
apply Zle_trans with (2 := H'9).
apply Zmin_Zle; auto.
rewrite H'6; auto.
apply Zle_trans with (Fexp q); auto with zarith.
rewrite H'6; auto.
case (plusExpMin b radix precision) with (P := Closest b radix) (5 := uDef);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
intros u' (H'0, (H'2, H'3)).
case (errorBoundedPlus b radix precision) with (p := q) (q := r) (pq := u');
auto.
apply
(ClosestCompatible b radix (FtoR radix q + FtoR radix r)%R
(FtoR radix q + FtoR radix r)%R u); auto.
intros v' H'; elim H'; intros H'1 H'4; elim H'4; intros H'5 H'6; clear H'4 H'.
case (errorBoundedPlus b radix precision) with (p := p) (q := u') (pq := p');
auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
auto.
rewrite H'2; auto.
intros w' (H'4, (H'8, H'9)).
case
(plusExpBound b radix precision)
with (P := Closest b radix) (p := w') (q := v') (pq := q');
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply
(ClosestCompatible b radix (w + v)%R (FtoR radix w' + FtoR radix v')%R q');
auto.
rewrite wDef; unfold FtoRradix in |- *; rewrite H'4; auto.
unfold FtoRradix in vDef; rewrite vDef; unfold FtoRradix in |- *;
rewrite <- H'2; rewrite H'1; auto.
intros q'' (H'7, (H'11, (H'13, H'14))).
case
(errorBoundedPlus b radix precision) with (p := v') (q := w') (pq := q'');
auto.
apply
(ClosestCompatible b radix (w + v)%R (FtoR radix v' + FtoR radix w')%R q');
auto.
rewrite wDef; rewrite vDef; rewrite H'4; rewrite H'1;
unfold FtoRradix in |- *; repeat rewrite H'2; ring;
ring.
intros r'' (H'10, (H'15, H'16)).
∃ p'; ∃ q''; ∃ r''; split; [ idtac | split ];
(split; [ idtac | split ]); auto.
rewrite r'Def; rewrite wDef; rewrite vDef; unfold FtoRradix in |- *;
rewrite H'10; rewrite H'4; rewrite H'1; repeat rewrite H'2;
rewrite H'11; ring; ring.
rewrite H'16; apply Zmin_Zle; auto with zarith.
rewrite H'6; apply Zmin_Zle; auto with zarith.
rewrite H'9; apply Zmin_Zle; auto with zarith.
apply Zle_trans with (2 := H'3); apply Zmin_Zle; auto with zarith.
split.
rewrite H'16; rewrite Zmin_sym; auto.
apply Zle_trans with (1 := H'14).
rewrite Zmax_le1; auto.
apply Zlt_le_succ; auto.
rewrite H'9.
apply plusExact1bis with (b := b) (radix := radix) (precision := precision);
auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
auto.
rewrite H'2; auto.
Contradict Hw; auto.
rewrite wDef; auto.
unfold FtoRradix in |- *; rewrite <- H'2.
rewrite <- Hw; ring; ring.
rewrite H'9.
apply Zmin_Zle; auto.
rewrite H'6; rewrite Zmin_le2; auto with zarith.
rewrite H'6; auto.
rewrite H'16.
rewrite H'6.
rewrite H'9.
replace (Zmin (Fexp q) (Fexp r)) with (Fexp r).
apply Zmin_le1.
apply Zmin_Zle; auto.
apply Zle_trans with (Fexp q); auto.
rewrite <- (Zmin_le2 (Fexp q) (Fexp r)); auto.
apply sym_eq; apply Zmin_le2; auto.
Qed.
Theorem OutSum3 :
r' ≠ 0%R :>R →
(Float 1%nat (Fexp r) <
3%nat ×
(radix ×
(radix × (Rabs p' × / (pPred (vNum b) × (radix × pPred (vNum b) - radix))))))%R.
intros H; case exp3Sum;
intros p''
(q'',
(r'', ((H'1, (H'2, H'3)), ((H'4, (H'5, H'6)), (H'7, ((H'8, H'9), H'10)))))).
cut (¬ is_Fzero q'); [ intros Z1 | idtac ].
2: Contradict H; auto with real float.
2: replace (FtoRradix r') with (w + v - q')%R; auto.
2: apply TwoSumNul; auto.
2: unfold is_Fzero in H.
2: unfold FtoRradix, FtoR in |- ×.
2: replace (Fnum q') with 0%Z; simpl; ring.
apply Rle_lt_trans with (Rabs r'').
apply Rle_trans with (FtoR radix (Float 1%nat (Fexp r''))).
unfold FtoRradix in |- ×.
replace (Fexp r) with (Fexp r''); auto with real.
rewrite <- (Fabs_correct radix); auto with arith.
apply Fop.RleFexpFabs; auto with arith.
fold FtoRradix in |- ×.
rewrite H'6; auto.
apply Rlt_trans with (Rabs q' × / radix × (radix × / pPred (vNum b)))%R.
replace (FtoRradix r'') with (w + v - q')%R.
replace (Rabs (w + v - q')) with (Rabs (q' - (w + v))).
apply
plusErrorBound1
with (b := b) (radix := radix) (precision := precision) (p := w) (q := v);
auto with arith.
apply Rabs_minus_sym.
rewrite H'6; auto.
cut
((Rabs q' <
3%nat × (radix × (Rabs p' × / pPred (vNum b))) +
Rabs q' × / pPred (vNum b))%R →
(Rabs q' × / radix × (radix × / pPred (vNum b)) <
3%nat ×
(radix ×
(radix ×
(Rabs p' × / (pPred (vNum b) × (radix × pPred (vNum b) - radix))))))%R).
intros C; apply C.
apply
Rlt_trans with (3%nat × (radix × (Rabs p' × / pPred (vNum b))) + Rabs r')%R.
apply Rle_lt_trans with (Rabs (q' + r') + Rabs r')%R.
replace (Rabs q') with (Rabs (q' + r' + - r')).
replace (Rabs r') with (Rabs (- r')).
apply Rabs_triang.
apply Rabs_Ropp.
replace (q' + r' + - r')%R with (FtoRradix q'); [ auto | ring ].
replace (Rabs (q' + r') + Rabs r')%R with (Rabs r' + Rabs (q' + r'))%R;
[ auto | ring ].
replace (3%nat × (radix × (Rabs p' × / pPred (vNum b))) + Rabs r')%R with
(Rabs r' + 3%nat × (radix × (Rabs p' × / pPred (vNum b))))%R;
[ auto | ring ].
apply Rplus_lt_compat_l.
replace (3%nat × (radix × (Rabs p' × / pPred (vNum b))))%R with
(3%nat × radix × / pPred (vNum b) × Rabs p')%R; [ auto | ring ].
apply bound3Sum; auto.
apply Rplus_lt_compat_l.
replace (FtoRradix r') with (w + v - q')%R; auto.
replace (Rabs (FtoRradix w + FtoRradix v - FtoRradix q')) with
(Rabs (q' - (w + v))).
replace (Rabs q' × / pPred (vNum b))%R with
(Rabs q' × / radix × (radix × / pPred (vNum b)))%R.
apply
plusErrorBound1
with
(b := b)
(radix := radix)
(precision := precision)
(r := q')
(p := w)
(q := v); auto.
replace (Rabs (FtoRradix q') × / radix × (radix × / pPred (vNum b)))%R with
(Rabs (FtoRradix q') × (/ radix × radix) × / pPred (vNum b))%R;
[ rewrite Rinv_l; auto with real zarith | idtac ];
ring.
replace (q' - (w + v))%R with (- (w + v - q'))%R;
[ rewrite Rabs_Ropp | idtac ]; ring.
intros H'0.
replace (Rabs q' × / radix × (radix × / pPred (vNum b)))%R with
(radix × / radix × (/ pPred (vNum b) × Rabs q'))%R;
try ring.
rewrite Rinv_r; auto with real zarith; try rewrite Rmult_1_l.
replace (radix × pPred (vNum b) - radix)%R with
(radix × (pPred (vNum b) - 1))%R; [ idtac | simpl in |- *; ring; ring ].
cut (1 < pPred (vNum b))%Z;
[ intros Rlt1
| apply Zle_lt_trans with radix;
try apply (pPredMoreThanRadix b radix precision);
auto with zarith ].
cut ((pPred (vNum b) - 1)%R ≠ 0%R);
[ intros Rlt2
| replace (pPred (vNum b) - 1)%R with (IZR (pPred (vNum b) - 1));
auto with real zarith; rewrite <- Z_R_minus; simpl in |- *;
auto ].
repeat rewrite Rinv_mult_distr; auto with real zarith.
replace
(3%nat ×
(radix ×
(radix ×
(Rabs p' × (/ pPred (vNum b) × (/ radix × / (pPred (vNum b) - 1)))))))%R
with
(radix × / radix ×
(/ pPred (vNum b) × (3%nat × (radix × (Rabs p' × / (pPred (vNum b) - 1))))))%R;
[ idtac | ring ].
rewrite Rinv_r; auto with real zarith; rewrite Rmult_1_l.
apply Rmult_lt_compat_l; auto with real.
apply Rinv_0_lt_compat; auto with real.
apply Rlt_IZRO.
apply (pPredMoreThanOne b radix precision); auto with arith.
apply Rmult_lt_reg_l with (r := (pPred (vNum b) - 1)%R); auto with real.
replace
((pPred (vNum b) - 1) ×
(3%nat × (radix × (Rabs (FtoRradix p') × / (pPred (vNum b) - 1)))))%R with
(3%nat ×
(radix ×
(Rabs (FtoRradix p') × ((pPred (vNum b) - 1) × / (pPred (vNum b) - 1)))))%R;
[ rewrite Rinv_r; auto with real zarith; try rewrite Rmult_1_r
| ring; ring ].
apply Rplus_lt_reg_r with (Rabs (FtoRradix q'));
repeat rewrite (Rplus_comm (Rabs (FtoRradix q'))).
replace ((pPred (vNum b) - 1) × Rabs (FtoRradix q') + Rabs (FtoRradix q'))%R
with (pPred (vNum b) × Rabs (FtoRradix q'))%R; [ idtac | ring ].
apply Rmult_lt_reg_l with (r := (/ pPred (vNum b))%R); auto with real zarith.
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real zarith;
rewrite Rmult_1_l.
rewrite (fun x ⇒ Rmult_comm (/ x)); rewrite Rmult_plus_distr_r;
repeat rewrite <- Rmult_assoc; repeat rewrite <- Rmult_assoc in H'0;
auto.
Qed.
Theorem TwoSumNonNul :
∀ p q r pq : float,
Fbounded b p →
Fbounded b q →
Closest b radix (p + q) pq →
r = (p + q - pq)%R :>R → r ≠ 0%R :>R → pq ≠ 0%R :>R.
intros.
Contradict H3.
rewrite H2.
apply TwoSumNul; auto with real.
Qed.
Theorem TwoSumOneNul :
∀ p q pq : float,
Fbounded b p →
Fbounded b q →
Fbounded b pq → Closest b radix (p + q) pq → p = 0%R :>R → pq = q :>R.
intros.
generalize H2.
rewrite H3.
replace (0 + q0)%R with (FtoRradix q0); [ idtac | ring ].
intro.
apply sym_eq;
apply
(RoundedModeProjectorIdemEq b radix precision) with (P := Closest b radix);
auto with real float arith zarith.
apply (ClosestRoundedModeP b radix precision);
auto with real float arith zarith.
Qed.
Theorem TwoSumOneNul2 :
∀ p q pq r : float,
Fbounded b p →
Fbounded b q →
Fbounded b pq →
Closest b radix (p + q) pq →
p = 0%R :>R → r = (p + q - pq)%R :>R → r = 0%R :>R.
intros.
rewrite H4; rewrite H3.
apply Rminus_diag_eq; ring_simplify.
apply sym_eq; apply TwoSumOneNul with (p := p0); auto.
Qed.
End F2.
Section F2.
Variable b : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Coercion Local FtoRradix := FtoR radix.
Let TMTO : (1 < radix)%Z := TwoMoreThanOne.
Hint Resolve TMTO: zarith.
Hypothesis precisionNotZero : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Variables p q r u v w p' q' r' : float.
Hypothesis Fp : Fbounded b p.
Hypothesis Fq : Fbounded b q.
Hypothesis Fr : Fbounded b r.
Hypothesis Fu : Fbounded b u.
Hypothesis Fv : Fbounded b v.
Hypothesis Fw : Fbounded b w.
Hypothesis Fp' : Fbounded b p'.
Hypothesis Fq' : Fbounded b q'.
Hypothesis Fr' : Fbounded b r'.
Hypothesis epq : (Fexp q ≤ Fexp p)%Z.
Hypothesis eqr : (Fexp r ≤ Fexp q)%Z.
Hypothesis uDef : Closest b radix (q + r) u.
Hypothesis vDef : v = (q + r - u)%R :>R.
Hypothesis p'Def : Closest b radix (p + u) p'.
Hypothesis wDef : w = (p + u - p')%R :>R.
Hypothesis q'Def : Closest b radix (w + v) q'.
Hypothesis r'Def : r' = (w + v - q')%R :>R.
Theorem TwoSumNul :
∀ f g x : float,
Closest b radix (f + g) x →
x = 0%R :>R → Fbounded b f → Fbounded b g → (f + g - x)%R = 0%R.
intros f g x H H0 H1 H2.
replace (FtoRradix f + FtoRradix g - FtoRradix x)%R with
(FtoRradix f + FtoRradix g)%R; [ idtac | rewrite H0; ring ].
replace 0%R with (FtoRradix (Fzero (- dExp b)));
[ idtac | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
apply sym_eq; apply (plusExact1 b radix) with (precision := precision);
auto with arith.
cut (CompatibleP b radix (Closest b radix));
[ intros Cp | apply ClosestCompatible; auto ].
apply Cp with (r1 := (f + g)%R) (p := x); auto with real.
fold FtoRradix in |- *; rewrite H0; unfold FtoRradix, FtoR in |- *;
simpl in |- *; ring.
repeat split; simpl in |- *; auto with zarith.
simpl in |- *; apply Zmin_Zle; auto with float.
Qed.
Theorem bound3Sum :
r' ≠ 0%R :>R →
(Rabs (q' + r') < 3%nat × radix × / pPred (vNum b) × Rabs p')%R.
intros H'; case (Req_dec w 0); intros Hw.
Contradict H'.
rewrite r'Def; auto.
rewrite Hw; rewrite Rplus_0_l.
apply Rminus_diag_eq.
unfold FtoRradix in |- *; apply ClosestIdem with (b := b); auto.
replace (FtoR radix v) with (w + v)%R; auto.
rewrite Hw; rewrite Rplus_0_l; auto.
rewrite r'Def; rewrite Rplus_minus.
apply Rle_lt_trans with (1 := Rabs_triang w v).
apply
Rlt_le_trans
with
(3%nat × radix × / pPred (vNum b) × (/ radix × Rmax (Rabs p) (Rabs u)))%R.
replace (3%nat × radix × / pPred (vNum b))%R with
(radix × radix × / pPred (vNum b) + radix × / pPred (vNum b))%R;
[ idtac | simpl in |- *; ring ].
rewrite (fun x y : R ⇒ Rmult_comm x (/ radix × y));
rewrite Rmult_plus_distr_l;
repeat rewrite (fun y : R ⇒ Rmult_comm (/ radix × y)).
apply Rplus_lt_compat.
replace
(radix × radix × / pPred (vNum b) × (/ radix × Rmax (Rabs p) (Rabs u)))%R
with
(radix × / radix × (radix × / pPred (vNum b) × Rmax (Rabs p) (Rabs u)))%R;
[ rewrite Rinv_r; auto with real zarith; try rewrite Rmult_1_l | ring ].
rewrite wDef.
rewrite <- Ropp_minus_distr; rewrite Rabs_Ropp.
apply (plusErrorBound2 b precision); auto.
Contradict Hw.
rewrite wDef.
apply Rminus_diag_eq.
unfold FtoRradix in |- *; rewrite (is_Fzero_rep1 radix _ Hw); auto.
rewrite <- (FzeroisZero radix b).
apply sym_eq; apply (plusExact1 b radix precision); auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u)%R p');
auto.
rewrite FzeroisZero; apply is_Fzero_rep1; auto.
apply FboundedFzero; auto.
simpl in |- *; unfold Zmin in |- *; case (Fexp p ?= Fexp u)%Z;
auto with float.
apply Rlt_le_trans with (radix × / pPred (vNum b) × (/ radix × Rabs u))%R.
rewrite vDef.
rewrite <- Ropp_minus_distr; rewrite Rabs_Ropp.
replace (radix × / pPred (vNum b) × (/ radix × Rabs u))%R with
(Rabs u × / radix × (radix × / pPred (vNum b)))%R;
[ idtac | ring ].
unfold FtoRradix in |- *; apply (plusErrorBound1 b radix precision); auto.
Contradict Hw.
rewrite wDef.
unfold FtoRradix in |- *; rewrite (is_Fzero_rep1 radix _ Hw).
rewrite Rplus_0_r.
apply Rminus_diag_eq.
unfold FtoRradix in |- *; apply ClosestIdem with (b := b); auto.
replace (FtoR radix p) with (p + u)%R; auto.
unfold FtoRradix in |- *; rewrite (is_Fzero_rep1 radix _ Hw).
rewrite Rplus_0_r; auto.
apply Rmult_le_compat_l; auto with real.
replace 0%R with (radix × 0)%R; auto with real; apply Rmult_le_compat_l;
auto with real arith.
apply Rlt_le; apply Rinv_0_lt_compat; auto with real arith.
apply Rlt_IZRO.
apply (pPredMoreThanOne b radix precision); auto with arith.
apply Rmult_le_compat_l; auto with real arith.
apply RmaxLess2; auto.
apply Rmult_le_compat_l; auto with real arith.
replace 0%R with (3%nat × radix × 0)%R; auto with real;
apply Rmult_le_compat_l; auto with real arith.
replace (3%nat × radix)%R with (INR 6); [ idtac | simpl in |- *; ring ].
replace 0%R with (INR 0); auto with real arith.
apply Rlt_le; apply Rinv_0_lt_compat; auto with real arith.
apply Rlt_IZRO.
apply (pPredMoreThanOne b radix precision); auto with arith.
apply (plusClosestLowerBound b precision); auto with real.
Contradict Hw.
rewrite wDef.
unfold FtoRradix, radix in |- *; rewrite Hw; ring.
Qed.
Theorem exp3Sum :
∃ p'' : float,
(∃ q'' : float,
(∃ r'' : float,
(Fbounded b p'' ∧ Fbounded b q'' ∧ Fbounded b r'') ∧
(p'' = p' :>R ∧ q'' = q' :>R ∧ r'' = r' :>R) ∧
(Fexp r ≤ Fexp r'')%Z ∧
((Fexp r'' ≤ Fexp q'')%Z ∧ (Fexp q'' ≤ Fexp p'')%Z) ∧
Fexp r'' = Fexp r)).
cut (Fbounded b (Fzero (Fexp r))); [ intros Fbr | apply FboundedZeroSameExp ];
auto.
case (Req_dec v 0); intros Hv.
cut (Fzero (Fexp r) = r' :>R);
[ intros EqZr
| rewrite (FzeroisReallyZero radix); rewrite r'Def; rewrite Hv;
rewrite Rplus_0_r; apply sym_eq; apply Rminus_diag_eq;
unfold FtoRradix in |- *; apply (ClosestIdem b radix);
auto; apply (ClosestCompatible b radix (w + v)%R w q');
auto; rewrite Hv; ring ].
case (plusExpMin b radix precision) with (P := Closest b radix) (5 := uDef);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
intros u' (H'0, (H'2, H'3)).
case (Req_dec w 0); intros Hw.
case
(plusExpMin b radix precision)
with (P := Closest b radix) (p := p) (q := u') (pq := p');
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
auto.
rewrite H'2; auto.
intros p'' (H'1, (H'5, H'6)).
∃ p''; ∃ (Fzero (Fexp r)); ∃ (Fzero (Fexp r)); split;
[ idtac | split ]; (split; [ idtac | split ]); auto.
rewrite (FzeroisReallyZero radix); auto.
rewrite <- (FzeroisZero radix b).
unfold FtoRradix in |- *; apply (ClosestIdem b radix); auto.
apply FboundedFzero; auto.
apply (ClosestCompatible b radix (w + v)%R (Fzero (- dExp b)) q'); auto.
rewrite Hw; rewrite Hv; unfold FtoRradix in |- *;
rewrite (FzeroisZero radix b); ring.
simpl in |- *; auto with zarith.
split; simpl in |- *; auto with zarith.
simpl in |- ×.
apply Zle_trans with (2 := H'6).
apply Zmin_Zle; auto.
apply Zle_trans with (Fexp q); auto.
rewrite <- (Zmin_le2 (Fexp q) (Fexp r)); auto.
case (errorBoundedPlus b radix precision) with (p := p) (q := u') (pq := p');
auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
auto.
rewrite H'2; auto.
intros w' (H'1, (H'5, H'6)).
∃ p'; ∃ w'; ∃ (Fzero (Fexp r)); split; [ idtac | split ];
(split; [ idtac | split ]); auto.
unfold FtoRradix in |- *; apply (ClosestIdem b radix); auto.
apply (ClosestCompatible b radix (w + v)%R (FtoR radix w') q'); auto.
rewrite Hv; rewrite Rplus_0_r; auto.
rewrite wDef; unfold FtoRradix in |- *; rewrite <- H'2; auto.
simpl in |- *; auto with zarith.
split; simpl in |- *; auto with zarith.
simpl in |- *; rewrite H'6.
apply Zmin_Zle; auto.
apply Zle_trans with (Fexp q); auto.
apply Zle_trans with (2 := H'3); auto with zarith.
rewrite Zmin_le2; auto with zarith.
rewrite H'6.
apply Zlt_le_weak.
apply (plusExact1bis b radix precision); auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
auto.
rewrite H'2; auto.
Contradict Hw.
rewrite wDef; auto.
unfold FtoRradix in |- *; rewrite <- H'2.
rewrite <- Hw; ring; ring.
case (Req_dec w 0); intros Hw.
cut (Fzero (Fexp r) = r' :>R);
[ intros EqZr
| rewrite (FzeroisReallyZero radix); rewrite r'Def; rewrite Hw;
rewrite Rplus_0_l; apply sym_eq; apply Rminus_diag_eq;
unfold FtoRradix in |- *; apply (ClosestIdem b radix);
auto; apply (ClosestCompatible b radix (w + v)%R (FtoR radix v) q');
auto; rewrite Hw; unfold FtoRradix in |- *; ring ].
case (plusExpMin b radix precision) with (P := Closest b radix) (5 := uDef);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
intros u' (H'0, (H'2, H'3)).
case (errorBoundedPlus b radix precision) with (p := q) (q := r) (pq := u');
auto.
apply
(ClosestCompatible b radix (FtoR radix q + FtoR radix r)%R
(FtoR radix q + FtoR radix r)%R u); auto.
intros v' H'; elim H'; intros H'1 H'4; elim H'4; intros H'5 H'6; clear H'4 H'.
case
(plusExpMin b radix precision)
with (P := Closest b radix) (p := p) (q := u') (pq := p');
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
auto.
rewrite H'2; auto.
intros p'' (H'4, (H'8, H'9)).
∃ p''; ∃ v'; ∃ (Fzero (Fexp r)); split; [ idtac | split ];
(split; [ idtac | split ]); auto.
replace (FtoRradix v') with (FtoRradix v); [ idtac | rewrite vDef; auto ].
unfold FtoRradix in |- *; apply (ClosestIdem b radix); auto;
apply (ClosestCompatible b radix (w + v)%R (FtoR radix v) q');
auto; rewrite Hw; unfold FtoRradix in |- *; ring.
unfold FtoRradix in |- *; rewrite H'1; auto.
rewrite H'2; auto.
simpl in |- *; auto with zarith.
split; simpl in |- *; auto with zarith.
rewrite H'6; rewrite Zmin_le2; auto with zarith.
apply Zle_trans with (2 := H'9).
apply Zmin_Zle; auto.
rewrite H'6; auto.
apply Zle_trans with (Fexp q); auto with zarith.
rewrite H'6; auto.
case (plusExpMin b radix precision) with (P := Closest b radix) (5 := uDef);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
intros u' (H'0, (H'2, H'3)).
case (errorBoundedPlus b radix precision) with (p := q) (q := r) (pq := u');
auto.
apply
(ClosestCompatible b radix (FtoR radix q + FtoR radix r)%R
(FtoR radix q + FtoR radix r)%R u); auto.
intros v' H'; elim H'; intros H'1 H'4; elim H'4; intros H'5 H'6; clear H'4 H'.
case (errorBoundedPlus b radix precision) with (p := p) (q := u') (pq := p');
auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
auto.
rewrite H'2; auto.
intros w' (H'4, (H'8, H'9)).
case
(plusExpBound b radix precision)
with (P := Closest b radix) (p := w') (q := v') (pq := q');
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply
(ClosestCompatible b radix (w + v)%R (FtoR radix w' + FtoR radix v')%R q');
auto.
rewrite wDef; unfold FtoRradix in |- *; rewrite H'4; auto.
unfold FtoRradix in vDef; rewrite vDef; unfold FtoRradix in |- *;
rewrite <- H'2; rewrite H'1; auto.
intros q'' (H'7, (H'11, (H'13, H'14))).
case
(errorBoundedPlus b radix precision) with (p := v') (q := w') (pq := q'');
auto.
apply
(ClosestCompatible b radix (w + v)%R (FtoR radix v' + FtoR radix w')%R q');
auto.
rewrite wDef; rewrite vDef; rewrite H'4; rewrite H'1;
unfold FtoRradix in |- *; repeat rewrite H'2; ring;
ring.
intros r'' (H'10, (H'15, H'16)).
∃ p'; ∃ q''; ∃ r''; split; [ idtac | split ];
(split; [ idtac | split ]); auto.
rewrite r'Def; rewrite wDef; rewrite vDef; unfold FtoRradix in |- *;
rewrite H'10; rewrite H'4; rewrite H'1; repeat rewrite H'2;
rewrite H'11; ring; ring.
rewrite H'16; apply Zmin_Zle; auto with zarith.
rewrite H'6; apply Zmin_Zle; auto with zarith.
rewrite H'9; apply Zmin_Zle; auto with zarith.
apply Zle_trans with (2 := H'3); apply Zmin_Zle; auto with zarith.
split.
rewrite H'16; rewrite Zmin_sym; auto.
apply Zle_trans with (1 := H'14).
rewrite Zmax_le1; auto.
apply Zlt_le_succ; auto.
rewrite H'9.
apply plusExact1bis with (b := b) (radix := radix) (precision := precision);
auto.
apply
(ClosestCompatible b radix (p + u)%R (FtoR radix p + FtoR radix u')%R p');
auto.
rewrite H'2; auto.
Contradict Hw; auto.
rewrite wDef; auto.
unfold FtoRradix in |- *; rewrite <- H'2.
rewrite <- Hw; ring; ring.
rewrite H'9.
apply Zmin_Zle; auto.
rewrite H'6; rewrite Zmin_le2; auto with zarith.
rewrite H'6; auto.
rewrite H'16.
rewrite H'6.
rewrite H'9.
replace (Zmin (Fexp q) (Fexp r)) with (Fexp r).
apply Zmin_le1.
apply Zmin_Zle; auto.
apply Zle_trans with (Fexp q); auto.
rewrite <- (Zmin_le2 (Fexp q) (Fexp r)); auto.
apply sym_eq; apply Zmin_le2; auto.
Qed.
Theorem OutSum3 :
r' ≠ 0%R :>R →
(Float 1%nat (Fexp r) <
3%nat ×
(radix ×
(radix × (Rabs p' × / (pPred (vNum b) × (radix × pPred (vNum b) - radix))))))%R.
intros H; case exp3Sum;
intros p''
(q'',
(r'', ((H'1, (H'2, H'3)), ((H'4, (H'5, H'6)), (H'7, ((H'8, H'9), H'10)))))).
cut (¬ is_Fzero q'); [ intros Z1 | idtac ].
2: Contradict H; auto with real float.
2: replace (FtoRradix r') with (w + v - q')%R; auto.
2: apply TwoSumNul; auto.
2: unfold is_Fzero in H.
2: unfold FtoRradix, FtoR in |- ×.
2: replace (Fnum q') with 0%Z; simpl; ring.
apply Rle_lt_trans with (Rabs r'').
apply Rle_trans with (FtoR radix (Float 1%nat (Fexp r''))).
unfold FtoRradix in |- ×.
replace (Fexp r) with (Fexp r''); auto with real.
rewrite <- (Fabs_correct radix); auto with arith.
apply Fop.RleFexpFabs; auto with arith.
fold FtoRradix in |- ×.
rewrite H'6; auto.
apply Rlt_trans with (Rabs q' × / radix × (radix × / pPred (vNum b)))%R.
replace (FtoRradix r'') with (w + v - q')%R.
replace (Rabs (w + v - q')) with (Rabs (q' - (w + v))).
apply
plusErrorBound1
with (b := b) (radix := radix) (precision := precision) (p := w) (q := v);
auto with arith.
apply Rabs_minus_sym.
rewrite H'6; auto.
cut
((Rabs q' <
3%nat × (radix × (Rabs p' × / pPred (vNum b))) +
Rabs q' × / pPred (vNum b))%R →
(Rabs q' × / radix × (radix × / pPred (vNum b)) <
3%nat ×
(radix ×
(radix ×
(Rabs p' × / (pPred (vNum b) × (radix × pPred (vNum b) - radix))))))%R).
intros C; apply C.
apply
Rlt_trans with (3%nat × (radix × (Rabs p' × / pPred (vNum b))) + Rabs r')%R.
apply Rle_lt_trans with (Rabs (q' + r') + Rabs r')%R.
replace (Rabs q') with (Rabs (q' + r' + - r')).
replace (Rabs r') with (Rabs (- r')).
apply Rabs_triang.
apply Rabs_Ropp.
replace (q' + r' + - r')%R with (FtoRradix q'); [ auto | ring ].
replace (Rabs (q' + r') + Rabs r')%R with (Rabs r' + Rabs (q' + r'))%R;
[ auto | ring ].
replace (3%nat × (radix × (Rabs p' × / pPred (vNum b))) + Rabs r')%R with
(Rabs r' + 3%nat × (radix × (Rabs p' × / pPred (vNum b))))%R;
[ auto | ring ].
apply Rplus_lt_compat_l.
replace (3%nat × (radix × (Rabs p' × / pPred (vNum b))))%R with
(3%nat × radix × / pPred (vNum b) × Rabs p')%R; [ auto | ring ].
apply bound3Sum; auto.
apply Rplus_lt_compat_l.
replace (FtoRradix r') with (w + v - q')%R; auto.
replace (Rabs (FtoRradix w + FtoRradix v - FtoRradix q')) with
(Rabs (q' - (w + v))).
replace (Rabs q' × / pPred (vNum b))%R with
(Rabs q' × / radix × (radix × / pPred (vNum b)))%R.
apply
plusErrorBound1
with
(b := b)
(radix := radix)
(precision := precision)
(r := q')
(p := w)
(q := v); auto.
replace (Rabs (FtoRradix q') × / radix × (radix × / pPred (vNum b)))%R with
(Rabs (FtoRradix q') × (/ radix × radix) × / pPred (vNum b))%R;
[ rewrite Rinv_l; auto with real zarith | idtac ];
ring.
replace (q' - (w + v))%R with (- (w + v - q'))%R;
[ rewrite Rabs_Ropp | idtac ]; ring.
intros H'0.
replace (Rabs q' × / radix × (radix × / pPred (vNum b)))%R with
(radix × / radix × (/ pPred (vNum b) × Rabs q'))%R;
try ring.
rewrite Rinv_r; auto with real zarith; try rewrite Rmult_1_l.
replace (radix × pPred (vNum b) - radix)%R with
(radix × (pPred (vNum b) - 1))%R; [ idtac | simpl in |- *; ring; ring ].
cut (1 < pPred (vNum b))%Z;
[ intros Rlt1
| apply Zle_lt_trans with radix;
try apply (pPredMoreThanRadix b radix precision);
auto with zarith ].
cut ((pPred (vNum b) - 1)%R ≠ 0%R);
[ intros Rlt2
| replace (pPred (vNum b) - 1)%R with (IZR (pPred (vNum b) - 1));
auto with real zarith; rewrite <- Z_R_minus; simpl in |- *;
auto ].
repeat rewrite Rinv_mult_distr; auto with real zarith.
replace
(3%nat ×
(radix ×
(radix ×
(Rabs p' × (/ pPred (vNum b) × (/ radix × / (pPred (vNum b) - 1)))))))%R
with
(radix × / radix ×
(/ pPred (vNum b) × (3%nat × (radix × (Rabs p' × / (pPred (vNum b) - 1))))))%R;
[ idtac | ring ].
rewrite Rinv_r; auto with real zarith; rewrite Rmult_1_l.
apply Rmult_lt_compat_l; auto with real.
apply Rinv_0_lt_compat; auto with real.
apply Rlt_IZRO.
apply (pPredMoreThanOne b radix precision); auto with arith.
apply Rmult_lt_reg_l with (r := (pPred (vNum b) - 1)%R); auto with real.
replace
((pPred (vNum b) - 1) ×
(3%nat × (radix × (Rabs (FtoRradix p') × / (pPred (vNum b) - 1)))))%R with
(3%nat ×
(radix ×
(Rabs (FtoRradix p') × ((pPred (vNum b) - 1) × / (pPred (vNum b) - 1)))))%R;
[ rewrite Rinv_r; auto with real zarith; try rewrite Rmult_1_r
| ring; ring ].
apply Rplus_lt_reg_r with (Rabs (FtoRradix q'));
repeat rewrite (Rplus_comm (Rabs (FtoRradix q'))).
replace ((pPred (vNum b) - 1) × Rabs (FtoRradix q') + Rabs (FtoRradix q'))%R
with (pPred (vNum b) × Rabs (FtoRradix q'))%R; [ idtac | ring ].
apply Rmult_lt_reg_l with (r := (/ pPred (vNum b))%R); auto with real zarith.
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real zarith;
rewrite Rmult_1_l.
rewrite (fun x ⇒ Rmult_comm (/ x)); rewrite Rmult_plus_distr_r;
repeat rewrite <- Rmult_assoc; repeat rewrite <- Rmult_assoc in H'0;
auto.
Qed.
Theorem TwoSumNonNul :
∀ p q r pq : float,
Fbounded b p →
Fbounded b q →
Closest b radix (p + q) pq →
r = (p + q - pq)%R :>R → r ≠ 0%R :>R → pq ≠ 0%R :>R.
intros.
Contradict H3.
rewrite H2.
apply TwoSumNul; auto with real.
Qed.
Theorem TwoSumOneNul :
∀ p q pq : float,
Fbounded b p →
Fbounded b q →
Fbounded b pq → Closest b radix (p + q) pq → p = 0%R :>R → pq = q :>R.
intros.
generalize H2.
rewrite H3.
replace (0 + q0)%R with (FtoRradix q0); [ idtac | ring ].
intro.
apply sym_eq;
apply
(RoundedModeProjectorIdemEq b radix precision) with (P := Closest b radix);
auto with real float arith zarith.
apply (ClosestRoundedModeP b radix precision);
auto with real float arith zarith.
Qed.
Theorem TwoSumOneNul2 :
∀ p q pq r : float,
Fbounded b p →
Fbounded b q →
Fbounded b pq →
Closest b radix (p + q) pq →
p = 0%R :>R → r = (p + q - pq)%R :>R → r = 0%R :>R.
intros.
rewrite H4; rewrite H3.
apply Rminus_diag_eq; ring_simplify.
apply sym_eq; apply TwoSumOneNul with (p := p0); auto.
Qed.
End F2.