Closest2Plus.v

(****************************************************************************                                                                                         IEEE754  :  Closest2Plus                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export ClosestPlus.
Require Export Closest2Prop.
Section F2.
Variable b:Fbound.
Variable precision:nat.

Local FtoRradix := (FtoR (2)).
Coercion FtoRradix : float >-> R.

Theorem TwoMoreThanOne: (lt (S O) (2)).
Auto.
Qed.
Hints Resolve TwoMoreThanOne.
Hypothesis precisionNotZero:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp (2) precision) (1)).

Theorem plusUpperBound:
  (P:?) (RoundedModeP b (2) P) ->
  (p, q, pq:float) (P (Rplus p q) pq) -> (Fbounded b p) -> (Fbounded b q) ->
  (Rle (Rabsolu pq) (Rmult (2) (Rmax (Rabsolu p) (Rabsolu q)))).
Intros P H' p q pq H'0 H'1 H'2.
Rewrite <- (Rabsolu_simpl1 (INR (2))); Auto with real arith.
Rewrite <- RmaxRmult; Auto with real.
Repeat Rewrite <- Rabsolu_mult.
Case (Rle_or_lt p q); Intros Rltp.
Apply RmaxAbs; Auto.
Apply (RoundedModeMultLess b (2)) with P := P r := (Rplus p q); Auto.
Replace (Rmult (2) (FtoR (2) p)) with (Rplus p p);
[Auto with real | Simpl; Ring].
Unfold FtoRradix; Apply (RoundedModeMult b (2)) with P := P r := (Rplus p q);
Auto.
Replace (Rmult (2) (FtoR (2) q)) with (Rplus q q);
[Auto with real | Simpl; Ring].
Rewrite RmaxSym.
Apply RmaxAbs; Auto.
Apply (RoundedModeMultLess b (2)) with P := P r := (Rplus p q); Auto.
Replace (Rmult (2) (FtoR (2) q)) with (Rplus q q);
[Auto with real | Simpl; Ring].
Repeat Rewrite [x:?](Rmult_sym x q); Apply Rplus_le; Auto with real.
Apply Rlt_le; Auto.
Unfold FtoRradix; Apply (RoundedModeMult b (2)) with P := P r := (Rplus p q);
Auto.
Replace (Rmult (2) (FtoR (2) p)) with (Rplus p p);
[Auto with real | Simpl; Ring].
Apply Rplus_le; Auto with real.
Apply Rlt_le; Auto.
Replace R0 with (INR O); Auto with real arith.
Qed.

Theorem plusErrorBound2:
  (p, q, r:float)
  (Fbounded b p) ->
  (Fbounded b q) -> (Closest b (2) (Rplus p q) r) -> ~ (is_Fzero r) ->
  (Rlt
     (Rabsolu (Rminus r (Rplus p q)))
     (Rmult (Rmult (2) (Rinv (vNum b))) (Rmax (Rabsolu p) (Rabsolu q)))).
Intros p q r H' H'0 H'1 H'2.
Apply Rlt_le_trans
     with (Rmult
             (Rmult (Rabsolu (FtoR (2) r)) (Rinv (2)))
             (Rmult (2) (Rinv (vNum b)))); Auto.
Unfold FtoRradix; Apply plusErrorBound1 with precision := precision;
Auto with arith.
Replace (Rmult
           (Rmult (Rabsolu (FtoR (2) r)) (Rinv (2))) (Rmult (2) (Rinv (vNum b))))
     with (Rmult (Rmult (2) (Rinv (vNum b))) (Rmult (Rabsolu r) (Rinv (2))));
[Idtac | Ring].
Apply Rle_monotony; Auto.
Replace R0 with (Rmult (2) R0); [Apply Rle_monotony | Ring].
Replace R0 with (INR O); Auto with real arith.
Apply Rlt_le; Apply Rlt_Rinv; Replace R0 with (INR O); Auto with real arith;
Apply Rlt_INR.
Apply lt_vNum with radix := (2) precision := precision; Auto with real arith.
Apply Rle_mult_anticompatibility with z := (INR (2)); Auto with real.
Rewrite (Rmult_sym (Rabsolu r)); Rewrite <- Rmult_assoc; Rewrite Rinv_r;
Auto with real; Rewrite Rmult_ne_r.
Apply plusUpperBound with P := (Closest b (2)); Auto.
Apply ClosestRoundedModeP with precision := precision; Auto.
Qed.

Theorem Rlt_Rinv2: (r:R) (Rlt R0 r) ->(Rlt (Rmult (Rinv (2)) r) r).
Intros r H'.
Apply Rlt_mult_anticompatibility with z := (INR (2)); Auto with real.
Rewrite <- Rmult_assoc; Rewrite Rinv_r.
Apply Rlt_monotony_r; Replace R1 with (INR (1)); Auto with real arith.
Replace R0 with (INR O); Auto with real arith.
Qed.

Theorem plusClosestLowerBoundAux1:
  (p, q, pq:float)
  (Rle (Rabsolu q) p) ->
  (Closest b (2) (Rplus p q) pq) ->
  (Fbounded b p) -> (Fbounded b q) -> ~ pq==(Rplus p q) ->
  (Rle (Rmult (Rinv (2)) p) pq).
Intros p q pq H' H'0 H'1 H'2 H'3.
Cut (Rle R0 p);
[Intros Rl0; Casec Rl0; Intros H0 |
   Apply Rle_trans with 2 := H'; Auto with real].
Apply (FmultRadixInv b precision) with 4 := H'0; Auto.
Case (Rle_or_lt R0 q); Intros Rl0.
Apply Rlt_le_trans with (FtoRradix p); Auto.
Apply Rlt_Rinv2; Auto.
Pattern 1 (FtoRradix p); Replace (FtoRradix p) with (Rplus p R0); Auto with real.
Apply Rlt_mult_anticompatibility with z := (INR (2)); Auto with real.
Rewrite <- Rmult_assoc; Rewrite Rinv_r.
Rewrite Rmult_Rplus_distr.
Rewrite Rmult_ne_r.
Apply Rlt_anti_compatibility with r := (Ropp (Rmult (2) p)).
Replace (Rplus (Ropp (Rmult (2) p)) (FtoR (2) p)) with (Ropp p);
[Idtac | Simpl; Unfold FtoRradix; Ring; Auto; Ring].
Replace (Rplus (Ropp (Rmult (2) p)) (Rplus (Rmult (2) p) (Rmult (2) q)))
     with (Rmult (2) q); [Idtac | Simpl; Ring].
Rewrite <- (Ropp_Ropp (Rmult (2) q)); Apply Rlt_Ropp.
Replace (Ropp (Rmult (2) q)) with (Rmult (2) (Ropp q)); [Idtac | Ring].
Case (Rle_or_lt (FtoRradix p) (Rmult (2) (Ropp q))); Auto.
Intros H'4; Contradict H'3.
Rewrite <- (Fplus_correct (2)); Auto.
Unfold FtoRradix; Apply sym_eqT; Apply ClosestIdem with b := b; Auto.
Replace (Fplus (2) p q) with (Fminus (2) p (Fopp q)).
Rewrite <- Fopp_Fminus.
Apply oppBounded; Auto.
Apply Sterbenz; Auto.
Apply oppBounded; Auto.
Apply Rle_mult_anticompatibility with z := (INR (2)); Auto with real.
Rewrite <- Rmult_assoc; Rewrite Rinv_r.
Rewrite Rmult_ne_r; Rewrite Fopp_correct; Auto.
Replace R0 with (INR O); Auto with real arith.
Apply Rle_trans with (FtoR (2) p); Auto with real.
Rewrite Fopp_correct; Auto.
Rewrite <- Rabsolu_simpl2; Auto.
Apply Rlt_le; Auto.
Apply Rledouble; Apply Rlt_le; Auto.
Unfold Fminus; Rewrite Fopp_Fopp; Auto.
Apply (ClosestCompatible b (2) (Rplus p q) (FtoR (2) (Fplus (2) p q)) pq pq);
Auto.
Apply sym_eqT; Unfold FtoRradix; Apply Fplus_correct; Auto.
Apply RoundedModeBounded with radix := (2) P := (Closest b (2)) r := (Rplus p q);
Auto.
Apply ClosestRoundedModeP with precision := precision; Auto.
Replace R0 with (INR O); Auto with real arith.
Rewrite <- H0; AutoRewrite [Rsimpl].
Replace (FtoRradix pq) with (FtoRradix p); Auto.
Rewrite <- H0; Auto with real.
Unfold FtoRradix; Apply ClosestIdem with b := b; Auto.
Apply (ClosestCompatible b (2) (Rplus p q) (FtoR (2) p) pq pq); Auto.
Replace (FtoR (2) p) with (FtoRradix p); Auto.
Rewrite <- H0; Replace (FtoRradix q) with R0; Try Ring.
Apply sym_eqT; Apply RabsoluR0Inv; Auto.
Rewrite H0; Auto.
Apply RoundedModeBounded with radix := (2) P := (Closest b (2)) r := (Rplus p q);
Auto.
Apply ClosestRoundedModeP with precision := precision; Auto.
Qed.

Theorem plusClosestLowerBoundAux2:
  (p, q, pq:float)
  (Closest b (2) (Rplus p q) pq) ->
  (Fbounded b p) ->
  (Fbounded b q) -> ~ pq==(Rplus p q) -> (Rle (Rabsolu p) (Rabsolu q)) ->
  (Rle (Rmult (Rinv (2)) (Rabsolu q)) (Rabsolu pq)).
Intros p q pq H' H'0 H'1 H'2 H'3.
Cut (Fbounded b pq);
[Intros Fb0 |
   Apply RoundedModeBounded
        with radix := (2) P := (Closest b (2)) r := (Rplus p q); Auto;
    Apply ClosestRoundedModeP with precision := precision]; Auto.
Case (Rle_or_lt R0 q); Intros Rl2;
[Idtac | Cut (Rle q R0); [Intros Rl2' | Apply Rlt_le; Auto]].
Repeat Rewrite Rabsolu_simpl1; Auto.
Apply plusClosestLowerBoundAux1 with q := p; Auto.
Rewrite <- (Rabsolu_simpl1 q); Auto.
Apply (ClosestCompatible b (2) (Rplus p q) (Rplus q p) pq pq); Auto; Try Ring.
Rewrite Rplus_sym; Auto.
Unfold FtoRradix;
Apply RleRoundedR0
      with b := b precision := precision P := (Closest b (2)) r := (Rplus p q);
Auto.
Apply ClosestRoundedModeP with precision := precision; Auto.
Case (Rle_or_lt R0 p); Intros Rl3;
[Idtac | Cut (Rle p R0); [Intros Rl3' | Apply Rlt_le; Auto]]; Auto with real.
Replace R0 with (Rplus R0 R0); Auto with real.
Apply Rle_anti_compatibility with r := (Ropp p).
Replace (Rplus (Ropp p) R0) with (Ropp p); [Idtac | Ring].
Replace (Rplus (Ropp p) (Rplus p q)) with (FtoRradix q); [Idtac | Ring].
Rewrite <- (Rabsolu_simpl2 (FtoRradix p)); Auto.
Rewrite <- (Rabsolu_simpl1 (FtoRradix q)); Auto.
Repeat Rewrite Rabsolu_simpl2; Auto.
Unfold FtoRradix; Repeat Rewrite <- (Fopp_correct (2)); Auto.
Apply plusClosestLowerBoundAux1 with q := (Fopp p); Auto.
Unfold FtoRradix; Repeat Rewrite Fopp_correct; Rewrite Rabsolu_Ropp;
Rewrite <- Rabsolu_simpl2; Auto.
Apply (ClosestCompatible
         b (2) (Ropp (Rplus p q)) (Rplus (Fopp q) (Fopp p)) (Fopp pq) (Fopp pq));
Auto.
Apply ClosestOpp; Auto.
Unfold FtoRradix; Repeat Rewrite Fopp_correct; Ring.
Apply oppBounded; Auto.
Apply oppBounded; Auto.
Apply oppBounded; Auto.
Unfold FtoRradix; Repeat Rewrite Fopp_correct; Contradict H'2.
Unfold FtoRradix; Rewrite <- (Ropp_Ropp (FtoR (2) pq)); Rewrite H'2; Ring.
Unfold FtoRradix;
Apply RleRoundedLessR0
      with b := b precision := precision P := (Closest b (2)) r := (Rplus p q);
Auto.
Apply ClosestRoundedModeP with precision := precision; Auto.
Case (Rle_or_lt R0 p); Intros Rl3;
[Idtac | Cut (Rle p R0); [Intros Rl3' | Apply Rlt_le; Auto]]; Auto with real.
Apply Rle_anti_compatibility with r := (Ropp q).
Replace (Rplus (Ropp q) R0) with (Ropp q); [Idtac | Ring].
Replace (Rplus (Ropp q) (Rplus p q)) with (FtoRradix p); [Idtac | Ring].
Rewrite <- (Rabsolu_simpl1 (FtoRradix p)); Auto.
Rewrite <- (Rabsolu_simpl2 (FtoRradix q)); Auto.
Replace R0 with (Rplus R0 R0); Auto with real.
Qed.

Theorem plusClosestLowerBound:
  (p, q, pq:float)
  (Closest b (2) (Rplus p q) pq) ->
  (Fbounded b p) -> (Fbounded b q) -> ~ pq==(Rplus p q) ->
  (Rle (Rmult (Rinv (2)) (Rmax (Rabsolu p) (Rabsolu q))) (Rabsolu pq)).
Intros p q pq H' H'0 H'1 H'2.
Cut (Fbounded b pq);
[Intros Fb0 |
   Apply RoundedModeBounded
        with radix := (2) P := (Closest b (2)) r := (Rplus p q); Auto;
    Apply ClosestRoundedModeP with precision := precision]; Auto.
Unfold Rmax.
Case (total_order_Rle (Rabsolu p) (Rabsolu q)); Intros Rl1.
Apply plusClosestLowerBoundAux2 with p := p; Auto.
Apply plusClosestLowerBoundAux2 with p := q; Auto.
Apply (ClosestCompatible b (2) (Rplus p q) (Rplus q p) pq pq); Auto; Try Ring.
Rewrite Rplus_sym; Auto.
Case (Rle_or_lt (Rabsolu q) (Rabsolu p)); Auto; Intros H'3; Contradict Rl1;
Apply Rlt_le; Auto.
Qed.
End F2.

16/12/100, 18:18