FroundProp.v

(****************************************************************************                                                                                         IEEE754  :  FroundProp                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export Fround.
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)).

Definition Fulp :=
   [p:float](powerRZ radix (Fexp (Fnormalize radix b precision p))).

Theorem FulpComp:
  (p, q:float) (Fbounded b p) -> (Fbounded b q) -> <R> p==q ->(Fulp p)==(Fulp q).
Intros p q H' H'0 H'1; Unfold Fulp.
Rewrite FcanonicUnique with p := (Fnormalize radix b precision p)
                            q := (Fnormalize radix b precision q)
                            3 := pGivesBound; Auto with float arith.
Apply trans_eqT with (FtoR radix p).
Apply FnormalizeCorrect; Auto.
Apply trans_eqT with (FtoR radix q); Auto.
Apply sym_eqT; Apply FnormalizeCorrect; Auto.
Qed.

Theorem FulpLe: (p:float) (Fbounded b p) ->(Rle (Fulp p) (Float (1) (Fexp p))).
Intros p H'; Unfold Fulp FtoRradix FtoR Fnormalize; Simpl; AutoRewrite [Rsimpl].
Case (Z_zerop (Fnum p)); Simpl; Auto.
Intros H'0; Apply Rle_powerRZ; Auto with real arith.
Apply Rlt_le; Replace R1 with (INR (1)); Auto with real arith.
Intuition.
Intros H'0; Apply Rle_powerRZ; Auto with real arith.
Apply Rlt_le; Replace R1 with (INR (1)); Auto with real arith.
Auto with zarith.
Qed.

Theorem Fulp_zero:
  (x:float) (is_Fzero x) ->(Fulp x)==(powerRZ radix (Zopp (dExp b))).
Intros x; Unfold is_Fzero Fulp Fnormalize; Case (Z_zerop (Fnum x)); Simpl; Auto.
Intros H' H'0; Contradict H'; Auto.
Qed.

Theorem FulpSucCan:
  (p:float) (Fcanonic radix b precision p) ->
  (Rle (Rminus (FSucc b radix precision p) p) (Fulp p)).
Intros p H'.
Replace (Fulp p) with (powerRZ radix (Fexp p)).
2:Unfold Fulp; Replace (Fnormalize radix b precision p) with p; Auto;
   Apply sym_equal; Apply FcanonicUnique with 3 := pGivesBound; Auto with arith;
   Apply FnormalizeCanonic Orelse Apply FnormalizeCorrect; Auto with arith;
   Intuition.
Unfold FtoRradix; Rewrite <- Fminus_correct; Auto with arith.
Case (Z_eq_dec (Fnum p) (Zopp (nNormMin radix precision))); Intros H1'.
Case (Z_eq_dec (Fexp p) (Zopp (dExp b))); Intros H2'.
Rewrite FSuccDiff2; Auto with arith.
Unfold FtoR; Simpl; AutoRewrite [Rsimpl]; Auto with real.
Rewrite FSuccDiff3; Auto with arith.
Unfold FtoR; Simpl; AutoRewrite [Rsimpl]; Auto with real.
Apply Rlt_le; Apply Rlt_powerRZ; Auto with real zarith.
Replace R1 with (INR (1)); Auto with real arith.
Unfold Zpred; Auto with zarith.
Rewrite FSuccDiff1; Auto with arith.
Unfold FtoR; Simpl; AutoRewrite [Rsimpl]; Auto with real.
Qed.

Theorem FulpSuc:
  (p:float) (Fbounded b p) ->
  (Rle (Rminus (FNSucc b radix precision p) p) (Fulp p)).
Intros p H'.
Replace (Fulp p) with (Fulp (Fnormalize radix b precision p)).
Replace (FtoRradix p) with (FtoRradix (Fnormalize radix b precision p)).
Unfold FNSucc; Apply FulpSucCan; Auto with float arith.
Unfold FtoRradix; Apply FnormalizeCorrect; Auto.
Apply FulpComp; Auto with float arith.
Unfold FtoRradix; Apply FnormalizeCorrect; Auto.
Qed.

Theorem FulpPredCan:
  (p:float) (Fcanonic radix b precision p) ->
  (Rle (Rminus p (FPred b radix precision p)) (Fulp p)).
Intros p H'.
Replace (Fulp p) with (powerRZ radix (Fexp p)).
2:Unfold Fulp; Replace (Fnormalize radix b precision p) with p; Auto;
   Apply sym_equal; Apply FcanonicUnique with 3 := pGivesBound; Auto with arith;
   Apply FnormalizeCanonic Orelse Apply FnormalizeCorrect; Auto with arith;
   Intuition.
Unfold FtoRradix; Rewrite <- Fminus_correct; Auto with arith.
Case (Z_eq_dec (Fnum p) (nNormMin radix precision)); Intros H1'.
Case (Z_eq_dec (Fexp p) (Zopp (dExp b))); Intros H2'.
Rewrite FPredDiff2; Auto with arith.
Unfold FtoR; Simpl; AutoRewrite [Rsimpl]; Auto with real.
Rewrite FPredDiff3; Auto with arith.
Unfold FtoR; Simpl; AutoRewrite [Rsimpl]; Auto with real.
Apply Rlt_le; Apply Rlt_powerRZ; Auto with real zarith.
Replace R1 with (INR (1)); Auto with real arith.
Unfold Zpred; Auto with zarith.
Rewrite FPredDiff1; Auto with arith.
Unfold FtoR; Simpl; AutoRewrite [Rsimpl]; Auto with real.
Qed.

Theorem FulpPred:
  (p:float) (Fbounded b p) ->
  (Rle (Rminus p (FNPred b radix precision p)) (Fulp p)).
Intros p H'.
Replace (Fulp p) with (Fulp (Fnormalize radix b precision p)).
Replace (FtoRradix p) with (FtoRradix (Fnormalize radix b precision p)).
Unfold FNPred; Apply FulpPredCan; Auto with float arith.
Unfold FtoRradix; Apply FnormalizeCorrect; Auto.
Apply FulpComp; Auto with float arith.
Unfold FtoRradix; Apply FnormalizeCorrect; Auto.
Qed.

Theorem RoundedModeUlp:
  (P:?) (RoundedModeP b radix P) ->
  (p, q:float) (P p q) ->(Rlt (Rabsolu (Rminus p q)) (Fulp q)).
Intros P H' p q H'0.
Case (Req_EM p q); Intros Eq1.
Rewrite <- Eq1.
Replace (Rminus p p) with R0; [Idtac | Ring].
Rewrite Rabsolu_R0; Auto.
Unfold Fulp FtoRradix FtoR; Simpl; Auto with real arith.
Case H'.
Intros H'1 H'2; Elim H'2; Intros H'3 H'4; Elim H'4; Intros H'5 H'6;
Case H'5 with 1 := H'0; Clear H'5 H'4 H'2; Intros H'5.
Rewrite Rabsolu_simpl1; Auto.
Cut (Fbounded b q); [Intros B0 | Intuition].
Apply Rlt_le_trans with 2 := (FulpSuc q B0).
Apply Rlt_anti_compatibility with r := (FtoR radix q).
Repeat Rewrite Rplus_Rminus; Auto.
Case (Rle_or_lt (FNSucc b radix precision q) p); Auto.
Intros H'2; Absurd (Rle (FNSucc b radix precision q) q); Auto.
Unfold FtoRradix; Auto with real float arith.
Case H'5; Auto.
Intros H'4 H'7; Elim H'7; Intros H'8 H'9; Apply H'9; Clear H'7; Auto.
Apply (FcanonicBound radix b precision); Auto with float arith.
Apply Rle_anti_compatibility with r := (FtoR radix q).
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Intuition.
Rewrite Rabsolu_simpl2; Auto.
Rewrite Rminus_Ropp; Auto.
Cut (Fbounded b q); [Intros B0 | Intuition].
Apply Rlt_le_trans with 2 := (FulpPred q B0).
Apply Ropp_Rlt; Repeat Rewrite Rminus_Ropp.
Apply Rlt_anti_compatibility with r := (FtoR radix q).
Repeat Rewrite Rplus_Rminus; Auto.
Case (Rle_or_lt p (FNPred b radix precision q)); Auto.
Intros H'2; Absurd (Rle q (FNPred b radix precision q)); Auto.
Unfold FtoRradix; Auto with real float arith.
Case H'5; Auto.
Intros H'4 H'7; Elim H'7; Intros H'8 H'9; Apply H'9; Clear H'7; Auto.
Apply (FcanonicBound radix b precision); Auto with float arith.
Apply Rle_anti_compatibility with r := (FtoR radix q).
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Intuition.
Qed.

Theorem FBoundedScale:
  (p:float) (n:nat) (Fbounded b p) ->
  (Fbounded b (Float (Fnum p) (Zplus (Fexp p) n))).
Intros p n H'; Repeat Split; Simpl.
Intuition.
Intuition.
Apply Zle_trans with (Fexp p).
Intuition.
Pattern 1 (Fexp p);
(Replace (Fexp p) with (Zplus (Fexp p) O); [Idtac | Simpl; Ring]).
Apply Zle_reg_l.
Apply inj_le; Auto with arith.
Qed.

Theorem FvalScale:
  (p:float) (n:nat)
  <R> (Float (Fnum p) (Zplus (Fexp p) n))==(Rmult (powerRZ radix n) p).
Intros p n; Unfold FtoRradix FtoR; Simpl.
Rewrite powerRZ_add; Auto with real arith.
Ring.
Qed.

Theorem RoundedModeProjectorIdem:
  (P:?) (p:float) (RoundedModeP b radix P) -> (Fbounded b p) ->(P p p).
Intros P p H' H.
Elim H'; Intros H'0 H'1; Elim H'1; Intros H'2 H'3; Elim H'3; Intros H'4 H'5;
Clear H'3 H'1.
Case (H'0 p).
Intros x H'6.
Apply (H'2 p p x); Auto.
Apply sym_eqT; Apply (RoundedProjector ? ? P H'); Auto.
Qed.

Theorem RoundedModeBounded:
  (P:?) (r:R) (q:float) (RoundedModeP b radix P) -> (P r q) ->(Fbounded b q).
Intros P r q H' H'0.
Case H'.
Intros H'1 H'2; Elim H'2; Intros H'3 H'4; Elim H'4; Intros H'5 H'6;
Case H'5 with 1 := H'0; Clear H'4 H'2; Intuition.
Qed.

Theorem RoundedModeMult:
  (P:?) (RoundedModeP b radix P) ->
  (r:R) (q, q':float) (P r q) -> (Fbounded b q') -> (Rle r (Rmult radix q')) ->
  (Rle q (Rmult radix q')).
Intros P H' r q q' H'0 H'1.
Replace (Rmult radix q')
     with (FtoRradix (Float (Fnum q') (Zplus (Fexp q') (1)))).
Intros H'2; Case H'2.
Intros H'3; Case H'; Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Elim H'7;
Intros H'8 H'9; Apply H'9 with 1 := H'3; Clear H'7 H'5; Auto.
Apply RoundedModeProjectorIdem; Auto.
Apply FBoundedScale; Auto.
Intros H'3.
Replace (FtoRradix q) with (FtoRradix (Float (Fnum q') (Zplus (Fexp q') (1))));
Auto with real.
Apply (RoundedProjector ? ? P H'); Auto.
Apply FBoundedScale; Auto.
Case H'.
Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Clear H'5.
Apply (H'6 r (Float (Fnum q') (Zplus (Fexp q') (1))) q); Auto.
Apply RoundedModeBounded with P := P r := r; Auto.
Rewrite FvalScale.
Rewrite powerRZ_1; Auto.
Qed.

Theorem RoundedModeMultLess:
  (P:?) (RoundedModeP b radix P) ->
  (r:R) (q, q':float) (P r q) -> (Fbounded b q') -> (Rle (Rmult radix q') r) ->
  (Rle (Rmult radix q') q).
Intros P H' r q q' H'0 H'1.
Replace (Rmult radix q')
     with (FtoRradix (Float (Fnum q') (Zplus (Fexp q') (1)))).
Intros H'2; Case H'2.
Intros H'3; Case H'; Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Elim H'7;
Intros H'8 H'9; Apply H'9 with 1 := H'3; Clear H'7 H'5; Auto.
Apply RoundedModeProjectorIdem; Auto.
Apply FBoundedScale; Auto.
Intros H'3.
Replace (FtoRradix q) with (FtoRradix (Float (Fnum q') (Zplus (Fexp q') (1))));
Auto with real.
Apply (RoundedProjector ? ? P H'); Auto.
Apply FBoundedScale; Auto.
Unfold FtoRradix in H'3; Rewrite H'3; Auto.
Case H'.
Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Clear H'5.
Unfold FtoRradix; Rewrite FvalScale; Auto.
Rewrite powerRZ_1; Auto.
Qed.

Theorem RleMinR0:
  (r:R) (min:float) (Rle R0 r) -> (isMin b radix r min) ->(Rle R0 min).
Intros r min H' H'0.
Rewrite <- (FzeroisZero radix b).
Case H'; Intros H'1.
Apply (MonotoneMin b radix) with p := (FtoRradix (Fzero (Zopp (dExp b)))) q := r;
Auto.
Unfold FtoRradix; Rewrite (FzeroisZero radix b); Auto.
Apply (RoundedModeProjectorIdem (isMin b radix)); Auto.
Apply MinRoundedModeP with precision := precision; Auto with float.
Apply FboundedFzero; Auto.
Replace (FtoR radix (Fzero (Zopp (dExp b)))) with (FtoRradix min);
Auto with real.
Apply sym_eqT; Apply (ProjectMin b radix).
Apply FboundedFzero; Auto.
Rewrite <- H'1 in H'0; Rewrite <- (FzeroisZero radix b) in H'0; Auto.
Qed.

Theorem RleRoundedR0:
  (P:R -> float ->Prop)
  (p:float) (r:R) (RoundedModeP b radix P) -> (P r p) -> (Rle R0 r) ->(Rle R0 p).
Intros P p r H' H'0 H'1.
Case H'.
Intros H'2 H'3; Elimc H'3; Intros H'3 H'4; Elimc H'4; Intros H'4 H'5;
Case (H'4 r p); Auto; Intros H'6.
Apply RleMinR0 with r := r; Auto.
Apply Rle_trans with r; Auto; Intuition.
Qed.

Theorem RleMaxR0:
  (r:R) (max:float) (Rle r R0) -> (isMax b radix r max) ->(Rle max R0).
Intros r max H' H'0.
Rewrite <- (FzeroisZero radix b).
Case H'; Intros H'1.
Apply (MonotoneMax b radix) with q := (FtoRradix (Fzero (Zopp (dExp b)))) p := r;
Auto.
Unfold FtoRradix; Rewrite FzeroisZero; Auto.
Apply (RoundedModeProjectorIdem (isMax b radix)); Auto.
Apply MaxRoundedModeP with precision := precision; Auto.
Apply FboundedFzero; Auto.
Replace (FtoR radix (Fzero (Zopp (dExp b)))) with (FtoRradix max);
Auto with real.
Apply sym_eqT; Apply (ProjectMax b radix).
Apply FboundedFzero; Auto.
Rewrite H'1 in H'0; Rewrite <- (FzeroisZero radix b) in H'0; Auto.
Qed.

Theorem RleRoundedLessR0:
  (P:R -> float ->Prop)
  (p:float) (r:R) (RoundedModeP b radix P) -> (P r p) -> (Rle r R0) ->(Rle p R0).
Intros P p r H' H'0 H'1.
Case H'.
Intros H'2 H'3; Elimc H'3; Intros H'3 H'4; Elimc H'4; Intros H'4 H'5;
Case (H'4 r p); Auto; Intros H'6.
Apply Rle_trans with r; Auto; Intuition.
Apply RleMaxR0 with r := r; Auto.
Qed.

Theorem RoundedModeMultAbs:
  (P:?) (RoundedModeP b radix P) ->
  (r:R)
  (q, q':float)
  (P r q) -> (Fbounded b q') -> (Rle (Rabsolu r) (Rmult radix q')) ->
  (Rle (Rabsolu q) (Rmult radix q')).
Intros P H' r q q' H'0 H'1 H'2.
Case (Rle_or_lt R0 r); Intros Rl0.
Rewrite Rabsolu_simpl1; Auto.
Apply RoundedModeMult with P := P r := r; Auto.
Rewrite <- (Rabsolu_simpl1 r); Auto.
Apply RleRoundedR0 with P := P r := r; Auto.
Rewrite Rabsolu_simpl2; Auto.
Replace (Rmult radix q') with (Ropp (Rmult radix (Ropp q')));
[Apply Rle_Ropp | Ring].
Rewrite <- (Fopp_correct radix).
Apply RoundedModeMultLess with P := P r := r; Auto.
Apply oppBounded; Auto.
Unfold FtoRradix; Rewrite Fopp_correct.
Rewrite <- (Ropp_Ropp r).
Replace (Rmult radix (Ropp (FtoR radix q'))) with (Ropp (Rmult radix q'));
[Apply Rle_Ropp | Ring]; Auto.
Rewrite <- (Rabsolu_simpl2 r); Auto.
Apply Rlt_le; Auto.
Ring.
Apply RleRoundedLessR0 with P := P r := r; Auto.
Apply Rlt_le; Auto.
Qed.

Theorem isMinComp:
  (r1, r2:R)
  (min, max:float)
  (isMin b radix r1 min) ->
  (isMax b radix r1 max) -> (Rlt min r2) -> (Rlt r2 max) ->
  (isMin b radix r2 min).
Intros r1 r2 min max H' H'0 H'1 H'2; Split.
Intuition.
Split.
Apply Rlt_le; Auto.
Intros f H'3 H'4.
Case H'; Auto.
Intros H'5 H'6; Elim H'6; Intros H'7 H'8; Apply H'8; Clear H'6; Auto.
Case (Rle_or_lt (FtoR radix f) r1); Auto; Intros C1.
Absurd (Rlt (FtoR radix f) max).
Apply Rlt_not.
Case H'0.
Intros H'6 H'9; Elim H'9; Intros H'10 H'11; Apply H'11; Clear H'9; Auto.
Apply Rlt_le; Auto.
Apply Rle_lt_trans with 2 := H'2; Auto.
Qed.

Theorem isMaxComp:
  (r1, r2:R)
  (min, max:float)
  (isMin b radix r1 min) ->
  (isMax b radix r1 max) -> (Rlt min r2) -> (Rlt r2 max) ->
  (isMax b radix r2 max).
Intros r1 r2 min max H' H'0 H'1 H'2; Split.
Intuition.
Split.
Apply Rlt_le; Auto.
Intros f H'3 H'4.
Case H'0; Auto.
Intros H'5 H'6; Elim H'6; Intros H'7 H'8; Apply H'8; Clear H'6; Auto.
Case (Rle_or_lt r1 (FtoR radix f)); Auto; Intros C1.
Absurd (Rlt min (FtoR radix f)).
Apply Rlt_not.
Case H'.
Intros H'6 H'9; Elim H'9; Intros H'10 H'11; Apply H'11; Clear H'9; Auto.
Apply Rlt_le; Auto.
Apply Rlt_le_trans with 1 := H'1; Auto.
Qed.
End FRoundP.
Hints Resolve FulpSucCan FulpSuc FulpPredCan FulpPred :float.

14/12/100, 16:20