Fround.v

(****************************************************************************                                                                                         IEEE754  :  Fround                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Export Float.
Require Export Fnorm.
Require Export Fop.
Require Export Fcomp.
Require Export FSucc.
Require Export FPred.
Require Export Fmin.
Require Export Fodd.
Require Export Fprop.
Section FRound.
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 TotalP := [P:R -> float ->Prop] (r:R)(Ex [p:float] (P r p)).

Definition UniqueP :=
   [P:R -> float ->Prop] (r:R) (p, q:float) (P r p) -> (P r q) -><R> p==q.

Definition CompatibleP :=
   [P:R -> float ->Prop]
   (r1, r2:R) (p, q:float) (P r1 p) -> r1==r2 -> <R> p==q -> (Fbounded b q) ->
   (P r2 q).

Definition MinOrMaxP :=
   [P:R -> float ->Prop] (r:R) (p:float) (P r p) ->
   (isMin b radix r p) \/ (isMax b radix r p).

Definition RoundedModeP :=
   [P:R -> float ->Prop]
   (TotalP P) /\ ((CompatibleP P) /\ ((MinOrMaxP P) /\ (MonotoneP radix P))).

Theorem RoundedProjector: (P:?) (RoundedModeP P) ->(ProjectorP b radix P).
Intros P H'; Red.
Intros p q H'0 H'1.
Red in H'.
Elim H'; Intros H'2 H'3; Elim H'3; Intros H'4 H'5; Elim H'5; Intros H'6 H'7;
Case (H'6 p q); Clear H'5 H'3 H'; Auto.
Intros H'; Apply (ProjectMin b radix p); Auto.
Intros H'; Apply (ProjectMax b radix p); Auto.
Qed.

Theorem MinCompatible: (CompatibleP (isMin b radix)).
Red.
Intros r1 r2 p q H' H'0 H'1 H'2; Split; Auto.
Rewrite <- H'0; Unfold FtoRradix in H'1; Rewrite <- H'1; Auto; Intuition.
Qed.

Theorem MinRoundedModeP: (RoundedModeP (isMin b radix)).
Split; Try Red.
Intros r; Apply MinEx with precision := precision; Auto with arith.
Split; Try Exact MinCompatible.
Split; Try Apply MonotoneMin; Red; Auto.
Qed.

Theorem MaxCompatible: (CompatibleP (isMax b radix)).
Red.
Intros r1 r2 p q H' H'0 H'1 H'2; Split; Auto.
Rewrite <- H'0; Unfold FtoRradix in H'1; Rewrite <- H'1; Auto; Intuition.
Qed.

Theorem MaxRoundedModeP: (RoundedModeP (isMax b radix)).
Split; Try Red.
Intros r; Apply MaxEx with precision := precision; Auto with arith.
Split; Try Exact MaxCompatible.
Split; Try Apply MonotoneMax; Red; Auto.
Qed.

Definition ToZeroP :=
   [r:R] [p:float]
   (Rle R0 r) /\ (isMin b radix r p) \/ (Rle r R0) /\ (isMax b radix r p).

Theorem ToZeroTotal: (TotalP ToZeroP).
Red; Intros r; Case (Rle_or_lt r R0); Intros H1.
Case MaxEx with r := r 3 := pGivesBound; Auto with arith.
Intros x H'; Exists x; Red; Auto.
Case MinEx with r := r 3 := pGivesBound; Auto with arith.
Intros x H'; Exists x; Red; Left; Split; Auto.
Apply Rlt_le; Auto.
Qed.

Theorem ToZeroCompatible: (CompatibleP ToZeroP).
Red.
Intros r1 r2 p q H'; Case H'.
Intros H'0 H'1 H'2; Left; Split; Try Apply MinCompatible with p := p r1 := r1;
Try Rewrite <- H'1; Auto; Intuition.
Intros H'0 H'1 H'2; Right; Split; Try Apply MaxCompatible with p := p r1 := r1;
Try Rewrite <- H'1; Auto; Intuition.
Qed.

Theorem ToZeroMinOrMax: (MinOrMaxP ToZeroP).
Red.
Intros r p H'; Case H'; Clear H'; Intros H'.
Left; Intuition.
Right; Intuition.
Qed.

Theorem ToZeroMonotone: (MonotoneP radix ToZeroP).
Red.
Cut (FtoR radix (Fzero (Zopp (dExp b))))==R0;
[Intros Eq0 | Unfold FtoR; Simpl; AutoRewrite [Rsimpl]]; Auto.
Intros p q p' q' H' H'0; Case H'0; Clear H'0.
Intros H'0; Elim H'0; Intros H'1 H'2; Clear H'0; Intros H'0.
Case H'0; Intros H'3; Elim H'3; Clear H'3; Auto.
Intros H'3 H'4.
Apply (MonotoneMin b radix) with p := p q := q; Auto.
Intros H'3 H'4.
Apply Rle_trans with p; [Intuition | Idtac].
Apply Rle_trans with q; [Auto | Intuition].
Apply Rlt_le; Auto.
Intros H'0; Elim H'0; Intros H'1 H'2; Clear H'0.
Intros H'0; Case H'0; Clear H'0; Intros H'0; Case H'0; Intros H'3 H'4; Clear H'0.
Apply Rle_trans with (FtoRradix (Fzero (Zopp (dExp b)))); Auto.
Elim H'2.
Intros H'0 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Clear H'5; Auto.
Repeat Split; Simpl; Auto with zarith.
Rewrite Eq0; Auto.
Elim H'4.
Intros H'0 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Clear H'5; Auto.
Repeat Split; Simpl; Auto with zarith.
Rewrite Eq0; Auto.
Apply (MonotoneMax b radix) with p := p q := q; Auto.
Qed.

Theorem ToZeroRoundedModeP: (RoundedModeP ToZeroP).
Repeat Split.
Try Exact ToZeroTotal.
Try Exact ToZeroCompatible.
Try Exact ToZeroMinOrMax.
Try Exact ToZeroMonotone.
Qed.

Definition ToInfinityP :=
   [r:R] [p:float]
   (Rle r R0) /\ (isMin b radix r p) \/ (Rle R0 r) /\ (isMax b radix r p).

Theorem ToInfinityTotal: (TotalP ToInfinityP).
Red; Intros r; Case (Rle_or_lt r R0); Intros H1.
Case MinEx with r := r 3 := pGivesBound; Auto with arith.
Intros x H'; Exists x; Red; Auto.
Case MaxEx with r := r 3 := pGivesBound; Auto with arith.
Intros x H'; Exists x; Red; Right; Split; Auto.
Apply Rlt_le; Auto.
Qed.

Theorem ToInfinityCompatible: (CompatibleP ToInfinityP).
Red.
Intros r1 r2 p q H'; Case H'.
Intros H'0 H'1 H'2; Left; Split; Try Apply MinCompatible with p := p r1 := r1;
Try Rewrite <- H'1; Intuition.
Intros H'0 H'1 H'2; Right; Split; Try Apply MaxCompatible with p := p r1 := r1;
Try Rewrite <- H'1; Intuition.
Qed.

Theorem ToInfinityMinOrMax: (MinOrMaxP ToInfinityP).
Red.
Intros r p H'; Case H'; Clear H'; Intros H'.
Left; Intuition.
Right; Intuition.
Qed.

Theorem ToInfinityMonotone: (MonotoneP radix ToInfinityP).
Red.
Cut (FtoR radix (Fzero (Zopp (dExp b))))==R0;
[Intros Eq0 | Unfold FtoR; Simpl; AutoRewrite [Rsimpl]]; Auto.
Intros p q p' q' H' H'0; Case H'0; Clear H'0.
Intros H'0; Elim H'0; Intros H'1 H'2; Clear H'0; Intros H'0.
Case H'0; Intros H'3; Elim H'3; Clear H'3; Auto.
Intros H'3 H'4.
Apply (MonotoneMin b radix) with p := p q := q; Auto.
Intros H'3 H'4.
Apply Rle_trans with p; [Intuition | Idtac].
Apply Rle_trans with q; [Auto | Intuition].
Apply Rlt_le; Auto.
Intros H'0; Elim H'0; Intros H'1 H'2; Clear H'0.
Intros H'0; Case H'0; Clear H'0; Intros H'0; Case H'0; Intros H'3 H'4; Clear H'0.
2:Apply (MonotoneMax b radix) with p := p q := q; Auto.
Apply Rle_trans with (FtoRradix (Fzero (Zopp (dExp b)))); Auto.
Elim H'2.
Intros H'0 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Clear H'5; Auto.
Repeat Split; Simpl; Auto with zarith.
Apply Rle_trans with q; Auto.
Apply Rlt_le; Auto.
Rewrite Eq0; Auto.
Elim H'4.
Intros H'0 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Clear H'5; Auto.
Repeat Split; Simpl; Auto with zarith.
Apply Rle_trans with p; Auto.
Rewrite Eq0; Auto.
Apply Rlt_le; Auto.
Qed.

Theorem ToInfinityRoundedModeP: (RoundedModeP ToInfinityP).
Repeat Split.
Try Exact ToInfinityTotal.
Try Exact ToInfinityCompatible.
Try Exact ToInfinityMinOrMax.
Try Exact ToInfinityMonotone.
Qed.

Theorem MinUniqueP: (UniqueP (isMin b radix)).
Red.
Intros r p q H' H'0.
Unfold FtoRradix; Apply MinEq with 1 := H'; Auto.
Qed.

Theorem MaxUniqueP: (UniqueP (isMax b radix)).
Red.
Intros r p q H' H'0.
Unfold FtoRradix; Apply MaxEq with 1 := H'; Auto.
Qed.

Theorem ToZeroUniqueP: (UniqueP ToZeroP).
Red.
Intros r p q H' H'0.
Inversion H'; Inversion H'0; Elim H0; Elim H; Clear H0 H; Intros H'1 H'2 H'3 H'4.
Apply (MinUniqueP r); Auto.
Cut <R> r==(Fzero (Zopp (dExp b)));
[Intros Eq0 |
   Apply Rle_antisym; Unfold FtoRradix Fzero FtoR; Simpl; AutoRewrite [Rsimpl]];
Auto.
Apply trans_eqT with (FtoRradix (Fzero (Zopp (dExp b)))).
Apply sym_eqT; Unfold FtoRradix; Apply (RoundedProjector ? ToZeroRoundedModeP);
Auto with float.
Unfold FtoRradix in Eq0; Rewrite <- Eq0; Auto.
Unfold FtoRradix; Apply (RoundedProjector ? ToZeroRoundedModeP); Auto with float.
Unfold FtoRradix in Eq0; Rewrite <- Eq0; Auto.
Cut <R> r==(Fzero (Zopp (dExp b)));
[Intros Eq0 |
   Apply Rle_antisym; Unfold FtoRradix Fzero FtoR; Simpl; AutoRewrite [Rsimpl]];
Auto.
Apply trans_eqT with (FtoRradix (Fzero (Zopp (dExp b)))).
Apply sym_eqT; Unfold FtoRradix; Apply (RoundedProjector ? ToZeroRoundedModeP);
Auto with float.
Unfold FtoRradix in Eq0; Rewrite <- Eq0; Auto.
Unfold FtoRradix; Apply (RoundedProjector ? ToZeroRoundedModeP); Auto with float.
Unfold FtoRradix in Eq0; Rewrite <- Eq0; Auto.
Apply (MaxUniqueP r); Auto.
Qed.

Theorem ToInfinityUniqueP: (UniqueP ToInfinityP).
Red.
Intros r p q H' H'0.
Inversion H'; Inversion H'0; Elim H0; Elim H; Clear H0 H; Intros H'1 H'2 H'3 H'4.
Apply (MinUniqueP r); Auto.
Cut <R> r==(Fzero (Zopp (dExp b)));
[Intros Eq0 |
   Apply Rle_antisym; Unfold FtoRradix Fzero FtoR; Simpl; AutoRewrite [Rsimpl]];
Auto.
Apply trans_eqT with (FtoRradix (Fzero (Zopp (dExp b)))).
Apply sym_eqT; Unfold FtoRradix;
Apply (RoundedProjector ? ToInfinityRoundedModeP); Auto.
Apply FboundedFzero; Auto.
Unfold FtoRradix in Eq0; Rewrite <- Eq0; Auto.
Unfold FtoRradix; Apply (RoundedProjector ? ToInfinityRoundedModeP); Auto.
Apply FboundedFzero; Auto.
Unfold FtoRradix in Eq0; Rewrite <- Eq0; Auto.
Cut <R> r==(Fzero (Zopp (dExp b)));
[Intros Eq0 |
   Apply Rle_antisym; Unfold FtoRradix Fzero FtoR; Simpl; AutoRewrite [Rsimpl]];
Auto.
Apply trans_eqT with (FtoRradix (Fzero (Zopp (dExp b)))).
Apply sym_eqT; Unfold FtoRradix;
Apply (RoundedProjector ? ToInfinityRoundedModeP); Auto.
Apply FboundedFzero; Auto.
Unfold FtoRradix in Eq0; Rewrite <- Eq0; Auto.
Unfold FtoRradix; Apply (RoundedProjector ? ToInfinityRoundedModeP); Auto.
Apply FboundedFzero; Auto.
Unfold FtoRradix in Eq0; Rewrite <- Eq0; Auto.
Apply (MaxUniqueP r); Auto.
Qed.

Theorem FnOddNEven:
  (n:float) (FNodd b radix precision n) ->~ (FNeven b radix precision n).
Intros n H'; Unfold FNeven Feven; Apply OddNEven; Auto.
Qed.

Theorem MinOrMaxRep:
  (P:?) (MinOrMaxP P) ->
  (p, q:float) (P p q) ->(Ex [m:Z] <R> q==(Float m (Fexp p))).
Intros P H' p q H'0; Case (H' p q); Auto; Intros H'1.
Apply FminRep with 3 := pGivesBound; Auto with arith.
Apply FmaxRep with 3 := pGivesBound; Auto with arith.
Qed.

Theorem RoundedModeRep:
  (P:?) (RoundedModeP P) ->
  (p, q:float) (P p q) ->(Ex [m:Z] <R> q==(Float m (Fexp p))).
Intros P H' p q H'0.
Apply MinOrMaxRep with P := P; Auto.
Intuition; Auto.
Qed.

Definition SymmetricP :=
   [P:R -> float ->Prop] (r:R) (p:float) (P r p) ->(P (Ropp r) (Fopp p)).

Theorem ToZeroSymmetric: (SymmetricP ToZeroP).
Red; Intros r p H'; Case H'; Clear H'; Intros H'; Case H'; Intros H'1 H'2.
Right; Split; Auto.
Replace R0 with (Ropp R0); Auto with real.
Apply MinOppMax; Auto.
Left; Split; Auto.
Replace R0 with (Ropp R0); Auto with real.
Apply MaxOppMin; Auto.
Qed.

Theorem ToInfinitySymmetric: (SymmetricP ToInfinityP).
Red; Intros r p H'; Case H'; Clear H'; Intros H'; Case H'; Intros H'1 H'2.
Right; Split; Auto.
Replace R0 with (Ropp R0); Auto with real.
Apply MinOppMax; Auto.
Left; Split; Auto.
Replace R0 with (Ropp R0); Auto with real.
Apply MaxOppMin; Auto.
Qed.
End FRound.
Hints Resolve
RoundedProjector MinCompatible MinRoundedModeP MaxCompatible MaxRoundedModeP
ToZeroTotal ToZeroCompatible ToZeroMinOrMax ToZeroMonotone ToZeroRoundedModeP
ToInfinityTotal ToInfinityCompatible ToInfinityMinOrMax ToInfinityMonotone
ToInfinityRoundedModeP MinUniqueP MaxUniqueP ToZeroUniqueP ToInfinityUniqueP
FnOddNEven ToZeroSymmetric ToInfinitySymmetric :float.

14/12/100, 15:43