FroundPlus.v

(****************************************************************************                                                                                         IEEE754  :  FroundPlus                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export FroundProp.
Section FRoundP.
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 plusExpMin:
  (P:?) (RoundedModeP b radix P) ->
  (p, q, pq:float) (P (Rplus p q) pq) ->
  (Ex [s:float]
  (Fbounded b s) /\ (<R> s==pq /\ (Zle (Zmin (Fexp p) (Fexp q)) (Fexp s)))).
Intros P H' p q pq H'0.
Case (RoundedModeRep b radix precision) with p := (Fplus radix p q) q := pq
                                             P := P; Auto with float arith.
Rewrite Fplus_correct; Auto with float arith.
Simpl; Intros x H'1.
Case (eqExpLess ? radixMoreThanOne b) with p := pq
                                           q :=
                                           (Float x (Fexp (Fplus radix p q)));
Auto.
Apply (RoundedModeBounded b radix) with P := P r := (Rplus p q); Auto.
Simpl; Intros x0 H'2; Elim H'2; Intros H'3 H'4; Elim H'4; Intros H'5 H'6;
Clear H'4 H'2.
Exists x0; Split; [Idtac | Split]; Auto.
Unfold FtoRradix; Rewrite H'5; Auto.
Apply le_IZR; Auto.
Qed.

Theorem plusExpUpperBound:
  (P:?) (RoundedModeP b radix P) ->
  (p, q, pq:float) (P (Rplus p q) pq) -> (Fbounded b p) -> (Fbounded b q) ->
  (Ex [r:float]
  (Fbounded b r) /\ (<R> r==pq /\ (Zle (Fexp r) (Zs (Zmax (Fexp p) (Fexp q)))))).
Intros P H' p q pq H'0 H'1 H'2.
Replace (Zs (Zmax (Fexp p) (Fexp q)))
     with (Fexp (Float (vNum b) (Zs (Zmax (Fexp p) (Fexp q)))));
[Idtac | Simpl; Auto].
Unfold FtoRradix; Apply eqExpMax; Auto.
Apply RoundedModeBounded with radix := radix P := P r := (Rplus p q);
Auto with float arith.
Apply maxFbounded; Auto.
Apply Zle_trans with (Fexp p); [Intuition | Idtac].
Apply Zle_trans with (Zs (Fexp p)); [Auto with zarith | Idtac].
Generalize (ZmaxLe1 (Fexp p) (Fexp q)); Auto with zarith.
Replace (FtoR radix (Float (vNum b) (Zs (Zmax (Fexp p) (Fexp q)))))
     with (Rmult radix (Float (vNum b) (Zmax (Fexp p) (Fexp q)))).
Rewrite Fabs_correct; Auto with zarith.
(Unfold FtoRradix;
  Apply RoundedModeMultAbs
       with b := b precision := precision P := P r := (Rplus p q)); Auto.
Apply maxFbounded; Auto.
Apply Zle_trans with (Fexp p); [Intuition | Idtac].
Generalize (ZmaxLe1 (Fexp p) (Fexp q)); Auto with zarith.
Apply Rle_trans with (Rplus (Rabsolu p) (Rabsolu q)).
Apply Rabsolu_triang; Auto.
Apply Rle_trans
     with (Rmult (2) (FtoR radix (Float (vNum b) (Zmax (Fexp p) (Fexp q)))));
Auto.
Cut (r:R)(Rmult (2) r)==(Rplus r r);
[Intros tmp; Rewrite tmp; Clear tmp | Intros; Simpl; Ring].
Apply Rplus_le; Auto.
Rewrite <- (Fabs_correct radix); Auto with arith; Apply maxMax; Auto;
Apply ZmaxLe1.
Rewrite <- (Fabs_correct radix); Auto with arith; Apply maxMax; Auto;
Apply ZmaxLe2.
Apply Rle_Rmult_comp; Auto with real arith.
Replace R0 with (INR O); Auto with real arith.
Apply LeFnumZERO; Simpl; Auto; Replace ZERO with (inject_nat O);
Auto with zarith.
Unfold FtoRradix FtoR; Simpl.
Rewrite powerRZ_Zs; Auto with real arith; Ring.
Qed.

Theorem Zabs_Zmult: (z1, z2:Z)(Zabs (Zmult z1 z2))=(Zmult (Zabs z1) (Zabs z2)).
Intros z1 z2; Case z1; Case z2; Simpl; Auto with zarith.
Qed.

Theorem Zle_Zmult_comp_r:
  (x, y, z:Z) (Zle ZERO z) -> (Zle x y) ->(Zle (Zmult x z) (Zmult y z)).
Intros x y z H' H'0; Case (Zle_lt_or_eq ? ? H'); Intros Zlt1.
Apply Zle_Zmult_right; Auto with zarith.
Rewrite <- Zlt1; Auto with zarith.
Qed.

Theorem Zle_Zmult_comp_l:
  (x, y, z:Z) (Zle ZERO z) -> (Zle x y) ->(Zle (Zmult z x) (Zmult z y)).
Intros x y z H' H'0; Repeat Rewrite (Zmult_sym z); Apply Zle_Zmult_comp_r; Auto.
Qed.

Theorem Fbounded_Zabs:
  (f:float) (Fbounded b f) ->(Zle (Zabs (Fnum f)) (vNum b)).
Intros f H'.
Case (Zle_or_lt ZERO (Fnum f)); Intros Zl1; Auto.
Rewrite Zabs_eq; Auto; Intuition.
Replace (Zabs (Fnum f)) with (Zabs (Zopp (Fnum f)));
[Idtac | Case (Fnum f); Simpl; Auto].
Rewrite Zabs_eq;
[Rewrite <- (Zopp_Zopp (vNum b)); Apply Zle_Zopp; Intuition |
   Replace ZERO with (Zopp ZERO); Auto with zarith].
Qed.

Theorem FboundedShiftLess:
  (f:float) (n, m:nat) (le m n) -> (Fbounded b (Fshift radix n f)) ->
  (Fbounded b (Fshift radix m f)).
Intros f n m H' H'0; Apply FboundAlt; Auto.
Simpl; Auto.
Apply Zle_trans with (Zabs (Fnum (Fshift radix n f))).
Simpl; Replace m with (plus m O); Auto with arith.
Replace n with (plus m (minus n m)); Auto with arith.
Repeat Rewrite Zpower_nat_is_exp.
Repeat Rewrite Zabs_Zmult; Auto.
Apply Zle_Zmult_comp_l; Auto with zarith.
Case (Fnum f); Unfold Zle; Simpl; Auto; Intros; Red; Intros; Discriminate.
Apply Zle_Zmult_comp_l; Auto with zarith.
Case (Zpower_nat radix m); Unfold Zle; Simpl; Auto; Intros; Red; Intros;
Discriminate.
Repeat Rewrite Zabs_eq; Auto with zarith.
Apply le_IZR; Auto.
Rewrite <- (absolu_INR O).
Rewrite <- (absolu_INR (minus n m)).
Repeat Rewrite Zpower_nat_powerRZ; Auto.
Repeat Rewrite [x, y, z:Z](Zmult_sym (Zmult x y) z).
Apply Rle_powerRZ; Auto with real arith.
Replace R1 with (INR (1)); Auto with real arith.
Auto with zarith arith.
Rewrite <- (absolu_INR (minus n m)).
Apply le_IZR; Simpl; Auto.
Repeat Rewrite Zpower_nat_powerRZ; Auto with real arith.
Rewrite <- (absolu_INR O).
Apply le_IZR; Simpl; Apply Rlt_le; Auto with real.
Repeat Rewrite Zpower_nat_powerRZ; Auto with real arith.
Apply Fbounded_Zabs; Auto.
Apply Zle_trans with (Fexp (Fshift radix n f)); Auto.
Intuition.
Simpl; Auto with zarith.
Qed.

Theorem Zmin_Zmax: (z1, z2:Z)(Zle (Zmin z1 z2) (Zmax z1 z2)).
Intros z1 z2; Case (Zle_or_lt z1 z2); Unfold Zle Zlt Zmin Zmax;
CaseEq (Zcompare z1 z2); Auto; Intros H1 H2; Try Rewrite H1; Try Rewrite H2;
Red; Intros; Discriminate.
Qed.

Theorem plusExpBound:
  (P:?) (RoundedModeP b radix P) ->
  (p, q, pq:float) (P (Rplus p q) pq) -> (Fbounded b p) -> (Fbounded b q) ->
  (Ex [r:float]
  (Fbounded b r) /\
  (<R> r==pq /\
   ((Zle (Zmin (Fexp p) (Fexp q)) (Fexp r)) /\
    (Zle (Fexp r) (Zs (Zmax (Fexp p) (Fexp q))))))).
Intros P H' p q pq H'0 H'1 H'2.
Case (plusExpMin P H' ? ? ? H'0).
Intros r' H'3; Elim H'3; Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Clear H'5 H'3.
Case (Zle_or_lt (Fexp r') (Zs (Zmax (Fexp p) (Fexp q)))); Intros Zl1.
Exists r'; Repeat (Split; Auto).
Case (plusExpUpperBound P H' ? ? ? H'0); Auto.
Intros r'' H'3; Elim H'3; Intros H'5 H'8; Elim H'8; Intros H'9 H'10;
Clear H'8 H'3.
Exists (Fshift
          radix (absolu (Zminus (Fexp r') (Zs (Zmax (Fexp p) (Fexp q))))) r');
Split.
Apply FboundedShiftLess with n := (absolu (Zminus (Fexp r') (Fexp r''))); Auto.
Apply ZleLe; Auto.
Repeat Rewrite <- Zabs_absolu.
Repeat Rewrite Zabs_eq; Auto with zarith.
Rewrite FshiftCorrectInv; Auto.
Apply trans_eqT with (FtoRradix pq); Auto.
Apply Zle_trans with 1 := H'10; Auto with zarith.
Split.
Unfold FtoRradix; Rewrite FshiftCorrect; Auto.
Split.
Simpl.
Repeat Rewrite inj_abs; Auto with zarith arith.
Apply Zle_trans with (Zmax (Fexp p) (Fexp q)); Auto with zarith.
Apply Zmin_Zmax; Auto.
Simpl.
Repeat Rewrite inj_abs; Auto with zarith arith.
Qed.
End FRoundP.

16/12/100, 17:39