Fast2Sum.v

(****************************************************************************                                                                                         IEEE754  :  Fast2Sum                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export Closest2Plus.
Section Fast.
Variable b:Fbound.
Variable precision:nat.

Local FtoRradix := (FtoR (2)).
Coercion FtoRradix : float >-> R.
Hypothesis precisionGreaterThanOne:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp (2) precision) (1)).
Variable Iplus:float -> float ->float.
Hypothesis IplusCorrect:
           (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
           (Closest b (2) (Rplus p q) (Iplus p q)).
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 IminusCorrect:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
  (Closest b (2) (Rminus p q) (Iminus p q)).
Intros p q H' H'0.
Rewrite IminusPlus.
Unfold Rminus.
Unfold FtoRradix; Rewrite <- Fopp_correct.
Apply IplusCorrect; Auto.
Apply oppBounded; Auto.
Qed.
Hints Resolve IminusCorrect.

Theorem ErrorBoundedIplus:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) ->
  (Ex [error:float]
  <R> error==(Rminus (Rplus p q) (Iplus p q)) /\ (Fbounded b error)).
Intros p q H' H'0.
Case (errorBoundedPlus b (2) precision) with p := p q := q pq := (Iplus p q);
Auto.
Intros x H'1; Elim H'1; Intros H'2 H'3; Elim H'3; Intros H'4 H'5; Exists x; Auto.
Qed.

Theorem IplusOr:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> <R> q==R0 ->
  <R> (Iplus p q)==p.
Intros p q H' H'0 H'1.
Cut (Closest b (2) (Rplus p q) (Iplus p q)); Auto.
Rewrite H'1.
AutoRewrite [Rsimpl].
Intros H'2; Apply sym_eqT.
Unfold FtoRradix; Apply (ClosestIdem b (2)); Auto.
Qed.

Theorem IminusId:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> <R> p==q ->
  <R> (Iminus p q)==R0.
Intros p q H' H'0 H'1.
Cut (Closest b (2) (Rminus p q) (Iminus p q)); Auto.
Replace (Rminus p q) with R0; [Idtac | Rewrite <- H'1; Ring].
Replace R0 with (FtoRradix (Fzero (Zopp (dExp b)))).
Intros H'2; Apply sym_eqT.
Unfold FtoRradix; Apply (ClosestIdem b (2)); Auto.
Apply FboundedFzero; Auto.
Unfold Fzero FtoRradix FtoR; Simpl; Ring.
Qed.

Theorem IminusOl:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> <R> p==R0 ->
  <R> (Iminus p q)==(Ropp q).
Intros p q H' H'0 H'1.
Cut (Closest b (2) (Rminus p q) (Iminus p q)); Auto.
Rewrite H'1.
Replace (Rminus R0 q) with (FtoRradix (Fopp q)).
Intros H'2; Apply sym_eqT.
Unfold FtoRradix; Rewrite <- Fopp_correct; Apply (ClosestIdem b (2)); Auto.
Apply oppBounded; Auto.
Unfold FtoRradix; Rewrite Fopp_correct; Auto; Ring.
Qed.

Theorem IplusBounded:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) ->(Fbounded b (Iplus p q)).
Intros p q H' H'0; Cut (Closest b (2) (Rplus p q) (Iplus p q)); Auto; Intuition.
Qed.

Theorem IminusBounded:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) ->(Fbounded b (Iminus p q)).
Intros p q H' H'0; Cut (Closest b (2) (Rminus p q) (Iminus p q)); Auto;
Intuition.
Qed.

Theorem IminusInv:
  (p, q, r, s:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Fbounded b r) -> (Fbounded b s) -> <R> p==s -> <R> r==(Rminus s q) ->
  <R> (Iminus p q)==r.
Intros p q r s H' H'0 H'1 H'2 H'3 H'4.
Cut (Closest b (2) (Rminus p q) (Iminus p q)); Auto.
Rewrite H'3.
Rewrite <- H'4.
Intros H'5; Apply sym_eqT.
Unfold FtoRradix; Apply (ClosestIdem b (2)); Auto.
Qed.

Theorem IminusFminus:
  (p, q:float)
  (Fbounded b p) -> (Fbounded b q) -> (Fbounded b (Fminus (2) p q)) ->
  <R> (Iminus p q)==(Fminus (2) p q).
Intros p q H' H'0 H'1.
Cut (Closest b (2) (Rminus p q) (Iminus p q)); Auto.
Intros H'2.
Apply sym_eqT; Apply (ClosestIdem b (2)); Auto.
Rewrite Fminus_correct; Auto.
Qed.

Theorem MDekkerAux1:
  (p, q:float)
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p) ->
  (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus q (Iminus (Iplus p q) p))==(Rminus (Rplus p q) (Iplus p q)).
Intros p q H' H'0 H'1.
Elim (ErrorBoundedIplus p q);
[Intros error E; Elim E; Intros H'7 H'8; Clear E | Idtac | Idtac]; Auto.
Cut (Closest
       b (2) (Rminus q (Iminus (Iplus p q) p)) (Iminus q (Iminus (Iplus p q) p)));
Auto.
Rewrite H'.
Replace (Rminus q (Rminus (Iplus p q) p)) with (Rminus (Rplus p q) (Iplus p q));
[Idtac | Ring].
Rewrite <- H'7.
Intros H'2.
Apply sym_eqT; Apply (ClosestIdem b (2)); Auto.
Apply IminusCorrect; Auto.
Apply IminusBounded; Auto.
Apply IplusBounded; Auto.
Qed.

Theorem MDekkerAux2:
  (p, q:float)
  <R> (Iplus p q)==(Rplus p q) -> (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).
Intros p q H' H'0 H'1.
Cut (Closest b (2) (Rminus (Iplus p q) p) (Iminus (Iplus p q) p)); Auto.
Repeat Rewrite H'.
Replace (Rminus (Rplus p q) p) with (FtoRradix q); [Idtac | Ring].
Intros H'2.
Apply sym_eqT; Apply (ClosestIdem b (2)); Auto.
Apply IminusCorrect; Auto.
Apply IplusBounded; Auto.
Qed.

Theorem MDekkerAux3:
  (p, q:float)
  (Fbounded b (Fplus (2) p q)) -> (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).
Intros p q H' H'0 H'1.
Apply MDekkerAux2; Auto.
Unfold FtoRradix; Rewrite <- Fplus_correct; Auto.
Apply sym_eqT; Apply (ClosestIdem b (2)); Auto.
Rewrite Fplus_correct; Auto.
Qed.

Theorem MDekkerAux4:
  (p, q:float)
  (Fbounded b (Fminus (2) (Iplus p q) p)) -> (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).
Intros p q H' H'0 H'1.
Unfold FtoRradix; Rewrite <- Fminus_correct; Auto.
Apply sym_eqT; Apply (ClosestIdem b (2)); Auto.
Rewrite Fminus_correct; Auto.
Apply IminusCorrect; Auto.
Apply IplusBounded; Auto.
Qed.

Theorem Dekker1:
  (p, q:float) (Rle R0 q) -> (Rle q p) -> (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).
Intros p q H' H'0 H'1 H'2.
Apply MDekkerAux4; Auto.
Apply oppBoundedInv; Auto.
Rewrite Fopp_Fminus; Auto.
Apply Sterbenz; Auto.
Apply IplusBounded; Auto.
Apply Rle_mult_anticompatibility with z := (INR (2)); Auto with real arith.
Rewrite <- Rmult_assoc; Rewrite Rinv_r; Auto with real arith; Rewrite Rmult_ne_r.
Apply (RoundedModeMult b (2)) with P := (Closest b (2)) r := (Rplus p q); Auto.
Apply ClosestRoundedModeP with precision := precision; Auto.
Replace (Rmult (2) (FtoR (2) p)) with (Rplus p p); [Idtac | Simpl; Ring];
Auto with real.
Case H'; Clear H'; Intros H'.
Apply Rle_mult_anticompatibility with z := (Rinv (2)); Auto with real.
Rewrite <- Rmult_assoc; Rewrite Rinv_l; Auto with real; Rewrite Rmult_ne_r.
Apply (FmultRadixInv b precision) with y := (Rplus p q); Auto.
Apply Rlt_mult_anticompatibility with z := (INR (2)); Auto with real.
Rewrite <- Rmult_assoc; Rewrite Rinv_r; Auto with real; Rewrite Rmult_ne_r.
Apply Rle_lt_trans with (Rmult (2) p).
Apply Rledouble; Auto.
(Apply Rlt_le; Apply Rlt_le_trans with (FtoRradix q)); Auto.
Apply Rlt_mult_anticompatibility with z := (Rinv (2)); Auto with real.
Repeat Rewrite <- Rmult_assoc; Repeat Rewrite Rinv_l; Auto with real;
Repeat Rewrite Rmult_ne_r.
Pattern 1 (FtoRradix p); Replace (FtoRradix p) with (Rplus p R0);
[Idtac | Ring]; Auto with real.
Apply Rlt_compatibility; Auto.
Rewrite IplusOr; Auto.
Apply Rledouble; Auto.
Rewrite H'; Auto.
Qed.

Theorem Dekker2:
  (p, q:float)
  (Rle R0 p) ->
  (Rle (Ropp q) p) ->
  (Rle p (Rmult (2) (Ropp q))) -> (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).
Intros p q H' H'0 H'1 H'2 H'3.
Apply MDekkerAux3; Auto.
Rewrite <- (Fopp_Fopp q).
Change (Fbounded b (Fminus (2) p (Fopp q))).
Apply Sterbenz; Auto.
Apply oppBounded; Auto.
Apply Rle_mult_anticompatibility with z := (INR (2)); Auto with real arith.
Rewrite <- Rmult_assoc; Rewrite Rinv_r; Auto with real arith;
Rewrite Rmult_ne_r; Auto.
Rewrite Fopp_correct; Auto.
Apply Rle_trans with (FtoRradix p); Auto.
Apply Rledouble; Auto.
Rewrite Fopp_correct; Auto.
Qed.

Theorem Dekker3:
  (p, q:float)
  (Rle q R0) ->
  (Rlt (Rmult (2) (Ropp q)) p) -> (Fbounded b p) -> (Fbounded b q) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).
Intros p q H' H'0 H'1 H'2.
Apply MDekkerAux4; Auto.
Apply Sterbenz; Auto.
Apply IplusBounded; Auto.
Apply (FmultRadixInv b precision) with y := (Rplus p q); Auto.
Apply Rlt_mult_anticompatibility with z := (INR (2)); Auto with real arith.
Rewrite <- Rmult_assoc; Rewrite Rinv_r; Auto with real arith; Rewrite Rmult_ne_r.
Replace (Rmult (2) (Rplus p q)) with (Rplus (Rmult (2) p) (Rmult (2) q));
[Idtac | Simpl; Ring].
Apply Rlt_anti_compatibility with r := (Ropp (FtoR (2) p)).
Replace (Rplus (Ropp (FtoR (2) p)) (FtoR (2) p)) with R0; [Idtac | Simpl; Ring].
Replace (Rplus (Ropp (FtoR (2) p)) (Rplus (Rmult (2) p) (Rmult (2) q)))
     with (Rplus p (Rmult (2) q)); [Idtac | Simpl; Unfold FtoRradix; Ring].
Apply Rlt_anti_compatibility with r := (Rmult (2) (Ropp q)).
Replace (Rplus (Rmult (2) (Ropp q)) R0) with (Rmult (2) (Ropp q));
[Idtac | Simpl; Ring].
Replace (Rplus (Rmult (2) (Ropp q)) (Rplus p (Rmult (2) q))) with (FtoRradix p);
[Idtac | Simpl; Ring]; Auto.
Ring.
Apply (RoundedModeMult b (2)) with P := (Closest b (2)) r := (Rplus p q); Auto.
Apply ClosestRoundedModeP with precision := precision; Auto.
Apply Rle_trans with (FtoR (2) p); Auto.
Replace (FtoR (2) p) with (Rplus p R0); [Idtac | Ring].
Apply Rle_compatibility; Auto.
Apply Rledouble; Auto.
Apply Rlt_le; Auto.
Apply Rle_lt_trans with 2 := H'0.
Apply Rle_trans with (Ropp q); Auto.
Replace R0 with (Ropp R0); Auto with real.
Apply Rledouble; Auto.
Replace R0 with (Ropp R0); Auto with real.
Qed.

Theorem MDekkerAux5:
  (p, q:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  <R>
    (Iminus (Iplus (Fopp p) (Fopp q)) (Fopp p))==
    (Rminus (Iplus (Fopp p) (Fopp q)) (Fopp p)) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).
Intros p q H' H'0 H'1.
Rewrite <- (Fopp_Fopp (Iminus (Iplus p q) p)); Auto.
Repeat Rewrite IminusPlus; Auto.
Rewrite IplusOp; Auto.
Rewrite <- IminusPlus.
Rewrite IplusOp; Auto.
Unfold FtoRradix; Rewrite Fopp_correct.
Unfold FtoRradix in H'1; Rewrite H'1.
Rewrite <- IplusOp; Auto.
Repeat Rewrite Fopp_correct.
Ring.
Qed.

Theorem MDekker:
  (p, q:float)
  (Fbounded b p) -> (Fbounded b q) -> (Rle (Rabsolu q) (Rabsolu p)) ->
  <R> (Iminus (Iplus p q) p)==(Rminus (Iplus p q) p).
Intros p q H' H'0 H'1.
Case (Rle_or_lt R0 p); Intros Rl1.
Rewrite (Rabsolu_simpl1 p) in H'1; Auto.
Case (Rle_or_lt R0 q); Intros Rl2.
Rewrite (Rabsolu_simpl1 q) in H'1; Auto.
Apply Dekker1; Auto.
Rewrite (Rabsolu_simpl2 q) in H'1; Auto.
Case (Rle_or_lt p (Rmult (2) (Ropp q))); Intros Rl3.
Apply Dekker2; Auto.
Apply Dekker3; Auto.
Apply Rlt_le; Auto.
Apply Rlt_le; Auto.
Rewrite (Rabsolu_simpl2 p) in H'1; Auto.
2:Apply Rlt_le; Auto.
Apply MDekkerAux5; Auto.
Case (Rle_or_lt R0 q); Intros Rl2.
Rewrite (Rabsolu_simpl1 q) in H'1; Auto.
Case (Rle_or_lt (Ropp p) (Rmult (2) q)); Intros Rl3.
Apply Dekker2; Auto.
Unfold FtoRradix; Rewrite Fopp_correct; Auto.
Replace R0 with (Ropp R0); Auto with real.
Apply Rlt_le; Auto with real.
Unfold FtoRradix; Repeat Rewrite Fopp_correct; Auto.
Rewrite Ropp_Ropp; Auto.
Unfold FtoRradix; Repeat Rewrite Fopp_correct; Auto.
Rewrite Ropp_Ropp; Auto.
Apply oppBounded; Auto.
Apply oppBounded; Auto.
Apply Dekker3; Auto.
Unfold FtoRradix; Rewrite Fopp_correct; Auto.
Replace R0 with (Ropp R0); Auto with real.
Unfold FtoRradix; Repeat Rewrite Fopp_correct; Auto.
Rewrite Ropp_Ropp; Auto.
Apply oppBounded; Auto.
Apply oppBounded; Auto.
Rewrite (Rabsolu_simpl2 q) in H'1; Auto.
Apply Dekker1; Auto.
Unfold FtoRradix; Rewrite Fopp_correct; Auto.
Replace R0 with (Ropp R0); Auto with real.
Apply Rlt_le; Auto with real.
Unfold FtoRradix; Repeat Rewrite Fopp_correct; Auto.
Apply oppBounded; Auto.
Apply oppBounded; Auto.
Apply Rlt_le; Auto with real.
Qed.

Theorem Dekker:
  (p, q:float)
  (Fbounded b p) -> (Fbounded b q) -> (Rle (Rabsolu q) (Rabsolu p)) ->
  <R> (Iminus q (Iminus (Iplus p q) p))==(Rminus (Rplus p q) (Iplus p q)).
Intros p q H' H'0 H'1.
Apply MDekkerAux1; Auto.
Apply MDekker; Auto.
Qed.
End Fast.

14/12/100, 18:43