Library Float.Expansions.TwoSum
Require Export Fast2Sum.
Section EFast.
Variable b : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Let TMTO : (1 < radix)%Z := TwoMoreThanOne.
Hint Resolve TMTO: zarith.
Coercion Local FtoRradix := FtoR radix.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Variable Iplus : float → float → float.
Hypothesis
IplusCorrect :
∀ p q : float,
Fbounded b p → Fbounded b q → Closest b radix (p + q) (Iplus p q).
Hypothesis
IplusComp :
∀ p q r s : float,
Fbounded b p →
Fbounded b q →
Fbounded b r →
Fbounded b s → p = r :>R → q = s :>R → Iplus p q = Iplus r s :>R.
Hypothesis IplusSym : ∀ p q : float, Iplus p q = Iplus q p.
Hypothesis
IplusOp : ∀ p q : float, Fopp (Iplus p q) = Iplus (Fopp p) (Fopp q).
Variable Iminus : float → float → float.
Hypothesis IminusPlus : ∀ p q : float, Iminus p q = Iplus p (Fopp q).
Theorem IplusOl :
∀ p q : float,
Fbounded b p → Fbounded b q → p = 0%R :>R → Iplus p q = q :>R.
intros p q H' H'0 H'1.
rewrite IplusSym.
apply (IplusOr b); auto.
Qed.
Let IminusCorrect := IminusCorrect b Iplus IplusCorrect Iminus IminusPlus.
Let IplusBounded := IplusBounded b Iplus IplusCorrect.
Let IminusBounded := IminusBounded b Iplus IplusCorrect Iminus IminusPlus.
Let IminusId := IminusId b Iplus IplusCorrect Iminus IminusPlus.
Theorem MKnuth :
∀ p q : float,
Fbounded b p →
Fbounded b q →
Iminus (Iplus p q) p = (Iplus p q - p)%R :>R →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1.
rewrite IplusOl; auto with float.
case
(errorBoundedPlus b radix precision)
with (p := p) (q := q) (pq := Iplus p q); auto.
intros x H'2; elim H'2; intros H'3 H'4; elim H'4; intros H'5 H'6;
clear H'4 H'2.
unfold FtoRradix in |- *; rewrite <- H'3.
apply sym_eq; apply (ClosestIdem b); auto.
apply
(ClosestCompatible b radix (q - Iminus (Iplus p q) p)%R (
FtoR radix x) (Iminus q (Iminus (Iplus p q) p)));
auto.
rewrite H'3.
rewrite H'1.
unfold FtoRradix in |- *; ring; ring.
replace 0%R with (FtoRradix (Iminus p p)).
repeat rewrite IminusPlus; apply IplusComp; repeat rewrite <- IminusPlus;
auto with float.
unfold FtoRradix in |- *; repeat rewrite Fopp_correct.
replace (FtoR radix (Iminus (Iplus p q) (Iminus (Iplus p q) p))) with
(FtoR radix p); auto.
apply (ClosestIdem b); auto.
apply
(ClosestCompatible b radix (Iplus p q - Iminus (Iplus p q) p)%R
(FtoR radix p) (Iminus (Iplus p q) (Iminus (Iplus p q) p)));
auto.
rewrite H'1; auto.
unfold FtoRradix in |- *; ring; ring.
apply IminusId; auto.
Qed.
Theorem IplusCorrectEq :
∀ (p q pq : float) (r : R),
Fbounded b p →
Fbounded b q →
Fbounded b pq → r = pq :>R → (p + q)%R = pq :>R → Iplus p q = r :>R.
intros p q pq r H' H'0 H'1 H'2 H'3; rewrite H'2.
unfold FtoRradix in |- *; apply sym_eq; apply (ClosestIdem b radix); auto.
apply (ClosestCompatible b radix (p + q)%R pq (Iplus p q)); auto.
Qed.
Theorem IminusCorrectEq :
∀ (p q pq : float) (r : R),
Fbounded b p →
Fbounded b q →
Fbounded b pq → r = pq :>R → (p - q)%R = pq :>R → Iminus p q = r :>R.
intros p q pq r H' H'0 H'1 H'2 H'3; rewrite H'2.
unfold FtoRradix in |- *; apply sym_eq; apply (ClosestIdem b radix); auto.
apply (ClosestCompatible b radix (p - q)%R pq (Iminus p q)); auto.
Qed.
Theorem Iminus2Exact :
∀ p q : float,
(0 ≤ p)%R →
(p ≤ q)%R →
Fbounded b p →
Fbounded b q → Iminus q (Iminus q p) = (q - Iminus q p)%R :>R.
intros p q H' H'0 H'1 H'2.
case
(minusRoundRep b radix precision)
with (P := Closest b radix) (p := p) (q := q) (qmp := Iminus q p);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
intros pq H'3; elim H'3; intros H'4 H'5; clear H'3.
apply IminusCorrectEq with (pq := pq); auto.
Qed.
Theorem MKnuth1 :
∀ p q : float,
Fbounded b p →
Fbounded b q →
Iminus q (Iminus (Iplus p q) p) = (q - Iminus (Iplus p q) p)%R :>R →
Iminus (Iplus p q) (Iminus (Iplus p q) p) =
(Iplus p q - Iminus (Iplus p q) p)%R :>R →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1 H'2.
cut
(Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)) =
(p - Iminus (Iplus p q) (Iminus (Iplus p q) p))%R :>R);
[ intros H'3 | idtac ].
case
(errorBoundedPlus b radix precision)
with (p := p) (q := q) (pq := Iplus p q); auto.
intros pq H'4; elim H'4; intros H'5 H'6; elim H'6; intros H'7 H'8;
clear H'6 H'4.
apply IplusCorrectEq with (pq := pq); auto.
repeat rewrite H'3; repeat rewrite H'2; repeat rewrite H'1.
unfold FtoRradix in |- *; rewrite H'5.
ring.
rewrite H'2.
case
(errorBoundedPlus b radix precision)
with (p := Iplus p q) (q := Fopp p) (pq := Iminus (Iplus p q) p);
auto with float.
apply
(ClosestCompatible b radix (Iplus p q - p)%R (Iplus p q + Fopp p)%R
(Iminus (Iplus p q) p)); auto.
rewrite (Fopp_correct radix); auto.
intros pq H'3; elim H'3; intros H'4 H'5; elim H'5; intros H'6 H'7;
clear H'5 H'3.
rewrite (IminusPlus p); apply IplusCorrectEq with (pq := Fopp pq);
auto with float.
unfold FtoRradix in |- *; rewrite (Fopp_correct radix); auto; rewrite H'4;
rewrite (Fopp_correct radix); auto; ring; ring.
unfold FtoRradix in |- *; repeat rewrite (Fopp_correct radix); auto;
rewrite H'4; rewrite (Fopp_correct radix); auto.
unfold FtoRradix in H'2; rewrite H'2; ring.
Qed.
Theorem MKnuth2 :
∀ p q : float,
(Rabs q ≤ Rabs p)%R →
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1.
apply MKnuth; auto.
apply (MDekker b precision); auto.
Qed.
Theorem IminusOp :
∀ p q : float, Fopp (Iminus p q) = Iminus (Fopp p) (Fopp q).
intros p q; repeat rewrite IminusPlus; repeat rewrite <- IplusOp; auto.
Qed.
Theorem MKnuthOpp :
∀ p q : float,
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) =
Fopp
(Iplus
(Iminus (Fopp p)
(Iminus (Iplus (Fopp p) (Fopp q))
(Iminus (Iplus (Fopp p) (Fopp q)) (Fopp p))))
(Iminus (Fopp q) (Iminus (Iplus (Fopp p) (Fopp q)) (Fopp p)))) :>R.
intros p q; repeat rewrite <- IplusOp || rewrite <- IminusOp;
rewrite Fopp_Fopp; auto.
Qed.
Theorem MKnuth3 :
∀ p q : float,
(0 ≤ q)%R →
(q ≤ radix × - p)%R →
(- p ≤ q)%R →
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1 H'2 H'3.
apply MKnuth; auto.
cut (FtoRradix (Iplus p q) = (p + q)%R :>R); [ intros Eq1 | idtac ].
apply IminusCorrectEq with (pq := q); auto.
rewrite Eq1; ring.
rewrite Eq1; ring.
apply IplusCorrectEq with (pq := Fminus radix q (Fopp p)); auto.
apply Sterbenz; auto with float.
2: repeat rewrite (Fopp_correct radix); auto.
2: rewrite (Fminus_correct radix); repeat rewrite (Fopp_correct radix);
unfold FtoRradix in |- *; auto; ring; ring.
2: rewrite (Fminus_correct radix); repeat rewrite (Fopp_correct radix);
unfold FtoRradix in |- *; auto; ring; ring.
apply Rle_trans with (2 := H'1).
apply Rmult_le_reg_l with (r := IZR radix); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith;
rewrite Rmult_1_l.
rewrite (Fopp_correct radix).
apply Rle_trans with (1 := H'1); auto.
Qed.
Theorem MKnuth4 :
∀ p q : float,
(0 < - p)%R →
(0 < q)%R →
(radix × - p < q)%R →
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1 H'2 H'3.
cut (/ radix × q ≤ Iplus p q)%R; [ intros Rle1 | idtac ].
cut (Iplus p q ≤ Iminus (Iplus p q) p)%R; [ intros Rle2 | idtac ].
cut (Iminus (Iplus p q) p ≤ radix × Iplus p q)%R; [ intros Rle3 | idtac ].
cut (radix × Iplus p q ≤ radix × q)%R; [ intros Rle4 | idtac ].
apply MKnuth1; auto with float.
apply IminusCorrectEq with (pq := Fminus radix q (Iminus (Iplus p q) p));
auto with float.
rewrite <- (Fopp_Fopp (Fminus radix q (Iminus (Iplus p q) p))).
apply oppBounded.
rewrite Fopp_Fminus.
apply Sterbenz; auto.
apply Rle_trans with (1 := Rle1); auto.
apply Rle_trans with (1 := Rle3); auto.
apply sym_eq; apply (Fminus_correct radix); auto.
apply sym_eq; apply (Fminus_correct radix); auto.
apply
IminusCorrectEq with (pq := Fminus radix (Iplus p q) (Iminus (Iplus p q) p));
auto.
rewrite <- (Fopp_Fopp (Fminus radix (Iplus p q) (Iminus (Iplus p q) p))).
apply oppBounded.
rewrite Fopp_Fminus.
apply Sterbenz; auto.
apply Rle_trans with (2 := Rle2); auto.
apply Rmult_le_reg_l with (r := IZR radix); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith;
rewrite Rmult_1_l.
apply Rledouble.
apply Rle_trans with (2 := Rle1).
apply Rmult_le_reg_l with (r := IZR radix); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real zarith;
rewrite Rmult_1_l; rewrite Rmult_0_r; apply Rlt_le;
auto.
apply sym_eq; apply (Fminus_correct radix); auto.
apply sym_eq; apply (Fminus_correct radix); auto.
apply Rmult_le_reg_l with (r := (/ radix)%R); auto with real.
repeat rewrite <- Rmult_assoc; repeat rewrite Rinv_l; auto with real zarith;
repeat rewrite Rmult_1_l; auto with real.
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp (p + q)%R q); auto.
apply Rplus_lt_reg_r with (r := (- q)%R); auto.
replace (- q + (p + q))%R with (- - p)%R; [ idtac | ring ].
replace (- q + q)%R with (-0)%R; [ auto with real | ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply ClosestMonotone; auto.
apply
(RoundedModeMult b radix)
with (P := Closest b radix) (r := (Iplus p q - p)%R);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply Rplus_le_reg_l with (r := (- Iplus p q)%R); auto.
replace (- Iplus p q + (Iplus p q - p))%R with (- p)%R; [ idtac | ring ].
replace (- FtoRradix (Iplus p q) + radix × FtoR radix (Iplus p q))%R with
(FtoRradix (Iplus p q));
[ idtac | unfold FtoRradix in |- *; simpl in |- *; ring; ring ].
rewrite <- (Fopp_correct radix); auto.
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp (Fopp p) (p + q)%R); auto.
rewrite (Fopp_correct radix); auto.
apply Rplus_lt_reg_r with (r := (- p)%R); auto.
replace (- p + - FtoR radix p)%R with (radix × - p)%R;
[ idtac | simpl in |- *; fold FtoRradix; ring ].
replace (- p + (p + q))%R with (FtoRradix q); [ auto | simpl in |- *; ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply oppBounded; auto.
apply ClosestMonotone; auto.
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp (Iplus p q) (Iplus p q - p)%R); auto.
apply Rplus_lt_reg_r with (r := (- Iplus p q)%R); auto.
replace (- Iplus p q + Iplus p q)%R with 0%R; [ auto | simpl in |- *; ring ].
replace (- Iplus p q + (Iplus p q - p))%R with (- p)%R;
[ auto | simpl in |- *; ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply ClosestMonotone; auto.
apply (FmultRadixInv b radix precision) with (y := (p + q)%R); auto.
apply Rmult_lt_reg_l with (r := IZR radix); auto with real.
repeat rewrite <- Rmult_assoc; repeat rewrite Rinv_r; auto with real arith;
repeat rewrite Rmult_1_l; auto.
apply Rplus_lt_reg_r with (r := (- q)%R); auto.
apply Rplus_lt_reg_r with (r := (radix × - p)%R); auto.
replace (radix × - p + (- q + FtoR radix q))%R with (radix × - p)%R;
[ auto | unfold FtoRradix in |- *; simpl in |- *; ring ].
replace (radix × - p + (- q + radix × (p + q)))%R with (FtoRradix q);
[ auto | simpl in |- *; ring ].
Qed.
Theorem MKnuth5 :
∀ p q : float,
(0 < p)%R →
(p < q)%R →
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1 H'2.
cut
(Iminus (Iplus p q) (Iminus (Iplus p q) p) =
(Iplus p q - Iminus (Iplus p q) p)%R :>R); [ intros Eq1 | idtac ].
apply MKnuth1; auto.
cut (Iminus (Iplus p q) p ≤ Iplus p q)%R; [ intros Rle1 | idtac ].
cut (Iplus p q ≤ radix × q)%R; [ intros Rle2 | idtac ].
case (Rle_or_lt q (Iminus (Iplus p q) p)); intros Rle3.
apply IminusCorrectEq with (pq := Fminus radix q (Iminus (Iplus p q) p));
auto with float.
rewrite <- (Fopp_Fopp (Fminus radix q (Iminus (Iplus p q) p))).
apply oppBounded.
rewrite Fopp_Fminus.
apply Sterbenz; auto.
apply Rle_trans with (2 := Rle3); auto.
apply Rmult_le_reg_l with (r := IZR radix); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith;
rewrite Rmult_1_l.
apply Rledouble.
apply Rlt_le; apply Rlt_trans with (1 := H'); auto.
apply Rle_trans with (1 := Rle1); auto.
apply sym_eq; apply (Fminus_correct radix); auto.
apply sym_eq; apply (Fminus_correct radix); auto.
case
(ExactMinusInterval b radix precision)
with
(P := Closest b radix)
(p := Iminus (Iplus p q) p)
(q := Iplus p q)
(r := q); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply
(RleRoundedR0 b radix precision)
with (P := Closest b radix) (r := (Iplus p q - p)%R);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply Rplus_le_reg_l with (r := FtoRradix p); auto.
replace (p + 0)%R with (FtoRradix p); [ idtac | ring ].
replace (p + (Iplus p q - p))%R with (FtoRradix (Iplus p q));
[ idtac | ring ].
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp p (p + q)%R); auto.
apply Rplus_lt_reg_r with (r := (- p)%R); auto.
replace (- p + p)%R with 0%R; [ idtac | ring ].
replace (- p + (p + q))%R with (FtoRradix q);
[ apply Rlt_trans with (1 := H'); auto | ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply ClosestMonotone; auto.
∃ (Iminus (Iplus p q) (Iminus (Iplus p q) p)); split; auto.
apply Rlt_le; auto.
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp q (p + q)%R); auto.
apply Rplus_lt_reg_r with (r := (- q)%R); auto.
replace (- q + q)%R with 0%R; [ idtac | ring ].
replace (- q + (p + q))%R with (FtoRradix p); [ auto | ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply ClosestMonotone; auto.
intros x H'4; elim H'4; intros H'5 H'6; clear H'4.
apply IminusCorrectEq with (pq := x); auto.
apply (RoundedModeMult b radix) with (P := Closest b radix) (r := (p + q)%R);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply Rplus_le_reg_l with (r := (- q)%R); auto.
replace (- q + (p + q))%R with (FtoRradix p); [ idtac | ring ].
replace (- FtoRradix q + radix × FtoR radix q)%R with (FtoRradix q);
[ apply Rlt_le; auto | unfold FtoRradix in |- *; simpl in |- *; ring ].
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp (Iplus p q - p)%R (Iplus p q)); auto.
apply Rplus_lt_reg_r with (r := (- Iplus p q)%R); auto.
replace (- Iplus p q + (Iplus p q - p))%R with (- p)%R; [ idtac | ring ].
replace (- Iplus p q + Iplus p q)%R with (-0)%R; [ auto with real | ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply ClosestMonotone; auto.
case
(minusRoundRep b radix precision)
with
(P := Closest b radix)
(p := p)
(q := Iplus p q)
(qmp := Iminus (Iplus p q) p); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply Rlt_le; auto.
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp (FtoRradix p) (p + q)%R); auto.
apply Rplus_lt_reg_r with (r := (- p)%R); auto.
replace (- p + p)%R with 0%R; [ idtac | ring ].
replace (- p + (p + q))%R with (FtoRradix q);
[ apply Rlt_trans with (1 := H'); auto | ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply ClosestMonotone; auto.
intros x H'4; elim H'4; intros H'5 H'6; clear H'4; auto with float.
apply IminusCorrectEq with (pq := x); auto.
Qed.
Theorem MKnuth6 :
∀ p q : float,
Iplus p q = (p + q)%R :>R →
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1.
apply MKnuth; auto.
apply IminusCorrectEq with (pq := q); auto.
rewrite H'; ring.
rewrite H'; ring.
Qed.
Theorem MKnuth7 :
∀ p q : float,
(Rabs p < q)%R →
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1.
cut (0 < q)%R;
[ intros Rlt1 | apply Rle_lt_trans with (2 := H'); auto with real ].
case (Rle_or_lt 0 p); intros Rle1; [ Casec Rle1; intros Rle1 | idtac ].
apply MKnuth5; auto.
rewrite <- (Rabs_right p); auto with real; apply Rle_ge; apply Rlt_le; auto.
apply MKnuth6; auto.
apply IplusCorrectEq with (pq := q); auto; rewrite <- Rle1; ring.
case (Rle_or_lt q (radix × - p)); intros Rle2.
apply MKnuth3; auto.
apply Rlt_le; auto.
rewrite <- (Faux.Rabsolu_left1 p); auto; apply Rlt_le; auto.
apply MKnuth4; auto.
replace 0%R with (-0)%R; [ auto with real | ring ].
Qed.
Theorem Knuth :
∀ p q : float,
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0; case (Rle_or_lt (Rabs q) (Rabs p)); intros Rle1.
apply MKnuth2; auto.
case (Rle_or_lt 0 q); intros Rle2.
apply MKnuth7; auto.
rewrite <- (Rabs_right q); auto with real; apply Rle_ge; apply Rlt_le; auto.
rewrite MKnuthOpp.
rewrite (Fopp_correct radix).
replace (p + q - Iplus p q)%R with
(- (Fopp p + Fopp q - Iplus (Fopp p) (Fopp q)))%R.
cut (∀ x y : R, x = y → (- x)%R = (- y)%R);
[ intros tmp; apply tmp; clear tmp | intros x y tmp; rewrite tmp; auto ].
apply MKnuth7; auto with float.
repeat rewrite (Fopp_correct radix); auto.
rewrite <- (Faux.Rabsolu_left1 (FtoR radix q)); try apply Rlt_le; auto.
rewrite Rabs_Ropp; auto.
rewrite <- IplusOp; repeat rewrite (Fopp_correct radix);
unfold FtoRradix in |- *; ring.
Qed.
End EFast.
Section EFast.
Variable b : Fbound.
Variable precision : nat.
Let radix := 2%Z.
Let TMTO : (1 < radix)%Z := TwoMoreThanOne.
Hint Resolve TMTO: zarith.
Coercion Local FtoRradix := FtoR radix.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
Variable Iplus : float → float → float.
Hypothesis
IplusCorrect :
∀ p q : float,
Fbounded b p → Fbounded b q → Closest b radix (p + q) (Iplus p q).
Hypothesis
IplusComp :
∀ p q r s : float,
Fbounded b p →
Fbounded b q →
Fbounded b r →
Fbounded b s → p = r :>R → q = s :>R → Iplus p q = Iplus r s :>R.
Hypothesis IplusSym : ∀ p q : float, Iplus p q = Iplus q p.
Hypothesis
IplusOp : ∀ p q : float, Fopp (Iplus p q) = Iplus (Fopp p) (Fopp q).
Variable Iminus : float → float → float.
Hypothesis IminusPlus : ∀ p q : float, Iminus p q = Iplus p (Fopp q).
Theorem IplusOl :
∀ p q : float,
Fbounded b p → Fbounded b q → p = 0%R :>R → Iplus p q = q :>R.
intros p q H' H'0 H'1.
rewrite IplusSym.
apply (IplusOr b); auto.
Qed.
Let IminusCorrect := IminusCorrect b Iplus IplusCorrect Iminus IminusPlus.
Let IplusBounded := IplusBounded b Iplus IplusCorrect.
Let IminusBounded := IminusBounded b Iplus IplusCorrect Iminus IminusPlus.
Let IminusId := IminusId b Iplus IplusCorrect Iminus IminusPlus.
Theorem MKnuth :
∀ p q : float,
Fbounded b p →
Fbounded b q →
Iminus (Iplus p q) p = (Iplus p q - p)%R :>R →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1.
rewrite IplusOl; auto with float.
case
(errorBoundedPlus b radix precision)
with (p := p) (q := q) (pq := Iplus p q); auto.
intros x H'2; elim H'2; intros H'3 H'4; elim H'4; intros H'5 H'6;
clear H'4 H'2.
unfold FtoRradix in |- *; rewrite <- H'3.
apply sym_eq; apply (ClosestIdem b); auto.
apply
(ClosestCompatible b radix (q - Iminus (Iplus p q) p)%R (
FtoR radix x) (Iminus q (Iminus (Iplus p q) p)));
auto.
rewrite H'3.
rewrite H'1.
unfold FtoRradix in |- *; ring; ring.
replace 0%R with (FtoRradix (Iminus p p)).
repeat rewrite IminusPlus; apply IplusComp; repeat rewrite <- IminusPlus;
auto with float.
unfold FtoRradix in |- *; repeat rewrite Fopp_correct.
replace (FtoR radix (Iminus (Iplus p q) (Iminus (Iplus p q) p))) with
(FtoR radix p); auto.
apply (ClosestIdem b); auto.
apply
(ClosestCompatible b radix (Iplus p q - Iminus (Iplus p q) p)%R
(FtoR radix p) (Iminus (Iplus p q) (Iminus (Iplus p q) p)));
auto.
rewrite H'1; auto.
unfold FtoRradix in |- *; ring; ring.
apply IminusId; auto.
Qed.
Theorem IplusCorrectEq :
∀ (p q pq : float) (r : R),
Fbounded b p →
Fbounded b q →
Fbounded b pq → r = pq :>R → (p + q)%R = pq :>R → Iplus p q = r :>R.
intros p q pq r H' H'0 H'1 H'2 H'3; rewrite H'2.
unfold FtoRradix in |- *; apply sym_eq; apply (ClosestIdem b radix); auto.
apply (ClosestCompatible b radix (p + q)%R pq (Iplus p q)); auto.
Qed.
Theorem IminusCorrectEq :
∀ (p q pq : float) (r : R),
Fbounded b p →
Fbounded b q →
Fbounded b pq → r = pq :>R → (p - q)%R = pq :>R → Iminus p q = r :>R.
intros p q pq r H' H'0 H'1 H'2 H'3; rewrite H'2.
unfold FtoRradix in |- *; apply sym_eq; apply (ClosestIdem b radix); auto.
apply (ClosestCompatible b radix (p - q)%R pq (Iminus p q)); auto.
Qed.
Theorem Iminus2Exact :
∀ p q : float,
(0 ≤ p)%R →
(p ≤ q)%R →
Fbounded b p →
Fbounded b q → Iminus q (Iminus q p) = (q - Iminus q p)%R :>R.
intros p q H' H'0 H'1 H'2.
case
(minusRoundRep b radix precision)
with (P := Closest b radix) (p := p) (q := q) (qmp := Iminus q p);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
intros pq H'3; elim H'3; intros H'4 H'5; clear H'3.
apply IminusCorrectEq with (pq := pq); auto.
Qed.
Theorem MKnuth1 :
∀ p q : float,
Fbounded b p →
Fbounded b q →
Iminus q (Iminus (Iplus p q) p) = (q - Iminus (Iplus p q) p)%R :>R →
Iminus (Iplus p q) (Iminus (Iplus p q) p) =
(Iplus p q - Iminus (Iplus p q) p)%R :>R →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1 H'2.
cut
(Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)) =
(p - Iminus (Iplus p q) (Iminus (Iplus p q) p))%R :>R);
[ intros H'3 | idtac ].
case
(errorBoundedPlus b radix precision)
with (p := p) (q := q) (pq := Iplus p q); auto.
intros pq H'4; elim H'4; intros H'5 H'6; elim H'6; intros H'7 H'8;
clear H'6 H'4.
apply IplusCorrectEq with (pq := pq); auto.
repeat rewrite H'3; repeat rewrite H'2; repeat rewrite H'1.
unfold FtoRradix in |- *; rewrite H'5.
ring.
rewrite H'2.
case
(errorBoundedPlus b radix precision)
with (p := Iplus p q) (q := Fopp p) (pq := Iminus (Iplus p q) p);
auto with float.
apply
(ClosestCompatible b radix (Iplus p q - p)%R (Iplus p q + Fopp p)%R
(Iminus (Iplus p q) p)); auto.
rewrite (Fopp_correct radix); auto.
intros pq H'3; elim H'3; intros H'4 H'5; elim H'5; intros H'6 H'7;
clear H'5 H'3.
rewrite (IminusPlus p); apply IplusCorrectEq with (pq := Fopp pq);
auto with float.
unfold FtoRradix in |- *; rewrite (Fopp_correct radix); auto; rewrite H'4;
rewrite (Fopp_correct radix); auto; ring; ring.
unfold FtoRradix in |- *; repeat rewrite (Fopp_correct radix); auto;
rewrite H'4; rewrite (Fopp_correct radix); auto.
unfold FtoRradix in H'2; rewrite H'2; ring.
Qed.
Theorem MKnuth2 :
∀ p q : float,
(Rabs q ≤ Rabs p)%R →
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1.
apply MKnuth; auto.
apply (MDekker b precision); auto.
Qed.
Theorem IminusOp :
∀ p q : float, Fopp (Iminus p q) = Iminus (Fopp p) (Fopp q).
intros p q; repeat rewrite IminusPlus; repeat rewrite <- IplusOp; auto.
Qed.
Theorem MKnuthOpp :
∀ p q : float,
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) =
Fopp
(Iplus
(Iminus (Fopp p)
(Iminus (Iplus (Fopp p) (Fopp q))
(Iminus (Iplus (Fopp p) (Fopp q)) (Fopp p))))
(Iminus (Fopp q) (Iminus (Iplus (Fopp p) (Fopp q)) (Fopp p)))) :>R.
intros p q; repeat rewrite <- IplusOp || rewrite <- IminusOp;
rewrite Fopp_Fopp; auto.
Qed.
Theorem MKnuth3 :
∀ p q : float,
(0 ≤ q)%R →
(q ≤ radix × - p)%R →
(- p ≤ q)%R →
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1 H'2 H'3.
apply MKnuth; auto.
cut (FtoRradix (Iplus p q) = (p + q)%R :>R); [ intros Eq1 | idtac ].
apply IminusCorrectEq with (pq := q); auto.
rewrite Eq1; ring.
rewrite Eq1; ring.
apply IplusCorrectEq with (pq := Fminus radix q (Fopp p)); auto.
apply Sterbenz; auto with float.
2: repeat rewrite (Fopp_correct radix); auto.
2: rewrite (Fminus_correct radix); repeat rewrite (Fopp_correct radix);
unfold FtoRradix in |- *; auto; ring; ring.
2: rewrite (Fminus_correct radix); repeat rewrite (Fopp_correct radix);
unfold FtoRradix in |- *; auto; ring; ring.
apply Rle_trans with (2 := H'1).
apply Rmult_le_reg_l with (r := IZR radix); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith;
rewrite Rmult_1_l.
rewrite (Fopp_correct radix).
apply Rle_trans with (1 := H'1); auto.
Qed.
Theorem MKnuth4 :
∀ p q : float,
(0 < - p)%R →
(0 < q)%R →
(radix × - p < q)%R →
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1 H'2 H'3.
cut (/ radix × q ≤ Iplus p q)%R; [ intros Rle1 | idtac ].
cut (Iplus p q ≤ Iminus (Iplus p q) p)%R; [ intros Rle2 | idtac ].
cut (Iminus (Iplus p q) p ≤ radix × Iplus p q)%R; [ intros Rle3 | idtac ].
cut (radix × Iplus p q ≤ radix × q)%R; [ intros Rle4 | idtac ].
apply MKnuth1; auto with float.
apply IminusCorrectEq with (pq := Fminus radix q (Iminus (Iplus p q) p));
auto with float.
rewrite <- (Fopp_Fopp (Fminus radix q (Iminus (Iplus p q) p))).
apply oppBounded.
rewrite Fopp_Fminus.
apply Sterbenz; auto.
apply Rle_trans with (1 := Rle1); auto.
apply Rle_trans with (1 := Rle3); auto.
apply sym_eq; apply (Fminus_correct radix); auto.
apply sym_eq; apply (Fminus_correct radix); auto.
apply
IminusCorrectEq with (pq := Fminus radix (Iplus p q) (Iminus (Iplus p q) p));
auto.
rewrite <- (Fopp_Fopp (Fminus radix (Iplus p q) (Iminus (Iplus p q) p))).
apply oppBounded.
rewrite Fopp_Fminus.
apply Sterbenz; auto.
apply Rle_trans with (2 := Rle2); auto.
apply Rmult_le_reg_l with (r := IZR radix); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith;
rewrite Rmult_1_l.
apply Rledouble.
apply Rle_trans with (2 := Rle1).
apply Rmult_le_reg_l with (r := IZR radix); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real zarith;
rewrite Rmult_1_l; rewrite Rmult_0_r; apply Rlt_le;
auto.
apply sym_eq; apply (Fminus_correct radix); auto.
apply sym_eq; apply (Fminus_correct radix); auto.
apply Rmult_le_reg_l with (r := (/ radix)%R); auto with real.
repeat rewrite <- Rmult_assoc; repeat rewrite Rinv_l; auto with real zarith;
repeat rewrite Rmult_1_l; auto with real.
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp (p + q)%R q); auto.
apply Rplus_lt_reg_r with (r := (- q)%R); auto.
replace (- q + (p + q))%R with (- - p)%R; [ idtac | ring ].
replace (- q + q)%R with (-0)%R; [ auto with real | ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply ClosestMonotone; auto.
apply
(RoundedModeMult b radix)
with (P := Closest b radix) (r := (Iplus p q - p)%R);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply Rplus_le_reg_l with (r := (- Iplus p q)%R); auto.
replace (- Iplus p q + (Iplus p q - p))%R with (- p)%R; [ idtac | ring ].
replace (- FtoRradix (Iplus p q) + radix × FtoR radix (Iplus p q))%R with
(FtoRradix (Iplus p q));
[ idtac | unfold FtoRradix in |- *; simpl in |- *; ring; ring ].
rewrite <- (Fopp_correct radix); auto.
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp (Fopp p) (p + q)%R); auto.
rewrite (Fopp_correct radix); auto.
apply Rplus_lt_reg_r with (r := (- p)%R); auto.
replace (- p + - FtoR radix p)%R with (radix × - p)%R;
[ idtac | simpl in |- *; fold FtoRradix; ring ].
replace (- p + (p + q))%R with (FtoRradix q); [ auto | simpl in |- *; ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply oppBounded; auto.
apply ClosestMonotone; auto.
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp (Iplus p q) (Iplus p q - p)%R); auto.
apply Rplus_lt_reg_r with (r := (- Iplus p q)%R); auto.
replace (- Iplus p q + Iplus p q)%R with 0%R; [ auto | simpl in |- *; ring ].
replace (- Iplus p q + (Iplus p q - p))%R with (- p)%R;
[ auto | simpl in |- *; ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply ClosestMonotone; auto.
apply (FmultRadixInv b radix precision) with (y := (p + q)%R); auto.
apply Rmult_lt_reg_l with (r := IZR radix); auto with real.
repeat rewrite <- Rmult_assoc; repeat rewrite Rinv_r; auto with real arith;
repeat rewrite Rmult_1_l; auto.
apply Rplus_lt_reg_r with (r := (- q)%R); auto.
apply Rplus_lt_reg_r with (r := (radix × - p)%R); auto.
replace (radix × - p + (- q + FtoR radix q))%R with (radix × - p)%R;
[ auto | unfold FtoRradix in |- *; simpl in |- *; ring ].
replace (radix × - p + (- q + radix × (p + q)))%R with (FtoRradix q);
[ auto | simpl in |- *; ring ].
Qed.
Theorem MKnuth5 :
∀ p q : float,
(0 < p)%R →
(p < q)%R →
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1 H'2.
cut
(Iminus (Iplus p q) (Iminus (Iplus p q) p) =
(Iplus p q - Iminus (Iplus p q) p)%R :>R); [ intros Eq1 | idtac ].
apply MKnuth1; auto.
cut (Iminus (Iplus p q) p ≤ Iplus p q)%R; [ intros Rle1 | idtac ].
cut (Iplus p q ≤ radix × q)%R; [ intros Rle2 | idtac ].
case (Rle_or_lt q (Iminus (Iplus p q) p)); intros Rle3.
apply IminusCorrectEq with (pq := Fminus radix q (Iminus (Iplus p q) p));
auto with float.
rewrite <- (Fopp_Fopp (Fminus radix q (Iminus (Iplus p q) p))).
apply oppBounded.
rewrite Fopp_Fminus.
apply Sterbenz; auto.
apply Rle_trans with (2 := Rle3); auto.
apply Rmult_le_reg_l with (r := IZR radix); auto with real.
rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith;
rewrite Rmult_1_l.
apply Rledouble.
apply Rlt_le; apply Rlt_trans with (1 := H'); auto.
apply Rle_trans with (1 := Rle1); auto.
apply sym_eq; apply (Fminus_correct radix); auto.
apply sym_eq; apply (Fminus_correct radix); auto.
case
(ExactMinusInterval b radix precision)
with
(P := Closest b radix)
(p := Iminus (Iplus p q) p)
(q := Iplus p q)
(r := q); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply
(RleRoundedR0 b radix precision)
with (P := Closest b radix) (r := (Iplus p q - p)%R);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply Rplus_le_reg_l with (r := FtoRradix p); auto.
replace (p + 0)%R with (FtoRradix p); [ idtac | ring ].
replace (p + (Iplus p q - p))%R with (FtoRradix (Iplus p q));
[ idtac | ring ].
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp p (p + q)%R); auto.
apply Rplus_lt_reg_r with (r := (- p)%R); auto.
replace (- p + p)%R with 0%R; [ idtac | ring ].
replace (- p + (p + q))%R with (FtoRradix q);
[ apply Rlt_trans with (1 := H'); auto | ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply ClosestMonotone; auto.
∃ (Iminus (Iplus p q) (Iminus (Iplus p q) p)); split; auto.
apply Rlt_le; auto.
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp q (p + q)%R); auto.
apply Rplus_lt_reg_r with (r := (- q)%R); auto.
replace (- q + q)%R with 0%R; [ idtac | ring ].
replace (- q + (p + q))%R with (FtoRradix p); [ auto | ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply ClosestMonotone; auto.
intros x H'4; elim H'4; intros H'5 H'6; clear H'4.
apply IminusCorrectEq with (pq := x); auto.
apply (RoundedModeMult b radix) with (P := Closest b radix) (r := (p + q)%R);
auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply Rplus_le_reg_l with (r := (- q)%R); auto.
replace (- q + (p + q))%R with (FtoRradix p); [ idtac | ring ].
replace (- FtoRradix q + radix × FtoR radix q)%R with (FtoRradix q);
[ apply Rlt_le; auto | unfold FtoRradix in |- *; simpl in |- *; ring ].
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp (Iplus p q - p)%R (Iplus p q)); auto.
apply Rplus_lt_reg_r with (r := (- Iplus p q)%R); auto.
replace (- Iplus p q + (Iplus p q - p))%R with (- p)%R; [ idtac | ring ].
replace (- Iplus p q + Iplus p q)%R with (-0)%R; [ auto with real | ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply ClosestMonotone; auto.
case
(minusRoundRep b radix precision)
with
(P := Closest b radix)
(p := p)
(q := Iplus p q)
(qmp := Iminus (Iplus p q) p); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply Rlt_le; auto.
cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ].
apply (Cp (FtoRradix p) (p + q)%R); auto.
apply Rplus_lt_reg_r with (r := (- p)%R); auto.
replace (- p + p)%R with 0%R; [ idtac | ring ].
replace (- p + (p + q))%R with (FtoRradix q);
[ apply Rlt_trans with (1 := H'); auto | ring ].
apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto.
apply ClosestRoundedModeP with (precision := precision); auto.
apply ClosestMonotone; auto.
intros x H'4; elim H'4; intros H'5 H'6; clear H'4; auto with float.
apply IminusCorrectEq with (pq := x); auto.
Qed.
Theorem MKnuth6 :
∀ p q : float,
Iplus p q = (p + q)%R :>R →
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1.
apply MKnuth; auto.
apply IminusCorrectEq with (pq := q); auto.
rewrite H'; ring.
rewrite H'; ring.
Qed.
Theorem MKnuth7 :
∀ p q : float,
(Rabs p < q)%R →
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0 H'1.
cut (0 < q)%R;
[ intros Rlt1 | apply Rle_lt_trans with (2 := H'); auto with real ].
case (Rle_or_lt 0 p); intros Rle1; [ Casec Rle1; intros Rle1 | idtac ].
apply MKnuth5; auto.
rewrite <- (Rabs_right p); auto with real; apply Rle_ge; apply Rlt_le; auto.
apply MKnuth6; auto.
apply IplusCorrectEq with (pq := q); auto; rewrite <- Rle1; ring.
case (Rle_or_lt q (radix × - p)); intros Rle2.
apply MKnuth3; auto.
apply Rlt_le; auto.
rewrite <- (Faux.Rabsolu_left1 p); auto; apply Rlt_le; auto.
apply MKnuth4; auto.
replace 0%R with (-0)%R; [ auto with real | ring ].
Qed.
Theorem Knuth :
∀ p q : float,
Fbounded b p →
Fbounded b q →
Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p)))
(Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
intros p q H' H'0; case (Rle_or_lt (Rabs q) (Rabs p)); intros Rle1.
apply MKnuth2; auto.
case (Rle_or_lt 0 q); intros Rle2.
apply MKnuth7; auto.
rewrite <- (Rabs_right q); auto with real; apply Rle_ge; apply Rlt_le; auto.
rewrite MKnuthOpp.
rewrite (Fopp_correct radix).
replace (p + q - Iplus p q)%R with
(- (Fopp p + Fopp q - Iplus (Fopp p) (Fopp q)))%R.
cut (∀ x y : R, x = y → (- x)%R = (- y)%R);
[ intros tmp; apply tmp; clear tmp | intros x y tmp; rewrite tmp; auto ].
apply MKnuth7; auto with float.
repeat rewrite (Fopp_correct radix); auto.
rewrite <- (Faux.Rabsolu_left1 (FtoR radix q)); try apply Rlt_le; auto.
rewrite Rabs_Ropp; auto.
rewrite <- IplusOp; repeat rewrite (Fopp_correct radix);
unfold FtoRradix in |- *; ring.
Qed.
End EFast.