(****************************************************************************
                                                                             
          IEEE754  :  Closest                                                   
                                                                             
          Laurent Thery                                                      
                                                                             
  *****************************************************************************
  Properties about the closest rounding mode *)
Require Export Fround.
Section Fclosest.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.
 
Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.

Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
 
Definition Closest (r : R) (p : float) :=
  Fbounded b p /\
  (forall f : float, Fbounded b f -> (Rabs (p - r) <= Rabs (f - r))%R).
 
Theorem ClosestTotal : TotalP Closest.
(* Goal: TotalP EvenClosest *)
red in |- *; intros r.
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case MinEx with (r := r) (3 := pGivesBound); auto with arith.
(* Goal: forall (x : float) (_ : isMin b radix r x), @ex float (fun p : float => EvenClosest r p) *)
intros min H'.
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case MaxEx with (r := r) (3 := pGivesBound); auto with arith.
(* Goal: forall (x : float) (_ : isMax b radix r x), @ex float (fun p : float => EvenClosest r p) *)
intros max H'0.
(* Goal: @ex float (fun p : float => Closest r p) *)
cut (min <= r)%R; [ intros Rl1 | apply isMin_inv1 with (1 := H') ].
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
cut (r <= max)%R; [ intros Rl2 | apply isMax_inv1 with (1 := H'0) ].
(* Goal: @ex float (fun p : float => Closest r p) *)
case (Rle_or_lt (Rabs (min - r)) (Rabs (max - r))); intros H'1.
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
exists min; split.
(* Goal: Closest r p *)
case H'; auto.
(* Goal: forall (f : float) (_ : Fbounded b f), Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
intros f H'2.
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
case (Rle_or_lt f r); intros H'3.
(* Goal: Rle (Rabs (Rminus (FtoRradix min) r)) (Rabs (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix min) r)) (Rabs (Rminus (FtoRradix f) r)) *)
repeat rewrite Faux.Rabsolu_left1.
(* Goal: Rle (Ropp (Rminus (FtoRradix min) r)) (Ropp (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
apply Ropp_le_contravar; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (Rabs (Rminus (FtoR radix p) r)) (Rabs (Rminus (FtoR radix f) r)) *)
(* Goal: Rle (Rminus r (FtoR radix f)) (IZR Z0) *)
(* Goal: Rle (Rminus r (FtoR radix p)) (IZR Z0) *)
elim H'; auto.
(* Goal: forall (_ : Fbounded b max) (_ : and (Rle r (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f))), Rle (FtoRradix max) (FtoRradix f) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (Rabs (Rminus (FtoRradix min) r)) (Rabs (Rminus (FtoRradix f) r)) *)
(* Goal: @ex float (fun p : float => Closest r p) *)
apply Rle_trans with (1 := H'1).
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
repeat rewrite Rabs_right.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix max) (FtoRradix f) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
elim H'0; auto.
(* Goal: forall (_ : Fbounded b max) (_ : and (Rle r (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f))), Rle (FtoRradix max) (FtoRradix f) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: Rle r (FtoR radix p) *)
apply Rlt_le; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (Rplus r (IZR Z0)) (FtoRradix f) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: @ex float (fun p : float => Closest r p) *)
rewrite Rplus_0_r.
(* Goal: Rle r (FtoR radix p) *)
apply Rlt_le; auto.
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: @ex float (fun p : float => Closest r p) *)
exists max; split.
(* Goal: Fbounded b max *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision min)) (FtoR radix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case H'0; auto.
(* Goal: forall (f : float) (_ : Fbounded b f), Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
intros f H'2.
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
case (Rle_or_lt f r); intros H'3.
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
apply Rle_trans with (1 := Rlt_le _ _ H'1).
(* Goal: Rle (Rabs (Rminus (FtoRradix min) r)) (Rabs (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix min) r)) (Rabs (Rminus (FtoRradix f) r)) *)
repeat rewrite Faux.Rabsolu_left1.
(* Goal: Rle (Ropp (Rminus (FtoRradix min) r)) (Ropp (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
apply Ropp_le_contravar; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (Rabs (Rminus (FtoR radix p) r)) (Rabs (Rminus (FtoR radix f) r)) *)
(* Goal: Rle (Rminus r (FtoR radix f)) (IZR Z0) *)
(* Goal: Rle (Rminus r (FtoR radix p)) (IZR Z0) *)
elim H'; auto.
(* Goal: forall (_ : Fbounded b max) (_ : and (Rle r (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f))), Rle (FtoRradix max) (FtoRradix f) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
repeat rewrite Rabs_right; auto with real.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix max) (FtoRradix f) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
elim H'0; auto.
(* Goal: forall (_ : Fbounded b max) (_ : and (Rle r (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f))), Rle (FtoRradix max) (FtoRradix f) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: Rle r (FtoR radix p) *)
apply Rlt_le; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle r (FtoR radix p) *)
apply Rlt_le; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
Qed.
 
Theorem ClosestCompatible : CompatibleP b radix Closest.
(* Goal: UniqueP radix EvenClosest *)
red in |- *; simpl in |- *.
(* Goal: forall (r1 r2 : R) (p q : float) (_ : Closest r1 p) (_ : @eq R r1 r2) (_ : @eq R (FtoR radix p) (FtoR radix q)) (_ : Fbounded b q), Closest r2 q *)
intros r1 r2 p q H'; case H'.
(* Goal: forall (_ : Fbounded b p) (_ : forall (f : float) (_ : Fbounded b f), Rle (Rabs (Rminus (FtoRradix p) r1)) (Rabs (Rminus (FtoRradix f) r1))) (_ : @eq R r1 r2) (_ : @eq R (FtoR radix p) (FtoR radix q)) (_ : Fbounded b q), Closest r2 q *)
intros H'0 H'1 H'2 H'3 H'4.
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
split; auto.
(* Goal: forall (f : float) (_ : Fbounded b f), Rle (Rabs (Rminus (FtoRradix q) r2)) (Rabs (Rminus (FtoRradix f) r2)) *)
intros f H'5.
(* Goal: Rle (Rabs (Rminus (FtoRradix q) r2)) (Rabs (Rminus (FtoRradix f) r2)) *)
unfold FtoRradix in |- *; rewrite <- H'3; rewrite <- H'2; auto.
Qed.
 
Theorem ClosestMin :
 forall (r : R) (min max : float),
 isMin b radix r min ->
 isMax b radix r max -> (2%nat * r <= min + max)%R -> Closest r min.
(* Goal: forall (r : R) (min max : float) (_ : isMin b radix r min) (_ : isMax b radix r max) (_ : Rle (Rplus (FtoRradix min) (FtoRradix max)) (Rmult (INR (S (S O))) r)), Closest r max *)
intros r min max H' H'0 H'1; split.
(* Goal: Closest r p *)
case H'; auto.
(* Goal: forall (f : float) (_ : Fbounded b f), Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
intros f H'2.
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
case (Rle_or_lt f r); intros H'3.
(* Goal: Rle (Rabs (Rminus (FtoRradix min) r)) (Rabs (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix min) r)) (Rabs (Rminus (FtoRradix f) r)) *)
repeat rewrite Faux.Rabsolu_left1.
(* Goal: Rle (Ropp (Rminus r (FtoR radix f))) (Ropp (Rminus r (FtoR radix p))) *)
(* Goal: or (isMin b radix r p) (isMax b radix r p) *)
apply Ropp_le_contravar.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Closest r p *)
case H'; auto.
(* Goal: forall (_ : Fbounded b max) (_ : and (Rle r (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f))), Rle (FtoRradix max) (FtoRradix f) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (FtoRradix min) r *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply isMin_inv1 with (1 := H'); auto.
(* Goal: Rgt (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite (Faux.Rabsolu_left1 (min - r)).
(* Goal: Rle (Ropp (Rminus (FtoRradix min) r)) (Rabs (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
rewrite (Rabs_right (f - r)).
(* Goal: Rle (Ropp (Rminus (FtoRradix min) r)) (Rminus (FtoRradix f) r) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
apply Rle_trans with (max - r)%R.
cut (forall x y : R, (- y + x)%R = (- (y - x))%R);
 [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ].
cut (forall x y : R, (- (x - y))%R = (y - x)%R);
 [ intros Eq0; repeat rewrite Eq0; clear Eq0
 | intros; unfold Rminus in |- *; ring ].
(* Goal: Rle (Rminus r (FtoRradix min)) (Rminus (FtoRradix max) r) *)
(* Goal: Rle (Rminus (FtoRradix max) r) (Rminus (FtoRradix f) r) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
apply Rplus_le_reg_l with (r := FtoR radix min).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r r) (Rplus r (Rplus (FtoR radix min) (Rminus (FtoRradix max) r))) *)
(* Goal: Rle (Rminus (FtoRradix max) r) (Rminus (FtoRradix f) r) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
replace (r + (FtoR radix min + (max - r)))%R with (min + max)%R.
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (Rplus r r) *)
(* Goal: @eq R (Rplus (FtoRradix min) (FtoRradix max)) (Rplus r (Rplus (FtoRradix min) (Rminus (FtoRradix max) r))) *)
(* Goal: Rle (Rminus r (FtoRradix min)) (Ropp (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
replace (r + r)%R with (2%nat * r)%R; auto.
(* Goal: @eq R (Ropp (Rminus (FtoRradix min) r)) (Rminus r (FtoRradix min)) *)
(* Goal: Rle (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
simpl in |- *; ring.
(* Goal: @eq R (Rplus (FtoRradix min) (FtoRradix max)) (Rplus r (Rplus (FtoR radix min) (Rminus (FtoRradix max) r))) *)
(* Goal: Rle (Rminus (FtoRradix max) r) (Rminus (FtoRradix f) r) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
simpl in |- *; fold FtoRradix; ring.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Fbounded b max *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision min)) (FtoR radix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case H'0; auto.
(* Goal: forall (_ : Fbounded b max) (_ : and (Rle r (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f))), Rle (FtoRradix max) (FtoRradix f) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: Rle r (FtoR radix p) *)
apply Rlt_le; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle r (FtoR radix p) *)
apply Rlt_le; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (FtoRradix min) r *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply isMin_inv1 with (1 := H'); auto.
Qed.
 
Theorem ClosestMax :
 forall (r : R) (min max : float),
 isMin b radix r min ->
 isMax b radix r max -> (min + max <= 2%nat * r)%R -> Closest r max.
(* Goal: forall (r : R) (min max : float) (_ : isMin b radix r min) (_ : isMax b radix r max) (_ : Rle (Rplus (FtoRradix min) (FtoRradix max)) (Rmult (INR (S (S O))) r)), Closest r max *)
intros r min max H' H'0 H'1; split.
(* Goal: Fbounded b max *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision min)) (FtoR radix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case H'0; auto.
(* Goal: forall (f : float) (_ : Fbounded b f), Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
intros f H'2.
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
case (Rle_or_lt f r); intros H'3.
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
rewrite (Rabs_right (max - r)).
(* Goal: Rle (Rminus (FtoRradix max) r) (Rabs (Rminus (FtoRradix f) r)) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
rewrite (Faux.Rabsolu_left1 (f - r)).
(* Goal: Rle (Rminus (FtoRradix max) r) (Ropp (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
apply Rle_trans with (r - min)%R.
(* Goal: Rle (Rminus (FtoRradix max) r) (Rminus r (FtoRradix min)) *)
(* Goal: Rle (Rminus r (FtoRradix min)) (Ropp (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
apply Rplus_le_reg_l with (r := FtoRradix min).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rplus (FtoRradix min) (Rminus (FtoRradix max) r))) (Rplus r r) *)
(* Goal: Rle (Rminus r (FtoRradix min)) (Ropp (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
replace (r + (min + (max - r)))%R with (min + max)%R.
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (Rplus r r) *)
(* Goal: @eq R (Rplus (FtoRradix min) (FtoRradix max)) (Rplus r (Rplus (FtoRradix min) (Rminus (FtoRradix max) r))) *)
(* Goal: Rle (Rminus r (FtoRradix min)) (Ropp (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
replace (r + r)%R with (2%nat * r)%R; auto.
(* Goal: @eq R (Ropp (Rminus (FtoRradix min) r)) (Rminus r (FtoRradix min)) *)
(* Goal: Rle (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
simpl in |- *; ring.
(* Goal: @eq R (Ropp (Rminus (FtoRradix min) r)) (Rminus r (FtoRradix min)) *)
(* Goal: Rle (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
simpl in |- *; ring.
(* Goal: Rle (Rminus r (FtoRradix min)) (Ropp (Rminus (FtoRradix f) r)) *)
(* Goal: Rle (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
replace (r - min)%R with (- (min - r))%R.
(* Goal: Rle (Ropp (Rminus r (FtoR radix f))) (Ropp (Rminus r (FtoR radix p))) *)
(* Goal: or (isMin b radix r p) (isMax b radix r p) *)
apply Ropp_le_contravar.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Closest r p *)
case H'; auto.
(* Goal: forall (_ : Fbounded b max) (_ : and (Rle r (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f))), Rle (FtoRradix max) (FtoRradix f) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: @eq R (Ropp (Rminus (FtoRradix min) r)) (Rminus r (FtoRradix min)) *)
(* Goal: Rle (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
simpl in |- *; ring.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle r (FtoRradix max) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply isMax_inv1 with (1 := H'0); auto.
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r)) *)
repeat rewrite Rabs_right.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Fbounded b max *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision min)) (FtoR radix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case H'0; auto.
(* Goal: forall (_ : Fbounded b max) (_ : and (Rle r (FtoR radix max)) (forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoR radix f)), Rle (FtoR radix max) (FtoR radix f))), Rle (FtoRradix max) (FtoRradix f) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto.
(* Goal: Rle r (FtoR radix p) *)
apply Rlt_le; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle r (FtoR radix p) *)
apply Rlt_le; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle r (FtoRradix max) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply isMax_inv1 with (1 := H'0); auto.
Qed.
 
Theorem ClosestMinOrMax : MinOrMaxP b radix Closest.
(* Goal: MinOrMaxP b radix Closest *)
red in |- *.
(* Goal: forall (r : R) (p : float) (_ : Closest r p), or (isMin b radix r p) (isMax b radix r p) *)
intros r p H'.
(* Goal: or (isMin b radix r p) (isMax b radix r p) *)
case (Rle_or_lt p r); intros H'1.
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
left; split; auto.
(* Goal: Closest r p *)
case H'; auto.
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
split; auto.
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoR radix f)), Rle (FtoR radix p) (FtoR radix f) *)
intros f H'0 H'2.
(* Goal: Rle (FtoR radix p) (FtoR radix f) *)
apply Rplus_le_reg_l with (r := (- r)%R).
cut (forall x y : R, (- y + x)%R = (- (y - x))%R);
 [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ].
(* Goal: Rle (Ropp (Rminus r (FtoR radix f))) (Ropp (Rminus r (FtoR radix p))) *)
(* Goal: or (isMin b radix r p) (isMax b radix r p) *)
apply Ropp_le_contravar.
(* Goal: Rle (Rminus r (FtoR radix p)) (Rminus r (FtoR radix f)) *)
(* Goal: or (isMin b radix r p) (isMax b radix r p) *)
rewrite <- (Rabs_right (r - FtoR radix p)).
(* Goal: Rle (Rabs (Rminus r (FtoR radix p))) (Rminus r (FtoR radix f)) *)
(* Goal: Rge (Rminus r (FtoR radix p)) (IZR Z0) *)
(* Goal: or (isMin b radix r p) (isMax b radix r p) *)
rewrite <- (Rabs_right (r - FtoR radix f)).
cut (forall x y : R, Rabs (x - y) = Rabs (y - x));
 [ intros Eq0; repeat rewrite (Eq0 r); clear Eq0
 | intros x y; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr ];
 auto.
(* Goal: Rle (Rabs (Rminus (FtoR radix p) r)) (Rabs (Rminus (FtoR radix f) r)) *)
(* Goal: Rle (Rminus r (FtoR radix f)) (IZR Z0) *)
(* Goal: Rle (Rminus r (FtoR radix p)) (IZR Z0) *)
elim H'; auto.
(* Goal: Rge (Rminus r (FtoR radix f)) (IZR Z0) *)
(* Goal: Rge (Rminus r (FtoR radix p)) (IZR Z0) *)
(* Goal: or (isMin b radix r p) (isMax b radix r p) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix f).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rge (Rminus r (FtoR radix p)) (IZR Z0) *)
(* Goal: or (isMin b radix r p) (isMax b radix r p) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix p).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
right; split; auto.
(* Goal: Closest r p *)
case H'; auto.
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
split; auto.
(* Goal: Rle r (FtoR radix p) *)
apply Rlt_le; auto.
(* Goal: forall (f : float) (_ : Fbounded b f) (_ : Rle r (FtoR radix f)), Rle (FtoR radix p) (FtoR radix f) *)
intros f H'0 H'2.
(* Goal: Rle (FtoR radix p) (FtoR radix f) *)
apply Rplus_le_reg_l with (r := (- r)%R).
cut (forall x y : R, (- y + x)%R = (- (y - x))%R);
 [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ].
(* Goal: Rle (Ropp (Rminus r (FtoR radix p))) (Ropp (Rminus r (FtoR radix f))) *)
rewrite <- (Faux.Rabsolu_left1 (r - FtoR radix p)).
(* Goal: Rle (Rabs (Rminus r (FtoR radix p))) (Ropp (Rminus r (FtoR radix f))) *)
(* Goal: Rle (Rminus r (FtoR radix p)) (IZR Z0) *)
rewrite <- (Faux.Rabsolu_left1 (r - FtoR radix f)).
cut (forall x y : R, Rabs (x - y) = Rabs (y - x));
 [ intros Eq0; repeat rewrite (Eq0 r); clear Eq0
 | intros x y; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr ];
 auto.
(* Goal: Rle (Rabs (Rminus (FtoR radix p) r)) (Rabs (Rminus (FtoR radix f) r)) *)
(* Goal: Rle (Rminus r (FtoR radix f)) (IZR Z0) *)
(* Goal: Rle (Rminus r (FtoR radix p)) (IZR Z0) *)
elim H'; auto.
(* Goal: Rle (Rminus r (FtoR radix f)) (IZR Z0) *)
(* Goal: Rle (Rminus r (FtoR radix p)) (IZR Z0) *)
apply Rplus_le_reg_l with (r := FtoR radix f).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (Rminus r (FtoR radix p)) (IZR Z0) *)
apply Rplus_le_reg_l with (r := FtoR radix p).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle r (FtoR radix p) *)
apply Rlt_le; auto.
Qed.
 
Theorem ClosestMinEq :
 forall (r : R) (min max p : float),
 isMin b radix r min ->
 isMax b radix r max ->
 (2%nat * r < min + max)%R -> Closest r p -> p = min :>R.
(* Goal: forall (r : R) (min max p : float) (_ : isMin b radix r min) (_ : isMax b radix r max) (_ : Rlt (Rmult (INR (S (S O))) r) (Rplus (FtoRradix min) (FtoRradix max))) (_ : Closest r p), @eq R (FtoRradix p) (FtoRradix min) *)
intros r min max p H' H'0 H'1 H'2.
(* Goal: @eq R (FtoRradix p) (FtoRradix min) *)
case (ClosestMinOrMax r p); auto; intros H'3.
(* Goal: @eq R (FtoRradix p) (FtoRradix min) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix min) *)
unfold FtoRradix in |- *; apply MinEq with (1 := H'3); auto.
(* Goal: @eq R (FtoRradix p) (FtoRradix min) *)
absurd (Rabs (max - r) <= Rabs (min - r))%R.
(* Goal: not (Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r))) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rgt_not_le.
(* Goal: Rgt (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite (Faux.Rabsolu_left1 (min - r)).
(* Goal: Rgt (Rabs (Rminus (FtoRradix max) r)) (Ropp (Rminus (FtoRradix min) r)) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rabs_right.
(* Goal: Rgt (Rminus (FtoRradix max) r) (Ropp (Rminus (FtoRradix min) r)) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
replace (- (min - r))%R with (r - min)%R; [ idtac | ring ].
(* Goal: Rgt (Rminus (FtoRradix max) r) (Rminus r (FtoRradix min)) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
red in |- *; apply Rplus_lt_reg_l with (r := FtoRradix min).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rlt r (Rplus (FtoRradix min) (Rminus (FtoRradix max) r)) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_lt_reg_l with (r := r).
(* Goal: Rlt (Rplus r r) (Rplus r (Rplus (FtoRradix min) (Rminus (FtoRradix max) r))) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
replace (r + r)%R with (2%nat * r)%R; [ idtac | simpl in |- *; ring ].
(* Goal: Rlt (Rmult (INR (S (S O))) r) (Rplus r (Rplus (FtoRradix min) (Rminus (FtoRradix max) r))) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
replace (r + (min + (max - r)))%R with (min + max)%R; [ idtac | ring ]; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle r (FtoRradix max) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply isMax_inv1 with (1 := H'0); auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (FtoRradix min) r *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply isMin_inv1 with (1 := H'); auto.
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
cut (Closest r max).
(* Goal: forall _ : Closest r max, Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
(* Goal: Closest r max *)
intros H'4; case H'4.
(* Goal: forall (_ : Fbounded b max) (_ : forall (f : float) (_ : Fbounded b f), Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r))), Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
(* Goal: Closest r max *)
intros H'5 H'6; apply H'6; auto.
(* Goal: Closest r p *)
case H'; auto.
(* Goal: Closest r max *)
apply ClosestCompatible with (1 := H'2); auto.
(* Goal: @eq R (FtoR radix p) (FtoR radix max) *)
(* Goal: Fbounded b max *)
apply MaxEq with (1 := H'3); auto.
(* Goal: Fbounded b max *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision min)) (FtoR radix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case H'0; auto.
Qed.
 
Theorem ClosestMaxEq :
 forall (r : R) (min max p : float),
 isMin b radix r min ->
 isMax b radix r max ->
 (min + max < 2%nat * r)%R -> Closest r p -> p = max :>R.
(* Goal: forall (r : R) (min max p : float) (_ : isMin b radix r min) (_ : isMax b radix r max) (_ : Rlt (Rmult (INR (S (S O))) r) (Rplus (FtoRradix min) (FtoRradix max))) (_ : Closest r p), @eq R (FtoRradix p) (FtoRradix min) *)
intros r min max p H' H'0 H'1 H'2.
(* Goal: @eq R (FtoRradix p) (FtoRradix min) *)
case (ClosestMinOrMax r p); auto; intros H'3.
(* Goal: @eq R (FtoR radix p) (FtoR radix max) *)
(* Goal: Fbounded b max *)
2: unfold FtoRradix in |- *; apply MaxEq with (1 := H'3); auto.
absurd (Rabs (min - r) <= Rabs (max - r))%R.
(* Goal: not (Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r))) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rgt_not_le.
(* Goal: Rgt (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite (Faux.Rabsolu_left1 (min - r)).
(* Goal: Rgt (Rabs (Rminus (FtoRradix max) r)) (Ropp (Rminus (FtoRradix min) r)) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rabs_right.
(* Goal: Rgt (Rminus (FtoRradix max) r) (Ropp (Rminus (FtoRradix min) r)) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
replace (- (min - r))%R with (r - min)%R; [ idtac | ring ].
(* Goal: Rgt (Rminus (FtoRradix max) r) (Rminus r (FtoRradix min)) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
red in |- *; apply Rplus_lt_reg_l with (r := FtoRradix min).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rlt r (Rplus (FtoRradix min) (Rminus (FtoRradix max) r)) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_lt_reg_l with (r := r).
(* Goal: Rlt (Rplus r r) (Rplus r (Rplus (FtoRradix min) (Rminus (FtoRradix max) r))) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
replace (r + r)%R with (2%nat * r)%R; [ idtac | simpl in |- *; ring ].
(* Goal: Rlt (Rmult (INR (S (S O))) r) (Rplus r (Rplus (FtoRradix min) (Rminus (FtoRradix max) r))) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
replace (r + (min + (max - r)))%R with (min + max)%R; [ idtac | ring ]; auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rle_ge; apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle r (FtoRradix max) *)
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply isMax_inv1 with (1 := H'0); auto.
(* Goal: Rle (Rminus (FtoRradix min) r) (IZR Z0) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rplus_le_reg_l with (r := r).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (FtoRradix min) r *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply isMin_inv1 with (1 := H'); auto.
cut (Closest r min).
(* Goal: forall _ : Closest r max, Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
(* Goal: Closest r max *)
intros H'4; case H'4.
(* Goal: forall (_ : Fbounded b max) (_ : forall (f : float) (_ : Fbounded b f), Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix f) r))), Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
(* Goal: Closest r max *)
intros H'5 H'6; apply H'6; auto.
(* Goal: Fbounded b max *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision min)) (FtoR radix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case H'0; auto.
(* Goal: Closest r max *)
apply ClosestCompatible with (1 := H'2); auto.
apply MinEq with (1 := H'3); auto.
(* Goal: Closest r p *)
case H'; auto.
Qed.
 
Theorem ClosestMonotone : MonotoneP radix Closest.
(* Goal: UniqueP radix EvenClosest *)
red in |- *; simpl in |- *.
intros p q p' q' H' H'0 H'1.
change (p' <= q')%R in |- *.
case (Rle_or_lt p p'); intros Rl0.
case (Rle_or_lt p q'); intros Rl1.
apply Rplus_le_reg_l with (r := (- p)%R).
cut (forall x y : R, (- y + x)%R = (- (y - x))%R);
 [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ].
rewrite <- (Faux.Rabsolu_left1 (p - p')).
rewrite <- (Faux.Rabsolu_left1 (p - q')).
cut (forall x y : R, Rabs (x - y) = Rabs (y - x));
 [ intros Eq0; repeat rewrite (Eq0 p); clear Eq0
 | intros x y; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr ];
 auto.
(* Goal: Rle (FtoRradix max) (FtoRradix f) *)
(* Goal: Rge (Rminus (FtoRradix f) r) (IZR Z0) *)
(* Goal: Rge (Rminus (FtoRradix max) r) (IZR Z0) *)
elim H'0; auto.
intros H'2 H'3; apply H'3; auto.
case H'1; auto.
apply Rplus_le_reg_l with (r := FtoR radix q').
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
apply Rplus_le_reg_l with (r := FtoR radix p').
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
case (Rle_or_lt p' q); intros Rl2.
apply Rplus_le_reg_l with (r := (- q)%R).
cut (forall x y : R, (- y + x)%R = (- (y - x))%R);
 [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ].
rewrite <- (Rabs_right (q - p')).
2: apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix p').
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
2: repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
2: rewrite Rplus_0_r; auto.
rewrite <- (Rabs_right (q - q')).
2: apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix q').
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
2: repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
2: rewrite Rplus_0_r; auto.
(* Goal: Rle r (FtoR radix p) *)
2: apply Rle_trans with (1 := Rlt_le _ _ Rl1); apply Rlt_le; auto.
cut (forall x y : R, Rabs (x - y) = Rabs (y - x));
 [ intros Eq0; repeat rewrite (Eq0 q); clear Eq0
 | intros x y; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr ];
 auto.
(* Goal: Rle (Ropp (Rminus r (FtoR radix f))) (Ropp (Rminus r (FtoR radix p))) *)
(* Goal: or (isMin b radix r p) (isMax b radix r p) *)
apply Ropp_le_contravar.
elim H'1; auto.
intros H'2 H'3; apply H'3; auto.
(* Goal: Fbounded b max *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision min)) (FtoR radix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case H'0; auto.
case (Rle_or_lt (p - q') (p' - q)); intros Rl3.
absurd (Rabs (p' - p) <= Rabs (q' - p))%R.
(* Goal: not (Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r))) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rgt_not_le.
rewrite (Faux.Rabsolu_left1 (q' - p)).
2: apply Rplus_le_reg_l with (r := p).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
2: repeat rewrite Rplus_minus; auto.
(* Goal: Rle r (FtoR radix p) *)
2: rewrite Rplus_0_r; apply Rlt_le; auto.
rewrite (Rabs_right (p' - p)).
2: apply Rle_ge; apply Rplus_le_reg_l with (r := p).
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
2: rewrite Rplus_0_r; auto.
cut (forall x y : R, (- (y - x))%R = (x - y)%R);
 [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ].
red in |- *; apply Rle_lt_trans with (1 := Rl3).
replace (p' - p)%R with (p' - q + (q - p))%R.
pattern (p' - q)%R at 1 in |- *; replace (p' - q)%R with (p' - q + 0)%R.
apply Rplus_lt_compat_l; auto.
apply Rplus_lt_reg_l with (r := p).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
ring.
replace (p + (p' - p))%R with (FtoRradix p'); auto; ring.
case H'0; intros H'2 H'3; apply H'3; auto.
case H'1; auto.
absurd (Rabs (q' - q) <= Rabs (p' - q))%R.
(* Goal: not (Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r))) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
apply Rgt_not_le.
rewrite (Faux.Rabsolu_left1 (q' - q)).
2: apply Rplus_le_reg_l with (r := q).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
2: repeat rewrite Rplus_minus; auto.
(* Goal: Rle r (FtoR radix p) *)
2: rewrite Rplus_0_r; apply Rlt_le; auto.
2: apply Rlt_trans with (1 := Rl1); auto.
rewrite (Rabs_right (p' - q)).
2: apply Rle_ge; apply Rplus_le_reg_l with (r := q).
(* Goal: Rle r (FtoR radix p) *)
2: rewrite Rplus_0_r; apply Rlt_le; auto.
cut (forall x y : R, (- (y - x))%R = (x - y)%R);
 [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ].
red in |- *; apply Rlt_trans with (1 := Rl3).
replace (q - q')%R with (p - q' + (q - p))%R.
pattern (p - q')%R at 1 in |- *; replace (p - q')%R with (p - q' + 0)%R.
apply Rplus_lt_compat_l; auto.
apply Rplus_lt_reg_l with (r := p).
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
ring.
replace (q + (p' - q))%R with (FtoRradix p'); auto; ring.
case H'1; intros H'2 H'3; apply H'3; auto.
(* Goal: Fbounded b max *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision min)) (FtoR radix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case H'0; auto.
case (Rle_or_lt p q'); intros Rl1.
apply Rle_trans with p; auto.
(* Goal: Rle r (FtoR radix p) *)
apply Rlt_le; auto.
apply Rplus_le_reg_l with (r := (- q)%R).
cut (forall x y : R, (- y + x)%R = (- (y - x))%R);
 [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ].
rewrite <- (Rabs_right (q - p')).
rewrite <- (Rabs_right (q - q')).
(* Goal: Rle (Ropp (Rminus r (FtoR radix f))) (Ropp (Rminus r (FtoR radix p))) *)
(* Goal: or (isMin b radix r p) (isMax b radix r p) *)
apply Ropp_le_contravar.
cut (forall x y : R, Rabs (x - y) = Rabs (y - x));
 [ intros Eq0; repeat rewrite (Eq0 q); clear Eq0
 | intros x y; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr ];
 auto.
elim H'1; auto.
intros H'2 H'3; apply H'3; auto.
(* Goal: Fbounded b max *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision min)) (FtoR radix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case H'0; auto.
apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix q').
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
apply Rlt_le; apply Rlt_trans with (1 := Rl1); auto.
apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix p').
(* Goal: Rle (Rplus r (Rminus (FtoRradix min) r)) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
repeat rewrite Rplus_minus; auto.
(* Goal: Rle (FtoRradix min) (Rplus r (IZR Z0)) *)
(* Goal: Rle (Rabs (Rminus (FtoRradix max) r)) (Rabs (Rminus (FtoRradix min) r)) *)
rewrite Rplus_0_r; auto.
apply Rlt_le; apply Rlt_trans with (1 := Rl0); auto.
Qed.
 
Theorem ClosestRoundedModeP : RoundedModeP b radix Closest.
(* Goal: RoundedModeP b radix Closest *)
split; try exact ClosestTotal.
(* Goal: and (CompatibleP b radix Closest) (and (MinOrMaxP b radix Closest) (MonotoneP radix Closest)) *)
split; try exact ClosestCompatible.
(* Goal: and (MinOrMaxP b radix Closest) (MonotoneP radix Closest) *)
split; try exact ClosestMinOrMax.
(* Goal: MonotoneP radix Closest *)
try exact ClosestMonotone.
Qed.
 
Definition EvenClosest (r : R) (p : float) :=
  Closest r p /\
  (FNeven b radix precision p \/ (forall q : float, Closest r q -> q = p :>R)).
 
Theorem EvenClosestTotal : TotalP EvenClosest.
(* Goal: TotalP EvenClosest *)
red in |- *; intros r.
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case MinEx with (r := r) (3 := pGivesBound); auto with arith.
(* Goal: forall (x : float) (_ : isMin b radix r x), @ex float (fun p : float => EvenClosest r p) *)
intros min H'.
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case MaxEx with (r := r) (3 := pGivesBound); auto with arith.
(* Goal: forall (x : float) (_ : isMax b radix r x), @ex float (fun p : float => EvenClosest r p) *)
intros max H'0.
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
cut (min <= r)%R; [ intros Rl1 | apply isMin_inv1 with (1 := H'); auto ].
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
cut (r <= max)%R; [ intros Rl2 | apply isMax_inv1 with (1 := H'0) ].
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case (Rle_or_lt (r - min) (max - r)); intros H'1.
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case H'1; intros H'2; auto.
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
exists min; split.
(* Goal: Closest r min *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
apply ClosestMin with (max := max); auto.
(* Goal: Rlt (Rplus (FtoRradix min) (FtoRradix max)) (Rmult (INR (S (S O))) r) *)
replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (Rplus r r) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
apply Rminus_le; auto.
replace (r + r - (min + max))%R with (r - min - (max - r))%R;
 [ idtac | simpl in |- *; ring ].
(* Goal: Rle (Rminus (Rminus (FtoRradix max) r) (Rminus r (FtoRradix min))) (IZR Z0) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
apply Rle_minus; auto.
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
right; intros q H'3.
(* Goal: @eq R (FtoRradix q) (FtoRradix min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
apply ClosestMinEq with (r := r) (max := max); auto.
(* Goal: Rlt (Rplus (FtoRradix min) (FtoRradix max)) (Rmult (INR (S (S O))) r) *)
replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
(* Goal: Rlt (Rplus (FtoRradix min) (FtoRradix max)) (Rplus r r) *)
apply Rminus_lt; auto.
replace (r + r - (min + max))%R with (r - min - (max - r))%R;
 [ idtac | simpl in |- *; ring ].
(* Goal: Rlt (Rminus (Rminus (FtoRradix max) r) (Rminus r (FtoRradix min))) (IZR Z0) *)
apply Rlt_minus; auto.
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case (FNevenOrFNodd b radix precision min); intros Ev0.
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
exists min; split; auto.
(* Goal: Closest r min *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
apply ClosestMin with (max := max); auto.
(* Goal: Rlt (Rplus (FtoRradix min) (FtoRradix max)) (Rmult (INR (S (S O))) r) *)
replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (Rplus r r) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
apply Rminus_le; auto.
replace (r + r - (min + max))%R with (r - min - (max - r))%R;
 [ idtac | simpl in |- *; ring ].
(* Goal: Rle (Rminus (Rminus (FtoRradix max) r) (Rminus r (FtoRradix min))) (IZR Z0) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
apply Rle_minus; auto.
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
exists max; split; auto.
(* Goal: Closest r max *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
apply ClosestMax with (min := min); auto.
(* Goal: Rlt (Rplus (FtoRradix min) (FtoRradix max)) (Rmult (INR (S (S O))) r) *)
replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (Rplus r r) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
apply Rminus_le; auto.
replace (min + max - (r + r))%R with (max - r - (r - min))%R;
 [ idtac | simpl in |- *; ring ].
(* Goal: Rle (Rminus (Rminus (FtoRradix max) r) (Rminus r (FtoRradix min))) (IZR Z0) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
apply Rle_minus; auto.
(* Goal: Rle (Rminus (FtoRradix max) r) (Rminus r (FtoRradix min)) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
rewrite H'2; auto with real.
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case (Req_dec min max); intros H'5.
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
right; intros q H'3.
(* Goal: @eq R (FtoRradix q) (FtoRradix max) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case (ClosestMinOrMax _ _ H'3); intros isM0.
(* Goal: @eq R (FtoRradix q) (FtoRradix max) *)
(* Goal: @eq R (FtoRradix q) (FtoRradix max) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
rewrite <- H'5.
(* Goal: @eq R (FtoRradix q) (FtoRradix min) *)
(* Goal: @eq R (FtoRradix q) (FtoRradix max) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
apply MinEq with (1 := isM0); auto.
(* Goal: @eq R (FtoRradix q) (FtoRradix max) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
apply MaxEq with (1 := isM0); auto.
(* Goal: or (FNeven b radix precision (Fopp p)) (forall (q : float) (_ : Closest (Ropp r) q), @eq R (FtoRradix q) (FtoRradix (Fopp p))) *)
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
left.
(* Goal: FNeven b radix precision max *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
apply FNevenEq with (f1 := FNSucc b radix precision min); auto.
(* Goal: Fbounded b (FNSucc b radix precision min) *)
(* Goal: Fbounded b max *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision min)) (FtoR radix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
apply FcanonicBound with (radix := radix).
(* Goal: Fcanonic radix b (FNSucc b radix precision q) *)
(* Goal: Fbounded b p *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision q)) (FtoR radix p) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply FNSuccCanonic; auto with arith.
(* Goal: Closest r p *)
case H'; auto.
(* Goal: Fbounded b max *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision min)) (FtoR radix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
case H'0; auto.
(* Goal: @eq R (FtoR radix (FNSucc b radix precision min)) (FtoR radix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
apply MaxEq with (b := b) (r := r); auto.
(* Goal: isMax b radix r (FNSucc b radix precision q) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply MinMax; auto with arith.
(* Goal: not (@eq R r (FtoR radix q)) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
Contradict H'5; auto.
(* Goal: @eq R (FtoRradix min) (FtoRradix max) *)
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
fold FtoRradix in H'5; rewrite H'5 in H'2.
replace (FtoRradix max) with (min + (max - min))%R;
 [ rewrite <- H'2 | idtac ]; ring.
(* Goal: FNeven b radix precision (FNSucc b radix precision min) *)
(* Goal: @ex float (fun p : float => EvenClosest r p) *)
apply FNoddSuc; auto.
(* Goal: Closest r p *)
case H'; auto.
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
exists max; split; auto.
(* Goal: Closest r max *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
apply ClosestMax with (min := min); auto.
(* Goal: Rlt (Rplus (FtoRradix min) (FtoRradix max)) (Rmult (INR (S (S O))) r) *)
replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
(* Goal: Rle (Rplus (FtoRradix min) (FtoRradix max)) (Rplus r r) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
apply Rminus_le; auto.
replace (min + max - (r + r))%R with (max - r - (r - min))%R;
 [ idtac | simpl in |- *; ring ].
(* Goal: Rle (Rminus (Rminus (FtoRradix max) r) (Rminus r (FtoRradix min))) (IZR Z0) *)
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
apply Rle_minus; auto with real.
(* Goal: or (FNeven b radix precision max) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix max)) *)
right; intros q H'2.
(* Goal: @eq R (FtoRradix q) (FtoRradix max) *)
apply ClosestMaxEq with (r := r) (min := min); auto.
(* Goal: Rlt (Rplus (FtoRradix min) (FtoRradix max)) (Rmult (INR (S (S O))) r) *)
replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
(* Goal: Rlt (Rplus (FtoRradix min) (FtoRradix max)) (Rplus r r) *)
apply Rminus_lt; auto.
replace (min + max - (r + r))%R with (max - r - (r - min))%R;
 [ idtac | simpl in |- *; ring ].
(* Goal: Rlt (Rminus (Rminus (FtoRradix max) r) (Rminus r (FtoRradix min))) (IZR Z0) *)
apply Rlt_minus; auto.
Qed.
 
Theorem EvenClosestCompatible : CompatibleP b radix EvenClosest.
(* Goal: UniqueP radix EvenClosest *)
red in |- *; simpl in |- *.
(* Goal: MinOrMaxP b radix Closest *)
intros r1 r2 p q H' H'0 H'1 H'2; red in |- *.
(* Goal: and (Closest r2 q) (or (FNeven b radix precision q) (forall (q0 : float) (_ : Closest r2 q0), @eq R (FtoRradix q0) (FtoRradix q))) *)
inversion H'.
(* Goal: and (MinOrMaxP b radix EvenClosest) (MonotoneP radix EvenClosest) *)
split.
(* Goal: Closest r2 q *)
(* Goal: or (FNeven b radix precision q) (forall (q0 : float) (_ : Closest r2 q0), @eq R (FtoRradix q0) (FtoRradix q)) *)
apply (ClosestCompatible r1 r2 p q); auto.
(* Goal: or (FNeven b radix precision q) (forall (q0 : float) (_ : Closest r2 q0), @eq R (FtoRradix q0) (FtoRradix q)) *)
case H0; intros H1.
(* Goal: or (FNeven b radix precision (Fopp p)) (forall (q : float) (_ : Closest (Ropp r) q), @eq R (FtoRradix q) (FtoRradix (Fopp p))) *)
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
left.
(* Goal: FNeven b radix precision q *)
(* Goal: or (FNeven b radix precision q) (forall (q0 : float) (_ : Closest r2 q0), @eq R (FtoRradix q0) (FtoRradix q)) *)
apply FNevenEq with (f1 := p); auto.
(* Goal: Fbounded b p *)
(* Goal: or (FNeven b radix precision q) (forall (q0 : float) (_ : Closest r2 q0), @eq R (FtoRradix q0) (FtoRradix q)) *)
case H; auto.
(* Goal: or (FNeven b radix precision q) (forall (q0 : float) (_ : Closest r2 q0), @eq R (FtoRradix q0) (FtoRradix q)) *)
right; intros q0 H'3.
(* Goal: @eq R (FtoRradix q0) (FtoRradix q) *)
unfold FtoRradix in |- *; rewrite <- H'1; auto.
(* Goal: @eq R (FtoR radix q0) (FtoR radix p) *)
apply H1; auto.
(* Goal: Closest r1 q0 *)
apply (ClosestCompatible r2 r1 q0 q0); auto.
(* Goal: Fbounded b q *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
case H'3; auto.
Qed.
 
Theorem EvenClosestMinOrMax : MinOrMaxP b radix EvenClosest.
(* Goal: MinOrMaxP b radix EvenClosest *)
red in |- *; intros r p H'; case (ClosestMinOrMax r p); auto.
(* Goal: Closest r p *)
case H'; auto.
Qed.
 
Theorem EvenClosestMonotone : MonotoneP radix EvenClosest.
red in |- *; simpl in |- *; intros p q p' q' H' H'0 H'1.
apply (ClosestMonotone p q); auto; case H'0; case H'1; auto.
Qed.
 
Theorem EvenClosestRoundedModeP : RoundedModeP b radix EvenClosest.
(* Goal: and (MinOrMaxP b radix EvenClosest) (MonotoneP radix EvenClosest) *)
red in |- *; split.
(* Goal: TotalP EvenClosest *)
(* Goal: and (CompatibleP b radix EvenClosest) (and (MinOrMaxP b radix EvenClosest) (MonotoneP radix EvenClosest)) *)
exact EvenClosestTotal.
(* Goal: and (MinOrMaxP b radix EvenClosest) (MonotoneP radix EvenClosest) *)
split.
(* Goal: CompatibleP b radix EvenClosest *)
(* Goal: and (MinOrMaxP b radix EvenClosest) (MonotoneP radix EvenClosest) *)
exact EvenClosestCompatible.
(* Goal: and (MinOrMaxP b radix EvenClosest) (MonotoneP radix EvenClosest) *)
split.
(* Goal: MinOrMaxP b radix EvenClosest *)
(* Goal: MonotoneP radix EvenClosest *)
exact EvenClosestMinOrMax.
(* Goal: MonotoneP radix EvenClosest *)
exact EvenClosestMonotone.
Qed.
 
Theorem EvenClosestUniqueP : UniqueP radix EvenClosest.
(* Goal: UniqueP radix EvenClosest *)
red in |- *; simpl in |- *.
(* Goal: forall (r : R) (p q : float) (_ : EvenClosest r p) (_ : EvenClosest r q), @eq R (FtoR radix p) (FtoR radix q) *)
intros r p q H' H'0.
(* Goal: @eq R (FtoR radix p) (FtoR radix q) *)
inversion H'; inversion H'0; case H0; case H2; auto.
intros H'1 H'2; case (EvenClosestMinOrMax r p);
 case (EvenClosestMinOrMax r q); auto.
(* Goal: forall (_ : isMin b radix r q) (_ : isMin b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMin b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : isMin b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
intros H'3 H'4; apply (MinUniqueP b radix r); auto.
(* Goal: forall (_ : isMin b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
intros H'3 H'4; case (Req_dec p q); auto; intros H'5.
(* Goal: @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : isMin b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
Contradict H'1; auto.
(* Goal: not (FNeven b radix precision p) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply FnOddNEven; auto.
(* Goal: FNodd b radix precision q *)
(* Goal: forall (_ : isMin b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply FNoddEq with (f1 := FNSucc b radix precision p); auto.
(* Goal: Fbounded b (FNSucc b radix precision q) *)
(* Goal: Fbounded b p *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision q)) (FtoR radix p) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply FcanonicBound with (radix := radix); auto.
(* Goal: Fcanonic radix b (FNSucc b radix precision q) *)
(* Goal: Fbounded b p *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision q)) (FtoR radix p) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply FNSuccCanonic; auto with arith.
(* Goal: Fbounded b p *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision q)) (FtoR radix p) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
case H'4; auto.
(* Goal: Fbounded b q *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
case H'3; auto.
(* Goal: @eq R (FtoR radix (FNSucc b radix precision q)) (FtoR radix p) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply (MaxUniqueP b radix r); auto.
(* Goal: isMax b radix r (FNSucc b radix precision q) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply MinMax; auto with arith.
(* Goal: not (@eq R r (FtoR radix q)) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
Contradict H'5; auto.
apply
 (RoundedProjector b radix _
    (MaxRoundedModeP _ _ _ radixMoreThanOne precisionGreaterThanOne
       pGivesBound)); auto.
(* Goal: Fbounded b p *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision q)) (FtoR radix p) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
case H'4; auto.
(* Goal: isMax b radix (FtoR radix q) p *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
rewrite <- H'5; auto.
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply FNevenSuc; auto.
(* Goal: Fbounded b p *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision q)) (FtoR radix p) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
case H'4; auto.
(* Goal: forall (_ : isMin b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
intros H'3 H'4; case (Req_dec p q); auto; intros H'5.
(* Goal: @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
Contradict H'2; auto.
(* Goal: not (FNeven b radix precision p) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply FnOddNEven; auto.
(* Goal: FNodd b radix precision p *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply FNoddEq with (f1 := FNSucc b radix precision q); auto.
(* Goal: Fbounded b (FNSucc b radix precision q) *)
(* Goal: Fbounded b p *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision q)) (FtoR radix p) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply FcanonicBound with (radix := radix); auto.
(* Goal: Fcanonic radix b (FNSucc b radix precision q) *)
(* Goal: Fbounded b p *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision q)) (FtoR radix p) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply FNSuccCanonic; auto with arith.
(* Goal: Fbounded b q *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
case H'3; auto.
(* Goal: Fbounded b p *)
(* Goal: @eq R (FtoR radix (FNSucc b radix precision q)) (FtoR radix p) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
case H'4; auto.
(* Goal: @eq R (FtoR radix (FNSucc b radix precision q)) (FtoR radix p) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply (MaxUniqueP b radix r); auto.
(* Goal: isMax b radix r (FNSucc b radix precision q) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply MinMax; auto with arith.
(* Goal: not (@eq R r (FtoR radix q)) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
Contradict H'5; auto.
apply sym_eq;
 apply
  (RoundedProjector b radix _
     (MaxRoundedModeP _ _ _ radixMoreThanOne precisionGreaterThanOne
        pGivesBound)); auto.
(* Goal: Fbounded b q *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
case H'3; auto.
(* Goal: isMax b radix (FtoR radix q) p *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
rewrite <- H'5; auto.
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
apply FNevenSuc; auto.
(* Goal: Fbounded b q *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
case H'3; auto.
(* Goal: @eq R (FtoR radix (FNSucc b radix precision q)) (FtoR radix p) *)
(* Goal: FNodd b radix precision (FNSucc b radix precision q) *)
(* Goal: forall (_ : isMax b radix r q) (_ : isMax b radix r p), @eq R (FtoR radix p) (FtoR radix q) *)
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
intros H'3 H'4; apply (MaxUniqueP b radix r); auto.
(* Goal: forall (_ : FNeven b radix precision q) (_ : forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p)), @eq R (FtoR radix p) (FtoR radix q) *)
intros H'1 H'2; apply sym_eq; auto.
Qed.
 
Theorem ClosestSymmetric : SymmetricP Closest.
(* Goal: SymmetricP EvenClosest *)
red in |- *; intros r p H'; case H'; clear H'.
(* Goal: and (MinOrMaxP b radix EvenClosest) (MonotoneP radix EvenClosest) *)
intros H' H'0; split.
(* Goal: Fbounded b (Fopp f) *)
(* Goal: @eq R (Rabs (Rminus (FtoRradix (Fopp f)) r)) (Rabs (Rminus (FtoRradix f) (Ropp r))) *)
(* Goal: @eq R (Rabs (Rminus (FtoRradix p) r)) (Rabs (Rminus (FtoRradix (Fopp p)) (Ropp r))) *)
apply oppBounded; auto.
(* Goal: forall (f : float) (_ : Fbounded b f), Rle (Rabs (Rminus (FtoRradix (Fopp p)) (Ropp r))) (Rabs (Rminus (FtoRradix f) (Ropp r))) *)
intros f H'1.
(* Goal: Rle (Rabs (Rminus (FtoRradix (Fopp p)) (Ropp r))) (Rabs (Rminus (FtoRradix f) (Ropp r))) *)
replace (Rabs (Fopp p - - r)) with (Rabs (p - r)).
(* Goal: Rle (Rabs (Rminus (FtoRradix p) r)) (Rabs (Rminus (FtoRradix f) (Ropp r))) *)
(* Goal: @eq R (Rabs (Rminus (FtoRradix p) r)) (Rabs (Rminus (FtoRradix (Fopp p)) (Ropp r))) *)
replace (Rabs (f - - r)) with (Rabs (Fopp f - r)).
(* Goal: @eq R (FtoRradix (Fopp q)) (FtoRradix p) *)
apply H'0; auto.
(* Goal: Fbounded b (Fopp f) *)
(* Goal: @eq R (Rabs (Rminus (FtoRradix (Fopp f)) r)) (Rabs (Rminus (FtoRradix f) (Ropp r))) *)
(* Goal: @eq R (Rabs (Rminus (FtoRradix p) r)) (Rabs (Rminus (FtoRradix (Fopp p)) (Ropp r))) *)
apply oppBounded; auto.
(* Goal: @eq R (Rabs (Rminus (FtoRradix p) r)) (Rabs (Rminus (FtoRradix (Fopp p)) (Ropp r))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct.
(* Goal: @eq R (Rabs (Rminus (Ropp (FtoR radix f)) r)) (Rabs (Rminus (FtoR radix f) (Ropp r))) *)
(* Goal: @eq R (Rabs (Rminus (FtoRradix p) r)) (Rabs (Rminus (FtoRradix (Fopp p)) (Ropp r))) *)
pattern r at 1 in |- *; replace r with (- - r)%R; [ idtac | ring ].
replace (- FtoR radix f - - - r)%R with (- (FtoR radix f - - r))%R;
 [ idtac | ring ].
(* Goal: @eq R (Rabs (Ropp (Rminus (FtoR radix f) (Ropp r)))) (Rabs (Rminus (FtoR radix f) (Ropp r))) *)
(* Goal: @eq R (Rabs (Rminus (FtoRradix p) r)) (Rabs (Rminus (FtoRradix (Fopp p)) (Ropp r))) *)
apply Rabs_Ropp; auto.
(* Goal: @eq R (Rabs (Rminus (FtoRradix p) r)) (Rabs (Rminus (FtoRradix (Fopp p)) (Ropp r))) *)
unfold FtoRradix in |- *; rewrite Fopp_correct.
replace (- FtoR radix p - - r)%R with (- (FtoR radix p - r))%R;
 [ idtac | ring ].
(* Goal: @eq R (Rabs (Rminus (FtoR radix p) r)) (Rabs (Ropp (Rminus (FtoR radix p) r))) *)
apply sym_eq; apply Rabs_Ropp.
Qed.
 
Theorem EvenClosestSymmetric : SymmetricP EvenClosest.
(* Goal: SymmetricP EvenClosest *)
red in |- *; intros r p H'; case H'; clear H'.
(* Goal: forall (_ : Closest r p) (_ : or (FNeven b radix precision p) (forall (q : float) (_ : Closest r q), @eq R (FtoRradix q) (FtoRradix p))), EvenClosest (Ropp r) (Fopp p) *)
intros H' H'0; case H'0; clear H'0; intros H'0.
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
split; auto.
(* Goal: Closest (Ropp r) (Fopp p) *)
(* Goal: or (FNeven b radix precision (Fopp p)) (forall (q : float) (_ : Closest (Ropp r) q), @eq R (FtoRradix q) (FtoRradix (Fopp p))) *)
apply (ClosestSymmetric r p); auto.
(* Goal: or (FNeven b radix precision (Fopp p)) (forall (q : float) (_ : Closest (Ropp r) q), @eq R (FtoRradix q) (FtoRradix (Fopp p))) *)
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
left.
(* Goal: FNeven b radix precision (Fopp p) *)
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
apply FNevenFop; auto.
(* Goal: EvenClosest (Ropp r) (Fopp p) *)
split; auto.
(* Goal: Closest (Ropp r) (Fopp p) *)
(* Goal: or (FNeven b radix precision (Fopp p)) (forall (q : float) (_ : Closest (Ropp r) q), @eq R (FtoRradix q) (FtoRradix (Fopp p))) *)
apply (ClosestSymmetric r p); auto.
(* Goal: or (FNeven b radix precision (Fopp p)) (forall (q : float) (_ : Closest (Ropp r) q), @eq R (FtoRradix q) (FtoRradix (Fopp p))) *)
right.
(* Goal: forall (q : float) (_ : Closest (Ropp r) q), @eq R (FtoRradix q) (FtoRradix (Fopp p)) *)
intros q H'1.
(* Goal: @eq R (FtoRradix q) (FtoRradix (Fopp p)) *)
cut (Fopp q = p :>R).
(* Goal: @eq R (Rabs (Rminus (FtoRradix p) r)) (Rabs (Rminus (FtoRradix (Fopp p)) (Ropp r))) *)
intros H'2; unfold FtoRradix in |- *; rewrite Fopp_correct.
(* Goal: @eq R (FtoR radix q) (Ropp (FtoR radix p)) *)
(* Goal: @eq R (FtoRradix (Fopp q)) (FtoRradix p) *)
unfold FtoRradix in H'2; rewrite <- H'2.
rewrite Fopp_correct; ring.
(* Goal: @eq R (FtoRradix (Fopp q)) (FtoRradix p) *)
apply H'0; auto.
(* Goal: Closest r (Fopp q) *)
replace r with (- - r)%R; [ idtac | ring ].
(* Goal: Closest (Ropp (Ropp r)) (Fopp q) *)
apply (ClosestSymmetric (- r)%R q); auto.
Qed.
End Fclosest.
Hint Resolve ClosestTotal ClosestCompatible ClosestMin ClosestMax
  ClosestMinOrMax ClosestMonotone ClosestRoundedModeP EvenClosestTotal
  EvenClosestCompatible EvenClosestMinOrMax EvenClosestMonotone
  EvenClosestRoundedModeP FnOddNEven EvenClosestUniqueP ClosestSymmetric
  EvenClosestSymmetric: float.