Closest.v

Require Export Fround.
Section Fclosest.
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 Closest :=
   [r:R] [p:float]
   (Fbounded b p) /\
   ((f:float) (Fbounded b f) ->
    (Rle (Rabsolu (Rminus p r)) (Rabsolu (Rminus f r)))).

Theorem ClosestTotal: (TotalP Closest).
Red; Intros r.
Case MinEx with r := r 3 := pGivesBound; Auto with arith.
Intros min H'.
Case MaxEx with r := r 3 := pGivesBound; Auto with arith.
Intros max H'0.
Cut (Rle min r); [Intros Rl1 | Intuition].
Cut (Rle r max); [Intros Rl2 | Intuition].
Case (Rle_or_lt (Rabsolu (Rminus min r)) (Rabsolu (Rminus max r))); Intros H'1.
Exists min; Split.
Intuition.
Intros f H'2.
Case (Rle_or_lt f r); Intros H'3.
Rewrite (Rabsolu_simpl2 (Rminus min r)); Auto with real.
Rewrite Rabsolu_simpl2; Auto with real.
Apply Rle_Ropp; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
Elim H'; Auto.
Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Clear H'5; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rle_trans with 1 := H'1.
Rewrite (Rabsolu_simpl1 (Rminus max r)); Auto with real.
Rewrite Rabsolu_simpl1; Auto with real.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
Elim H'0; Auto.
Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Clear H'5; Auto.
Apply Rlt_le; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rlt_le; Auto.
Repeat Rewrite Rplus_Rminus; Auto.
Apply Rle_anti_compatibility with r := r.
AutoRewrite [Rsimpl]; Auto.
Exists max; Split.
Intuition.
Intros f H'2.
Case (Rle_or_lt f r); Intros H'3.
Apply Rle_trans with 1 := (Rlt_le ? ? H'1).
Rewrite (Rabsolu_simpl2 (Rminus min r)); Auto with real.
Rewrite Rabsolu_simpl2; Auto with real.
Apply Rle_Ropp; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
Elim H'; Auto.
Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Clear H'5; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Rewrite (Rabsolu_simpl1 (Rminus max r)); Auto with real.
Rewrite Rabsolu_simpl1; Auto with real.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
Elim H'0; Auto.
Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Clear H'5; Auto.
Apply Rlt_le; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rlt_le; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Qed.

Theorem ClosestCompatible: (CompatibleP b radix Closest).
Red.
Intros r1 r2 p q H'; Case H'.
Intros H'0 H'1 H'2 H'3 H'4.
Split; Auto.
Intros f H'4.
Unfold FtoRradix; Rewrite <- H'3; Rewrite <- H'2; Auto.
Qed.

Theorem ClosestMin:
  (r:R)
  (min, max:float)
  (isMin b radix r min) ->
  (isMax b radix r max) -> (Rle (Rmult (2) r) (Rplus min max)) ->(Closest r min).
Intros r min max H' H'0 H'1; Split.
Intuition.
Intros f H'2.
Case (Rle_or_lt f r); Intros H'3.
Rewrite (Rabsolu_simpl2 (Rminus min r)).
Rewrite (Rabsolu_simpl2 (Rminus f r)).
Apply Rle_Ropp.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
Case H'; Auto.
Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Clear H'5; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Intuition; Auto.
Rewrite (Rabsolu_simpl2 (Rminus min r)).
Rewrite (Rabsolu_simpl1 (Rminus f r)).
Apply Rle_trans with (Rminus max r).
Cut (x, y:R)(Rplus (Ropp y) x)==(Ropp (Rminus y x));
[Intros Eq0; Repeat Rewrite Eq0; Clear Eq0 | Intros; Ring].
Cut (x, y:R)(Ropp (Rminus x y))==(Rminus y x);
[Intros Eq0; Repeat Rewrite Eq0; Clear Eq0 | Intros; Unfold Rminus; Ring].
Apply Rle_anti_compatibility with r := (FtoR radix min).
Repeat Rewrite Rplus_Rminus; Auto.
Apply Rle_anti_compatibility with r := r.
Replace (Rplus r (Rplus (FtoR radix min) (Rminus max r))) with (Rplus min max).
Replace (Rplus r r) with (Rmult (2) r); Auto.
Simpl; Ring.
Simpl; Ring.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
Case H'0; Auto.
Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Clear H'5; Auto.
Apply Rlt_le; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rlt_le; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Intuition.
Qed.

Theorem ClosestMax:
  (r:R)
  (min, max:float)
  (isMin b radix r min) ->
  (isMax b radix r max) -> (Rle (Rplus min max) (Rmult (2) r)) ->(Closest r max).
Intros r min max H' H'0 H'1; Split.
Intuition.
Intros f H'2.
Case (Rle_or_lt f r); Intros H'3.
Rewrite (Rabsolu_simpl1 (Rminus max r)).
Rewrite (Rabsolu_simpl2 (Rminus f r)).
Apply Rle_trans with (Rminus r min).
Apply Rle_anti_compatibility with r := (FtoRradix min).
Repeat Rewrite Rplus_Rminus; Auto.
Apply Rle_anti_compatibility with r := r.
Replace (Rplus r (Rplus min (Rminus max r))) with (Rplus min max).
Replace (Rplus r r) with (Rmult (2) r); Auto.
Simpl; Ring.
Simpl; Ring.
Replace (Rminus r min) with (Ropp (Rminus min r)).
Apply Rle_Ropp.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
Case H'; Auto.
Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Clear H'5; Auto.
Simpl; Ring.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Intuition.
Rewrite (Rabsolu_simpl1 (Rminus max r)).
Rewrite (Rabsolu_simpl1 (Rminus f r)).
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
Case H'0; Auto.
Intros H'4 H'5; Elim H'5; Intros H'6 H'7; Apply H'7; Clear H'5; Auto.
Apply Rlt_le; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rlt_le; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Intuition; Auto.
Qed.

Theorem ClosestMinOrMax: (MinOrMaxP b radix Closest).
Red.
Intros r p H'.
Case (Rle_or_lt p r); Intros H'1.
Left; Split; Auto.
Intuition; Auto.
Split; Auto.
Intros f H'0 H'2.
Apply Rle_anti_compatibility with r := (Ropp r).
Cut (x, y:R)(Rplus (Ropp y) x)==(Ropp (Rminus y x));
[Intros Eq0; Repeat Rewrite Eq0; Clear Eq0 | Intros; Ring].
Apply Rle_Ropp.
Rewrite <- (Rabsolu_simpl1 (Rminus r (FtoR radix p))).
Rewrite <- (Rabsolu_simpl1 (Rminus r (FtoR radix f))).
Cut (x, y:R)(Rabsolu (Rminus x y))==(Rabsolu (Rminus y x));
[Intros Eq0; Repeat Rewrite (Eq0 r); Clear Eq0 |
   Intros x y; Rewrite <- (Rabsolu_Ropp (Rminus x y)); Rewrite Ropp_distr2];
Auto.
Elim H'; Auto.
Apply Rle_anti_compatibility with r := (FtoR radix f).
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rle_anti_compatibility with r := (FtoR radix p).
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Right; Split; Auto.
Intuition; Auto.
Split; Auto.
Apply Rlt_le; Auto.
Intros f H'0 H'2.
Apply Rle_anti_compatibility with r := (Ropp r).
Cut (x, y:R)(Rplus (Ropp y) x)==(Ropp (Rminus y x));
[Intros Eq0; Repeat Rewrite Eq0; Clear Eq0 | Intros; Ring].
Rewrite <- (Rabsolu_simpl2 (Rminus r (FtoR radix p))).
Rewrite <- (Rabsolu_simpl2 (Rminus r (FtoR radix f))).
Cut (x, y:R)(Rabsolu (Rminus x y))==(Rabsolu (Rminus y x));
[Intros Eq0; Repeat Rewrite (Eq0 r); Clear Eq0 |
   Intros x y; Rewrite <- (Rabsolu_Ropp (Rminus x y)); Rewrite Ropp_distr2];
Auto.
Elim H'; Auto.
Apply Rle_anti_compatibility with r := (FtoR radix f).
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rle_anti_compatibility with r := (FtoR radix p).
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rlt_le; Auto.
Qed.

Theorem ClosestMinEq:
  (r:R)
  (min, max, p:float)
  (isMin b radix r min) ->
  (isMax b radix r max) ->
  (Rlt (Rmult (2) r) (Rplus min max)) -> (Closest r p) -><R> p==min.
Intros r min max p H' H'0 H'1 H'2.
Case (ClosestMinOrMax r p); Auto; Intros H'3.
Unfold FtoRradix; Apply MinEq with 1 := H'3; Auto.
Absurd (Rle (Rabsolu (Rminus max r)) (Rabsolu (Rminus min r))).
Apply Rle_not.
Rewrite (Rabsolu_simpl2 (Rminus min r)).
Rewrite Rabsolu_simpl1.
Replace (Ropp (Rminus min r)) with (Rminus r min); [Idtac | Ring].
Apply Rlt_anti_compatibility with r := (FtoRradix min).
Repeat Rewrite Rplus_Rminus; Auto.
Apply Rlt_anti_compatibility with r := r.
Replace (Rplus r r) with (Rmult (2) r); [Idtac | Simpl; Ring].
Replace (Rplus r (Rplus min (Rminus max r))) with (Rplus min max);
[Idtac | Ring]; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Intuition.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Intuition.
Cut (Closest r max).
Intros H'4; Case H'4.
Intros H'5 H'6; Apply H'6; Auto.
Intuition.
Apply ClosestCompatible with 1 := H'2; Auto.
Apply MaxEq with 1 := H'3; Auto.
Intuition.
Qed.

Theorem ClosestMaxEq:
  (r:R)
  (min, max, p:float)
  (isMin b radix r min) ->
  (isMax b radix r max) ->
  (Rlt (Rplus min max) (Rmult (2) r)) -> (Closest r p) -><R> p==max.
Intros r min max p H' H'0 H'1 H'2.
Case (ClosestMinOrMax r p); Auto; Intros H'3.
2:Unfold FtoRradix; Apply MaxEq with 1 := H'3; Auto.
Absurd (Rle (Rabsolu (Rminus min r)) (Rabsolu (Rminus max r))).
Apply Rle_not.
Rewrite (Rabsolu_simpl2 (Rminus min r)).
Rewrite Rabsolu_simpl1.
Replace (Ropp (Rminus min r)) with (Rminus r min); [Idtac | Ring].
Apply Rlt_anti_compatibility with r := (FtoRradix min).
Repeat Rewrite Rplus_Rminus; Auto.
Apply Rlt_anti_compatibility with r := r.
Replace (Rplus r r) with (Rmult (2) r); [Idtac | Simpl; Ring].
Replace (Rplus r (Rplus min (Rminus max r))) with (Rplus min max);
[Idtac | Ring]; Auto.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Intuition.
Apply Rle_anti_compatibility with r := r.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Intuition.
Cut (Closest r min).
Intros H'4; Case H'4.
Intros H'5 H'6; Apply H'6; Auto.
Intuition.
Apply ClosestCompatible with 1 := H'2; Auto.
Apply MinEq with 1 := H'3; Auto.
Intuition.
Qed.

Theorem ClosestMonotone: (MonotoneP radix Closest).
Red.
Intros p q p' q' H' H'0 H'1.
Change (Rle p' q').
Case (Rle_or_lt p p'); Intros Rl0.
Case (Rle_or_lt p q'); Intros Rl1.
Apply Rle_anti_compatibility with r := (Ropp p).
Cut (x, y:R)(Rplus (Ropp y) x)==(Ropp (Rminus y x));
[Intros Eq0; Repeat Rewrite Eq0; Clear Eq0 | Intros; Ring].
Rewrite <- (Rabsolu_simpl2 (Rminus p p')).
Rewrite <- (Rabsolu_simpl2 (Rminus p q')).
Cut (x, y:R)(Rabsolu (Rminus x y))==(Rabsolu (Rminus y x));
[Intros Eq0; Repeat Rewrite (Eq0 p); Clear Eq0 |
   Intros x y; Rewrite <- (Rabsolu_Ropp (Rminus x y)); Rewrite Ropp_distr2];
Auto.
Elim H'0; Auto.
Intros H'2 H'3; Apply H'3; Auto.
Intuition.
Apply Rle_anti_compatibility with r := (FtoR radix q').
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rle_anti_compatibility with r := (FtoR radix p').
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Case (Rle_or_lt p' q); Intros Rl2.
Apply Rle_anti_compatibility with r := (Ropp q).
Cut (x, y:R)(Rplus (Ropp y) x)==(Ropp (Rminus y x));
[Intros Eq0; Repeat Rewrite Eq0; Clear Eq0 | Intros; Ring].
Rewrite <- (Rabsolu_simpl1 (Rminus q p')).
2:Apply Rle_anti_compatibility with r := (FtoR radix p').
2:Repeat Rewrite Rplus_Rminus; Auto.
2:AutoRewrite [Rsimpl]; Auto.
Rewrite <- (Rabsolu_simpl1 (Rminus q q')).
2:Apply Rle_anti_compatibility with r := (FtoR radix q').
2:Repeat Rewrite Rplus_Rminus; Auto.
2:AutoRewrite [Rsimpl]; Auto.
2:Apply Rle_trans with 1 := (Rlt_le ? ? Rl1); Apply Rlt_le; Auto.
Cut (x, y:R)(Rabsolu (Rminus x y))==(Rabsolu (Rminus y x));
[Intros Eq0; Repeat Rewrite (Eq0 q); Clear Eq0 |
   Intros x y; Rewrite <- (Rabsolu_Ropp (Rminus x y)); Rewrite Ropp_distr2];
Auto.
Apply Rle_Ropp.
Elim H'1; Auto.
Intros H'2 H'3; Apply H'3; Auto.
Intuition.
Case (Rle_or_lt (Rminus p q') (Rminus p' q)); Intros Rl3.
Absurd (Rle (Rabsolu (Rminus p' p)) (Rabsolu (Rminus q' p))).
Apply Rle_not.
Rewrite (Rabsolu_simpl2 (Rminus q' p)).
2:Apply Rle_anti_compatibility with r := p.
2:Repeat Rewrite Rplus_Rminus; Auto.
2:AutoRewrite [Rsimpl]; Apply Rlt_le; Auto.
Rewrite (Rabsolu_simpl1 (Rminus p' p)).
2:Apply Rle_anti_compatibility with r := p.
2:AutoRewrite [Rsimpl]; Auto.
Cut (x, y:R)(Ropp (Rminus y x))==(Rminus x y);
[Intros Eq0; Repeat Rewrite Eq0; Clear Eq0 | Intros; Ring].
Apply Rle_lt_trans with 1 := Rl3.
Replace (Rminus p' p) with (Rplus (Rminus p' q) (Rminus q p)).
Pattern 1 (Rminus p' q); Replace (Rminus p' q) with (Rplus (Rminus p' q) R0).
Apply Rlt_compatibility; Auto.
Apply Rlt_anti_compatibility with r := p.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
AutoRewrite [Rsimpl]; Auto.
Ring.
Case H'0; Intros H'2 H'3; Apply H'3; Auto; Intuition.
Absurd (Rle (Rabsolu (Rminus q' q)) (Rabsolu (Rminus p' q))).
Apply Rle_not.
Rewrite (Rabsolu_simpl2 (Rminus q' q)).
2:Apply Rle_anti_compatibility with r := q.
2:Repeat Rewrite Rplus_Rminus; Auto.
2:AutoRewrite [Rsimpl]; Apply Rlt_le; Auto.
2:Apply Rlt_trans with 1 := Rl1; Auto.
Rewrite (Rabsolu_simpl1 (Rminus p' q)).
2:Apply Rle_anti_compatibility with r := q.
2:AutoRewrite [Rsimpl]; Apply Rlt_le; Auto.
Cut (x, y:R)(Ropp (Rminus y x))==(Rminus x y);
[Intros Eq0; Repeat Rewrite Eq0; Clear Eq0 | Intros; Ring].
Apply Rlt_trans with 1 := Rl3.
Replace (Rminus q q') with (Rplus (Rminus p q') (Rminus q p)).
Pattern 1 (Rminus p q'); Replace (Rminus p q') with (Rplus (Rminus p q') R0).
Apply Rlt_compatibility; Auto.
Apply Rlt_anti_compatibility with r := p.
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
AutoRewrite [Rsimpl]; Auto.
Ring.
Case H'1; Intros H'2 H'3; Apply H'3; Auto; Intuition.
Case (Rle_or_lt p q'); Intros Rl1.
Apply Rle_trans with p; Auto.
Apply Rlt_le; Auto.
Apply Rle_anti_compatibility with r := (Ropp q).
Cut (x, y:R)(Rplus (Ropp y) x)==(Ropp (Rminus y x));
[Intros Eq0; Repeat Rewrite Eq0; Clear Eq0 | Intros; Ring].
Rewrite <- (Rabsolu_simpl1 (Rminus q p')).
Rewrite <- (Rabsolu_simpl1 (Rminus q q')).
Apply Rle_Ropp.
Cut (x, y:R)(Rabsolu (Rminus x y))==(Rabsolu (Rminus y x));
[Intros Eq0; Repeat Rewrite (Eq0 q); Clear Eq0 |
   Intros x y; Rewrite <- (Rabsolu_Ropp (Rminus x y)); Rewrite Ropp_distr2];
Auto.
Elim H'1; Auto.
Intros H'2 H'3; Apply H'3; Auto.
Intuition.
Apply Rle_anti_compatibility with r := (FtoR radix q').
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rlt_le; Apply Rlt_trans with 1 := Rl1; Auto.
Apply Rle_anti_compatibility with r := (FtoR radix p').
Repeat Rewrite Rplus_Rminus; Auto.
AutoRewrite [Rsimpl]; Auto.
Apply Rlt_le; Apply Rlt_trans with 1 := Rl0; Auto.
Qed.

Theorem ClosestRoundedModeP: (RoundedModeP b radix Closest).
Split; Try Exact ClosestTotal.
Split; Try Exact ClosestCompatible.
Split; Try Exact ClosestMinOrMax.
Try Exact ClosestMonotone.
Qed.

Definition EvenClosest :=
   [r:R] [p:float]
   (Closest r p) /\
   ((FNeven b radix precision p) \/ ((q:float) (Closest r q) -><R> q==p)).

Theorem FNevenOrFNodd:
  (p:float)(FNeven b radix precision p) \/ (FNodd b radix precision p).
Intros p; Unfold FNeven FNodd; Apply FevenOrFodd.
Qed.

Theorem EvenClosestTotal: (TotalP EvenClosest).
Red; Intros r.
Case MinEx with r := r 3 := pGivesBound; Auto with arith.
Intros min H'.
Case MaxEx with r := r 3 := pGivesBound; Auto with arith.
Intros max H'0.
Cut (Rle min r); [Intros Rl1 | Intuition].
Cut (Rle r max); [Intros Rl2 | Intuition].
Case (Rle_or_lt (Rabsolu (Rminus min r)) (Rabsolu (Rminus max r))); Intros H'1.
Case H'1; Intros H'1; Auto.
Exists min; Split.
Apply ClosestMin with max := max; Auto.
Replace (Rmult (2) r) with (Rplus r r); [Idtac | Simpl; Ring].
Apply Rminus_le; Auto.
Replace (Rminus (Rplus r r) (Rplus min max))
     with (Rminus (Rminus r min) (Rminus max r)); [Idtac | Simpl; Ring].
Apply Rle_minus; Auto.
Rewrite Rabsolu_minus_sym in H'1; Auto.
Rewrite Rminus_Rabsolu in H'1; Auto; Rewrite Rminus_Rabsolu in H'1; Auto.
Right; Intros q H'3.
Apply ClosestMinEq with r := r max := max; Auto.
Replace (Rmult (2) r) with (Rplus r r); [Idtac | Simpl; Ring].
Apply Rminus_lt; Auto.
Replace (Rminus (Rplus r r) (Rplus min max))
     with (Rminus (Rminus r min) (Rminus max r)); [Idtac | Simpl; Ring].
Apply Rlt_minus; Auto.
Rewrite Rabsolu_minus_sym in H'2; Auto.
Rewrite Rminus_Rabsolu in H'2; Auto; Rewrite Rminus_Rabsolu in H'2; Auto.
Case (FNevenOrFNodd min); Intros Ev0.
Exists min; Split; Auto.
Apply ClosestMin with max := max; Auto.
Replace (Rmult (2) r) with (Rplus r r); [Idtac | Simpl; Ring].
Apply Rminus_le; Auto.
Replace (Rminus (Rplus r r) (Rplus min max))
     with (Rminus (Rminus r min) (Rminus max r)); [Idtac | Simpl; Ring].
Apply Rle_minus; Auto.
Rewrite Rabsolu_minus_sym in H'1; Auto.
Rewrite Rminus_Rabsolu in H'1; Auto; Rewrite Rminus_Rabsolu in H'1; Auto.
Exists max; Split; Auto.
Apply ClosestMax with min := min; Auto.
Replace (Rmult (2) r) with (Rplus r r); [Idtac | Simpl; Ring].
Apply Rminus_le; Auto.
Replace (Rminus (Rplus min max) (Rplus r r))
     with (Rminus (Rminus max r) (Rminus r min)); [Idtac | Simpl; Ring].
Apply Rle_minus; Auto.
Rewrite Rabsolu_minus_sym in H'2; Auto.
Rewrite Rminus_Rabsolu in H'2; Auto; Rewrite Rminus_Rabsolu in H'2; Auto.
Rewrite H'2; Auto with real.
Case (Req_EM min max); Intros H'5.
Right; Intros q H'3.
Case (ClosestMinOrMax ? ? H'3); Intros isM0.
Rewrite <- H'5.
Apply MinEq with 1 := isM0; Auto.
Apply MaxEq with 1 := isM0; Auto.
Left.
Apply FNevenEq with f1 := (FNSucc b radix precision min); Auto.
Apply FcanonicBound with radix := radix precision := precision.
Apply FNSuccCanonic; Auto with arith.
Intuition.
Intuition.
Apply MaxEq with b := b r := r; Auto.
Apply MinMax; Auto with arith.
Contradict H'5; Auto.
Rewrite H'5 in H'2.
Generalize H'2.
Replace (Rminus min (FtoR radix min)) with R0.
AutoRewrite [Rsimpl].
Rewrite Rminus_Rabsolu; Auto.
Intros H'3;
Replace (FtoRradix max)
      with (Rplus (FtoR radix min) (Rminus max (FtoR radix min))).
Rewrite <- H'3; Ring.
Unfold FtoRradix; Ring.
Apply Rle_trans with r; Intuition.
Unfold FtoRradix; Ring.
AutoRewrite [Rsimpl]; Auto.
Apply FNoddSuc; Auto.
Intuition.
Exists max; Split; Auto.
Apply ClosestMax with min := min; Auto.
Replace (Rmult (2) r) with (Rplus r r); [Idtac | Simpl; Ring].
Apply Rminus_le; Auto.
Replace (Rminus (Rplus min max) (Rplus r r))
     with (Rminus (Rminus max r) (Rminus r min)); [Idtac | Simpl; Ring].
Apply Rle_minus; Auto.
Rewrite (Rabsolu_minus_sym min) in H'1; Auto.
Rewrite Rminus_Rabsolu in H'1; Auto; Rewrite Rminus_Rabsolu in H'1; Auto.
Apply Rlt_le; Auto.
Right; Intros q H'2.
Apply ClosestMaxEq with r := r min := min; Auto.
Replace (Rmult (2) r) with (Rplus r r); [Idtac | Simpl; Ring].
Apply Rminus_lt; Auto.
Replace (Rminus (Rplus min max) (Rplus r r))
     with (Rminus (Rminus max r) (Rminus r min)); [Idtac | Simpl; Ring].
Apply Rlt_minus; Auto.
Rewrite (Rabsolu_minus_sym min) in H'1; Auto.
Rewrite Rminus_Rabsolu in H'1; Auto; Rewrite Rminus_Rabsolu in H'1; Auto.
Qed.

Theorem EvenClosestCompatible: (CompatibleP b radix EvenClosest).
Red.
Intros r1 r2 p q H' H'0 H'1 H'2; Red.
Inversion H'.
Split.
Apply (ClosestCompatible r1 r2 p q); Auto.
Case H0; Intros H1.
Left.
Apply FNevenEq with f1 := p; Auto.
Intuition.
Right; Intros q0 H'3.
Unfold FtoRradix; Rewrite <- H'1; Auto.
Apply H1; Auto.
Apply (ClosestCompatible r2 r1 q0 q0); Auto.
Intuition.
Qed.

Theorem EvenClosestMinOrMax: (MinOrMaxP b radix EvenClosest).
Red; Intros r p H'; Case (ClosestMinOrMax r p); Auto.
Intuition.
Qed.

Theorem EvenClosestMonotone: (MonotoneP radix EvenClosest).
Red; Intros p q p' q' H' H'0 H'1.
Apply (ClosestMonotone p q); Auto; Intuition.
Qed.

Theorem EvenClosestRoundedModeP: (RoundedModeP b radix EvenClosest).
Red; Split.
Exact EvenClosestTotal.
Split.
Exact EvenClosestCompatible.
Split.
Exact EvenClosestMinOrMax.
Exact EvenClosestMonotone.
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 EvenClosestUniqueP: (UniqueP radix EvenClosest).
Red.
Intros r p q H' H'0.
Inversion H'; Inversion H'0; Case H0; Case H2; Auto.
Intros H'1 H'2; Case (EvenClosestMinOrMax r p); Case (EvenClosestMinOrMax r q);
Auto.
Intros H'3 H'4; Apply (MinUniqueP b radix r); Auto.
Intros H'3 H'4; Case (Req_EM p q); Auto; Intros H'5.
Contradict H'1; Auto.
Apply FnOddNEven; Auto.
Apply FNoddEq with f1 := (FNSucc b radix precision p); Auto.
Apply FcanonicBound with radix := radix precision := precision; Auto.
Apply FNSuccCanonic; Auto with arith.
Intuition.
Intuition.
Apply (MaxUniqueP b radix r); Auto.
Apply MinMax; Auto with arith.
Contradict H'5; Auto.
Apply (RoundedProjector
         b radix ?
         (MaxRoundedModeP
            ? ? ? radixMoreThanOne precisionGreaterThanOne pGivesBound)); Auto.
Intuition.
Rewrite <- H'5; Auto.
Apply FNevenSuc; Auto.
Intuition.
Intros H'3 H'4; Case (Req_EM p q); Auto; Intros H'5.
Contradict H'2; Auto.
Apply FnOddNEven; Auto.
Apply FNoddEq with f1 := (FNSucc b radix precision q); Auto.
Apply FcanonicBound with radix := radix precision := precision; Auto.
Apply FNSuccCanonic; Auto with arith.
Intuition.
Intuition.
Apply (MaxUniqueP b radix r); Auto.
Apply MinMax; Auto with arith.
Contradict H'5; Auto.
Apply sym_eqT;
Apply (RoundedProjector
          b radix ?
          (MaxRoundedModeP
             ? ? ? radixMoreThanOne precisionGreaterThanOne pGivesBound)); Auto.
Intuition.
Rewrite <- H'5; Auto.
Apply FNevenSuc; Auto.
Intuition.
Intros H'3 H'4; Apply (MaxUniqueP b radix r); Auto.
Intros H'1 H'2; Apply sym_eqT; Auto.
Qed.

Theorem ClosestSymmetric: (SymmetricP Closest).
Red; Intros r p H'; Case H'; Clear H'.
Intros H' H'0; Split.
Apply oppBounded; Auto.
Intros f H'1.
Replace (Rabsolu (Rminus (Fopp p) (Ropp r))) with (Rabsolu (Rminus p r)).
Replace (Rabsolu (Rminus f (Ropp r))) with (Rabsolu (Rminus (Fopp f) r)).
Apply H'0; Auto.
Apply oppBounded; Auto.
Unfold FtoRradix; Rewrite Fopp_correct.
Pattern 1 r; Replace r with (Ropp (Ropp r)); [Idtac | Ring].
Replace (Rminus (Ropp (FtoR radix f)) (Ropp (Ropp r)))
     with (Ropp (Rminus (FtoR radix f) (Ropp r))); [Idtac | Ring].
Apply Rabsolu_Ropp; Auto.
Unfold FtoRradix; Rewrite Fopp_correct.
Replace (Rminus (Ropp (FtoR radix p)) (Ropp r))
     with (Ropp (Rminus (FtoR radix p) r)); [Idtac | Ring].
Apply sym_eqT; Apply Rabsolu_Ropp.
Qed.

Theorem EvenClosestSymmetric: (SymmetricP EvenClosest).
Red; Intros r p H'; Case H'; Clear H'.
Intros H' H'0; Case H'0; Clear H'0; Intros H'0.
Split; Auto.
Apply (ClosestSymmetric r p); Auto.
Left.
Apply FNevenFop; Auto.
Split; Auto.
Apply (ClosestSymmetric r p); Auto.
Right.
Intros q H'1.
Cut <R> (Fopp q)==p.
Intros H'2; Unfold FtoRradix; Rewrite Fopp_correct.
Unfold FtoRradix in H'2; Rewrite <- H'2.
Rewrite Fopp_correct; Ring.
Apply H'0; Auto.
Replace r with (Ropp (Ropp r)); [Idtac | Ring].
Apply (ClosestSymmetric (Ropp r) q); Auto.
Qed.
End Fclosest.
Hints Resolve
ClosestTotal ClosestCompatible ClosestMin ClosestMax ClosestMinOrMax
ClosestMonotone ClosestRoundedModeP EvenClosestTotal EvenClosestCompatible
EvenClosestMinOrMax EvenClosestMonotone EvenClosestRoundedModeP FnOddNEven
EvenClosestUniqueP ClosestSymmetric EvenClosestSymmetric :float.

14/12/100, 15:59