ClosestPlus.v

(****************************************************************************                                                                                         IEEE754  :  ClosestPlus                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export FroundPlus.
Require Export ClosestProp.
Section ClosestP.
Variable b:Fbound.
Variable radix:nat.
Variable precision:nat.

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne:(lt (S O) radix).
Hypothesis precisionGreaterThanOne:(lt (1) precision).
Hypothesis pGivesBound:(vNum b)=(minus (exp radix precision) (1)).

Theorem errorBoundedPlusLe:
  (p, q, pq:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Zle (Fexp p) (Fexp q)) -> (Closest b radix (Rplus p q) pq) ->
  (Ex [error:float]
  <R> error==(Rabsolu (Rminus (Rplus p q) pq)) /\
  ((Fbounded b error) /\ (Fexp error)=(Zmin (Fexp p) (Fexp q)))).
Intros p q pq H' H'0 H'1 H'2.
Cut (ex Z [m:Z]<R> pq==(Float m (Fexp (Fplus radix p q)))).
2:Unfold FtoRradix;
   Apply RoundedModeRep
        with b := b precision := precision P := (Closest b radix); Auto.
2:Apply ClosestRoundedModeP with precision := precision; Auto.
2:Rewrite (Fplus_correct radix); Auto with arith.
Intros H'3; Elim H'3; Intros m E; Clear H'3.
Exists (Fabs
          (Fminus radix q (Fminus radix (Float m (Fexp (Fplus radix p q))) p))).
Cut (A, B:Prop) A -> (A ->B) ->A /\ B; [Intros tmp; Apply tmp; Clear tmp | Auto].
Unfold FtoRradix; Rewrite Fabs_correct; Auto with arith.
Cut (p, q:R) p==q ->(Rabsolu p)==(Rabsolu q);
[Intros tmp; Apply tmp; Clear tmp | Intros p q H; Rewrite H; Auto].
Unfold FtoRradix; Repeat Rewrite Fminus_correct; Auto with arith.
Unfold FtoRradix in E; Rewrite E; Auto.
Ring.
Ring.
Intros H'4.
Cut (Rle (Rabsolu (Rminus pq (Rplus p q))) (Rabsolu (Rminus q (Rplus p q)))).
2:Elim H'2; Auto.
Replace (Rminus q (Rplus p q)) with (Ropp (FtoRradix p)).
2:Ring.
Rewrite Rabsolu_Ropp.
Unfold FtoRradix; Rewrite <- Fabs_correct; Auto with arith.
Rewrite <- Rabsolu_Ropp; Rewrite Rminus_Ropp.
Unfold FtoRradix in H'4; Rewrite <- H'4.
Simpl.
Rewrite Zmin_le1; Auto.
Generalize H'1 H'; Case p; Case q; Unfold Fabs Fminus Fopp Fplus; Simpl;
Clear H'1 H'.
Intros Fnum1 Fexp1 Fnum2 Fexp2 H'5 H'6.
Repeat Rewrite Zmin_n_n; Auto.
Repeat Rewrite (Zmin_le2 ? ? H'5); Auto with zarith.
Replace (absolu (Zminus Fexp2 Fexp2)) with O.
Rewrite Zpower_nat_O.
Cut (z:Z)(Zmult z (1))=z;
[Intros tmp; Repeat Rewrite tmp; Clear tmp | Auto with zarith].
Unfold FtoRradix FtoR; Simpl.
Intros H'.
Repeat Split; Simpl.
Apply Zle_trans with ZERO; Auto with zarith.
Cut (z:Z)(Zle ZERO (Zabs z));
[Intros tmp; Apply tmp; Clear tmp |
   Intros z; Case z; Unfold Zle; Simpl; (Try Intros; Red; Intros; Discriminate);
    Auto with zarith].
Apply Zle_trans with (Zabs Fnum2); Auto.
Apply le_IZR.
Apply (Rle_mult_anticompatibility_exp radix) with z := Fexp2; Auto.
Cut (Zle Fnum2 (vNum b)) /\ (Zle (Zopp (vNum b)) Fnum2);
[Case Fnum2; Simpl | Intuition]; Auto.
Intros H'1; Elim H'1; Auto.
Intros p0 H'1; Elim H'1; Auto.
Intros p0 H'1; Elim H'1; Intros H'7 H'8; Clear H'1.
Rewrite <- (Zopp_Zopp (POS p0)); Rewrite <- (Zopp_Zopp (vNum b));
Auto with zarith.
Intuition.
Intros; Simpl; Ring.
Replace (Zminus Fexp2 Fexp2) with ZERO; Simpl; Auto with zarith.
Qed.

Theorem errorBoundedPlusAbs:
  (p, q, pq:float)
  (Fbounded b p) -> (Fbounded b q) -> (Closest b radix (Rplus p q) pq) ->
  (Ex [error:float]
  <R> error==(Rabsolu (Rminus (Rplus p q) pq)) /\
  ((Fbounded b error) /\ (Fexp error)=(Zmin (Fexp p) (Fexp q)))).
Intros p q pq H' H'0 H'1.
Case (Zle_or_lt (Fexp p) (Fexp q)); Intros H'2.
Apply errorBoundedPlusLe; Auto.
Replace (Rplus p q) with (Rplus q p); [Idtac | Ring].
Replace (Zmin (Fexp p) (Fexp q)) with (Zmin (Fexp q) (Fexp p));
[Idtac | Apply Zmin_sym].
Apply errorBoundedPlusLe; Auto.
Auto with zarith.
Apply (ClosestCompatible b radix (Rplus p q) (Rplus q p) pq); Auto.
Ring.
Intuition.
Qed.

Theorem errorBoundedPlus:
  (p, q, pq:float)
  (Fbounded b p) -> (Fbounded b q) -> (Closest b radix (Rplus p q) pq) ->
  (Ex [error:float]
  <R> error==(Rminus (Rplus p q) pq) /\
  ((Fbounded b error) /\ (Fexp error)=(Zmin (Fexp p) (Fexp q)))).
Intros p q pq H' H'0 H'1.
Case (errorBoundedPlusAbs p q pq); 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.
Generalize H'3; Clear H'3.
Unfold Rabsolu; Case (case_Rabsolu (Rminus (Rplus p q) pq)).
Intros H'2 H'3; Exists (Fopp x); Split; Auto.
Unfold FtoRradix; Rewrite Fopp_correct; Auto.
Unfold FtoRradix in H'3; Rewrite H'3; Ring.
Split.
Apply oppBounded; Auto.
Rewrite <- H'6; Auto.
Intros H'2 H'3; Exists x; Split; Auto.
Qed.

Theorem plusExact1:
  (p, q, r:float)
  (Fbounded b p) ->
  (Fbounded b q) ->
  (Closest b radix (Rplus p q) r) -> (Zle (Fexp r) (Zmin (Fexp p) (Fexp q))) ->
  <R> r==(Rplus p q).
Intros p q r H' H'0 H'1 H'2.
Cut (Rle
       (Rmult
          (2) (Rabsolu (Rminus (FtoR radix (Fplus radix p q)) (FtoR radix r))))
       (Float (1) (Fexp r)));
[Rewrite Fplus_correct; Auto with arith; Intros Rl1 | Idtac].
Case errorBoundedPlus with p := p q := q pq := r; Auto.
Intros x H'3; Elim H'3; Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Clear H'5 H'3.
Unfold FtoRradix in H'4; Rewrite <- H'4 in Rl1.
2:Apply Rle_trans with (Fulp b radix precision r); Auto.
2:Apply (ClosestUlp b radix precision); Auto.
2:Rewrite Fplus_correct; Auto with arith.
2:Unfold FtoRradix; Apply FulpLe; Auto.
2:Apply RoundedModeBounded
       with radix := radix P := (Closest b radix) r := (Rplus p q); Auto.
2:Apply ClosestRoundedModeP with precision := precision; Auto.
Cut <R> x==R0; [Unfold FtoRradix; Intros Eq1 | Idtac].
Replace (FtoR radix r) with (Rplus (FtoR radix r) R0); [Idtac | Ring].
Rewrite <- Eq1.
Rewrite H'4; Ring.
Apply (is_Fzero_rep1 radix).
Case (Z_zerop (Fnum x)); Simpl; Auto.
Intros H'3; Contradict Rl1.
Apply Rle_not.
Apply Rle_lt_trans with (Rabsolu (FtoR radix x)).
Unfold FtoRradix FtoR; Simpl; Auto.
Rewrite Rabsolu_mult.
Apply Rle_Rmult_comp; Auto with real arith.
Apply Rlt_le; Auto with real.
Generalize H'3; Case (Fnum x); Simpl; Auto with real arith.
Intros H'5; Case H'5; Auto.
Intros p0 H'5; Rewrite Rabsolu_simpl1; Auto with real arith.
Replace R1 with (INR (1)); Auto with real arith.
Replace R0 with (INR O); Auto with real arith.
Intros p0 H'5; Rewrite Rabsolu_simpl2; Auto.
Rewrite Ropp_Ropp.
Replace R1 with (INR (1)); Auto with real arith.
Replace R0 with (Ropp O); Auto with real; Apply Rle_Ropp; Auto with real arith.
Rewrite Rabsolu_simpl1; Auto with real arith.
Apply Rle_powerRZ; Auto with real arith.
Replace R1 with (INR (1)); Auto with real arith.
Auto with zarith.
Cut (r:R)(Rmult (2) r)==(Rplus r r);
[Intros tmp; Rewrite tmp; Clear tmp | Intros f; Simpl; Ring].
Pattern 1 (Rabsolu (FtoR radix x));
Replace (Rabsolu (FtoR radix x)) with (Rplus (Rabsolu (FtoR radix x)) R0);
[Idtac | Ring].
Apply Rlt_compatibility; Auto.
Case (RabsoluR0 (FtoR radix x)); Auto.
Rewrite <- Fabs_correct; Auto with arith.
Intros H'5; Contradict H'3.
Cut (Fnum (Fabs x))=ZERO.
Unfold Fabs; Simpl; Case (Fnum x); Simpl; Auto; Intros; Discriminate.
Change (is_Fzero (Fabs x)).
Apply (is_Fzero_rep2 radix); Auto with arith.
Qed.

Theorem plusExact1bis:
  (p, q, r:float)
  (Fbounded b p) ->
  (Fbounded b q) -> (Closest b radix (Rplus p q) r) -> ~ <R> r==(Rplus p q) ->
  (Zlt (Zmin (Fexp p) (Fexp q)) (Fexp r)).
Intros p0 q0 r0 H' H'0 H'1 H'2;
Case (Zle_or_lt (Fexp r0) (Zmin (Fexp p0) (Fexp q0))); Auto.
Intros H'3; Contradict H'2.
Apply plusExact1; Auto.
Qed.

Theorem plusExact2Aux:
  (p, q, r:float)
  (Rle R0 p) ->
  (Fcanonic radix b precision p) ->
  (Fbounded b q) ->
  (Closest b radix (Rplus p q) r) -> (Zlt (Fexp r) (Zpred (Fexp p))) ->
  <R> r==(Rplus p q).
Intros p q r H' H'0 H'1 H'2 H'3.
Apply plusExact1; Auto.
Intuition.
Case (Zle_or_lt (Fexp p) (Fexp q)); Intros Zl1.
Rewrite Zmin_le1; Auto with zarith.
Apply Zle_trans with (Zpred (Fexp p)); Auto with zarith.
Unfold Zpred; Auto with zarith.
Rewrite Zmin_le2; Auto with zarith.
Case (Zlt_next ? ? Zl1); Intros Zl2.
Rewrite Zl2 in H'3.
Replace (Fexp q) with (Zpred (Zs (Fexp q))); Auto with zarith; Unfold Zpred Zs;
Ring.
Case H'0; Clear H'0; Intros H'0.
Absurd (Rlt r (Float (nNormMin radix precision) (Zpred (Fexp p)))).
Apply Rlt_not; Auto.
Unfold FtoRradix;
Apply (ClosestMonotone
          b radix (Float (nNormMin radix precision) (Zpred (Fexp p)))
          (Rplus p q)); Auto; Auto.
Cut (Rle (Float (nNormMin radix precision) (Fexp p)) p); [Intros Eq1 | Idtac].
Case (Rle_or_lt R0 q); Intros Rl1.
Apply Rlt_le_trans with (FtoRradix p).
Apply Rlt_le_trans with (FtoRradix (Float (nNormMin radix precision) (Fexp p)));
Auto.
Unfold FtoRradix FtoR; Simpl; Auto.
Apply Rlt_monotony; Auto with real arith.
Replace R0 with (INR O); Auto with real; Rewrite <- INR_IZR_INZ;
Auto with real float arith.
Unfold Zpred; Auto with real float zarith arith.
Pattern 1 (FtoRradix p); Replace (FtoRradix p) with (Rplus p R0); Auto with real.
Apply Rlt_anti_compatibility with r := (Ropp q); Auto.
Replace (Rplus (Ropp q) (Rplus p q)) with (FtoRradix p); [Idtac | Ring].
Apply Rlt_le_trans with (FtoRradix (Float (nNormMin radix precision) (Fexp p)));
Auto.
Apply Rlt_le_trans
     with (Rmult (2) (Float (nNormMin radix precision) (Zpred (Fexp p)))); Auto.
Cut (r:R)(Rmult (2) r)==(Rplus r r);
[Intros tmp; Rewrite tmp; Clear tmp | Intros; Simpl; Ring].
Rewrite (Rplus_sym (Ropp q)).
Apply Rlt_compatibility.
Rewrite <- Rabsolu_simpl2; Auto.
Rewrite <- (Fabs_correct radix); Auto with arith.
Unfold FtoRradix; Apply maxMaxBis with b := b; Auto with zarith.
Apply Zlt_S_n; Auto with zarith.
Replace (Zs (Zpred (Fexp p))) with (Fexp p); Auto with zarith.
Apply Rlt_le; Auto.
Apply Rle_trans
     with (Rmult radix (Float (nNormMin radix precision) (Zpred (Fexp p)))).
Apply Rle_monotony_r; Auto.
Apply (LeFnumZERO radix); Simpl; Auto with arith.
Replace ZERO with (inject_nat O); Auto with zarith.
Apply Rle_INR; Auto.
Pattern 2 (Fexp p); Replace (Fexp p) with (Zs (Zpred (Fexp p)));
[Idtac | Unfold Zs Zpred; Ring].
Unfold FtoRradix FtoR; Simpl.
Rewrite powerRZ_Zs; Auto with real arith.
Repeat Rewrite <- Rmult_assoc.
Rewrite (Rmult_sym radix); Auto with real.
Unfold FtoRradix FtoR; Simpl; Auto.
Apply Rle_monotony_r; Auto with real arith.
Rewrite <- (inj_abs (Fnum p)); Auto.
Repeat Rewrite <- INR_IZR_INZ; Apply Rle_INR.
Apply pNormal_absolu_min with b := b; Auto with arith.
Apply (LeR0Fnum radix); Auto with arith.
Apply (RoundedModeProjectorIdem b radix (Closest b radix)); Auto.
Apply ClosestRoundedModeP with precision := precision; Auto.
Repeat Split; Simpl.
Apply Zle_trans with (Zopp O); Auto with zarith.
Apply inj_le; Apply nNrMMimLevNum; Auto with arith.
Apply Zle_trans with (Fexp q).
Intuition.
Apply Zle_S_n; Auto with zarith.
Replace (Zs (Zpred (Fexp p))) with (Fexp p); Auto with zarith.
Case (Rle_or_lt R0 r); Intros Rl1.
Rewrite <- (Rabsolu_simpl1 r); Auto.
Rewrite <- (Fabs_correct radix); Auto with arith.
Unfold FtoRradix; Apply maxMaxBis with b := b; Auto with zarith.
Apply RoundedModeBounded
     with radix := radix P := (Closest b radix) r := (Rplus p q); Auto.
Apply ClosestRoundedModeP with precision := precision; Auto.
Apply Rlt_le_trans with R0; Auto.
Apply (LeFnumZERO radix); Simpl; Auto with arith.
Replace ZERO with (inject_nat O); Auto with zarith.
Absurd (Zle (Zopp (dExp b)) (Fexp q)); Auto.
Apply Zlt_not_le.
Case H'0; Auto.
Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Rewrite <- H'6; Clear H'5.
Apply Zlt_trans with (Zs (Fexp q)); Auto with zarith.
Intuition.
Qed.

Theorem plusExact2:
  (p, q, r:float)
  (Fcanonic radix b precision p) ->
  (Fbounded b q) ->
  (Closest b radix (Rplus p q) r) -> (Zlt (Fexp r) (Zpred (Fexp p))) ->
  <R> r==(Rplus p q).
Intros p q r H' H'0 H'1 H'2.
Case (Rle_or_lt R0 p); Intros Rl1.
Apply plusExact2Aux; Auto.
Replace (Rplus p q) with (Ropp (Rplus (Fopp p) (Fopp q))).
Rewrite <- (plusExact2Aux (Fopp p) (Fopp q) (Fopp r)); Auto.
Unfold FtoRradix; Rewrite Fopp_correct; Ring.
Unfold FtoRradix; Rewrite Fopp_correct.
Apply Rlt_le; Replace R0 with (Ropp R0); Auto with real.
Apply FcanonicFopp; Auto with arith.
Apply oppBounded; Auto.
Replace (Rplus (Fopp p) (Fopp q)) with (Ropp (Rplus p q)).
Apply ClosestOpp; Auto.
Unfold FtoRradix; Repeat Rewrite Fopp_correct; Ring.
Unfold FtoRradix; Repeat Rewrite Fopp_correct; Ring.
Qed.

Theorem plusExactR0:
  (p, q, r:float)
  (Fbounded b p) ->
  (Fbounded b q) -> (Closest b radix (Rplus p q) r) -> <R> r==R0 ->
  <R> r==(Rplus p q).
Intros p q r H' H'0 H'1 H'2.
Cut <R> r==(FtoRradix (Fzero (Zopp (dExp b))));
[Intros Eq1; Rewrite Eq1 |
   Rewrite H'2; Apply sym_eqT; Unfold FtoRradix; Apply FzeroisZero].
Apply plusExact1; Auto.
Apply (ClosestCompatible b radix (Rplus p q) (Rplus p q) r); Auto.
Apply FboundedFzero; Auto.
Simpl; Auto.
Unfold Zmin; Case (Zcompare (Fexp p) (Fexp q)); Intuition.
Qed.

Theorem plusErrorBound1:
  (p, q, r:float)
  (Fbounded b p) ->
  (Fbounded b q) -> (Closest b radix (Rplus p q) r) -> ~ (is_Fzero r) ->
  (Rlt
     (Rabsolu (Rminus r (Rplus p q)))
     (Rmult (Rmult (Rabsolu r) (Rinv (2))) (Rmult radix (Rinv (vNum b))))).
Intros p q r H' H'0 H'1 H'2.
Cut (Fcanonic radix b precision (Fnormalize radix b precision r));
[Intros tmp; Casec tmp; Intros Fs | Idtac].
3:Apply FnormalizeCanonic; Auto with arith.
3:Apply RoundedModeBounded
       with radix := radix P := (Closest b radix) r := (Rplus p q); Auto.
3:Apply ClosestRoundedModeP with precision := precision; Auto.
2:Rewrite <- (plusExact1 p q (Fnormalize radix b precision r)); Auto.
2:Unfold FtoRradix; Rewrite FnormalizeCorrect.
2:Replace (Rminus (FtoR radix r) (FtoR radix r)) with R0; [Idtac | Ring].
2:Rewrite Rabsolu_R0.
2:Replace R0 with (Rmult R0 (Rmult radix (Rinv (vNum b))));
   [Apply Rlt_monotony_r | Ring].
2:Replace R0 with (Rmult R0 (Rinv (vNum b))); [Apply Rlt_monotony_r | Ring].
2:Apply Rlt_Rinv; Replace R0 with (INR O); Auto with real arith; Apply Rlt_INR.
2:Apply lt_vNum with radix := radix precision := precision; Auto with real arith.
2:Replace R0 with (INR O); Auto with real arith.
2:Replace R0 with (Rmult R0 (Rinv (2))); [Apply Rlt_monotony_r | Ring];
   Auto with real.
2:Case (RabsoluR0 (FtoR radix r)); Auto.
2:Intros H'3; Contradict H'2.
2:Apply is_Fzero_rep2 with radix := radix; Auto with real arith.
2:Apply RabsoluR0Inv; Rewrite <- H'3; Auto with real.
2:Auto with arith.
2:Apply (ClosestCompatible b radix (Rplus p q) (Rplus p q) r); Auto.
2:Apply sym_eqT; Apply FnormalizeCorrect; Auto.
2:Apply FnormalizeBounded; Auto with arith.
2:Apply RoundedModeBounded
       with radix := radix P := (Closest b radix) r := (Rplus p q); Auto.
2:Apply ClosestRoundedModeP with precision := precision; Auto.
2:Replace (Fexp (Fnormalize radix b precision r)) with (Zopp (dExp b)).
2:Unfold Zmin; Case (Zcompare (Fexp p) (Fexp q)); Intuition.
2:Apply sym_equal; Intuition.
Apply Rle_lt_trans with (Rmult (Rinv (2)) (Fulp b radix precision r)).
Apply Rle_mult_anticompatibility with z := (INR (2)); Auto with real.
Rewrite <- Rmult_assoc; Rewrite Rinv_r; Auto with real; Rewrite Rmult_ne_r.
Unfold FtoRradix; Rewrite <- Rabsolu_Ropp; Rewrite Rminus_Ropp;
Rewrite <- (Fplus_correct radix); Auto with arith; Apply ClosestUlp; Auto.
Rewrite Fplus_correct; Auto with arith.
Replace (Rmult (Rmult (Rabsolu r) (Rinv (2))) (Rmult radix (Rinv (vNum b))))
     with (Rmult (Rinv (2)) (Rmult (Rabsolu r) (Rmult radix (Rinv (vNum b)))));
[Apply Rlt_monotony; Auto with real | Ring].
Replace (Fulp b radix precision r)
     with (Rmult
             (Float (vNum b) (Zpred (Fexp (Fnormalize radix b precision r))))
             (Rmult radix (Rinv (vNum b)))).
Apply Rlt_monotony_r.
Replace R0 with (Rmult radix R0); [Apply Rlt_monotony | Ring];
Auto with real arith.
Apply Rlt_Rinv; Replace R0 with (INR O); Auto with real arith; Apply Rlt_INR.
Apply lt_vNum with radix := radix precision := precision; Auto with real arith.
Unfold FtoRradix;
Rewrite <- (FnormalizeCorrect ? radixMoreThanOne b precision r).
Rewrite <- (Fabs_correct radix); Auto with arith.
Apply FnormalBoundAbs with precision := precision; Auto with arith.
Unfold Fulp FtoRradix FtoR; Simpl.
Apply trans_eqT
     with (Rmult
             (Rmult (vNum b) (Rinv (vNum b)))
             (Rmult
                radix
                (powerRZ radix (Zpred (Fexp (Fnormalize radix b precision r))))));
[Rewrite <- INR_IZR_INZ; Ring | Idtac]; Auto.
Rewrite Rinv_r; Auto with real arith.
Rewrite <- powerRZ_Zs; Auto with real.
Cut (r:Z)(Zs (Zpred r))=r; [Intros Er; Rewrite Er | Intros r; Unfold Zs Zpred];
Ring.
Apply imp_not_Req; Right; Red.
Replace R0 with (INR O); Auto with real arith; Apply Rlt_INR.
Apply imp_not_Req; Right; Red; Apply Rlt_INR0.
Apply lt_vNum with radix := radix precision := precision; Auto with real arith.
Qed.
End ClosestP.

16/12/100, 17:44